29 #define _CVC3_TRUSTED_
45 TheoryBitvector::createProofRules() {
52 d_theoryBitvector(theoryBV) {
70 "TheoryBitvector::bitvectorFalseRule: "
71 "premise must be a iff theorem:\n e = "
74 "TheoryBitvector::bitvectorFalseRule: "
75 "premise must be iff Theorem, with False as the RHS:\n e = "
79 "TheoryBitvector::bitvectorFalseRule: "
80 "premise must be iff Theorem, with False as the RHS:\n e = "
84 "TheoryBitvector::bitvectorFalseRule: "
85 "premise must be iff Theorem, with False as the RHS:\n e = "
89 const Expr& t1 = e[0][0][0];
90 const Expr& t2 = e[0][1][0];
108 "TheoryBitvector::bitvectorFalseRule: "
109 "premise must be a iff theorem:\n e = "
112 "TheoryBitvector::bitvectorFalseRule: "
113 "premise must be iff Theorem, with False as the RHS:\n e = "
118 "TheoryBitvector::bitvectorFalseRule: "
119 "premise must be iff Theorem, with False as the RHS:\n e = "
123 "TheoryBitvector::bitvectorFalseRule: "
124 "premise must be iff Theorem, with False as the RHS:\n e = "
130 const Expr& t1 = e[0][0][0][0];
131 const Expr& t2 = e[0][1][0];
146 "TheoryBitvector::bitBlastEqnRule: "
147 "premise must be a rewrite theorem:\n e = "
149 const Expr& lhs = e[0];
150 const Expr& rhs = e[1];
151 const Type& leftType = lhs.getType();
155 "TheoryBitvector::bitBlastEqnRule: "
156 "lhs & rhs must be bitvectors:\n e ="
161 "TheoryBitvector::bitBlastEqnRule: "
162 "lhs & rhs must be bitvectors of same bvLength.\n size(lhs) = "
169 "TheoryBitvector::bitBlastEqnRule: "
170 "consequence of the rule must be an AND.\n f = "
173 "TheoryBitvector::bitBlastEqnRule: "
174 "the arity of the consequence AND must "
175 "equal the bvLength of the bitvector:\n f = "
177 for (
int i=0; i < bvLength; ++i) {
178 const Expr& conjunct = f[i];
180 "TheoryBitvector::bitBlastEqnRule: "
181 "each conjunct in consequent must be an IFF.\n f = "
183 const Expr& leftExtract = conjunct[0];
184 const Expr& rightExtract = conjunct[1];
186 "TheoryBitvector::bitBlastEqnRule: "
187 "each conjunct in consequent must be boolextract.\n"
190 "TheoryBitvector::bitBlastEqnRule: "
191 "each conjunct in consequent must be boolextract.\n"
193 const Expr& leftBV = leftExtract[0];
194 const Expr& rightBV = rightExtract[0];
196 "TheoryBitvector::bitBlastEqnRule: each boolextract"
197 " must be applied to the correct bitvector.\n conjunct = "
199 +
"\n leftBV = "+ leftBV.toString()
200 +
"\n lhs = "+ lhs.toString()
203 int leftBitPosition =
205 int rightBitPosition =
207 CHECK_SOUND(leftBitPosition == i && rightBitPosition == i,
208 "TheoryBitvector::bitBlastEqnRule: "
209 "boolextract positions must match i= "+
int2string(i)
210 +
"\n conjunct = "+conjunct.
toString());
216 pf =
newPf(
"bit_blast_equations", e, f);
228 TRACE(
"bitvector",
"input to bitBlastDisEqnRule(", notE.
toString(),
")");
230 "TheoryBitvector::bitBlastDisEqnRule:"
236 "TheoryBitvector::bitBlastDisEqnRule:"
237 "premise must be a rewrite theorem" + e.toString());
238 const Expr& lhs = e[0];
239 const Expr& rhs = e[1];
240 const Type& leftType = lhs.getType();
244 "TheoryBitvector::bitBlastDisEqnRule:"
245 "lhs & rhs must be bitvectors" + e.toString());
248 "TheoryBitvector::bitBlastDisEqnRule:"
249 "lhs & rhs must be bitvectors of same bvLength");
252 "TheoryBitvector::bitBlastDisEqnRule:"
253 "consequence of the rule must be an OR" + f.
toString());
255 "TheoryBitvector::bitBlastDisEqnRule:"
256 "the arity of the consequence OR must be"
257 "equal to the bvLength of the bitvector" +
259 for(
int i=0; i <bvLength; i++) {
260 const Expr& disjunct = f[i];
263 "TheoryBitvector::bitBlastDisEqnRule:"
264 "each conjunct in consequent must be an Iff"+f.
toString());
265 const Expr& leftExtract = (disjunct[0])[0];
266 const Expr& rightExtract = disjunct[1];
268 "TheoryBitvector::bitBlastDisEqnRule:"
269 "each disjunct in consequent must be boolextract" +
272 "TheoryBitvector::bitBlastDisEqnRule:"
273 "each conjunct in consequent must be boolextract" +
275 const Expr& leftBV = leftExtract[0];
276 const Expr& rightBV = rightExtract[0];
278 "TheoryBitvector::bitBlastDisEqnRule:"
279 "each boolextract must be applied to the correct bitvector"+
280 disjunct.
toString() + leftBV.toString() + lhs.toString() +
282 int leftBitPosition =
284 int rightBitPosition =
286 CHECK_SOUND(leftBitPosition == i && rightBitPosition == i,
287 "TheoryBitvector::bitBlastDisEqnRule:"
288 "boolextract positions must match" + disjunct.
toString());
309 "BitvectorTheoremProducer::padBVLTRule: "
310 "input must e be a BVLT/BVLE: e = " + e.
toString());
312 BITVECTOR==e[1].getType().getExpr().getOpKind(),
313 "BitvectorTheoremProducer::padBVLTRule: "
314 "for BVMULT terms e[0],e[1] must be a BV: " + e.
toString());
316 "BitvectorTheoremProducer::padBVLTRule: "
317 "input len must be >=0 and an integer: len = " +
332 pf =
newPf(
"pad_bvlt_rule", e);
342 "input must be a bitvector. \n e = " + e.
toString());
344 "input must be SX(e).\n e = " + e.
toString());
346 "input cannot have nested SX.\n e = " + e.
toString());
357 if(bvLength0 == bvLength) {
359 }
else if(bvLength0 < bvLength) {
361 int c = bvLength - bvLength0;
373 pf =
newPf(
"sign_extend_rule", e);
389 pf =
newPf(
"bitExtract_SX_rule",e,
rat(i));
401 "BitvectorTheoremProducer::padBVSLTRule: "
402 "input must e be a BVSLT/BVSLE: e = " + e.
toString());
404 BITVECTOR==e[1].getType().getExpr().getOpKind(),
405 "BitvectorTheoremProducer::padBVSLTRule: "
406 "for BVMULT terms e[0],e[1] must be a BV: " + e.
toString());
408 "BitvectorTheoremProducer::padBVSLTRule: "
409 "input len must be >=0 and an integer: len = " +
424 pf =
newPf(
"pad_bvslt_rule", e);
443 "BitvectorTheoremProducer::signedBVLTRule: "
444 "input must e be a BVSLT/BVSLE: e = " + e.
toString());
446 BITVECTOR==e[1].getType().getExpr().getOpKind(),
447 "BitvectorTheoremProducer::signedBVLTRule: "
448 "for BVMULT terms e[0],e[1] must be a BV: " + e.
toString());
450 const Expr e0 = e[0];
451 const Expr e1 = e[1];
461 "BitvectorTheoremProducer::signedBVLTRule: "
462 "topBit0.getLHS() is the un-rewritten form of MSB of e0\n"
463 "topBit0 is screwed up: topBit0 = " +
466 "BitvectorTheoremProducer::signedBVLTRule: "
467 "topBit1.getLHS() is the un-rewritten form of MSB of e1\n"
468 "topBit1 is screwed up: topBit1 = " +
471 "BitvectorTheoremProducer::signedBVLTRule: "
472 "both e[0] and e[1] must have the same length\n. e =" +
505 output = eKind==
BVSLT ? fExpr : tExpr;
506 else if(b0==0 && b1==1)
508 else if(b0==1 && b1==0)
510 else if(b0==1 && b1==1)
511 output = eKind==
BVSLT ? fExpr : tExpr;
512 else if(b0==0 && b1==-1)
513 output = eKind==
BVSLT ? fExpr : MSB1isZero;
514 else if(b0==1 && b1==-1)
515 output = eKind==
BVSLT ? MSB1isZero : tExpr;
516 else if(b0==-1 && b1==0)
517 output = eKind==
BVSLT ? MSB0isOne : tExpr;
518 else if(b0==-1 && b1==1)
519 output = eKind==
BVSLT ? fExpr : MSB0isOne;
524 MSB0isOne.
andExpr(MSB1isZero) :
525 MSB0isOne.
orExpr(MSB1isZero);
541 if(-1 != b0 && -1 !=b1) {
543 if(b0 == 1 && b1 == 0)
546 else if(b0 == 0 && b1 == 1)
553 else if(-1 != b0 && -1 == b1) {
568 else if(-1 == b0 && -1 != b1) {
599 pf =
newPf(
"sign_bvlt_rule", e);
610 "BitvectorTheoremProducer::notBVEQ1Rule: "
611 "input kind must be a NOT:\n e = " + e.
toString());
613 "BitvectorTheoremProducer::notBVEQ1Rule: "
614 "e[0] must be EQ: \n e = " + e.
toString());
616 "BitvectorTheoremProducer::notBVEQ1Rule: "
617 "BVSize(e[0][0]) must be 1: \n e = " + e.
toString());
623 pf =
newPf(
"not_eq1_rule", e);
634 "BitvectorTheoremProducer::notBVLTRule: "
635 "input kind must be a NOT:\n e = " + e.
toString());
637 e[0].getOpKind() ==
BVLE,
638 "BitvectorTheoremProducer::notBVLTRule: "
639 "e[0] must be BVLT or BVLE: \n e = " + e.
toString());
643 const Expr& e00 = e[0][0];
644 const Expr& e01 = e[0][1];
645 if(
BVLT == e[0].getOpKind())
652 pf =
newPf(
"not_bvlt_rule", e);
661 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
662 "input kind must be BVLT or BVLE: e = " + e.
toString());
664 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
665 "input kind must match e.getOpKind(): "
668 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
669 "input arity must be 2, and e[0] must be equal to e[1]: "
680 pf =
newPf(
"lhs_eq_rhs_ineqn", e);
689 "BitvectorTheoremProducer::zeroLeq: "
690 "input kind must be BVLE: e = " + e.
toString());
693 "BitvectorTheoremProducer::zeroLeq: "
694 "unexpected input: e = " + e.
toString());
698 pf =
newPf(
"zeroLeq", e);
707 "BitvectorTheoremProducer::bvConstIneqn: "
708 "input kind must be BVLT or BVLE: e = " + e.
toString());
710 "BitvectorTheoremProducer::bvConstIneqn: "
711 "input kind must match e.getOpKind(): "
714 "BitvectorTheoremProducer::bvConstIneqn: "
715 "input arity must be 2: \ne = " + e.
toString());
717 "BitvectorTheoremProducer::bvConstIneqn: "
718 "e[0] and e[1] must both be constants:\n e = " +
726 "BitvectorTheoremProducer::bvConstIneqn: "
727 "e[0] and e[1] must have the same bvLength:\ne = " +
748 pf =
newPf(
"bv_const_ineqn", e);
768 "BitvectorTheoremProducer::generalIneqn: "
769 "input kind must be BVLT or BVLE: e = " + e.
toString());
771 "BitvectorTheoremProducer::generalIneqn: "
772 "input kind must match e.getOpKind(): "
775 "BitvectorTheoremProducer::generalIneqn: "
776 "input arity must be 2: \ne = " + e.
toString());
778 "BitvectorTheoremProducer::generalIneqn: "
779 "lhs_i and rhs_i must be rewrite theorems: "
791 "BitvectorTheoremProducer::generalIneqn: "
792 "lhs_i.getRHS() and rhs_i.getRHS() must be BOOLEXTRACTs:"
796 "BitvectorTheoremProducer::generalIneqn: "
797 "e[0] must be equal to LHS of lhs_i: \nlhs_i = " +
800 "BitvectorTheoremProducer::generalIneqn: "
801 "e[1] must be equal to LHS of rhs_i: \nrhs_i = " +
804 "BitvectorTheoremProducer::generalIneqn: "
805 "e[0] and e[1] must have the same bvLength:\ne = " +
812 e0_iBitIndex == e0len-1,
813 "BitvectorTheoremProducer::generalIneqn: "
814 "e0_iBit & e1_iBit must have same extract index: "
815 "\ne0_iBit = " + e0_iBit.
toString() +
816 "\ne1_iBit = " + e1_iBit.
toString());
826 "BitvectorTheoremProducer::generalIneqn: "
827 "b1 must be a boolean type: "
830 "BitvectorTheoremProducer::generalIneqn: "
831 "b2 must be boolean type: "
838 output = trueExpression;
840 output = falseExpression;
844 output = trueExpression;
846 output = falseExpression;
853 if (kind ==
BVLT || e0len > 1) {
854 output = (!b1) && b2;
857 output = (!b1) || b2;
877 output = output || (b1.
iffExpr(b2) && a);
883 pf =
newPf(
"general_ineqn", e);
900 for(i = 0; i < thms.size(); ++i) {
901 Expr e = thms[i].getExpr();
903 "Unexpected structure");
906 e[0][0] == thms[0].getExpr()[0][0] &&
908 "Unexpected structure");
911 Expr lhs = thms[0].getExpr()[0][0];
913 for (
unsigned i = 0; i < thms.size(); ++i) {
914 bits.push_back(thms[i].getExpr()[1].isTrue() ?
true :
false);
921 pf =
newPf(
"bit_extract_all_to_const_eq");
932 "BitvectorTheoremProducer::bitExtractToExtract:\n e = "
935 bool negative = e.
isNot();
936 const Expr& boolExtract = negative? e[0] : e;
951 "BitvectorTheoremProducer::bitExtractRewrite: x = "
956 const Expr& t = x[0];
961 "BitvectorTheoremProducer::bitExtractRewrite:"
969 pf =
newPf(
"bit_extract_rewrite", x);
979 TRACE(
"bitvector",
"bitExtractConstant(", x,
", "+
int2string(i) +
" ) {");
983 "BitvectorTheoremProducer::bitExtractConstant:"
984 "the bitvector must be a constant.");
986 CHECK_SOUND(0 <= i && (
unsigned)i < d_theoryBitvector->getBVConstSize(x),
987 "BitvectorTheoremProducer::bitExtractConstant:"
988 "illegal extraction attempted on the bitvector x = "
990 +
"\nat the position i = "
1008 TRACE(
"bitvector",
"bitExtractConstant => ", result,
" }");
1020 TRACE(
"bitvector",
"bitExtractConcatenation(",
1026 "BitvectorTheoremProducer::bitExtractConcatenation: "
1027 "term must be bitvector:\n x = "+x.
toString());
1029 "BitvectorTheoremProducer::bitExtractConcatenation: "
1030 "the bitvector must be a concat:\n x = " + x.
toString());
1037 "BitvectorTheoremProducer::bitExtractNot:"
1038 "illegal boolean extraction was attempted at position i = "
1040 +
"\non bitvector x = " + x.
toString()
1041 +
"\nwhose bvLength is = " +
1048 int numOfKids = x.
arity();
1049 int lenOfKidsSeen = 0;
1051 for(
int count = numOfKids-1; count >= 0; --count) {
1053 if(lenOfKidsSeen <= i && i < bvLengthOfKid + lenOfKidsSeen) {
1058 lenOfKidsSeen += bvLengthOfKid;
1061 "BitvectorTheoremProducer::bitExtractConcatenation: "
1062 "something's broken...");
1066 pf =
newPf(
"bit_extract_concatenation", x,
rat(i));
1068 TRACE(
"bitvector",
"bitExtractConcatenation => ", result,
" }");
1076 TRACE(
"bitvector",
"input to bitExtractConstBVMult(", t.
toString(),
")");
1077 TRACE(
"bitvector",
"input to bitExtractConstBVMult(",
int2string(i),
")");
1083 "BitvectorTheoremProducer::bitExtractConstBVMult:"
1084 "the term must be a bitvector: " + t.
toString());
1086 "BitvectorTheoremProducer::bitExtractConstBVMult:"
1087 "the term must be a MULT of arity 2: " + t.
toString());
1090 "BitvectorTheoremProducer::bitExtractConstBVMult:"
1091 "Expected inputs of same length");
1093 "BitvectorTheoremProducer::bitExtractNot:"
1094 "illegal boolean extraction was attempted at position i = "
1096 +
"\non bitvector x = " + t.
toString()
1097 +
"\nwhose bvLength is = " +
1100 "BitvectorTheoremProducer::bitExtractConstBVMult:"
1101 "illegal BVMULT expression" + t.
toString());
1104 std::vector<Expr> k;
1105 for(
int j=0; j < bvLength; ++j)
1107 Expr leftshiftTerm =
1109 k.push_back(leftshiftTerm);
1129 const Expr bitExtract =
1136 "output of bitExtract_const_bvmult(", result,
")");
1143 TRACE(
"bitvector",
"input to bitExtractBVMult(", t.
toString(),
")");
1150 "BitvectorTheoremProducer::bitExtractBVMult:"
1151 "the term must be a bitvector" + t.
toString());
1153 "BitvectorTheoremProducer::bitExtractBVMult:"
1154 "the term must be a bitvector" + t.
toString());
1157 "BitvectorTheoremProducer::bitExtractConstBVMult:"
1158 "Expected inputs of same length");
1160 "BitvectorTheoremProducer::bitExtractNot:"
1161 "illegal boolean extraction was attempted at position i = "
1163 +
"\non bitvector t = " + t.
toString()
1164 +
"\nwhose Length is = " +
1167 "BitvectorTheoremProducer::bitExtractBVMult:"
1168 "illegal BVMULT expression" + t.
toString());
1171 std::vector<Expr> k;
1172 for(
int j=bvLength-1; j >= 0; j--) {
1177 Expr iteTerm = cond.
iteExpr(leftshiftTerm, zeroString);
1178 k.push_back(iteTerm);
1183 "BitvectorTheoremProducer::bitExtractBVMult:"
1184 "size of output vector must be > 0");
1198 TRACE(
"bitvector",
"output of bitExtract_bvmult(", result,
")");
1208 TRACE(
"bitvector",
"input to bitExtractExtraction(", x.
toString(),
")");
1209 TRACE(
"bitvector",
"input to bitExtractExtraction(",
int2string(i),
")");
1215 "BitvectorTheoremProducer::bitExtract-Extraction:"
1216 "term must be bitvector.");
1218 "BitvectorTheoremProducer::bitExtract-Extraction:"
1219 "the bitvector must be an extract." + x.
toString());
1223 "BitvectorTheoremProducer::bitExtractNot:"
1224 "illegal boolean extraction was attempted at position i = "
1226 +
"\non bitvector t = " + x.
toString()
1227 +
"\nwhose Length is = " +
1231 CHECK_SOUND(extractLeft >= extractRight && extractLeft >= 0,
1232 "BitvectorTheoremProducer::bitExtract-Extraction:"
1233 "illegal boolean extraction was attempted." +
int2string(i) +
1235 CHECK_SOUND(0 <= i && i < extractLeft-extractRight+1,
1236 "BitvectorTheoremProducer::bitExtract-Extraction:"
1237 "illegal boolean extraction was attempted." +
int2string(i) +
1250 "output of bitExtractExtraction(", result,
")");
1257 const std::vector<Theorem>& t2BitExtractThms,
1258 const Expr& bvPlusTerm,
int bitPos)
1260 TRACE(
"bitvector",
"input to bitExtractBVPlus(", bvPlusTerm.
toString(),
")");
1261 TRACE(
"bitvector",
"input to bitExtractBVPlus(",
int2string(bitPos),
")");
1266 CHECK_SOUND(bitPos+1 == (
int)t1BitExtractThms.size() && bitPos+1 == (int)t2BitExtractThms.size(),
"BitvectorTheoremProducer::bitExtractBVPlus: illegal bitvector fed to the function." +
int2string(bitPos));
1267 const Expr& t1 = bvPlusTerm[0];
1268 const Expr& t2 = bvPlusTerm[1];
1269 std::vector<Theorem>::const_iterator i = t1BitExtractThms.begin();
1270 std::vector<Theorem>::const_iterator iend = t1BitExtractThms.end();
1271 std::vector<Theorem>::const_iterator j = t2BitExtractThms.begin();
1272 for(; i !=iend; ++i, ++j) {
1273 const Expr& t1Expr = i->getLHS();
1274 const Expr& t2Expr = j->getLHS();
1275 CHECK_SOUND(t1Expr[0] == t1 && t2Expr[0] == t2,
"BitvectorTheoremProducer::bitExtractBVPlus: illegal bitvector fed to the function." + t1Expr.
toString() +
" ==\n" + t1.toString() +
"\n" + t2.
toString() +
" == \n" + t2Expr.
toString());
1280 const Expr& t1_iBit = (t1BitExtractThms[bitPos]).getRHS();
1281 const Expr& t2_iBit = (t2BitExtractThms[bitPos]).getRHS();
1283 const Expr carry_iBit =
computeCarry(t1BitExtractThms, t2BitExtractThms, bitPos);
1294 rhs = !(t1_iBit.
iffExpr(t2_iBit));
1298 pf =
newPf(
"bit_extract_BVPlus_rule",bvPlusTerm,
rat(bitPos));
1300 TRACE(
"bitvector",
"output of bitExtractBVPlus(", result,
")");
1306 const std::vector<Theorem>& t2BitExtractThms,
1311 "computeCarry: negative bitExtract_Pos is illegal");
1313 const Expr& t1Thm = t1BitExtractThms[bitPos].getRHS();
1314 const Expr& t2Thm = t2BitExtractThms[bitPos].getRHS();
1315 carry.push_back(t1Thm.
andExpr(t2Thm));
1318 const Expr& t1Thm = t1BitExtractThms[bitPos-1].getRHS();
1319 const Expr& t2Thm = t2BitExtractThms[bitPos-1].getRHS();
1321 carry.push_back(iMinusOneTerm);
1323 const Expr iMinusOneCarry =
1324 computeCarry(t1BitExtractThms,t2BitExtractThms,bitPos-1);
1325 const Expr secondTerm = t1Thm.
andExpr(iMinusOneCarry);
1326 carry.push_back(secondTerm);
1328 const Expr thirdTerm = t2Thm.
andExpr(iMinusOneCarry);
1330 carry.push_back(thirdTerm);
1339 const Expr& bvPlusTerm,
1341 int precomputedFlag)
1344 "precomputedFlag cannot be 0");
1345 TRACE(
"bitvector",
"input to bitExtractBVPlus(", bvPlusTerm.
toString(),
")");
1346 TRACE(
"bitvector",
"input to bitExtractBVPlus(",
int2string(bitPos),
")");
1350 "BitvectorTheoremProducer::bitExtractBVPlus:"
1351 "illegal bitvector fed to the function." +
1354 "BitvectorTheoremProducer::bitExtractBVPlus:"
1355 "illegal bitvector fed to the function." +
1357 const Expr& t1 = bvPlusTerm[0];
1358 const Expr& t2 = bvPlusTerm[1];
1361 "BitvectorTheoremProducer::bitExtractBVPlus:"
1362 "illegal theorems fed to the function. Theorem1 = " +
1366 "BitvectorTheoremProducer::bitExtractBVPlus:"
1367 "illegal theorems fed to the function. Theorem1 = " +
1371 "BitvectorTheoremProducer::bitExtractBVPlus:"
1372 "illegal theorems fed to the function. Theorem1 = " +
1392 rhs = !(t1_iBit.
iffExpr(t2_iBit));
1396 pf =
newPf(
"bit_extract_BVPlus_precomputed_rule",bvPlusTerm,
rat(bitPos));
1398 TRACE(
"bitvector",
"output of bitExtractBVPlus(", result,
")");
1408 int bitPos,
int preComputed){
1415 "computeCarry: negative bitExtract_Pos is illegal");
1426 if(1 == preComputed)
1434 if(1 == preComputed) {
1439 "this should not happen");
1453 "this should not happen");
1473 "BitvectorTheoremProducer::zeroPaddingRule:"
1474 "Wrong Input: Input must be a bitvector. But the input is: " +
1483 "BitvectorTheoremProducer::zeroPaddingRule:"
1484 "bitPosition of extraction must be greater than bvLength" +
1491 pf =
newPf(
"zeropadding_rule", e,
rat(i));
1500 "input to bvPlusAssociativityRule(", bvPlusTerm.
toString(),
")");
1505 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
1506 "term must be BITVECTOR type.");
1508 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
1509 "term must have the kind BVPLUS.");
1511 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
1512 "term must have arity() greater than 2 for associativity.");
1514 std::vector<Expr> BVPlusTerms0;
1515 std::vector<Expr>::const_iterator j = (bvPlusTerm.
getKids()).begin();
1516 std::vector<Expr>::const_iterator jend = (bvPlusTerm.
getKids()).end();
1519 BVPlusTerms0.insert(BVPlusTerms0.end(), j, jend);
1524 std::vector<Expr> BVPlusTerms1;
1525 BVPlusTerms1.push_back(*((bvPlusTerm.
getKids()).begin()));
1526 BVPlusTerms1.push_back(bvplus0);
1531 if(
withProof()) pf =
newPf(
"bv_plus_associativityrule", bvPlusTerm);
1534 "output of bvPlusAssociativityRule(", result,
")");
1541 TRACE(
"bitvector",
"input to bitExtractNot(", x.
toString(),
")");
1548 "BitvectorTheoremProducer::bitExtractNot:"
1549 "term must be bitvector.");
1551 "BitvectorTheoremProducer::bitExtractNot:"
1552 "the bitvector must be an bitwise negation." + x.
toString());
1556 "BitvectorTheoremProducer::bitExtractNot:"
1557 "illegal boolean extraction was attempted at position i = "
1559 +
"\non bitvector x = " + x.
toString()
1560 +
"\nwhose Length is = " +
1570 TRACE(
"bitvector",
"output of bitExtractNot(", result,
")");
1578 TRACE(
"bitvector",
"bitExtractBitwise(", x,
", "+
int2string(i)+
") {");
1582 "BitvectorTheoremProducer::bitExtractBitwise: kind = "
1586 "BitvectorTheoremProducer::bitExtractBitwise: "
1587 "term must be bitvector.\n x = "+x.
toString()
1590 "BitvectorTheoremProducer::bitExtractBitwise: "
1591 "kind does not match.\n x = "
1596 "BitvectorTheoremProducer::bitExtractBitwise: "
1597 "illegal boolean extraction was attempted.\n i = "
1607 int resKind = kind ==
BVAND ?
AND :
1614 TRACE(
"bitvector",
"bitExtractBitwise => ", result.
toString(),
" }");
1621 TRACE(
"bitvector",
"input to bitExtractFixedleftshift(", x.
toString(),
")");
1622 TRACE(
"bitvector",
"input to bitExtractFixedleftshift(",
int2string(i),
")");
1628 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
1629 "term must be bitvector.");
1632 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
1633 "the bitvector must be a bitwise LEFTSHIFT." +
1636 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
1637 "the bitvector must be a bitwise LEFTSHIFT." +
1642 "BitvectorTheoremProducer::bitExtractNot:"
1643 "illegal boolean extraction was attempted at position i = "
1645 +
"\non bitvector x = " + x.
toString()
1646 +
"\nwhose bvLength is = " +
1653 if(0 <= i && i < shiftLength)
1661 pf =
newPf(
"bit_extract_bitwisefixedleftshift", x,
rat(i));
1664 "output of bitExtractFixedleftshift(", result,
")");
1670 TRACE(
"bitvector",
"input to bitExtractFixedRightShift(", x.
toString(),
")");
1671 TRACE(
"bitvector",
"input to bitExtractFixedRightShift(",
int2string(i),
")");
1677 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
1678 "term must be bitvector.");
1680 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
1681 "the bitvector must be an bitwise RIGHTSHIFT." +
1684 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
1685 "the bitvector must be an bitwise RIGHTSHIFT." +
1692 "BitvectorTheoremProducer::bitExtractNot:"
1693 "illegal boolean extraction was attempted at position i = "
1695 +
"\non bitvector t = " + x.
toString()
1696 +
"\nwhose Length is = " +
1703 if(bvLength > i && i > bvLength-shiftLength-1)
1711 pf =
newPf(
"bit_extract_bitwiseFixedRightShift", x,
rat(i));
1714 "output of bitExtractFixedRightShift(", result,
")");
1728 "BitvectorTheoremProducer::bitExtractBVSHL:"
1729 "term must be bitvector.");
1731 "BitvectorTheoremProducer::bitExtractBVSHL:"
1732 "the bitvector must be a BVSHL." +
1736 "BitvectorTheoremProducer::bitExtractBVSHL:"
1737 "illegal boolean extraction was attempted at position i = "
1739 +
"\non bitvector x = " + x.
toString()
1740 +
"\nwhose bvLength is = " +
1746 const Expr& term = x[0];
1747 const Expr& shift = x[1];
1751 for (
int j = 0; j <= i; ++j) {
1754 kids.push_back(eq && ext);
1758 if (kids.size() == 1) {
1767 pf =
newPf(
"bit_extract_bvshl", x,
rat(i));
1782 "BitvectorTheoremProducer::bitExtractBVSHL:"
1783 "term must be bitvector.");
1785 "BitvectorTheoremProducer::bitExtractBVSHL:"
1786 "the bitvector must be a BVSHL." +
1790 "BitvectorTheoremProducer::bitExtractBVSHL:"
1791 "illegal boolean extraction was attempted at position i = "
1793 +
"\non bitvector x = " + x.
toString()
1794 +
"\nwhose bvLength is = " +
1800 const Expr& term = x[0];
1801 const Expr& shift = x[1];
1805 for (
int j = 0; j <= bvLength-1-i; ++j) {
1808 kids.push_back(eq && ext);
1812 if (kids.size() == 1) {
1821 pf =
newPf(
"bit_extract_bvlshr", x,
rat(i));
1836 "BitvectorTheoremProducer::bitExtractBVSHL:"
1837 "term must be bitvector.");
1839 "BitvectorTheoremProducer::bitExtractBVSHL:"
1840 "the bitvector must be a BVSHL." +
1844 "BitvectorTheoremProducer::bitExtractBVSHL:"
1845 "illegal boolean extraction was attempted at position i = "
1847 +
"\non bitvector x = " + x.
toString()
1848 +
"\nwhose bvLength is = " +
1854 const Expr& term = x[0];
1855 const Expr& shift = x[1];
1859 for (; j < bvLength-1-i; ++j) {
1862 kids.push_back(eq && ext);
1867 kids.push_back(tmp && ext);
1870 if (kids.size() == 1) {
1879 pf =
newPf(
"bit_extract_bvashr", x,
rat(i));
1887 if(i->getOpKind() !=
BVCONST)
return false;
1897 "BitvectorTheoremProducer::eqConst: e = "+e.
toString());
1899 "BitvectorTheoremProducer::eqConst: e = "+e.
toString());
1903 pf =
newPf(
"bitvector_eq_const", e);
1914 "BitvectorTheoremProducer::eqToBits: eq = "+eq.
toString());
1922 "BitvectorTheoremProducer::eqToBits: eq = "+eq.
toString());
1925 "BitvectorTheoremProducer::eqToBits: eq = "+eq.
toString());
1929 vector<Expr> bitEqs;
1930 for(; i<size; i++) {
1933 bitEqs.push_back(l.
eqExpr(r));
1948 "BitvectorTheoremProducer::leftShiftConst: e = "+e.
toString());
1950 "BitvectorTheoremProducer::leftShiftConst: e = "+e.
toString());
1952 const Expr& e0 = e[0];
1956 if (shiftSize != 0) {
1963 pf =
newPf(
"leftshift_to_concat", e);
1972 "BitvectorTheoremProducer::leftShiftConst: e = "+e.
toString());
1974 "BitvectorTheoremProducer::leftShiftConst: e = "+e.
toString());
1976 const Expr& e0 = e[0];
1984 if (shiftSize >= bvLength)
1995 pf =
newPf(
"constWidthLeftShift_to_concat", e);
2004 "BitvectorTheoremProducer::rightShiftConst: e = "+e.
toString());
2006 "BitvectorTheoremProducer::rightShiftConst: e = "+e.
toString());
2013 if (shiftSize == 0) output = e[0];
2014 if (shiftSize >= bvLength)
2023 "BitvectorTheoremProducer::rightShiftConst: e = "+e.
toString());
2027 pf =
newPf(
"rightshift_to_concat", e);
2037 "BitvectorTheoremProducer::bvshlToConcat: e = "+e.
toString());
2039 "BitvectorTheoremProducer::bvshlToConcat: e = "+e.
toString());
2041 const Expr& e0 = e[0];
2045 if (shiftSize == 0) res = e0;
2048 if (shiftSize >= bvLength)
2059 pf =
newPf(
"bvshl_to_concat");
2075 "BitvectorTheoremProducer::bitExtractBVSHL:"
2076 "term must be bitvector.");
2078 "BitvectorTheoremProducer::bitExtractBVSHL:"
2079 "the bitvector must be a BVSHL." +
2083 const Expr& term = e[0];
2084 const Expr& shift = e[1];
2089 for (
int i = bvLength-1; i > 0; --i) {
2093 newExpr = eq.
iteExpr(tmp, newExpr);
2097 newExpr = eq.
iteExpr(term, newExpr);
2101 pf =
newPf(
"bvshl_split", e);
2111 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.
toString());
2113 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.
toString());
2120 if (shiftSize == 0) output = e[0];
2121 else if(shiftSize >= bvLength)
2131 pf =
newPf(
"bvlshr_to_concat", e);
2140 && e.
arity() == 2,
"BitvectorTheoremProducer::bvShiftZero: e = "+e.
toString());
2149 pf =
newPf(
"shift_zero", e);
2159 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.
toString());
2161 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.
toString());
2168 if (shiftSize > 0) {
2169 if (shiftSize >= bvLength) shiftSize = bvLength - 1;
2172 }
else output = e[0];
2176 pf =
newPf(
"bvashr_to_concat", e);
2185 "Bad call to rewriteXNOR");
2191 pf =
newPf(
"rewriteXNOR", e);
2200 "Bad call to rewriteNAND");
2205 pf =
newPf(
"rewriteNAND", e);
2215 "Bad call to rewriteNOR");
2220 pf =
newPf(
"rewriteNOR", e);
2230 "Bad call to rewriteBVCOMP");
2236 pf =
newPf(
"rewriteBVCOMP");
2247 "Bad call to rewriteBVSub");
2263 pf =
newPf(
"rewriteBVSub", e);
2272 "BitvectorTheoremProducer::constMultToPlus: this rule does not work\n");
2276 "BitvectorTheoremProducer::constMultToPlus:\n e = "
2281 const Expr& t = e[1];
2283 string coeffBinary =
abs(k).toString(2);
2284 int len = coeffBinary.length();
2289 int len = resLength;
2290 for(
int i=0; i<len; ++i) bits.push_back(
false);
2295 for(
int i=0; i<len; ++i) {
2296 if(coeffBinary[i] ==
'1')
2299 res = (kids.size() == 1)? kids[0]
2305 kk.push_back(
rat(1));
2312 pf =
newPf(
"const_mult_to_plus", e);
2321 "BitvectorTheoremProducer::bvplusZeroConcatRule: e = "
2325 "BitvectorTheoremProducer::bvplusZeroConcatRule: e = "
2330 const Expr& bvplus = e[1];
2338 if(i->getOpKind()==
CONCAT && i->arity()>=2
2341 if(size > maxKidSize) maxKidSize = size;
2343 int numKids = bvplus.
arity();
2346 for(
int i=1; i < numKids; i *=2, log2++);
2347 if(log2+maxKidSize > bvplusSize) {
2349 TRACE(
"bv 0@+",
"bvplusZeroConcatRule(", e,
"): skipped");
2358 pf =
newPf(
"bvplus_zero_concat", e);
2369 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
2371 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
2376 const Expr& e0 = e[0];
2380 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
2381 CHECK_SOUND((
unsigned)hi < d_theoryBitvector->getBVConstSize(e0),
2382 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
2386 for(
int bit=low; bit <= hi; bit++)
2391 pf =
newPf(
"extract_const", e);
2400 "BitvectorTheoremProducer::extractWhole: e = "+e.
toString());
2405 const Expr& e0 = e[0];
2409 "BitvectorTheoremProducer::extractWhole: e = "+e.
toString()
2414 pf =
newPf(
"extract_whole", e);
2424 "BitvectorTheoremProducer::extractExtract: e = "+e.
toString());
2429 const Expr& e0 = e[0];
2434 "BitvectorTheoremProducer::extractExtract: e = "+e.
toString());
2437 "BitvectorTheoremProducer::extractExtract: e0 = "
2443 const Expr& e00 = e0[0];
2447 CHECK_SOUND((0 <= low) && (low <= hi) && (hi <= hi0-low0),
2448 "BitvectorTheoremProducer::extractExtract:\n"
2458 pf =
newPf(
"extract_extract", e);
2466 TRACE(
"bitvector rules",
"extractConcat(", e,
") {");
2469 "BitvectorTheoremProducer::extractConcat: e = "+e.
toString());
2474 const Expr& e0 = e[0];
2479 "BitvectorTheoremProducer::extractConcat: e = "+e.
toString());
2481 "BitvectorTheoremProducer::extractConcat: e = "+e.
toString()
2485 "BitvectorTheoremProducer::extractConcat: e0 = "
2491 TRACE(
"bitvector rules",
"extractConcat: width=", width,
"");
2493 TRACE(
"bitvector rules",
"extractConcat: *i=", *i,
"");
2495 int newWidth = width-w;
2497 TRACE(
"bitvector rules",
"extractConcat: w=", w,
"");
2498 TRACE(
"bitvector rules",
"extractConcat: newWidth=", newWidth,
"");
2500 if(hi >= newWidth) {
2502 l = (newWidth <= low)? low-newWidth : 0;
2503 TRACE(
"bitvector rules",
"extractConcat[newWidth<=hi<width]: h=",
2507 }
else if(width > low) {
2510 l = (newWidth <= low)? low-newWidth : 0;
2511 TRACE(
"bitvector rules",
"extractConcat[low<width<=hi]: h=",
2516 TRACE(
"bitvector rules",
"extractConcat: width=", width,
"");
2518 Expr res = (kids.size()==1)? kids[0]
2522 pf =
newPf(
"extract_concat", e);
2524 TRACE(
"bitvector rules",
"extractConcat => ", thm.
getExpr(),
" }");
2533 const string& pfName) {
2536 "BitvectorTheoremProducer::"+pfName+
": e = "+e.
toString());
2540 "BitvectorTheoremProducer::"+pfName+
": kind = "
2546 const Expr& e0 = e[0];
2551 "BitvectorTheoremProducer::"+pfName+
": e = "+e.
toString());
2554 "BitvectorTheoremProducer::"+pfName+
": e0 = "
2565 pf =
newPf(pfName, e);
2594 "BitvectorTheoremProducer::iteExtractRule: "
2595 "input must be an bitvector EXTRACT expr:\n"+
2604 BITVECTOR == e[0].getType().getExpr().getOpKind(),
2605 "BitvectorTheoremProducer::iteExtractRule: "
2606 "input must be an bitvector EXTRACT expr over an ITE:\n" +
2609 "BitvectorTheoremProducer::iteExtractRule: "
2610 "i should be greater than j in e[i:j] = "
2613 const Expr ite = e[0];
2621 pf =
newPf(
"ite_extract_rule", e);
2630 "BitvectorTheoremProducer::itebvnegrule: "
2631 "input must be an bitvector EXTRACT expr:\n"+
2637 BITVECTOR == e[0].getType().getExpr().getOpKind(),
2638 "BitvectorTheoremProducer::itebvnegrule: "
2639 "input must be an bitvector EXTRACT expr over an ITE:\n" +
2642 const Expr ite = e[0];
2650 pf =
newPf(
"ite_bvneg_rule", e);
2659 "BitvectorTheoremProducer::negConst: e = "+e.
toString());
2661 "BitvectorTheoremProducer::negConst: e = "+e.
toString());
2663 const Expr& e0 = e[0];
2671 pf =
newPf(
"bitneg_const", e);
2682 "BitvectorTheoremProducer::negConcat: e = "+e.
toString());
2684 "BitvectorTheoremProducer::negConcat: e = "+e.
toString());
2687 const Expr& e0 = e[0];
2697 pf =
newPf(
"bitneg_concat", e);
2706 "BitvectorTheoremProducer::negNeg: e = "+e.
toString());
2708 "BitvectorTheoremProducer::negNeg: e = "+e.
toString());
2713 pf =
newPf(
"bitneg_neg", e);
2723 "BitvectorTheoremProducer::negNeg: e = "+e.
toString());
2730 vector<Expr> bvplusTerms;
2731 bvplusTerms.push_back(minus_one);
2737 pf =
newPf(
"bitneg_elim", e);
2747 "BitvectorTheoremProducer::negBVand: e = "+e.
toString());
2749 "BitvectorTheoremProducer::negBVand: e = "+e.
toString());
2752 std::vector<Expr> negated;
2759 pf =
newPf(
"bitneg_and", e);
2769 "BitvectorTheoremProducer::negBVor: e = "+e.
toString());
2771 "BitvectorTheoremProducer::negBVor: e = "+e.
toString());
2775 std::vector<Expr> negated;
2782 pf =
newPf(
"bitneg_or", e);
2792 "BitvectorTheoremProducer::negBVxor: e = "+e.
toString());
2794 "BitvectorTheoremProducer::negBVxor: e = "+e.
toString());
2798 std::vector<Expr> children;
2803 children.push_back(*i);
2808 pf =
newPf(
"bitneg_xor", e);
2818 "BitvectorTheoremProducer::negBVxor: e = "+e.
toString());
2820 "BitvectorTheoremProducer::negBVxor: e = "+e.
toString());
2824 if (e[0].arity() > 2) {
2825 std::vector<Expr> children;
2829 children.push_back(*i);
2836 pf =
newPf(
"bitneg_xnor", e);
2843 const vector<int>& idxs,
2849 "BitvectorTheoremProducer::bitwiseConst: e = "+e.
toString());
2853 CHECK_SOUND(idxs.size() >= 2,
"BitvectorTheoremProducer::bitwiseConst():\n e = "
2855 for(
size_t i=0; i<idxs.size(); ++i) {
2857 "BitvectorTheoremProducer::bitwiseConst: idxs["
2862 "BitvectorTheoremProducer::bitwiseConst: e = "+e.
toString());
2868 for(
int bit=0; bit<size; bit++) {
2869 bits.push_back(kind ==
BVAND);
2872 vector<Expr> kids(1);
2875 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
2876 const Expr& ei = e[i];
2880 "BitvectorTheoremProducer::bitwiseConst: e["
2883 "BitvectorTheoremProducer::bitwiseConst: e["
2887 for(
int bit=0; bit<size; bit++)
2893 if (ii < idxs.size() - 1)
2904 Expr res = (kids.size() == 1) ? kids[0] :
2912 vector<Expr> indices;
2913 for(
size_t i=0, iend=idxs.size(); i<iend; ++i)
2914 indices.push_back(
rat(idxs[i]));
2926 "BitvectorTheoremProducer::bitwiseConcat: e = "+e.
toString());
2929 int arity = e.
arity();
2931 for (idx = 0; idx < arity; ++idx) {
2932 if (e[idx].getOpKind() ==
CONCAT)
break;
2937 const Expr& ei = e[idx];
2940 vector<Expr> concatKids;
2945 for(
int i=0, iend=ei.
arity(); i<iend; ++i) {
2948 for(
int j=0; j<arity; ++j) {
2950 kids.push_back(ei[i]);
2954 concatKids.push_back(
Expr(kind, kids));
2964 pf =
newPf(
"bitwise_concat", e,
rat(idx));
2974 "BitvectorTheoremProducer::bitwiseFlatten: e = "+e.
toString());
2982 vector<Expr> flattenkids;
2984 if(i->getOpKind() == kind)
2985 flattenkids.insert(flattenkids.end(),
2986 i->getKids().begin(),i->getKids().end());
2988 flattenkids.push_back(*i);
2995 vector<Expr>::iterator j = flattenkids.begin();
2996 vector<Expr>::iterator jend = flattenkids.end();
2997 bool negate =
false;
2999 for(; output.
isNull() && j != flattenkids.end(); ++j) {
3013 if (kind ==
BVXOR) {
3022 else if (kind ==
BVOR)
3030 "control should not reach here");
3036 vector<Expr> outputkids;
3038 for(; it != likeTerms.
end(); ++it) {
3039 outputkids.push_back((*it).first);
3043 "TheoryBitvector:bitwiseFlatten: fatal error");
3045 if (outputkids.size() == 0) {
3051 if (outputkids.size() == 1) {
3052 output = outputkids[0];
3055 output =
Expr(kind, outputkids);
3061 pf =
newPf(
"bitwise_flatten", e);
3073 "BitvectorTheoremProducer::bitwiseConstElim: e = "+e.
toString());
3078 "BitvectorTheoremProducer::bitwiseConstElim: e = "+e.
toString()
3082 "BitvectorTheoremProducer::bitwiseConstElim: e["+
int2string(idx)
3083 +
"] = "+e[idx].toString());
3089 for (
int i = 0; i < e.
arity(); ++i) {
3090 if (i == idx)
continue;
3091 kids.push_back(e[i]);
3093 if (kids.size() == 1) output = kids[0];
3094 else output =
Expr(kind, kids);
3096 const Expr& c = e[idx];
3099 int hi = bvLength-1;
3101 vector<Expr> concatTerms;
3103 for(--i; i >= 0; --i) {
3105 if (kind ==
BVAND && curVal ==
false) {
3108 else if (kind ==
BVOR && curVal ==
true) {
3113 if (kind ==
BVXOR && curVal ==
true) {
3117 concatTerms.push_back(term);
3123 if (kind ==
BVAND && curVal ==
false) {
3126 else if (kind ==
BVOR && curVal ==
true) {
3130 if (hi < bvLength-1) {
3134 if (kind ==
BVXOR && curVal ==
true) {
3138 concatTerms.push_back(term);
3139 if (concatTerms.size() == 1) {
3140 output = concatTerms[0];
3148 pf =
newPf(
"bitwise_zero", e,
rat(idx));
3169 if(it==likeTerms.
end()) {
3173 if(it0!=likeTerms.
end())
3180 if(negIt!=likeTerms.
end())
3185 if (flag == 0) likeTerms[e] = 1;
3199 "BitvectorTheoremProducer::concatConst: e = "+e.
toString());
3201 "BitvectorTheoremProducer::concatConst: e = "+e.
toString());
3204 for(
int i=e.
arity()-1; i >= 0; --i) {
3210 pf =
newPf(
"concat_const", e);
3220 "BitvectorTheoremProducer::concatFlatten: e = "+e.
toString());
3225 if(i->getOpKind() ==
CONCAT)
3226 kids.insert(kids.end(), i->getKids().begin(), i->getKids().end());
3232 pf =
newPf(
"concat_flatten", e);
3242 "BitvectorTheoremProducer::concatMergeExtract: e = "
3245 "BitvectorTheoremProducer::concatMergeExtract: e = "
3248 "BitvectorTheoremProducer::concatMergeExtract: e = "
3252 const Expr& base = e[0][0];
3257 for(
int i=1, iend=e.
arity(); i<iend; ++i) {
3258 const Expr& ei = e[i];
3260 "BitvectorTheoremProducer::concatMergeExtract: e["
3264 "BitvectorTheoremProducer::concatMergeExtract: e["
3270 "BitvectorTheoremProducer::concatMergeExtract:\n e["
3272 +
"\n e["+
int2string(i)+
"] = "+ei.toString());
3283 pf =
newPf(
"concat_merge_extract", e);
3294 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
3296 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
3298 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
3305 TRACE(
"bitvector rewrite",
"bvplusConst: x(", *i,
") = "+x.
toString());
3307 TRACE(
"bitvector rewrite",
"bvplusConst: acc = ", acc,
"");
3311 vector<bool> res(resSize);
3312 for(
int i=0; i<resSize; i++) {
3313 res[i] = (mod(acc, 2) == 1);
3314 TRACE(
"bitvector rewrite",
"bvplusConst: acc = ", acc,
"");
3322 pf =
newPf(
"bvplus_const", e);
3333 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
3335 "BitvectorTheoremProducer::extractConst: e = "+e.
toString());
3343 vector<bool> res(resSize);
3344 for(
int i=0; i<resSize; i++) {
3345 res[i] = (mod(x, 2) == 1);
3351 pf =
newPf(
"bvmult_const", e);
3359 "BitvectorTheoremProducer::zeroCoeffBVMult: e = "+e.
toString());
3361 "BitvectorTheoremProducer::zeroCoeffBVMult: e = "+e.
toString());
3364 "BitvectorTheoremProducer::zeroCoeffBVMult:"
3365 "coeff must be zero:\n e = " +e.
toString());
3372 pf =
newPf(
"zerocoeff_bvmult", e);
3381 "BitvectorTheoremProducer::oneCoeffBVMult: e = "
3384 "BitvectorTheoremProducer::oneCoeffBVMult: e = "
3388 "BitvectorTheoremProducer::oneCoeffBVMult:"
3389 "coeff must be one:\n e = " +e.
toString());
3396 pf =
newPf(
"onecoeff_bvmult", e);
3406 "BVMULT must have exactly 2 kids: " + e.
toString());
3413 pf =
newPf(
"flip_bvmult", e);
3426 "TheoryBitvector::pad:"
3427 "padding bvLength must be a non-negative integer: "+
3430 "TheoryBitvector::newBVPlusExpr:"
3431 "input must be a BITVECTOR: " + e.
toString());
3437 else if (len < size)
3452 "BitvectorTheoremProducer::padBVPlus: "
3453 "input must be a BVPLUS: " + e.
toString());
3458 if(i->getOpKind() ==
BVMULT) {
3462 kids.push_back(out);
3465 kids.push_back(
pad(len, *i));
3472 pf =
newPf(
"pad_bvplus", e);
3482 "BitvectorTheoremProducer::padBVMult: "
3483 "input must be a BVMULT: " + e.
toString());
3485 BITVECTOR==e[1].getType().getExpr().getOpKind(),
3486 "for BVMULT terms e[0],e[1] must be a BV: " + e.
toString());
3496 pf =
newPf(
"pad_bvmult", e);
3506 "BitvectorTheoremProducer::bvConstMultAssocRule: "
3507 "input must be a BVMULT: " + e.
toString());
3509 "BitvectorTheoremProducer::bvConstMultAssocRule: "
3510 "e[1] must be a BVMULT:\n e= " + e.
toString());
3513 "BitvectorTheoremProducer::bvConstMultAssocRule: "
3514 "e[0] & e[1][0] must be a BVCONST:\n e = " + e.
toString());
3521 CHECK_SOUND(len == len0 && len0 == len10 && len0 == len11,
3522 "BitvectorTheoremProducer::bvConstMultAssocRule: "
3523 "kids of BVMULT must be equibvLength: ");
3532 pf =
newPf(
"bvconstmult_assoc_rule", e);
3544 "BitvectorTheoremProducer::bvMultAssocRule: "
3545 "input must be a BVMULT: " + e.
toString());
3547 BVMULT == e[1].getOpKind(),
3548 "BitvectorTheoremProducer::bvMultAssocRule: "
3549 "e[0] or e[1] must be a BVMULT:\n e= " + e.
toString());
3551 BVCONST == e[1][0].getOpKind()),
3552 "BitvectorTheoremProducer::bvMultAssocRule: "
3553 "e[0] & e[1][0] cannot be a BVCONST:\n e = " +
3561 "BitvectorTheoremProducer::bvMultAssocRule: "
3562 "kids of BVMULT must be equibvLength: ");
3567 std::vector<Expr> outputkids;
3568 if(
BVMULT == e[0].getOpKind() &&
BVMULT != e[1].getOpKind()) {
3569 outputkids.push_back(e0[0]);
3570 outputkids.push_back(e0[1]);
3571 outputkids.push_back(e1);
3573 }
else if(
BVMULT != e[0].getOpKind() &&
BVMULT == e[1].getOpKind()) {
3574 outputkids.push_back(e1[0]);
3575 outputkids.push_back(e1[1]);
3576 outputkids.push_back(e0);
3579 outputkids.push_back(e0[0]);
3580 outputkids.push_back(e0[1]);
3581 outputkids.push_back(e1[0]);
3582 outputkids.push_back(e1[1]);
3584 sort(outputkids.begin(),outputkids.end());
3587 switch(outputkids.size()) {
3608 pf =
newPf(
"bvmult_assoc_rule", e);
3618 "BitvectorTheoremProducer::bvMultDistRule: "
3619 "input must be a BVMULT: " + e.
toString());
3621 "BitvectorTheoremProducer::bvMultDistRule: "
3622 "input must be of the form a*(t1+...+tn): " + e.
toString());
3629 "BitvectorTheoremProducer::bvMultDistRule: "
3630 "all subterms must of equal bvLength: " + e.
toString());
3632 const Expr& e0 = e[0];
3633 const Expr& e1 = e[1];
3635 std::vector<Expr> v;
3638 for(;i != iend; ++i) {
3646 pf =
newPf(
"bvmult_distributivity_rule", e);
3658 "BitvectorTheoremProducer::flattenBVPlus: e = "+e.
toString());
3661 const int numOfKids = e.
arity();
3664 for(
int i=0; i<numOfKids; ++i)
3666 "BitvectorTheoremProducer::flattenBVPlus: "
3667 "summands must be of the same bvLength as BVPLUS:\n e = "
3673 std::vector<Expr> v;
3674 for(
int i = 0; i < numOfKids; ++i) {
3675 if(e[i].getOpKind() ==
BVPLUS) {
3676 const Expr& bvplusKid = e[i];
3677 const int bvplusArity = bvplusKid.
arity();
3678 for(
int j=0; j < bvplusArity; ++j)
3679 v.push_back(bvplusKid[j]);
3687 pf =
newPf(
"flatten_bvplus", e);
3699 if(it!=likeTerms.
end())
3700 likeTerms[term] += coefficient;
3703 bool foundNegated=
false;
3704 if (!likeTerms.
empty()) {
3707 it = likeTerms.
find(negTerm);
3708 if (it!= likeTerms.
end()) {
3709 foundNegated =
true;
3712 likeTerms[negTerm] += -coefficient;
3718 likeTerms[term] = coefficient;
3731 for(; i!=iend; ++i) {
3736 if (s[0].getKind() ==
BVCONST) {
3738 const Expr& var = s[1];
3744 "TheoryBitvector::combineLikeTerms: "
3745 "Unexpected MULT syntax:\n\n s = " + s.
toString()
3772 if (ret< lowerBound)
3788 std::vector<Expr> & result) {
3792 for(
int i=0; i<bvplusLength; i += 1) power2 *= 2;
3796 for(; j!=jend; ++j) {
3801 if(coefficient == 0)
3803 Expr multiplicand = j->first;
3805 if (coefficient<0) {
3810 coefficient= coefficient*-1;
3811 plusConstant +=coefficient;
3813 if(coefficient == 1)
3814 monomial = multiplicand;
3823 "TheoryBitvector::combineLikeTerms:"
3824 "each monomial must be a bitvector:\n"
3825 "monomial = " + monomial.
toString());
3827 "TheoryBitvector::combineLikeTerms:"
3828 "bvLength of each monomial must be the same as e:\n"
3831 result.push_back(monomial);
3837 if(plusConstant != 0) {
3840 result.push_back(c);
3846 const std::vector<Expr>&items){
3849 switch(items.size()) {
3866 TRACE(
"bitvector rewrite",
"combineLikeTermsRule(",e.
toString(),
") {");
3869 "TheoryBitvector::combineLikeTerms: "
3870 "input must be a BVPLUS term:\n e = " + e.
toString());
3878 "TheoryBitvector::combineLikeTerms: "
3879 "BVPLUS must be flattened:\n e = " + e.
toString());
3885 "TheoryBitvector::combineLikeTerms: "
3886 "BVPLUS must be padded:\n e = " + e.
toString());
3891 CHECK_SOUND(bvplusLength == s0len && s0len== s1len,
3892 "all monoms must have the samebvLength "
3893 "as the bvplus term: " + e.
toString());
3902 std::vector<Expr> collection;
3907 TRACE(
"bitvector rewrite",
3908 "combineLikeTermsRule =>",output.
toString(),
"}");
3911 pf=
newPf(
"bvplus_combine_like_terms", e);
3919 "BitvectorTheoremProducer::lhsMinusRhsRule: "
3920 "input must be an EQ: e = " +e.
toString());
3922 BVPLUS == e[1].getOpKind(),
3923 "BitvectorTheoremProducer::lhsMinusRhsRule: "
3924 "atleast one of the input subterms must be BVPLUS:"
3929 "BitvectorTheoremProducer::lhsMinusRhsRule: "
3930 "both sides of EQ must be same Length. e = " +e.
toString());
3934 "BitvectorTheoremProducer::lhsMinusRhsRule: "
3935 "all subterms of e[0] must be of same Length."
3941 "BitvectorTheoremProducer::lhsMinusRhsRule: "
3942 "all subterms of e[1] must be of same Length."
3948 std::vector<Expr> k;
3954 output =
Expr(
EQ, zeroStr, zeroStr);
3957 std::vector<Expr> e0K = e[0].
getKids();
3958 std::vector<Expr> e1K = e[1].
getKids();
3959 for(vector<Expr>::iterator i=e0K.begin(),iend=e0K.end();i!=iend;++i){
3960 for(vector<Expr>::iterator j=e1K.begin(),jend=e1K.end();j!=jend;++j){
3969 k.push_back(newLhs);
3974 k.push_back(uminus);
3978 output =
Expr(
EQ, lhsMinusRhs, zeroStr);
3983 pf =
newPf(
"lhs_minus_rhs_rule", e);
3992 "BitvectorTheoremProducer::bvuminusBitBlastRule: "
3993 "input must be bvuminus: e = " + e.
toString());
3996 std::vector<Expr> k;
4000 k.push_back(plusOne);
4005 pf =
newPf(
"bvuminus_bitblast_rule", e);
4015 "BitvectorTheoremProducer::bvuminusBVConst: "
4016 "e should be bvuminus, e[0] should be bvconst: e = " +
4032 pf =
newPf(
"bvuminus_bvconst_rule", e);
4041 "BitvectorTheoremProducer::bvuminusBVMult: "
4042 "e should be bvuminus: e =" + e.
toString());
4044 "Bitvectortheoremproducer::bvuminusBVMult: "
4045 "in input expression e = " + e.
toString() +
4046 "\ne[0] should be bvmult: e[0] = " + e[0].
toString());
4048 "Bitvectortheoremproducer::bvuminusBVMult: "
4049 "in input expression e = " + e.
toString() +
4050 "\ne[0][0] should be bvconst: e[0][0] = " + e[0][0].
toString());
4054 CHECK_SOUND(bvLength == e0Length && e0Length == e00Length,
4055 "Bitvectortheoremproducer::bvuminusBVMult: "
4056 "in input expression e = " + e.
toString() +
4057 "\nLengths of all subexprs must be equal: e = " + e.
toString());
4067 else if (1 == coeff)
4078 pf =
newPf(
"bvuminus_bvmult_rule", e);
4087 "BitvectorTheoremProducer::bvuminusBVUminus: "
4088 "e should be bvuminus: e =" + e.
toString());
4090 "Bitvectortheoremproducer::bvuminusBVUminus: "
4091 "in input expression e = " + e.
toString() +
4092 "\ne[0] should be bvmult: e[0] = " + e[0].
toString());
4099 pf =
newPf(
"bvuminus_bvuminus_rule", e);
4108 "BitvectorTheoremProducer::bvuminusVar: "
4109 "e should be bvuminus: e =" + e.
toString());
4112 std::vector<bool> res;
4114 for(
int i=0; i<e0Length; ++i) {
4115 res.push_back(
true);
4122 pf =
newPf(
"bvuminus_var_rule", e);
4131 "BitvectorTheoremProducer::bvmultBVUminus: "
4132 "e should be bvuminus: e =" + e.
toString());
4134 BVCONST == e[0][0].getKind() &&
4136 "Bitvectortheoremproducer::bvmultBVUminus: "
4137 "in input expression e = " + e.
toString() +
4138 "\ne[0] has to be bvmult"
4139 "e[0][1] must be bvuminus: e[0] = " + e[0].
toString());
4143 CHECK_SOUND(bvLength == e00Length && e00Length == e01Length,
4144 "Bitvectortheoremproducer::bvmultBVUminus: "
4145 "in input expression e = " + e.
toString() +
4146 "\nLengths of all subexprs must be equal.");
4150 const Expr& coeff = e[0][0];
4152 const Expr& e010 = e[0][1][0];
4154 if(0 == negatedcoeff)
4157 else if (1 == negatedcoeff)
4168 pf =
newPf(
"bvmult_bvuminus_rule", e);
4204 pf =
newPf(
"bvminus_bvplus_rule", e);
4214 "BitvectorTheoremProducer::extractBVMult: "
4215 "input must be an EXTRACT over BVMULT:\n e = "+e.
toString());
4217 const Expr& bvmult = e[0];
4224 "BitvectorTheoremProducer::extractBVMult: "
4225 "bvmult Length must be greater than extract Length:\n e = "
4236 pf =
newPf(
"extract_bvmult_rule", e);
4244 "BitvectorTheoremProducer::extractBVPlus: "
4245 "input must be an EXTRACT over BVPLUS:\n e = "+e.
toString());
4247 const Expr& bvplus = e[0];
4254 "BitvectorTheoremProducer::extractBVPlus: "
4255 "bvplus Length must be greater than extract bvLength:\n e = "
4260 if(bvplusLen == extractHi+1)
4270 pf =
newPf(
"extract_bvplus_rule", e);
4280 "BitvectorTheoremProducer::typePredBit: e = "+e.
toString());
4282 "BitvectorTheoremProducer::typePredBit: e = "+e.
toString());
4287 pf=
newPf(
"type_pred_bit", e);
4299 "BitvectorTheoremProducer::expandTypePred: "
4300 "Expected BV_TYPE_PRED wrapper:\n tp = "
4314 for(
int i=0; i<size; i++) {
4316 kids.push_back(bit.eqExpr(
bvZero()) || bit.eqExpr(
bvOne()));
4351 ( e[0] == bv_zero || e[1] == bv_zero ),
4352 "MarkNonSolvableEq: input must be a canonized equation" + e.
toString());
4353 if( e[1] == bv_zero )
4378 "isolate_var: input must be an equation with lhs non-cosnt and rhs must be zero" + e.
toString());
4390 if( lhs[0].getOpKind() ==
BVCONST )
4393 lhs[1].getOpKind() !=
BVPLUS,
"Should have been canonized");
4395 "Expected even coeff");
4401 int e_kid_arity = lhs.
arity();
4402 bool foundUnitCoeff =
false;
4403 Expr new_lhs, new_rhs, new_coeff;
4404 vector<Expr> newKids;
4406 for(
int i = 0; i < e_kid_arity; ++i)
4409 Expr e_sub_kid = lhs[i];
4412 DebugAssert(const_term == 0,
"Expected only one constant");
4417 if( e_sub_kid[0].getOpKind() ==
BVCONST )
4421 DebugAssert(tmp != 1,
"Expected coeff other than 1");
4422 tmp = (tmp * (modulus-1)) % modulus;
4432 if (!foundUnitCoeff) {
4433 foundUnitCoeff =
true;
4434 new_lhs = e_sub_kid;
4443 if (foundUnitCoeff) {
4444 DebugAssert(newKids.size() > 0,
"Expected non-empty kids");
4446 if (newKids.size() == 1) {
4447 new_rhs = newKids[0];
4452 res_expr =
Expr(
EQ, new_lhs, new_rhs);
4468 "Expected no change or solved form");
4623 "BitvectorTheoremProducer::BVMult_order_vars: input must be a BVMULT expression" + e.
toString());
4632 bool hasConst =
false;
4633 if (e[0].getOpKind() ==
BVCONST) {
4641 int vars_size = vars.size();
4644 for(
int i=0; i < vars_size; ++i)
4648 if( vars_map.
count( vars[i] ) == 0)
4649 vars_map[ vars[i] ] = 1;
4651 vars_map[ vars[i] ] = vars_map[ vars[i] ] + 1;
4657 new_expr = (*j).first;
4658 if ((*j).second != 1) {
4659 for(
int k=1; k < (*j).second; ++k) {
4664 for( ++j; j != vars_map.
end(); ++j) {
4666 if ((*j).second != 1) {
4667 for(
int k=1; k < (*j).second; ++k) {
4691 "BitvectorTheoremProducer::liftConcatBVMult: input must be a BVMULT expression" + e.
toString());
4698 for (; i< e.
arity(); ++i) {
4699 const Expr& kid = e[i];
4705 else if (kid[0].getKind() ==
BVCONST &&
4710 else kids.push_back(kid);
4712 else kids.push_back(kid);
4716 Expr concatHi, concatLo;
4720 if (e[idx].arity() == 2) {
4721 concatLo = e[idx][1];
4724 vector<Expr> concatKids;
4725 for (i = 1; i < e[idx].
arity(); ++i) {
4726 concatKids.push_back(e[idx][i]);
4730 concatHi = e[idx][0];
4734 vector<Expr> concatKids = e[idx].
getKids();
4735 concatLo = concatKids.back();
4736 concatKids.pop_back();
4737 if (concatKids.size() == 1) {
4738 concatHi = concatKids[0];
4746 kids.push_back(concatLo);
4749 kids.push_back(concatHi);
4772 TRACE(
"canonBVMult",
"canonBVMult: {\n ", e.
toString(),
" --");
4775 "BitvectorTheoremProducer::canonBVMult: input must be a BVMULT expression" + e.
toString());
4778 int expr_arity = e.
arity();
4781 std::vector<Expr> mult_vars;
4790 for(
int i = 0; i < expr_arity; ++i) {
4791 if (e[i].getOpKind() ==
BVUMINUS) {
4792 temp_coeff = (temp_coeff * (modulus-1)) % modulus;
4793 no_minus_kid = e[i][0];
4794 }
else no_minus_kid = e[i];
4801 temp_coeff = temp_coeff % modulus;
4806 if (no_minus_kid[0].getOpKind() ==
BVCONST) {
4809 temp_coeff = temp_coeff % modulus;
4811 no_minus_kid[1].getOpKind() !=
BVPLUS &&
4812 no_minus_kid[1].getOpKind() !=
BVUMINUS,
4813 "Expected canonized subterm");
4815 if (!new_prod.
isNull()) {
4821 new_prod = no_minus_kid[1];
4825 if (!new_prod.
isNull()) {
4831 new_prod = no_minus_kid;
4844 if (!new_prod.
isNull()) {
4850 new_prod = no_minus_kid;
4856 if (temp_coeff == 0 || new_prod.
isNull()) {
4886 "BitvectorTheoremProducer::distributive_rule: input must be a BVMULT expression" + e.
toString());
4893 vector<Expr> e0_kids, e1_kids, result_kids;
4895 if (e[0].getOpKind() ==
BVPLUS) {
4898 else e0_kids.push_back(e[0]);
4900 if (e[1].getOpKind() ==
BVPLUS) {
4903 else e1_kids.push_back(e[1]);
4905 unsigned e0_kids_size = e0_kids.size();
4906 unsigned e1_kids_size = e1_kids.size();
4907 for(
unsigned i = 0; i < e0_kids_size; ++i) {
4908 for(
unsigned j = 0; j < e1_kids_size; ++j) {
4910 result_kids.push_back( sum_term );
4928 "BitvectorTheoremProducer::liftConcatBVPlus: input must be a BVPLUS expression" + e.
toString());
4935 if (e[0].getOpKind() ==
BVCONST) {
4940 int chopSize = bv_size;
4942 bool nonzero =
false;
4943 bool nonconst =
false;
4946 for (; i< e.
arity(); ++i) {
4947 const Expr& kid = e[i];
4958 if (nonzero || size > chopSize) {
4972 if (size >= chopSize)
continue;
4982 if (size < chopSize) chopSize = size;
4990 if ((c % modulus) != 0) {
5002 vector<Expr> newKids;
5003 for (i = 0; i < e.
arity(); ++i) {
5026 vector<Expr> plusTerms;
5027 vector<Rational> coeffs;
5029 plusTerms.push_back(e);
5030 coeffs.push_back(1);
5033 for(i = 0; i < plusTerms.size(); ++i) {
5034 Expr kid = plusTerms[i];
5036 DebugAssert(kidSize <= bv_size,
"Expected kid no wider than bv_size");
5038 if (coeff == 0)
continue;
5044 known_term = known_term % modulus;
5048 DebugAssert(kidSize == bv_size,
"Unexpected size for uminus");
5049 plusTerms.push_back(plusTerms[i][0]);
5050 coeffs.push_back((coeff * (modulus - 1)) % modulus);
5054 if (kidSize < bv_size) {
5056 known_term += coeff * (m2-1);
5059 known_term += coeff * (modulus-1);
5061 known_term = known_term % modulus;
5062 plusTerms.push_back(plusTerms[i][0]);
5063 coeffs.push_back((coeff * (modulus-1)) % modulus);
5067 if (kidSize < bv_size) {
5070 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
5071 if (shift + kidSize < bv_size) {
5074 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
5079 if( kid[0].getOpKind() ==
BVCONST )
5082 plusTerms.push_back(kid[1]);
5087 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
5092 if (kidSize < bv_size) {
5095 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
5096 if (shift + kidSize < bv_size) {
5099 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
5104 int kid_arity = kid.
arity();
5105 for(
int j = 0; j < kid_arity; ++j) {
5106 plusTerms.push_back(kid[j]);
5107 coeffs.push_back(coeff);
5116 for (
int j = 0; j < kid.
arity(); ++j) {
5117 const Expr& concatKid = kid[j];
5120 plusTerms.push_back(concatKid);
5121 coeffs.push_back(concatConst % modulus);
5128 if (
false && kidSize < bv_size) {
5130 const Expr& ext_kid = kid[0];
5133 if (extractLeft < size-1) {
5136 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
5137 if (shift + kidSize >= bv_size) {
5138 int bitsToAdd = bv_size - kidSize;
5139 extractLeft += bitsToAdd;
5140 if (extractLeft > size - 1) extractLeft = size - 1;
5142 if (extractLeft == size-1 && extractRight == 0) {
5143 plusTerms.push_back(ext_kid);
5144 coeffs.push_back(coeff);
5148 coeffs.push_back(coeff);
5155 "Unexpected extract bounds");
5162 sumHashMap[ kid] = sumHashMap[ kid] + coeff;
5170 vector<Expr>& concatKids)
5172 int chopSize = bv_size;
5174 bool nonzero =
false;
5175 bool nonconst =
false;
5176 Expr term, kid, last;
5180 for (i = 0; i< concatKids.size(); ++i) {
5181 kid = concatKids[i];
5184 last = kid[kid.
arity()-1];
5191 if (nonzero || size > chopSize)
return Expr();
5203 if (size >= chopSize)
continue;
5204 if (nonconst)
return Expr();
5211 if (nonzero)
return Expr();
5213 if (size < chopSize) chopSize = size;
5222 if ((c % modulus) != 0)
return Expr();
5237 for (i = 0; i < concatKids.size(); ++i) {
5238 kid = concatKids[i];
5239 vector<Expr> kids = kid.
getKids();
5244 if (size != chopSize) {
5245 DebugAssert(size > chopSize,
"Expected last to be wider than chopSize");
5249 value = value - (value % modulus);
5250 value = value / modulus;
5254 DebugAssert(kids.size() > 0,
"Expected size > 0");
5255 if (kids.size() == 1) {
5256 concatKids[i] = kids[0];
5267 value = value % modulus;
5274 vector<Expr> kids = bvPlus.
getKids();
5275 kids.push_back(term);
5279 vector<Expr> newKids;
5283 for (i = 0; i < concatKids.size(); ++i) {
5284 newKids.push_back(concatKids[i]);
5286 DebugAssert(newKids.size() > 1,
"Expected more than one kid");
5293 bvPlus =
buildPlusTerm(bv_size-chopSize, known_term, sumHashMap);
5305 Rational tmask, tcoeff, marked = 0;
5308 vector<Expr> multKids, concatKids;
5310 for(; j != sumHashMap.
end(); ++j) {
5311 coeff = mod((*j).second, modulus);
5312 Expr term = (*j).first;
5316 if (coeff == 1 && nbits == bv_size) {
5317 if (nbits == 1 && known_term == 1) {
5323 multKids.push_back(term);
5328 while (coeff != 0) {
5330 for (pos = coeff, lg = 0; pos % 2 == 0; pos = pos / 2, ++lg);
5338 Rational tcoeff = coeff % tmodulus;
5340 if (tcoeff == pos) {
5344 else if (((tcoeff + pos) % tmodulus) == 0) {
5345 coeff = (coeff + pos) % modulus;
5349 if (nbits + lg < bv_size) {
5350 known_term += (modulus - tmodulus);
5352 if (pos == 1 && nbits == bv_size) {
5353 multKids.push_back(concatTerm);
5359 if (nbits + lg > bv_size) {
5361 int diff = nbits + lg - bv_size;
5370 high = nbits - 1 - diff;
5375 nbits = bv_size - lg;
5376 coeff = coeff / pos;
5381 multKids.push_back(term);
5391 int bits, size, k, t_arity;
5392 for (i = 0; i < concatKids.size(); ++i) {
5396 t_arity = t.
arity();
5397 for (k = 0; k < t_arity; ++k) {
5398 if (k > 0 && bits < lg + nbits)
break;
5400 if (bits - size <= lg) {
5401 if (t[k].getOpKind() ==
BVCONST) {
5407 tmp.push_back(t[k]);
5419 if (lg + nbits < bits) {
5422 if (lg + nbits > bits) {
5423 bool negate =
false;
5427 concatTerm = concatTerm[0];
5430 "Too big only OK for first child");
5432 int diff = lg + nbits - bits;
5438 concatTerm = concatTerm[0];
5441 high = nbits - 1 - diff;
5449 tmp.push_back(concatTerm);
5454 for (++k; k < t_arity; ++k) {
5455 tmp.push_back(t[k]);
5458 if (tmp.size() == 1) {
5460 multKids.push_back(tmp[0]);
5473 known_term = known_term % modulus;
5476 if (known_term != 0 && !concatKids.empty()) {
5478 for (i = 0; i < concatKids.size(); ++i) {
5479 Expr t = concatKids[i];
5483 bool anyChanged =
false;
5484 for (
int k = 0; k < t.
arity(); ++k) {
5486 bool changed =
false;
5487 if (known_term != 0 && t[k].getOpKind() ==
BVCONST) {
5489 Rational partConst = known_term % high;
5490 if (partConst != 0) {
5492 partConst = partConst - (partConst % low);
5493 if (partConst != 0) {
5494 anyChanged = changed =
true;
5496 known_term -= partConst;
5501 tmp.push_back(t[k]);
5507 if (known_term == 0)
break;
5517 if (multKids.size() == 0 &&
5518 (concatKids.size() > 1 ||
5519 (concatKids.size() == 1 && known_term != 0))) {
5520 expr_result =
chopConcat(bv_size, known_term, concatKids);
5521 if (!expr_result.
isNull())
return expr_result;
5524 if (known_term == 0) {
5525 for (i = 0; i < concatKids.size(); ++i) {
5526 multKids.push_back(concatKids[i]);
5528 if (multKids.size() == 0) {
5531 else if (multKids.size() == 1) {
5532 expr_result = multKids[0];
5539 vector<Expr> sumKids;
5541 for (i = 0; i < multKids.size(); ++i) {
5542 sumKids.push_back(multKids[i]);
5544 for (i = 0; i < concatKids.size(); ++i) {
5545 sumKids.push_back(concatKids[i]);
5547 if (sumKids.size() == 1) {
5548 expr_result = sumKids[0];
5561 TRACE(
"canonBVPlus",
"canonBVPlus: {\n ", e.
toString(),
" --");
5565 "BitvectorTheoremProducer::canonBVPlus: input must be a BVPLUS expression" + e.
toString());
5582 TRACE(
"canonBVPlus",
"--> ", expr_result.
toString(),
"\n}");
5591 "BitvectorTheoremProducer::canonBVUMinus: input must be a BVUMINUS expression" + e.
toString());
5615 "BitvectorTheoremProducer::processExtract: invalid input");
5617 "Expected same size");
5623 Expr child = ext[0];
5632 vector<Expr> boundVars;
5633 if (high < size-1) {
5635 boundVars.push_back(terms.back());
5637 if (solvedForm) terms.push_back(rhs);
5640 terms.push_back(lhs);
5641 boundVars.push_back(lhs);
5645 boundVars.push_back(terms.back());
5647 DebugAssert(terms.size() > 1,
"Expected at least two terms");
5649 if (!solvedForm) result = result && lhs.
eqExpr(rhs);
5680 FatalAssert(
false,
"unexpected kind in okToSplit");
5695 DebugAssert(maxEffort == 3 || maxEffort == 5 || maxEffort == 6,
5696 "Unexpected value for maxEffort");
5699 "BitvectorTheoremProducer::canonBVEQ: expression must be an equation");
5701 "input must be a bitvector eqn. \n e = " + e.
toString());
5729 DebugAssert(lsize <= bv_size && rsize <= bv_size,
"invariant violated");
5730 if (lsize < rsize) {
5740 else if (lsize > rsize) {
5755 if (splitSize != bv_size) {
5762 expr_result = tmp && expr_result;
5763 TRACE(
"canonBVEQ",
"--> ", expr_result.toString(),
"\n}");
5791 Expr xor_leaf, leaf, foundterm;
5792 unsigned xor_idx=0, xor_size=0;
5793 int priority, size, foundpriority = 7;
5795 for(; j != sumHashMap.
end(); ++j) {
5796 Expr t = (*j).first;
5797 coeff = (*j).second;
5799 if (j == fixCoeff) {
5800 coeff = (*j).second = mod(coeff, modulus);
5803 if (coeff == 0)
continue;
5807 if (coeff % 2 == 1) {
5809 if (size == bv_size) {
5810 leaf = t; priority = 1;
5811 }
else if (size > bv_size) {
5813 leaf = t; priority = 3;
5815 leaf = t; priority = 4;
5820 if (size >= bv_size) {
5821 leaf = t[0]; priority = 3;
5823 leaf = t[0]; priority = 4;
5826 if (foundpriority == 2)
continue;
5828 xor_size = t.
arity();
5829 for (xor_idx = 0; xor_idx < xor_size; ++xor_idx) {
5834 for (; l < xor_size; ++l) {
5835 if (l == xor_idx)
continue;
5838 if (l < xor_size)
continue;
5841 if (xor_idx < xor_size) {
5847 leaf = t; priority = 6;
5851 leaf = t; priority = 6;
5853 }
else if (maxEffort >= 5) {
5855 leaf = t; priority = 5;
5859 leaf = t[0]; priority = 5;
5863 if (priority < foundpriority) {
5866 while (k != sumHashMap.
end()) {
5870 if (k == fixCoeff) {
5871 (*k).second = mod((*k).second, modulus);
5874 if ((*k).second == 0) {
5878 if (priority == 2) {
5880 for (++xor_idx; xor_idx < xor_size; ++xor_idx) {
5885 for (; l < xor_size; ++l) {
5886 if (l == xor_idx)
continue;
5889 if (l < xor_size)
continue;
5892 if (xor_idx < xor_size) {
5896 k = sumHashMap.
begin();
5905 if (k == sumHashMap.
end()) {
5906 foundpriority = priority;
5908 if (coeff == 1 || priority == 5) foundCoeff = 1;
5910 if (priority == 1)
break;
5913 if (foundpriority > 6 && priority != 5) {
5916 if (coeff == 1) foundCoeff = 1;
5922 bool solving = (foundpriority <= maxEffort);
5924 if (foundpriority == 7) {
5926 if (known_term % 2 == 1) {
5932 else foundCoeff = foundCoeff /
Rational(2);
5934 bv_size = bv_size - 1;
5941 TRACE(
"canonBVEQ",
"--> ", e,
"\n}");
5948 if (solving || foundCoeff != 1) {
5949 known_term = (known_term * foundCoeff) % modulus;
5950 if (solving && known_term != 0)
5951 known_term = modulus - known_term;
5952 for(j = sumHashMap.
begin(); j != sumHashMap.
end(); ++j) {
5953 coeff = (*j).second;
5954 if (coeff == 0)
continue;
5955 (*j).second = (coeff * foundCoeff) % modulus;
5957 if ((*j).first == foundterm) {
5959 solveCoeff = (*j).second;
5963 (*j).second = modulus - (*j).second;
5972 Expr new_lhs, new_rhs, expr_result;
5975 DebugAssert(solveCoeff != 0,
"Expected solveCoeff != 0");
5980 switch (foundpriority) {
5987 DebugAssert(solveCoeff == 1,
"Expected coeff = 1");
5988 new_lhs = foundterm;
5993 DebugAssert(solveCoeff == 1,
"Expected coeff = 1");
5994 vector<Expr> rhsTerms;
5995 rhsTerms.push_back(plusTerm);
5996 for (
unsigned l = 0; l < xor_size; ++l) {
5997 if (l == xor_idx)
continue;
5998 rhsTerms.push_back(foundterm[l]);
6007 DebugAssert(solveCoeff == 1,
"Expected coeff = 1");
6019 new_lhs = foundterm;
6025 DebugAssert(solveCoeff == 1,
"Expected coeff = 1");
6027 DebugAssert(foundtermsize < bv_size,
"Expected undersized term");
6029 expr_result = foundterm.
eqExpr(new_rhs);
6032 expr_result = expr_result && new_lhs.
eqExpr(new_rhs);
6039 for (; solveCoeff % 2 == 0; solveCoeff = solveCoeff / 2, ++lg);
6043 expr_result = new_lhs.
eqExpr(new_rhs);
6046 expr_result = expr_result && new_lhs.
eqExpr(new_rhs);
6059 if (expr_result.
isNull()) {
6060 if ( new_lhs == new_rhs) {
6063 else if ( new_lhs >= new_rhs) {
6064 expr_result =
Expr(
EQ, new_lhs, new_rhs);
6067 expr_result =
Expr(
EQ, new_rhs, new_lhs);
6084 "input must be a bitvector. \n e = " + e.
toString());
6086 "input must be BVZEROEXTEND(e).\n e = " + e.
toString());
6091 if (extendLen == 0) {
6101 pf =
newPf(
"zero_extend_rule");
6112 "input must be a bitvector. \n e = " + e.
toString());
6114 "input must be BVREPEAT(e).\n e = " + e.
toString());
6116 "Expected positive repeat value");
6121 if (repeatVal == 1) {
6126 for (
int i = 0; i < repeatVal; ++i) {
6127 kids.push_back(e[0]);
6134 pf =
newPf(
"repeat_rule");
6145 "input must be a bitvector. \n e = " + e.
toString());
6147 "input must be BVROTL(e).\n e = " + e.
toString());
6152 rotation = rotation % bvsize;
6154 if (rotation == 0) {
6165 pf =
newPf(
"rotl_rule");
6176 "input must be a bitvector. \n e = " + e.
toString());
6178 "input must be BVROTR(e).\n e = " + e.
toString());
6183 rotation = rotation % bvsize;
6185 if (rotation == 0) {
6196 pf =
newPf(
"rotr_rule");
6202 const Expr& a = remExpr[0];
6203 const Expr& b = remExpr[1];
6212 Rational rem_value = a_value - floor(a_value / b_value)*b_value;
6215 static int div_by_zero_count = 0;
6216 div_by_zero_count ++;
6217 char var_name[10000];
6218 sprintf(var_name,
"mod_by_zero_const_%d", div_by_zero_count);
6224 pf =
newPf(
"bvUDivConst");
6230 Expr a = remExpr[0];
6231 Expr b = remExpr[1];
6238 pf =
newPf(
"bvURemRewrite", remExpr);
6245 const Expr& a = divExpr[0];
6246 const Expr& b = divExpr[1];
6255 Rational div_value = floor(a_value / b_value);
6258 static int div_by_zero_count = 0;
6259 div_by_zero_count ++;
6260 char var_name[10000];
6261 sprintf(var_name,
"div_by_zero_const_%d", div_by_zero_count);
6267 pf =
newPf(
"bvUDivConst");
6281 const Expr a = divExpr[0];
6282 const Expr b = divExpr[1];
6288 vector<Expr> boundVars;
6289 boundVars.push_back(div);
6290 boundVars.push_back(mod);
6292 vector<Expr> assertions;
6298 assertions.push_back(a_expanded.
eqExpr(
6318 pf =
newPf(
"bvUDiv");
6325 const Expr& a_times_b, std::vector<Theorem>& output_bits)
6331 CHECK_SOUND(a_bits.size() == b_bits.size(),
"given bit expansions of different size");
6335 int size = a_bits.size();
6361 vector<Expr> sum_bits;
6362 vector<Expr> carry_bits;
6366 for (a_bit = size - 1; a_bit >= 0 && a_bits[a_bit].getRHS() == falseExpr; a_bit --);
6367 for (b_bit = size - 1; b_bit >= 0 && b_bits[b_bit].getRHS() == falseExpr; b_bit --);
6371 int new_size = size;
6372 if (a_bit + b_bit + 2 < new_size) new_size = a_bit + b_bit + 2;
6375 for (
int i = 0; i < new_size; i ++) {
6376 sum_bits.push_back(a_bits[i].getRHS().
andExpr(b_bits[0].getRHS()));
6382 for (
int row = 1; row < new_size; row ++) {
6383 for (
int bit = new_size-1; bit >= row; bit --) {
6384 Expr m = a_bits[bit-row].getRHS().andExpr(b_bits[row].getRHS());
6385 Expr sum = sum_bits[bit].iffExpr(m).iffExpr(carry_bits[bit - 1]);
6386 Expr carry = sum_bits[bit].andExpr(m).orExpr(carry_bits[bit - 1].
andExpr(sum_bits[bit].
orExpr(m)));
6387 sum_bits[bit] = sum;
6388 carry_bits[bit] = carry;
6391 carry = carry.
orExpr(carry_bits[new_size - 1]);
6395 for (
int bit = 0; bit < size; bit ++) {
6398 pf =
newPf(
"bitblastBVMult", a_times_b,
rat(bit));
6408 const Expr& a_plus_b, std::vector<Theorem>& output_bits)
6414 CHECK_SOUND(a_bits.size() == b_bits.size(),
"given bit expansions of different size");
6418 int size = a_bits.size();
6421 Expr a = a_plus_b[0];
6422 for (
int bit = 0; bit < size; bit++) {
6427 Expr b = a_plus_b[1];
6428 for (
int bit = 0; bit < size; bit++) {
6435 vector<Expr> sum_bits;
6438 for (
int i = 0; i < size; i ++)
6440 Expr a_i = a_bits[i].getRHS();
6441 Expr b_i = b_bits[i].getRHS();
6447 for (
int bit = 0; bit < size; bit ++) {
6450 pf =
newPf(
"bitblastBVPlus", a_plus_b,
rat(bit));
6485 Expr s = sDivExpr[0];
6486 Expr t = sDivExpr[1];
6541 Expr s = sRemExpr[0];
6542 Expr t = sRemExpr[1];
6602 Expr s = sModExpr[0];
6603 Expr t = sModExpr[1];
6635 CHECK_SOUND(orEqZero[0].getKind() ==
BVOR,
"left-hand side must be a bitwise or. \n e = " + orEqZero.
toString());
6640 vector<Expr> conjuncts;
6642 for (
int disjunct = 0; disjunct < orEqZero[0].
arity(); disjunct ++)
6643 conjuncts.push_back(orEqZero[0][disjunct].
eqExpr(orEqZero[1]));
6657 CHECK_SOUND(andEqOne[0].getKind() ==
BVAND,
"left-hand side must be a bitwise and. \n e = " + andEqOne.
toString());
6662 vector<Expr> conjuncts;
6664 for (
int conjunct = 0; conjunct < andEqOne[0].
arity(); conjunct ++)
6665 conjuncts.push_back(andEqOne[0][conjunct].
eqExpr(andEqOne[1]));
6694 if (eq[0].getOpKind() !=
EXTRACT)
return false;
6695 if (eq[1].getOpKind() !=
EXTRACT)
return false;
6697 if (eq[0][0] != eq[1][0])
return false;
6706 if (i == k)
return false;
6708 return (k >= j && j > l);
6710 return (i >= l && l > j);
6734 vector<Expr> boundVars;
6741 if (i < x_size - 1) {
6743 terms.push_back(x_begin);
6744 boundVars.push_back(x_begin);
6747 if (2*k + 1 <= i + j)
6754 int o_size = k - j + 1;
6755 bool no_rest = (2*k + 1 == i + j);
6759 boundVars.push_back(a);
6769 boundVars.push_back(b);
6782 int o_size = k - j + 1;
6787 int different_pieces = r_size / d;
6789 for (
int p = 0; p < different_pieces; p ++) {
6791 boundVars.push_back(piece);
6792 terms.push_back(piece);
6795 int other_pieces = (o_size + r_size) / d;
6796 for (
int p = 0; p < other_pieces; p ++)
6797 terms.push_back(terms[terms.size() - different_pieces]);
6803 terms.push_back(x_end);
6804 boundVars.push_back(x_end);