32 #define HASH_VALUE_ZERO 380
33 #define HASH_VALUE_ONE 450
45 int TheoryBitvector::BVSize(
const Expr& e)
47 Type tp(getBaseType(e));
50 return getBitvectorTypeParam(tp);
59 Expr TheoryBitvector::pad(
int len,
const Expr& e)
62 "TheoryBitvector::newBVPlusExpr:"
63 "padding length must be a non-negative integer: "+
66 "TheoryBitvector::newBVPlusExpr:"
67 "input must be a BITVECTOR: " + e.
toString());
74 res = newBVExtractExpr(e,len-1,0);
77 Expr zero = newBVZeroString(len-size);
78 res = newConcatExpr(zero,e);
97 "TheoryBitvector::bitBlastEqn:"
98 "expecting an equation" + e.
toString());
99 const Expr& leftBV = e[0];
100 const Expr& rightBV = e[1];
104 BITVECTOR == rightType.getExpr().getOpKind(),
105 "TheoryBitvector::bitBlastEqn:"
106 "lhs & rhs must be bitvectors");
108 "TheoryBitvector::bitBlastEqn:\n e = "
111 Theorem result = reflexivityRule(e);
114 std::vector<Theorem> substThms;
115 std::vector<Theorem> leftBVrightBVThms;
116 int bvLength = BVSize(leftBV);
120 for(; bitPosition < bvLength; ++bitPosition) {
122 bitBlastLeftThm = bitBlastTerm(leftBV, bitPosition);
124 bitBlastRightThm = bitBlastTerm(rightBV, bitPosition);
127 leftBVrightBVThms.push_back(bitBlastLeftThm);
128 leftBVrightBVThms.push_back(bitBlastRightThm);
132 Theorem thm = substitutivityRule(
IFF, leftBVrightBVThms);
133 thm = transitivityRule(thm, rewriteBoolean(thm.
getRHS()));
134 leftBVrightBVThms.clear();
135 substThms.push_back(thm);
139 return transitivityRule(result,
140 d_rules->bitvectorFalseRule(thm));
144 Theorem thm = substitutivityRule(
AND, substThms);
147 thm = transitivityRule(thm, rewriteBoolean(thm.
getRHS()));
149 result = d_rules->bitBlastEqnRule(e, thm.
getLHS());
150 result = transitivityRule(result, thm);
151 TRACE(
"bitvector",
"bitBlastEqn => ", result.toString(),
" }");
166 TRACE(
"bitvector",
"bitBlastDisEqn(", notE,
") {");
167 IF_DEBUG(debugger.counter(
"bit-blasted diseq")++);
172 "TheoryBitvector::bitBlastDisEqn:"
176 const Expr& leftBV = e[0];
177 const Expr& rightBV = e[1];
179 IF_DEBUG(debugger.counter(
"bit-blasted diseq bits")+=
183 BITVECTOR == rightType.getExpr().getOpKind(),
184 "TheoryBitvector::bitBlastDisEqn:"
185 "lhs & rhs must be bitvectors");
187 "TheoryBitvector::bitBlastDisEqn: e = "
191 std::vector<Theorem> substThms;
192 std::vector<Theorem> leftBVrightBVThms;
193 int bvLength = BVSize(leftBV);
195 for(; bitPosition < bvLength; bitPosition = bitPosition+1) {
198 getCommonRules()->iffContrapositive(bitBlastTerm(leftBV, bitPosition));
200 bitBlastRightThm = bitBlastTerm(rightBV, bitPosition);
202 leftBVrightBVThms.push_back(bitBlastLeftThm);
203 leftBVrightBVThms.push_back(bitBlastRightThm);
208 Theorem thm = substitutivityRule(
IFF, leftBVrightBVThms);
209 thm = transitivityRule(thm, rewriteBoolean(thm.
getRHS()));
210 leftBVrightBVThms.clear();
211 substThms.push_back(thm);
216 return d_rules->bitvectorTrueRule(thm);
221 Theorem thm1 = substitutivityRule(
OR, substThms);
223 Theorem result = d_rules->bitBlastDisEqnRule(notE, thm1.
getLHS());
224 Theorem thm2 = transitivityRule(thm1, rewriteBoolean(thm1.
getRHS()));
225 result = iffMP(result, thm2);
226 TRACE(
"bitvector",
"bitBlastDisEqn => ", result.
toString(),
" }");
246 "TheoryBitvector::bitBlastIneqn: "
247 "input e must be BVLT/BVLE: e = " + e.
toString());
249 "TheoryBitvector::bitBlastIneqn: "
250 "arity of e must be 2: e = " + e.
toString());
253 int e0len = BVSize(lhs);
254 DebugAssert(e0len == BVSize(rhs),
"Expected sizes to match");
259 res = d_rules->lhsEqRhsIneqn(e, kind);
262 res = d_rules->bvConstIneqn(e, kind);
264 Theorem lhs_i = bitBlastTerm(lhs, e0len-1);
265 Theorem rhs_i = bitBlastTerm(rhs, e0len-1);
266 res = d_rules->generalIneqn(e, lhs_i, rhs_i, kind);
271 res = transitivityRule(res, output);
273 else if (e0len > 1) {
280 "Unexpected structure");
282 vector<unsigned> changed;
283 vector<Theorem> thms;
286 Theorem thm = bitBlastIneqn(resRHS[1][1]);
289 changed.push_back(1);
291 thm = substitutivityRule(resRHS[1], changed, thms);
296 thm = substitutivityRule(resRHS, changed, thms);
297 res = transitivityRule(res, thm);
346 TRACE(
"bitvector",
"bitBlastIneqn => ", res.
toString(),
" }");
359 Theorem TheoryBitvector::bitBlastTerm(
const Expr& t,
int bitPosition)
361 TRACE(
"bitvector",
"bitBlastTerm(", t,
", " +
int2string(bitPosition) +
") {");
364 DebugAssert(
BITVECTOR == type.getExpr().getOpKind(),
"TheoryBitvector::bitBlastTerm: The type of input to bitBlastTerm must be BITVECTOR.\n t = " +t.
toString());
365 DebugAssert(bitPosition >= 0,
"TheoryBitvector::bitBlastTerm: illegal bitExtraction attempted.\n bitPosition = " +
int2string(bitPosition));
370 Expr t_i = newBoolExtractExpr(t, bitPosition);
372 if (it != d_bitvecCache.
end()) {
373 result = (*it).second;
374 TRACE(
"bitvector",
"bitBlastTerm[cached] => ", result,
" }");
383 result = d_rules->bitExtractConstant(t, bitPosition);
387 Theorem thm = d_rules->bitExtractConcatenation(t, bitPosition);
390 const Expr& term = boolExtractTerm[0];
391 int bitPos = getBoolExtractIndex(boolExtractTerm);
392 TRACE(
"bitvector",
"term for bitblastTerm recursion:(", term.toString(),
")");
393 result = transitivityRule(thm, bitBlastTerm(term, bitPos));
398 Theorem thm = d_rules->bitExtractExtraction(t, bitPosition);
401 const Expr& term = boolExtractTerm[0];
402 int bitPos = getBoolExtractIndex(boolExtractTerm);
403 TRACE(
"bitvector",
"term for bitblastTerm recursion:(", term,
")");
404 result = transitivityRule(thm, bitBlastTerm(term, bitPos));
409 result = d_rules->bitExtractFixedLeftShift(t, bitPosition);
412 result = transitivityRule(result, bitBlastTerm(extractTerm[0], getBoolExtractIndex(extractTerm)));
420 Theorem thm = d_rules->bitExtractBVSHL(t, bitPosition);
422 vector<Theorem> thms, thms0;
423 int bvsize = BVSize(t);
424 for (
int i = 0; i <= bitPosition; ++i) {
425 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
426 thms0.push_back(bitBlastTerm(t[0], bitPosition-i));
427 thms.push_back(substitutivityRule(
AND, thms0));
431 if (thms.size() == 1) {
432 result = transitivityRule(thm, thms[0]);
435 Theorem thm2 = substitutivityRule(
OR, thms);
436 result = transitivityRule(thm, thm2);
445 Theorem thm = d_rules->bitExtractBVLSHR(t, bitPosition);
447 vector<Theorem> thms, thms0;
448 int bvsize = BVSize(t);
449 for (
int i = 0; i <= bvsize-1-bitPosition; ++i) {
450 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
451 thms0.push_back(bitBlastTerm(t[0], bitPosition+i));
452 thms.push_back(substitutivityRule(
AND, thms0));
456 if (thms.size() == 1) {
457 result = transitivityRule(thm, thms[0]);
460 Theorem thm2 = substitutivityRule(
OR, thms);
461 result = transitivityRule(thm, thm2);
470 Theorem thm = d_rules->bitExtractBVASHR(t, bitPosition);
472 vector<Theorem> thms, thms0;
473 int bvsize = BVSize(t);
475 for (; i < bvsize-1-bitPosition; ++i) {
476 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize))));
477 thms0.push_back(bitBlastTerm(t[0], bitPosition+i));
478 thms.push_back(substitutivityRule(
AND, thms0));
481 Expr leExpr = newBVLEExpr(newBVConstExpr(i, bvsize), t[1]);
482 thms0.push_back(bitBlastIneqn(leExpr));
483 thms0.push_back(bitBlastTerm(t[0], bvsize-1));
484 thms.push_back(substitutivityRule(
AND, thms0));
486 if (thms.size() == 1) {
487 result = transitivityRule(thm, thms[0]);
490 Theorem thm2 = substitutivityRule(
OR, thms);
491 result = transitivityRule(thm, thm2);
500 int resKind = (kind ==
BVOR) ?
OR :
502 Theorem thm = d_rules->bitExtractBitwise(t, bitPosition, kind);
505 vector<Theorem> substThms;
508 substThms.push_back(bitBlastTerm((*i)[0], getBoolExtractIndex(*i)));
510 result = transitivityRule(thm, substitutivityRule(resKind, substThms));
515 Theorem thm = d_rules->bitExtractNot(t, bitPosition);
517 DebugAssert(
NOT == extractTerm.
getKind(),
"TheoryBitvector::bitBlastTerm: recursion: term must be NOT");
518 const Expr& term0 = extractTerm[0];
519 DebugAssert(
BOOLEXTRACT == term0.getOpKind(),
"TheoryBitvector::bitBlastTerm: recursion:(terms must be BOOL-EXTRACT");
520 int bitPos0 = getBoolExtractIndex(term0);
521 std::vector<Theorem> res;
522 res.push_back(bitBlastTerm(term0[0], bitPos0));
523 result = transitivityRule(thm, substitutivityRule(
NOT, res));
529 if(t.
arity() > 2) thm_binary = d_rules->bvPlusAssociativityRule(t);
530 else thm_binary = reflexivityRule(t);
535 Expr b = bvPlusTerm[1];
536 vector<Theorem> b_bits(bitPosition + 1);
537 for (
int bit = bitPosition; bit >= 0; -- bit)
538 b_bits[bit] = bitBlastTerm(b, bit);
541 vector<Theorem> output_bits;
544 Expr a = bvPlusTerm[0];
545 vector<Theorem> a_bits(bitPosition + 1);
546 for (
int bit = bitPosition; bit >= 0; -- bit)
547 a_bits[bit] = bitBlastTerm(a, bit);
550 d_rules->bitblastBVPlus(a_bits, b_bits, bvPlusTerm, output_bits);
554 for (
int bit = 0; bit <= bitPosition; bit ++)
556 thm = output_bits[bit];
558 Expr original_boolextract = newBoolExtractExpr(t, bit);
563 if (it != d_bitvecCache.
end())
566 thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.
getRHS()));
567 if (boolextract != original_boolextract)
568 thm = d_bitvecCache[original_boolextract] = transitivityRule(substitutivityRule(original_boolextract, thm_binary), thm);
584 thm = d_rules->bitExtractConstBVMult(t, bitPosition);
586 const Expr& term = boolExtractTerm[0];
587 result = transitivityRule(thm, bitBlastTerm(term, bitPosition));
593 vector<Theorem> b_bits(bitPosition + 1);
594 for (
int bit = bitPosition; bit >= 0; -- bit)
595 b_bits[bit] = bitBlastTerm(b, bit);
598 vector<Theorem> output_bits;
602 vector<Theorem> a_bits(bitPosition + 1);
603 for (
int bit = bitPosition; bit >= 0; -- bit)
604 a_bits[bit] = bitBlastTerm(a, bit);
607 d_rules->bitblastBVMult(a_bits, b_bits, t, output_bits);
610 for (
int bit = 0; bit <= bitPosition; bit ++)
612 thm = output_bits[bit];
618 if (it != d_bitvecCache.
end())
621 thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.
getRHS()));
648 DebugAssert(
BITVECTOR == (type.getExpr()).getOpKind(),
"BitvectorTheoremProducer::bitBlastTerm: the type must be BITVECTOR");
651 DebugAssert(0 <= bitPosition && bitPosition < bvLength,
"BitvectorTheoremProducer::bitBlastTerm: the bitextract position must be legal");
652 TRACE(
"bitvector",
"bitBlastTerm: blasting variables(", t,
")");
653 const Expr bitExtract = newBoolExtractExpr(t, bitPosition);
654 result = reflexivityRule(bitExtract);
655 TRACE(
"bitvector",
"bitBlastTerm: blasting variables(", t,
")");
663 result = transitivityRule(result, simpThm);
664 d_bitvecCache[t_i] = result;
666 "TheoryBitvector::bitBlastTerm: "
667 "created wrong theorem.\n result = "
670 TRACE(
"bitvector",
"bitBlastTerm => ", result,
" }");
681 if(!i->isRational() && i->getKind() !=
BVCONST)
return false;
688 for(
int i=0, iend=e.
arity(); i<iend; ++i)
689 if(e[i].getKind() ==
BVCONST) idxs.push_back(i);
701 TRACE(
"pushNegation",
"pushNegationRec(", e,
") {");
704 if(i != d_pushNegCache.end()) {
705 TRACE(
"TheoryBitvector::pushNegation",
706 "pushNegationRec [cached] => ", (*i).second,
"}");
709 Theorem res(reflexivityRule(e));
711 switch(e[0].getOpKind()) {
713 res = d_rules->negConst(e);
716 res = d_rules->negNeg(e);
721 Theorem thm0 = d_rules->negBVand(e);
723 if (ee.
arity() == 0) res = thm0;
727 vector<Theorem> thms;
729 thms.push_back(pushNegationRec(*i));
730 res = substitutivityRule(op, thms);
731 res = transitivityRule(thm0, res);
737 Theorem thm0 = d_rules->negBVor(e);
739 if (ee.
arity() == 0) res = thm0;
743 vector<Theorem> thms;
745 thms.push_back(pushNegationRec(*i));
746 res = substitutivityRule(op, thms);
747 res = transitivityRule(thm0, res);
752 res = d_rules->negBVxor(e);
756 Theorem thm0 = pushNegationRec(ee[0]);
758 thm0 = substitutivityRule(ee, 0, thm0);
759 res = transitivityRule(res, thm0);
764 res = d_rules->negBVxnor(e);
769 Theorem thm0 = d_rules->negConcat(e);
771 if (ee.
arity() == 0) res = thm0;
775 vector<Theorem> thms;
777 thms.push_back(pushNegationRec(*i));
778 res = substitutivityRule(op, thms);
779 res = transitivityRule(thm0, res);
794 res = reflexivityRule(e);
797 TRACE(
"TheoryBitvector::pushNegation",
"pushNegationRec => ", res,
"}");
798 d_pushNegCache[e] = res;
805 d_pushNegCache.clear();
807 return pushNegationRec(e);
818 thm0 = pushNegation(e);
821 switch(e[0].getOpKind()) {
823 thm0 = d_rules->extractBVPlus(e);
826 thm0 = d_rules->extractBVMult(e);
829 thm0 = reflexivityRule(e);
845 thm0 = d_rules->rightShiftToConcat(e);
848 thm0 = d_rules->leftShiftToConcat(e);
851 thm0 = d_rules->constWidthLeftShiftToConcat(e);
854 thm0 = reflexivityRule(e);
857 vector<Theorem> newChildrenThm;
858 vector<unsigned> changed;
859 if(thm0.
isNull()) thm0 = reflexivityRule(e);
862 for(
int k = 0; k < ar; ++k) {
866 newChildrenThm.push_back(thm);
867 changed.push_back(k);
870 if(changed.size() > 0) {
871 Theorem thm1 = substitutivityRule(ee, changed, newChildrenThm);
872 return transitivityRule(thm0,thm1);
876 return reflexivityRule(e);
889 TRACE(
"bitvector rewrite",
"TheoryBitvector::rewriteBV(", e,
") {");
891 if (n <= 0)
return reflexivityRule(e);
898 vector<Theorem> thms;
899 vector<unsigned> changed;
900 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
901 thm = rewriteBV(e[i], cache, n-1);
904 changed.push_back(i);
907 if(changed.size() > 0) {
908 thm = substitutivityRule(e, changed, thms);
909 return transitivityRule(thm, rewriteBV(thm.
getRHS(), cache));
916 if (it != cache.
end()) {
919 +
"][cached] => ", res.
getExpr(),
" }");
920 IF_DEBUG(debugger.counter(
"bv rewriteBV[n] cache hits")++;)
927 switch (e[0].getKind()) {
930 res = d_rules->notBVLTRule(e);
932 res = transitivityRule(res, simplify(res.
getRHS()));
936 if (BVSize(e[0][0]) == 1) {
937 res = d_rules->notBVEQ1Rule(e);
938 res = transitivityRule(res, simplify(res.
getRHS()));
948 res = d_rules->constEq(e);
951 if (e[0].getKind() ==
BVOR && e[1].getKind() ==
BVCONST && computeBVConst(e[1]) == 0) {
952 res = d_rules->zeroBVOR(e);
953 res = transitivityRule(res, simplify(res.
getRHS()));
956 else if (e[0].getKind() ==
BVAND && e[1].getKind() ==
BVCONST && computeBVConst(e[1]) ==
pow(BVSize(e[1]), (
Unsigned)2) - 1) {
957 res = d_rules->oneBVAND(e);
958 res = transitivityRule(res, simplify(res.
getRHS()));
962 res = d_rules->canonBVEQ(e);
964 res = transitivityRule(res, simplify(res.
getRHS()));
972 res = reflexivityRule(e);
977 res = d_rules->concatFlatten(e);
978 TRACE(
"bitvector rewrite",
"rewriteBV (CONCAT): flattened = ",
985 vector<unsigned> idxs;
987 vector<Theorem> thms;
988 vector<Expr> nestedKids;
991 for(
int i=0, iend=e1.
arity(); i<iend; ++i) {
994 if(e1[i].getKind() ==
BVCONST) {
997 nestedKids.push_back(e1[i]);
998 TRACE(
"bitvector rewrite",
"rewriteBV: queued up BVCONST: ",
1001 if(nestedKids.size() > 0) {
1002 if(nestedKids.size() >= 2) {
1003 Expr cc = newConcatExpr(nestedKids);
1004 idxs.push_back(kids.size());
1006 thms.push_back(d_rules->concatConst(cc));
1007 TRACE(
"bitvector rewrite",
"rewriteBV: wrapping ", cc,
"");
1009 TRACE(
"bitvector rewrite",
"rewriteBV: single const ",
1011 kids.push_back(nestedKids[0]);
1016 kids.push_back(e1[i]);
1020 if(nestedKids.size() > 0) {
1021 if(nestedKids.size() >= 2) {
1022 Expr cc = newConcatExpr(nestedKids);
1023 idxs.push_back(kids.size());
1025 thms.push_back(d_rules->concatConst(cc));
1026 TRACE(
"bitvector rewrite",
"rewriteBV: wrapping ", cc,
"");
1028 kids.push_back(nestedKids[0]);
1029 TRACE(
"bitvector rewrite",
"rewriteBV: single const ",
1035 if(idxs.size() > 0) {
1037 if(kids.size() == 1) {
1038 DebugAssert(thms.size() == 1,
"TheoryBitvector::rewriteBV:\n"
1039 "case CONCAT: all constants. thms.size() == "
1041 res = transitivityRule(res, thms[0]);
1043 Expr ee = newConcatExpr(kids);
1045 Theorem constMerge = substitutivityRule(ee, idxs, thms);
1047 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
1049 res = transitivityRule(res, unFlatten);
1050 res = transitivityRule(res, constMerge);
1060 "rewriteBV() case CONCAT, end of const merge");
1063 int hi(-1), low(-1);
1066 for(
int i=0, iend=e1.
arity(); i<iend; ++i) {
1067 const Expr& ei = e1[i];
1069 if(nestedKids.size() > 0 && ei[0] == prevExpr
1070 && (low-1) == getExtractHi(ei)) {
1072 nestedKids.push_back(ei);
1073 low = getExtractLow(ei);
1076 if(nestedKids.size() >= 2) {
1077 Expr cc = newConcatExpr(nestedKids);
1078 idxs.push_back(kids.size());
1080 thms.push_back(d_rules->concatMergeExtract(cc));
1082 }
else if(nestedKids.size() == 1) {
1084 kids.push_back(nestedKids[0]);
1088 nestedKids.push_back(ei);
1089 hi = getExtractHi(ei);
1090 low = getExtractLow(ei);
1094 if(nestedKids.size() >= 2) {
1095 Expr cc = newConcatExpr(nestedKids);
1096 idxs.push_back(kids.size());
1098 thms.push_back(d_rules->concatMergeExtract(cc));
1099 }
else if(nestedKids.size() == 1) {
1101 kids.push_back(nestedKids[0]);
1109 if(nestedKids.size() >= 2) {
1110 Expr cc = newConcatExpr(nestedKids);
1111 idxs.push_back(kids.size());
1114 thms.push_back(rewriteBV(d_rules->concatMergeExtract(cc), cache, 1));
1115 }
else if(nestedKids.size() == 1) {
1117 kids.push_back(nestedKids[0]);
1120 if(idxs.size() > 0) {
1122 if(kids.size() == 1) {
1123 DebugAssert(thms.size() == 1,
"TheoryBitvector::rewriteBV:\n"
1124 "case CONCAT: all extracts merge. thms.size() == "
1128 Expr ee = newConcatExpr(kids);
1129 Theorem extractMerge = substitutivityRule(ee, idxs, thms);
1131 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
1133 res = transitivityRule(res, unFlatten);
1134 res = transitivityRule(res, extractMerge);
1163 res = transitivityRule(res, simplify(res.
getRHS()));
1170 if(getExtractLow(e) == 0 && getExtractHi(e) == BVSize(e[0])-1)
1171 res = d_rules->extractWhole(e);
1173 switch(e[0].getOpKind()) {
1175 res = d_rules->extractConst(e);
1178 res = d_rules->extractExtract(e);
1182 res = rewriteBV(d_rules->extractConcat(e), cache, 2);
1185 res = rewriteBV(d_rules->extractNeg(e), cache, 2);
1188 res = rewriteBV(d_rules->extractAnd(e), cache, 2);
1191 res = rewriteBV(d_rules->extractOr(e), cache, 2);
1195 rewriteBV(d_rules->extractBitwise(e,
BVXOR,
"extract_bvxor"), cache, 2);
1198 const Expr& bvmult = e[0];
1199 int hiBit = getExtractHi(e);
1200 int bvmultLen = BVSize(bvmult);
1202 if(hiBit+1 < bvmultLen) {
1203 res = d_rules->extractBVMult(e);
1204 res = rewriteBV(res, cache, 3);
1206 res = reflexivityRule(e);
1210 const Expr& bvplus = e[0];
1211 int hiBit = getExtractHi(e);
1212 int bvplusLen = BVSize(bvplus);
1213 if(hiBit+1 < bvplusLen) {
1214 res = d_rules->extractBVPlus(e);
1215 }
else res = reflexivityRule(e);
1219 res = reflexivityRule(e);
1224 res = transitivityRule(res, simplify(res.
getRHS()));
1231 if(BVSize(e[0]) > 1) {
1232 res = rewriteBV(d_rules->bitExtractRewrite(e), cache, 2);
1237 int low = getExtractLow(t[0]);
1238 if(getExtractHi(t[0]) == low) {
1239 Theorem thm(d_rules->bitExtractRewrite
1240 (newBoolExtractExpr(t[0][0], low)));
1241 thm = symmetryRule(thm);
1242 res = (res.
isNull())? thm : transitivityRule(res, thm);
1248 if(t != findThm.
getRHS()) {
1249 vector<Theorem> thms;
1250 thms.push_back(findThm);
1251 thm = substitutivityRule(res.
getRHS().
getOp(), thms);
1252 res = transitivityRule(res, thm);
1260 Theorem thm = d_rules->bitExtractConstant(t[0], getBoolExtractIndex(t));
1261 res = (res.
isNull())? thm : transitivityRule(res, thm);
1266 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1267 res = d_rules->bvShiftZero(e);
1269 res = d_rules->leftShiftToConcat(e);
1271 res = transitivityRule(res, simplify(res.
getRHS()));
1276 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1277 res = d_rules->bvShiftZero(e);
1279 res = d_rules->constWidthLeftShiftToConcat(e);
1281 res = transitivityRule(res, simplify(res.
getRHS()));
1286 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1287 res = d_rules->bvShiftZero(e);
1289 res = d_rules->rightShiftToConcat(e);
1291 res = transitivityRule(res, simplify(res.
getRHS()));
1296 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1297 res = d_rules->bvShiftZero(e);
1299 if (e[1].getKind() ==
BVCONST) {
1300 res = d_rules->bvshlToConcat(e);
1301 res = transitivityRule(res, simplify(res.
getRHS()));
1309 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1310 res = d_rules->bvShiftZero(e);
1312 if (e[1].getKind() ==
BVCONST) {
1313 res = d_rules->bvlshrToConcat(e);
1314 res = transitivityRule(res, simplify(res.
getRHS()));
1318 if (e[0].getKind() ==
BVCONST && computeBVConst(e[0]) == 0) {
1319 res = d_rules->bvShiftZero(e);
1321 if (e[1].getKind() ==
BVCONST) {
1322 res = d_rules->bvashrToConcat(e);
1323 res = transitivityRule(res, simplify(res.
getRHS()));
1327 res = d_rules->signExtendRule(e);
1328 res = transitivityRule(res, simplify(res.
getRHS()));
1333 res = d_rules->zeroExtendRule(e);
1334 res = transitivityRule(res, simplify(res.
getRHS()));
1338 res = d_rules->repeatRule(e);
1339 res = transitivityRule(res, simplify(res.
getRHS()));
1343 res = d_rules->rotlRule(e);
1344 res = transitivityRule(res, simplify(res.
getRHS()));
1348 res = d_rules->rotrRule(e);
1349 res = transitivityRule(res, simplify(res.
getRHS()));
1358 res = d_rules->bitwiseFlatten(e, kind);
1367 if(idxs.size() >= 2) {
1368 res = transitivityRule(res, d_rules->bitwiseConst(ee, idxs, kind));
1370 if (ee.getOpKind() != kind)
break;
1373 else if (idxs.size() == 1) {
1378 res = transitivityRule(res, d_rules->bitwiseConstElim(ee, idx, kind));
1382 res = transitivityRule(res, d_rules->bitwiseConcat(ee, kind));
1385 res = transitivityRule(res, simplify(res.
getRHS()));
1393 res = d_rules->rewriteXNOR(e);
1394 res = transitivityRule(res, simplify(res.
getRHS()));
1398 res = pushNegation(e);
1400 res = transitivityRule(res, simplify(res.
getRHS()));
1405 res = d_rules->rewriteNAND(e);
1406 res = transitivityRule(res, simplify(res.
getRHS()));
1410 res = d_rules->rewriteNOR(e);
1411 res = transitivityRule(res, simplify(res.
getRHS()));
1415 res = d_rules->rewriteBVCOMP(e);
1416 res = transitivityRule(res, simplify(res.
getRHS()));
1421 res = d_rules->canonBVUMinus( e );
1422 res = transitivityRule(res, simplify(res.
getRHS()));
1427 res = d_rules->canonBVPlus(e );
1429 res = transitivityRule(res, simplify(res.
getRHS()));
1435 res = d_rules->rewriteBVSub(e);
1436 res = transitivityRule(res, simplify(res.
getRHS()));
1441 res = d_rules->liftConcatBVMult(e);
1443 res = transitivityRule(res, simplify(res.
getRHS()));
1446 res = d_rules->canonBVMult( e );
1448 res = transitivityRule(res, simplify(res.
getRHS()));
1461 res = d_rules->bvUDivConst(e);
1465 if (theoryCore()->okToEnqueue())
1472 Theorem fullTheorem = d_rules->bvUDivTheorem(e);
1474 Theorem skolem_div = getCommonRules()->skolemize(fullTheorem);
1476 res = getCommonRules()->andElim(skolem_div, 0);
1478 Theorem additionalConstraint = getCommonRules()->andElim(skolem_div, 1);
1480 enqueueFact(additionalConstraint);
1481 res = transitivityRule(res, simplify(res.
getRHS()));
1483 res = reflexivityRule(e);
1488 res = d_rules->bvSDivRewrite(e);
1489 res = transitivityRule(res, simplify(res.
getRHS()));
1498 res = d_rules->bvURemConst(e);
1502 res = d_rules->bvURemRewrite(e);
1503 res = transitivityRule(res, theoryCore()->simplify(res.
getRHS()));
1508 res = d_rules->bvSRemRewrite(e);
1509 res = transitivityRule(res, simplify(res.
getRHS()));
1512 res = d_rules->bvSModRewrite(e);
1513 res = transitivityRule(res, simplify(res.
getRHS()));
1519 if (BVSize(lhs) != BVSize(rhs)) {
1520 res = d_rules->padBVLTRule(e, BVSize(lhs) > BVSize(rhs) ? BVSize(lhs) : BVSize(rhs));
1521 res = transitivityRule(res, simplify(res.
getRHS()));
1525 res = d_rules->lhsEqRhsIneqn(e, e.
getOpKind());
1527 res = d_rules->bvConstIneqn(e, e.
getOpKind());
1529 res = d_rules->zeroLeq(e);
1536 FatalAssert(
false,
"Should be eliminated at parse-time");
1554 int e0len = BVSize(e[0]);
1555 int e1len = BVSize(e[1]);
1556 int bvlength = e0len>=e1len ? e0len : e1len;
1559 std::vector<Theorem> thms;
1560 std::vector<unsigned> changed;
1563 Theorem thm = d_rules->padBVSLTRule(e, bvlength);
1567 Theorem thm0 = d_rules->signExtendRule(paddedE[0]);
1569 thm0 = transitivityRule(thm0, rewriteBV(rhs0, cache));
1571 thms.push_back(thm0);
1572 changed.push_back(0);
1575 Theorem thm1 = d_rules->signExtendRule(paddedE[1]);
1577 thm1 = transitivityRule(thm1, rewriteBV(rhs1, cache));
1579 thms.push_back(thm1);
1580 changed.push_back(1);
1583 if(changed.size() > 0) {
1584 thm0 = substitutivityRule(paddedE,changed,thms);
1585 thm0 = transitivityRule(thm, thm0);
1588 thm0 = reflexivityRule(e);
1594 "TheoryBitvector::RewriteBV");
1596 const Expr MSB0 = newBVExtractExpr(thm0RHS[0],bvlength-1,bvlength-1);
1598 const Expr MSB1 = newBVExtractExpr(thm0RHS[1],bvlength-1,bvlength-1);
1600 const Theorem topBit0 = rewriteBV(MSB0, cache, 2);
1602 const Theorem topBit1 = rewriteBV(MSB1, cache, 2);
1605 thm1 = d_rules->signBVLTRule(thm0RHS, topBit0, topBit1);
1606 thm1 = transitivityRule(thm1,simplify(thm1.
getRHS()));
1607 res = transitivityRule(thm0,thm1);
1612 FatalAssert(
false,
"Should be eliminated at parse-time");
1615 res = reflexivityRule(e);
1619 if (res.
isNull()) res = reflexivityRule(e);
1624 TRACE(
"bitvector rewrite",
"TheoryBitvector::rewriteBV => ",
1634 return rewriteBV(e, cache, n);
1644 thm = getCommonRules()->rewriteNotTrue(e);
1645 else if (e[0].isFalse())
1646 thm = getCommonRules()->rewriteNotFalse(e);
1647 else if (e[0].isNot())
1648 thm = getCommonRules()->rewriteNotNot(e);
1651 thm = getCommonRules()->rewriteIff(e);
1655 if (e != rhs && rhs.
isNot())
1656 thm = transitivityRule(thm, rewriteBoolean(rhs));
1660 std::vector<Theorem> newK;
1661 std::vector<unsigned> changed;
1664 Theorem temp = rewriteBoolean(*ii);
1666 newK.push_back(temp);
1667 changed.push_back(count);
1670 if(changed.size() > 0) {
1671 Theorem res = substitutivityRule(e,changed,newK);
1672 thm = transitivityRule(res, rewriteAnd(res.
getRHS()));
1674 thm = rewriteAnd(e);
1678 std::vector<Theorem> newK;
1679 std::vector<unsigned> changed;
1682 Theorem temp = rewriteBoolean(*ii);
1684 newK.push_back(temp);
1685 changed.push_back(count);
1688 if(changed.size() > 0) {
1689 Theorem res = substitutivityRule(e,changed,newK);
1690 thm = transitivityRule(res, rewriteOr(res.
getRHS()));
1699 if(thm.
isNull()) thm = reflexivityRule(e);
1709 :
Theory(core,
"Bitvector"),
1710 d_bvDelayEq(core->getStatistics().counter(
"bv delayed assert eqs")),
1711 d_bvAssertEq(core->getStatistics().counter(
"bv eager assert eqs")),
1712 d_bvDelayDiseq(core->getStatistics().counter(
"bv delayed assert diseqs")),
1713 d_bvAssertDiseq(core->getStatistics().counter(
"bv eager assert diseqs")),
1714 d_bvTypePreds(core->getStatistics().counter(
"bv type preds enqueued")),
1715 d_bvDelayTypePreds(core->getStatistics().counter(
"bv type preds delayed")),
1716 d_bvBitBlastEq(core->getStatistics().counter(
"bv bitblast eqs")),
1717 d_bvBitBlastDiseq(core->getStatistics().counter(
"bv bitblast diseqs")),
1718 d_bv32Flag(&(core->getFlags()[
"bv32-flag"].getBool())),
1719 d_bitvecCache(core->getCM()->getCurrentContext()),
1720 d_eq(core->getCM()->getCurrentContext()),
1721 d_eqPending(core->getCM()->getCurrentContext()),
1722 d_eq_index(core->getCM()->getCurrentContext(), 0, 0),
1723 d_bitblast(core->getCM()->getCurrentContext()),
1724 d_bb_index(core->getCM()->getCurrentContext(), 0, 0),
1725 d_sharedSubterms(core->getCM()->getCurrentContext()),
1726 d_sharedSubtermsList(core->getCM()->getCurrentContext()),
1728 d_index1(core->getCM()->getCurrentContext(), 0, 0),
1729 d_index2(core->getCM()->getCurrentContext(), 0, 0)
1777 std::vector<int> kinds;
1786 kinds.push_back(
BVSHL);
1789 kinds.push_back(
SX);
1794 kinds.push_back(
BVAND);
1795 kinds.push_back(
BVOR);
1796 kinds.push_back(
BVXOR);
1798 kinds.push_back(
BVNEG);
1800 kinds.push_back(
BVNOR);
1804 kinds.push_back(
BVSUB);
1811 kinds.push_back(
BVLT);
1812 kinds.push_back(
BVLE);
1813 kinds.push_back(
BVGT);
1814 kinds.push_back(
BVGE);
1815 kinds.push_back(
BVSLT);
1816 kinds.push_back(
BVSLE);
1817 kinds.push_back(
BVSGT);
1818 kinds.push_back(
BVSGE);
1828 vector<bool> bits(1);
1891 DebugAssert(expr[0].isEq(),
"Unexpected negation");
1960 result.push_back(e);
1977 Expr res(
EQ, new_lhs, new_rhs);
1991 if( new_expr_coeff == BV_one )
2004 int expr_arity= e.
arity();
2005 std::vector<Expr> tmp_list;
2006 for(
int i = 0; i < expr_arity; ++i)
2060 r = ( r*r ) % max_val;
2061 i = ( i*r ) % max_val;
2180 int bv_size =
BVSize(e[0]);
2184 "TheoryBitvector::Odd_coeff: the input expression has a non valid form ");
2187 if( lhs.getOpKind() ==
BVMULT )
2196 if( lhs.getOpKind() ==
BVPLUS )
2198 int lhs_arity = lhs.arity();
2200 for(
int i = 0; i < lhs_arity; ++i)
2207 for(
int j = 0; j < lhs_arity; ++j)
2208 if( j != i && !
isLeafIn( lhs[i], lhs[j] ))
2212 if( lhs[i].getOpKind() ==
BVMULT)
2220 for(
int j = 0; j < lhs_arity; ++j)
2224 if( j != i &&
isTermIn( lhs[i][1], lhs[j] ))
2235 if ( lhs[i].getOpKind() !=
BVCONST )
2239 for(
int j = 0; j < lhs_arity; ++j)
2240 if( j != i && !
isLeafIn( lhs[i][1], lhs[j] ))
2260 int e_arity= e.
arity();
2262 for(
int i=0; i < e_arity && flag == 1; ++i)
2293 if (e1 == e2)
return true;
2294 if (
theoryOf(e2) !=
this)
return false;
2322 DebugAssert(
false,
"TheoryBitvector::canSolveFor, input 'term' of not treated kind");
2330 int e_arity = e.
arity();
2338 for(
int i = 0; i < e_arity; ++i)
2378 int ar = lhs.arity();
2379 vector<Theorem> newChildrenThm;
2380 vector<unsigned> changed;
2382 for (
int k = 0; k < ar; ++k) {
2383 thm0 =
find(lhs[k]);
2385 newChildrenThm.push_back(thm0);
2386 changed.push_back(k);
2389 if(changed.size() > 0) {
2425 "Expected two equations");
2429 return iffMP(thm2, thm3);
2442 vector<Theorem> newChildrenThm;
2443 vector<unsigned> changed;
2445 for (
int k = 0; k < ar; ++k) {
2448 newChildrenThm.push_back(thm0);
2449 changed.push_back(k);
2452 if(changed.size() > 0) {
2468 DebugAssert(e[0].arity() == 2,
"Expected arity 2");
2469 vector<Theorem> newChildrenThm;
2470 vector<unsigned> changed;
2472 for (
int k = 0; k < 2; ++k) {
2473 thm0 =
find(e[0][k]);
2475 newChildrenThm.push_back(thm0);
2476 changed.push_back(k);
2479 if(changed.size() > 0) {
2494 FatalAssert(
false,
"TheoryBitvector::generalBitBlast: unknown expression kind");
2504 for (
int i = 0; i < e.
arity(); ++i) {
2506 if (!e_i.
isNull())
return e_i;
2518 vector<Theorem> thms1;
2532 for (
int i = 0; i < size; ++i) {
2537 thms1.push_back(c1);
2539 if (idx1 == -1) idx1 = i;
2558 if (!thm.getExpr().isTrue()) {
2587 cout<<
"d_eq [" << i <<
"]= "<< it_list[i].getExpr().toString() <<
endl;
2594 cout<<
"d_eqPending [" << i <<
"]= "<< it_list[i].getExpr().toString() <<
endl;
2601 cout<<
"d_bitblast [" << i <<
"]= "<< it_list[i].getExpr().toString() <<
endl;
2612 for(; eqIdx < eq_list_size; ++eqIdx) {
2648 bool bbflag =
d_bb_index < bb_list_size || bitBlastEq;
2685 int k(0), ar(e.
arity());
2687 for ( ; k < ar; ++k) {
2711 "Expected lhs to be shared");
2797 vector<Theorem> newChildrenThm;
2798 vector<unsigned> changed;
2800 for (
int k = 0; k < ar; ++k) {
2803 newChildrenThm.push_back(thm);
2804 changed.push_back(k);
2807 if(changed.size() > 0) {
2812 else return find(e);
2843 if (solvedForm)
return thm;
2852 if (solvedForm)
return thm;
2863 "Should be only case when lhs < rhs");
2866 DebugAssert(t2.getExpr() == e,
"Expected no change");
2869 if (e[0].getOpKind() ==
BVCONST) {
2939 FatalAssert(
false,
"Unexpected kind in TheoryBitvector::checkType"
2946 bool enumerate,
bool computeSize)
2949 "Unexpected kind in TheoryBitvector::finiteTypeInfo");
2950 if (enumerate || computeSize) {
2974 if(!(1 == e.
arity() &&
2977 "attempted extraction from non-bitvector \n"+
2980 if(!(0 <= extractLength))
2982 "attempted out of range extraction \n"+
2988 if(!(2 == e.
arity() &&
2992 (
"Not a bit-vector expression in BVMULT:\n\n "
3000 if(!(1 == e.
arity() &&
3003 (
"Not a bit-vector expression in bit-vector extraction:\n\n "
3005 int bvLength =
BVSize(e[0]);
3008 if(!(0 <= rightExtract &&
3009 rightExtract <= leftExtract && leftExtract < bvLength))
3011 (
"Wrong bounds in bit-vector extract:\n\n "+e.
toString());
3012 int extractLength = leftExtract - rightExtract + 1;
3019 if(!(0 <= bvPlusLength))
3021 (
"Bad bit-vector length specified in BVPLUS expression:\n\n "
3026 (
"Not a bit-vector expression in BVPLUS:\n\n "+e.
toString());
3033 if(!(1 == e.
arity() &&
3036 (
"Not a bit-vector expression in bit-vector shift:\n\n "
3038 int bvLength =
BVSize(e[0]);
3040 if(!(shiftLength >= 0))
3043 int newLength = bvLength + shiftLength;
3049 if(!(1 == e.
arity() &&
3052 (
"Not a bit-vector expression in bit-vector shift:\n\n "
3054 int bvLength =
BVSize(e[0]);
3056 if(!(shiftLength >= 0))
3064 if(!(1 == e.
arity() &&
3067 (
"Not a bit-vector expression in bit-vector shift:\n\n "
3069 int bvLength =
BVSize(e[0]);
3071 if(!(shiftLength >= 0))
3083 if(!(1 == e.
arity() &&
3088 if(!(1 <= bvLength))
3096 if(!(1 == e.
arity() &&
3101 if(!(1 <= bvLength))
3109 if(!(1 == e.
arity() &&
3114 if(!(1 <= bvLength))
3123 if(!(1 == e.
arity() &&
3132 "TheoryBitvector::computeType: unexpected kind in application" +
3165 (
"Concatenation must have at least 2 bit-vectors:\n\n "+e.
toString());
3169 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
3172 (
"Not a bit-vector expression (child #"+
int2string(i+1)
3173 +
") in concatenation:\n\n "+e[i].
toString()
3174 +
"\n\nIn the expression:\n\n "+e.
toString());
3175 bvLength +=
BVSize(e[i]);
3192 (
"Bit-wise "+kindStr+
" must have at least 2 bit-vectors:\n\n "
3197 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
3200 (
"Not a bit-vector expression (child #"+
int2string(i+1)
3201 +
") in bit-wise "+kindStr+
":\n\n "+e[i].
toString()
3202 +
"\n\nIn the expression:\n\n "+e.
toString());
3207 if(
BVSize(e[i]) != bvLength)
3209 (
"Mismatched bit-vector size in bit-wise "+kindStr+
" (child #"
3212 +
"\nFound: "+e[i].getType().toString()
3213 +
"\nIn the following expression:\n\n "+e.
toString());
3220 if(!(1 == e.
arity() &&
3223 (
"Not a bit-vector expression in bit-wise negation:\n\n "
3240 if(!(2 == e.
arity() &&
3244 (
"Expressions must have arity=2, and"
3245 "each subterm must be a bitvector term:\n"
3249 (
"Expected args of same size:\n"
3260 if(!(1 == e.
arity() &&
3263 (
"Not a bit-vector expression in BVUMINUS:\n\n "
3276 if(!(2 == e.
arity() &&
3280 (
"BVLT/BVLE expressions must have arity=2, and"
3281 "each subterm must be a bitvector term:\n"
3287 "TheoryBitvector::computeType: wrong input" +
3292 TRACE(
"bitvector",
"TheoryBitvector::computeType => ", e.
getType(),
" }");
3332 switch(tp.getExpr().getOpKind()) {
3335 for(
int i=0; i<n; i = i+1)
3384 switch(tp.getExpr().getOpKind()) {
3390 for(
int i=0; i<n; i++) {
3393 "TheoryBitvector::computeModel: unassigned bit: "
3403 FatalAssert(
false,
"TheoryBitvector::computeModel[not BITVECTOR type]("
3413 "TheoryBitvector::computeTypePred: t = "+t.
toString());
3435 if( e.
arity() == 0 )
3437 else if( e.
arity() == 1 )
3441 for( i = 0; i < e.
arity(); ++i ) {
3442 if( (i + 1) == e.
arity() ) {
3448 for( --i; i != 0; --i )
3457 os <<
"(bvlshr" <<
space << push << e[0] <<
space << push << e[1] << push
3461 os <<
"(bvashr" <<
space << push << e[0] <<
space << push << e[1] << push
3465 if( e.
arity() == 0 )
3467 else if( e.
arity() == 1 )
3471 for( i = 0; i < e.
arity(); ++i ) {
3472 if( (i + 1) == e.
arity() ) {
3478 for( --i; i != 0; --i )
3483 if( e.
arity() == 0 )
3485 else if( e.
arity() == 1 )
3489 for( i = 0; i < e.
arity(); ++i ) {
3490 if( (i + 1) == e.
arity() ) {
3496 for( --i; i != 0; --i )
3501 if( e.
arity() == 0 )
3503 else if( e.
arity() == 1 )
3507 for( i = 0; i < e.
arity(); ++i ) {
3508 if( (i + 1) == e.
arity() ) {
3514 for( --i; i != 0; --i )
3519 if( e.
arity() == 0 )
3521 else if( e.
arity() == 1 )
3525 for( i = 0; i < e.
arity(); ++i ) {
3526 if( (i + 1) == e.
arity() ) {
3532 for( --i; i != 0; --i )
3537 os <<
"(bvnot" <<
space << push << e[0] << push <<
")";
3540 os <<
"(bvnand" <<
space << push << e[0] <<
space << push << e[1] << push
3544 os <<
"(bvnor" <<
space << push << e[0] <<
space << push << e[1] << push
3548 os <<
"(bvcomp" <<
space << push << e[0] <<
space << push << e[1] << push
3553 os <<
"(bvneg" <<
space << push << e[0] << push <<
")";
3559 for( i = 0; i < e.
arity(); ++i ) {
3560 if( (i + 1) == e.
arity() ) {
3561 os <<
pad(length, e[i]);
3566 for( --i; i != 0; --i )
3571 os <<
"(bvsub" <<
space << push << e[0] <<
space << push << e[1] << push
3576 os <<
"(bvmul" <<
space << push <<
pad(length, e[0]) <<
space << push
3577 <<
pad(length, e[1]) << push <<
")";
3581 os <<
"(bvudiv" <<
space << push << e[0] <<
space << push << e[1] << push
3585 os <<
"(bvsdiv" <<
space << push << e[0] <<
space << push << e[1] << push
3589 os <<
"(bvurem" <<
space << push << e[0] <<
space << push << e[1] << push
3593 os <<
"(bvsrem" <<
space << push << e[0] <<
space << push << e[1] << push
3597 os <<
"(bvsmod" <<
space << push << e[0] <<
space << push << e[1] << push
3602 os <<
"(bvult" <<
space << push << e[0] <<
space << push << e[1] << push
3606 os <<
"(bvule" <<
space << push << e[0] <<
space << push << e[1] << push
3610 os <<
"(bvugt" <<
space << push << e[0] <<
space << push << e[1] << push
3614 os <<
"(bvuge" <<
space << push << e[0] <<
space << push << e[1] << push
3618 os <<
"(bvslt" <<
space << push << e[0] <<
space << push << e[1] << push
3622 os <<
"(bvsle" <<
space << push << e[0] <<
space << push << e[1] << push
3626 os <<
"(bvsgt" <<
space << push << e[0] <<
space << push << e[1] << push
3630 os <<
"(bvsge" <<
space << push << e[0] <<
space << push << e[1] << push
3636 "TheoryBitvector::print: INTTOBV, SMTLIB not supported");
3640 "TheoryBitvector::print: BVTOINT, SMTLIB not supported");
3645 "TheoryBitvector::print: BVTYPEPRED, SMTLIB not supported");
3647 os <<
"BVTYPEPRED[" << push << e.
getOp().
getExpr() << push <<
"," <<
pop
3648 <<
space << e[0] << push <<
"]";
3668 os <<
"BITVECTOR(" <<
push
3673 std::ostringstream ss;
3687 if(first) first=
false;
3695 os <<
"(" << push << e[0] << push <<
")" <<
pop <<
pop
3700 os <<
"BOOLEXTRACT(" << push << e[0] <<
","
3705 os <<
"(" << push << e[0] <<
space <<
"<<" <<
space
3709 os <<
"(" << push << e[0] <<
space <<
"<<" <<
space
3711 os <<
"[" << push <<
BVSize(e)-1 <<
":0]";
3714 os <<
"(" << push << e[0] <<
space <<
">>" <<
space
3718 os <<
"BVSHL(" << push << e[0] <<
"," << e[1] << push <<
")";
3721 os <<
"BVLSHR(" << push << e[0] <<
"," << e[1] << push <<
")";
3724 os <<
"BVASHR(" << push << e[0] <<
"," << e[1] << push <<
")";
3727 os <<
"BVZEROEXTEND(" << push << e[0] <<
"," <<
getBVIndex(e) << push <<
")";
3730 os <<
"BVREPEAT(" << push << e[0] <<
"," <<
getBVIndex(e) << push <<
")";
3733 os <<
"BVROTL(" << push << e[0] <<
"," <<
getBVIndex(e) << push <<
")";
3736 os <<
"BVROTR(" << push << e[0] <<
"," <<
getBVIndex(e) << push <<
")";
3739 os <<
"SX(" << push << e[0] <<
","
3749 if(first) first=
false;
3762 if(first) first=
false;
3771 if (e.
arity() == 1) os << e[0];
3774 for(i = 0; i < e.
arity(); ++i) {
3775 if ((i+1) == e.
arity()) {
3779 os <<
"BVXOR(" << push << e[i] <<
"," <<
push;
3782 for (--i; i != 0; --i) os << push <<
")";
3787 if (e.
arity() == 1) os << e[0];
3790 for(i = 0; i < e.
arity(); ++i) {
3791 if ((i+1) == e.
arity()) {
3795 os <<
"BVXNOR(" << push << e[i] <<
"," <<
push;
3798 for (--i; i != 0; --i) os << push <<
")";
3802 os <<
"(~(" << push << e[0] << push <<
"))";
3805 os <<
"BVNAND(" << push << e[0] <<
"," << e[1] << push <<
")";
3808 os <<
"BVNAND(" << push << e[0] <<
"," << e[1] << push <<
")";
3811 os <<
"BVCOMP(" << push << e[0] <<
"," << e[1] << push <<
")";
3815 os <<
"BVUMINUS(" << push << e[0] << push <<
")";
3820 os << push <<
"," <<
pop <<
space << (*i);
3825 os <<
"BVSUB(" << push <<
BVSize(e) <<
"," << e[0] <<
"," << e[1] << push <<
")";
3828 os <<
"BVMULT(" << push <<
getBVMultParam(e) <<
"," << e[0] <<
"," << e[1]<<push<<
")";
3831 os <<
"BVUDIV(" << push << e[0] <<
"," << e[1]<<push<<
")";
3834 os <<
"BVSDIV(" << push << e[0] <<
"," << e[1]<<push<<
")";
3837 os <<
"BVUREM(" << push << e[0] <<
"," << e[1]<<push<<
")";
3840 os <<
"BVSREM(" << push << e[0] <<
"," << e[1]<<push<<
")";
3843 os <<
"BVSMOD(" << push << e[0] <<
"," << e[1]<<push<<
")";
3846 os <<
"BVLT(" << push << e[0] <<
"," << e[1] << push <<
")";
3849 os <<
"BVLE(" << push << e[0] <<
"," << e[1] << push <<
")";
3852 os <<
"BVGT(" << push << e[0] <<
"," << e[1] << push <<
")";
3855 os <<
"BVGE(" << push << e[0] <<
"," << e[1] << push <<
")";
3858 os <<
"BVSLT(" << push << e[0] <<
"," << e[1] << push <<
")";
3861 os <<
"BVSLE(" << push << e[0] <<
"," << e[1] << push <<
")";
3864 os <<
"BVSGT(" << push << e[0] <<
"," << e[1] << push <<
")";
3867 os <<
"BVSGE(" << push << e[0] <<
"," << e[1] << push <<
")";
3871 FatalAssert(
false,
"INTTOBV not implemented yet");
3874 FatalAssert(
false,
"BVTOINT not implemented yet");
3880 << push <<
"," <<
pop <<
space << e[0]
3902 os <<
push <<
"bv" << r <<
"[" <<
BVSize(e) <<
"]";
3914 os <<
space << push << e[0] << push <<
")" <<
space <<
"bit1" << push
3920 if( bvLength != 0 ) {
3921 os <<
"(concat" <<
space << push << e[0] <<
space;
3922 os << push <<
"bv0[" << bvLength <<
"]" << push <<
")";
3928 os <<
"(bvshl" <<
space << push << e[0] <<
space << push <<
"bv"
3933 os <<
"(bvlshr" <<
space << push << e[0] <<
space << push <<
"bv"
3941 else if( extend < 0 )
3943 "TheoryBitvector::print: SX: extension is shorter than argument");
3945 os <<
"(sign_extend[" << extend <<
"]" <<
space << push << e[0] << push
3950 os <<
"(repeat[" <<
getBVIndex(e) <<
"]" <<
space << push << e[0] << push
3957 else if( extend < 0 )
3959 "TheoryBitvector::print: ZEROEXTEND: extension is less than zero");
3961 os <<
"(zero_extend[" << extend <<
"]" <<
space << push << e[0] << push
3966 os <<
"(rotate_left[" <<
getBVIndex(e) <<
"]" <<
space << push << e[0]
3970 os <<
"(rotate_right[" <<
getBVIndex(e) <<
"]" <<
space << push << e[0]
4001 os <<
space << push << e[0] << push <<
")" <<
space <<
"#b1" << push
4007 if( bvLength != 0 ) {
4008 os <<
"(concat" <<
space << push << e[0] <<
space;
4010 for (
int i = 0; i < bvLength; ++i) os <<
"0";
4028 else if( extend < 0 )
4030 "TheoryBitvector::print: SX: extension is shorter than argument");
4032 os <<
"((_ sign_extend" <<
space << extend <<
")" <<
space << push << e[0] << push
4044 else if( extend < 0 )
4046 "TheoryBitvector::print: ZEROEXTEND: extension is less than zero");
4048 os <<
"((_ zero_extend" <<
space << extend <<
")" <<
space << push << e[0] << push
4090 TRACE(
"parser",
"TheoryBitvector::parseExprOp(", e,
")");
4096 if(!(e.
arity() > 0))
4097 throw ParserException(
"TheoryBitvector::parseExprOp: wrong input:\n\n"
4100 const Expr& c1 = e[0][0];
4105 if(!(e.
arity() == 2))
4107 "kind should have exactly 1 arg:\n\n"
4109 if(!(e[1].
isRational() && e[1].getRational().isInteger()))
4111 "as its first argument:\n\n"
4113 if(!(e[1].getRational().getInt() >=0 ))
4122 "kind should have 1 or 2 args:\n\n"
4126 "kind should have arg of type Rational "
4132 "2nd argument must be an integer:\n\n"
4134 return newBVConstExpr(e[1].getRational(), e[2].getRational().getInt());
4137 }
else if(e[1].isString()) {
4138 if(e.
arity() == 3) {
4141 "2nd argument must be an integer:\n\n"
4143 return newBVConstExpr(e[1].getString(), e[2].getRational().getInt());
4150 if(!(e.
arity() >= 3))
4152 "kind should have at least 2 args:\n\n"
4164 if(!(e.
arity() == 4))
4166 "kind should have exactly 3 arg:\n\n"
4178 if(!(hi >= lo && lo >=0))
4184 if (lo == 0 && arg.getKind() ==
RAW_LIST && arg[0].getKind() ==
ID &&
4186 if(!(arg.arity() == 3))
4188 "kind should have exactly 2 arg:\n\n"
4190 if(!arg[2].
isRational() || !arg[2].getRational().isInteger())
4191 throw ParserException(
"LEFTSHIFT must have an integer constant as its "
4194 if(!(arg[2].getRational().getInt() >=0 ))
4198 if (
BVSize(ls_arg) == hi + 1) {
4206 if(!(e.
arity() == 3))
4208 "kind should have exactly 2 arg:\n\n"
4211 throw ParserException(
"BOOLEXTRACT must have an integer constant as its"
4212 " 2nd argument:\n\n"
4214 if(!(e[2].getRational().getInt() >=0 ))
4221 if(!(e.
arity() == 3))
4223 "kind should have exactly 2 arg:\n\n"
4226 throw ParserException(
"LEFTSHIFT must have an integer constant as its "
4229 if(!(e[2].getRational().getInt() >=0 ))
4235 if(!(e.
arity() == 3))
4236 throw ParserException(
"TheoryBitvector::parseExprOp: CONST_WIDTH_LEFTSHIFT"
4237 "kind should have exactly 2 arg:\n\n"
4240 throw ParserException(
"CONST_WIDTH_LEFTSHIFT must have an integer constant as its "
4243 if(!(e[2].getRational().getInt() >=0 ))
4249 if(!(e.
arity() == 3))
4251 "kind should have exactly 2 arg:\n\n"
4254 throw ParserException(
"RIGHTSHIFT must have an integer constant as its "
4257 if(!(e[2].getRational().getInt() >=0 ))
4268 if (e.
arity() == 4 &&
4272 throw ParserException(
"sign_extend must have an integer constant as its"
4273 " 1st argument:\n\n"
4275 if(!(e[2].getRational().getInt() >=0 ))
4276 throw ParserException(
"sign_extend must have an integer constant as its"
4277 " 1st argument >= 0:\n\n"
4282 if(!(e.
arity() == 3))
4284 "kind should have exactly 2 arg:\n\n"
4288 " 2nd argument:\n\n"
4290 if(!(e[2].getRational().getInt() >=0 ))
4292 " 2nd argument >= 0:\n\n"
4300 if(!(e.
arity() == 3))
4302 "kind should have exactly 2 arg:\n\n"
4305 throw ParserException(
"BVIndexExpr must have an integer constant as its"
4306 " 1st argument:\n\n"
4308 if (kind ==
BVREPEAT && !(e[1].getRational().getInt() >0 ))
4310 " 1st argument > 0:\n\n"
4312 if(!(e[1].getRational().getInt() >=0 ))
4313 throw ParserException(
"BVIndexExpr must have an integer constant as its"
4314 " 1st argument >= 0:\n\n"
4320 if(!(e.
arity() >= 3))
4322 "kind should have at least 2 arg:\n\n"
4325 for(
int i=1, iend=e.
arity(); i<iend; ++i)
4331 if(!(e.
arity() >= 3))
4333 "kind should have at least 2 arg:\n\n"
4336 for(
int i=1, iend=e.
arity(); i<iend; ++i)
4342 if(!(e.
arity() == 3))
4344 "kind should have exactly 2 arg:\n\n"
4350 if(!(e.
arity() == 3))
4352 "kind should have exactly 2 arg:\n\n"
4358 if(!(e.
arity() == 2))
4360 "kind should have exactly 1 arg:\n\n"
4365 if(!(e.
arity() == 3))
4367 "kind should have exactly 2 arg:\n\n"
4372 if(!(e.
arity() == 3))
4374 "kind should have exactly 2 arg:\n\n"
4379 if(!(e.
arity() == 3))
4381 "kind should have exactly 2 arg:\n\n"
4388 if(!(e.
arity() == 2))
4390 "kind should have exactly 1 arg:\n\n"
4401 for(++i; i!=iend; ++i) {
4409 if (e.
arity() == 1)
return k[0];
4413 if(!(e.
arity() >= 4))
4418 (
"Expected integer constant in BVPLUS:\n\n"
4420 if(!(e[1].getRational().getInt() > 0))
4429 for(; i!=iend; ++i) {
4441 if (e.
arity() == 3) {
4454 else if (e.
arity() != 4)
4459 "first argument:\n\n"
4461 if (!(e[1].getRational().getInt() > 0))
4471 summand1 =
pad(bvsublength, summand1);
4472 summand2 =
pad(bvsublength, summand2);
4480 if (e.
arity() != 3) {
4482 "expected exactly 2 args:\n\n"
4488 for(++i; i!=iend; ++i) {
4496 if (e.
arity() == 1)
return k[0];
4499 if(!(e.
arity() == 4))
4501 "expected exactly 3 args:\n\n"
4505 "as first argument:\n\n"
4507 if(!(e[1].getRational().getInt() > 0))
4527 if(!(e.
arity() == 3))
4529 "kind should have exactly 2 args:\n\n"
4533 if (e1.getType().getExpr().getOpKind() !=
BITVECTOR ||
4536 "Expected bitvector arguments:\n\n"
4540 "Expected bitvectors of same size:\n\n"
4542 if (kind ==
BVSHL) {
4547 else if (kind ==
BVLSHR) {
4551 return Expr(kind, e1, e2);
4556 if(!(e.
arity() == 3))
4558 "kind should have exactly 2 arg:\n\n"
4563 if(!(e.
arity() == 3))
4565 "kind should have exactly 2 arg:\n\n"
4570 if(!(e.
arity() == 3))
4572 "kind should have exactly 2 arg:\n\n"
4577 if(!(e.
arity() == 3))
4579 "kind should have exactly 2 arg:\n\n"
4584 if(!(e.
arity() == 3))
4586 "kind should have exactly 2 arg:\n\n"
4591 if(!(e.
arity() == 3))
4593 "kind should have exactly 2 arg:\n\n"
4598 if(!(e.
arity() == 3))
4600 "kind should have exactly 2 arg:\n\n"
4605 if(!(e.
arity() == 3))
4607 "kind should have exactly 2 arg:\n\n"
4625 "TheoryBitvector::parseExprOp: unrecognized input operator"
4641 "TheoryBitvector::newBitvectorTypeExpr:\n"
4642 "len of a BV must be a positive integer:\n bvlength = "+
4660 "TheoryBitvector::newBVAndExpr:"
4661 "inputs must have type BITVECTOR:\n t1 = " +
4664 "TheoryBitvector::bitwise operator"
4665 "inputs must have same length:\n t1 = " + t1.
toString()
4674 "TheoryBitvector::newBVAndExpr:"
4675 "# of subterms must be at least 2");
4676 for(
unsigned int i=0; i<kids.size(); ++i) {
4678 "TheoryBitvector::newBVAndExpr:"
4679 "inputs must have type BITVECTOR:\n t1 = " +
4680 kids[i].toString());
4681 if(i < kids.size()-1) {
4683 "TheoryBitvector::bitwise operator"
4684 "inputs must have same length:\n t1 = " + kids[i].toString()
4685 +
"\n t2 = " + kids[i+1].toString());
4696 "TheoryBitvector::newBVOrExpr: "
4697 "inputs must have type BITVECTOR:\n t1 = " +
4700 "TheoryBitvector::bitwise OR operator: "
4701 "inputs must have same length:\n t1 = " + t1.
toString()
4710 "TheoryBitvector::newBVOrExpr: "
4711 "# of subterms must be at least 2");
4712 for(
unsigned int i=0; i<kids.size(); ++i) {
4714 "TheoryBitvector::newBVOrExpr: "
4715 "inputs must have type BITVECTOR:\n t1 = " +
4716 kids[i].toString());
4717 if(i < kids.size()-1) {
4719 "TheoryBitvector::bitwise operator"
4720 "inputs must have same length:\n t1 = " + kids[i].toString()
4721 +
"\n t2 = " + kids[i+1].toString());
4732 "TheoryBitvector::newBVNandExpr:"
4733 "inputs must have type BITVECTOR:\n t1 = " +
4736 "TheoryBitvector::bitwise operator"
4737 "inputs must have same length:\n t1 = " + t1.
toString()
4747 "TheoryBitvector::newBVNorExpr:"
4748 "inputs must have type BITVECTOR:\n t1 = " +
4751 "TheoryBitvector::bitwise operator"
4752 "inputs must have same length:\n t1 = " + t1.
toString()
4762 "TheoryBitvector::newBVXorExpr:"
4763 "inputs must have type BITVECTOR:\n t1 = " +
4766 "TheoryBitvector::bitwise operator"
4767 "inputs must have same length:\n t1 = " + t1.
toString()
4776 "TheoryBitvector::newBVXorExpr:"
4777 "# of subterms must be at least 2");
4778 for(
unsigned int i=0; i<kids.size(); ++i) {
4780 "TheoryBitvector::newBVXorExpr:"
4781 "inputs must have type BITVECTOR:\n t1 = " +
4782 kids[i].toString());
4783 if(i < kids.size()-1) {
4785 "TheoryBitvector::bitwise operator"
4786 "inputs must have same length:\n t1 = " + kids[i].toString()
4787 +
"\n t2 = " + kids[i+1].toString());
4798 "TheoryBitvector::newBVXnorExpr:"
4799 "inputs must have type BITVECTOR:\n t1 = " +
4802 "TheoryBitvector::bitwise operator"
4803 "inputs must have same length:\n t1 = " + t1.
toString()
4813 "TheoryBitvector::newBVCompExpr:"
4814 "inputs must have type BITVECTOR:\n t1 = " +
4817 "TheoryBitvector::bitwise operator"
4818 "inputs must have same length:\n t1 = " + t1.
toString()
4827 "TheoryBitvector::newBVXnorExpr:"
4828 "# of subterms must be at least 2");
4829 for(
unsigned int i=0; i<kids.size(); ++i) {
4831 "TheoryBitvector::newBVXnorExpr:"
4832 "inputs must have type BITVECTOR:\n t1 = " +
4833 kids[i].toString());
4834 if(i < kids.size()-1) {
4836 "TheoryBitvector::bitwise operator"
4837 "inputs must have same length:\n t1 = " + kids[i].toString()
4838 +
"\n t2 = " + kids[i+1].toString());
4849 "TheoryBitvector::newBVLTExpr:"
4850 "inputs must have type BITVECTOR:\n t1 = " +
4860 "TheoryBitvector::newBVLEExpr:"
4861 "inputs must have type BITVECTOR:\n t1 = " +
4870 " TheoryBitvector::newSXExpr:"
4871 "SX index must be a non-negative integer"+
4874 "TheoryBitvector::newSXExpr:"
4875 "inputs must have type BITVECTOR:\n t1 = " +
4877 if(len==0)
return t1;
4885 "repeat requires index > 0");
4887 "TheoryBitvector::newBVIndexExpr:"
4888 "index must be a non-negative integer"+
4891 "TheoryBitvector::newBVIndexExpr:"
4892 "inputs must have type BITVECTOR:\n t1 = " +
4894 return Expr(
Expr(kind,
getEM()->newRatExpr(len)).mkOp(), t1);
4902 "TheoryBitvector::newBVSLTExpr:"
4903 "inputs must have type BITVECTOR:\n t1 = " +
4913 "TheoryBitvector::newBVSLEExpr:"
4914 "inputs must have type BITVECTOR:\n t1 = " +
4923 "TheoryBitvector::newBVNegExpr:"
4924 "inputs must have type BITVECTOR:\n t1 = " +
4933 "TheoryBitvector::newBVNegExpr:"
4934 "inputs must have type BITVECTOR:\n t1 = " +
4943 " TheoryBitvector::newBoolExtractExpr:"
4944 "bool_extract index must be a non-negative integer"+
4947 "TheoryBitvector::newBVBoolExtractExpr:"
4948 "inputs must have type BITVECTOR:\n t1 = " +
4957 " TheoryBitvector::newFixedleftshift:"
4958 "fixed_shift index must be a non-negative integer"+
4961 "TheoryBitvector::newBVFixedleftshiftExpr:"
4962 "inputs must have type BITVECTOR:\n t1 = " +
4971 " TheoryBitvector::newFixedConstWidthLeftShift:"
4972 "fixed_shift index must be a non-negative integer"+
4975 "TheoryBitvector::newBVFixedleftshiftExpr:"
4976 "inputs must have type BITVECTOR:\n t1 = " +
4985 " TheoryBitvector::newFixedRightShift:"
4986 "fixed_shift index must be a non-negative integer"+
4989 "TheoryBitvector::newBVFixedRightShiftExpr:"
4990 "inputs must have type BITVECTOR:\n t1 = " +
4992 if(shiftLength==0)
return t1;
5001 "TheoryBitvector::newBVConcatExpr:"
5002 "inputs must have type BITVECTOR:\n t1 = " +
5014 "TheoryBitvector::newBVConcatExpr:"
5015 "inputs must have type BITVECTOR:\n t1 = " +
5026 "TheoryBitvector::newBVConcatExpr:"
5027 "# of subterms must be at least 2");
5028 for(
unsigned int i=0; i<kids.size(); ++i) {
5030 "TheoryBitvector::newBVConcatExpr:"
5031 "inputs must have type BITVECTOR:\n t1 = " +
5032 kids[i].toString());
5042 "TheoryBitvector::newBVmultExpr:"
5043 "bvLength must be an integer > 0: bvLength = " +
5047 "TheoryBitvector::newBVmultExpr:"
5048 "inputs must have type BITVECTOR:\n t1 = " +
5051 bvLength ==
BVSize(t2),
"Expected same length");
5059 "TheoryBitvector::newBVmultExpr:"
5060 "bvLength must be an integer > 0: bvLength = " +
5062 for(
unsigned int i=0; i<kids.size(); ++i) {
5064 "TheoryBitvector::newBVPlusExpr:"
5065 "inputs must have type BITVECTOR:\n t1 = " +
5066 kids[i].toString());
5075 vector<Expr> newKids;
5076 for (
unsigned i = 0; i < kids.size(); ++i) {
5077 newKids.push_back(
pad(bvLength, kids[i]));
5093 "TheoryBitvector::newBVUDivExpr:"
5094 "inputs must have type BITVECTOR:\n t1 = " +
5104 "TheoryBitvector::newBVURemExpr:"
5105 "inputs must have type BITVECTOR:\n t1 = " +
5115 "TheoryBitvector::newBVSDivExpr:"
5116 "inputs must have type BITVECTOR:\n t1 = " +
5126 "TheoryBitvector::newBVSRemExpr:"
5127 "inputs must have type BITVECTOR:\n t1 = " +
5137 "TheoryBitvector::newBVSModExpr:"
5138 "inputs must have type BITVECTOR:\n t1 = " +
5148 "TheoryBitvector::newBVZeroString:must be >= 0: "
5150 std::vector<bool> bits;
5151 for(
int count=0; count < bvLength; count++) {
5152 bits.push_back(
false);
5162 "TheoryBitvector::newBVOneString:must be >= 0: "
5164 std::vector<bool> bits;
5165 for(
int count=0; count < bvLength; count++) {
5166 bits.push_back(
true);
5175 "TheoryBitvector::newBVConstExpr:"
5176 "size of bits should be > 0");
5185 "TheoryBitvector::newBVConstExpr: not an integer: "
5188 "TheoryBitvector::newBVConstExpr: bvLength = "
5191 size_t strsize = s.size();
5192 size_t length = bvLength;
5194 if(length > 0 && length != strsize) {
5196 if(length < strsize) {
5197 s = s.substr((strsize-length), length);
5200 for(
size_t i=0,
pad=length-strsize; i <
pad; ++i)
5217 "TheoryBitvector::newBVConstExpr:"
5218 "# of subterms must be at least 2");
5220 "TheoryBitvector::newBVConstExpr: base = "
5223 std::string str = s;
5240 " TheoryBitvector::newBVExtractExpr: "
5241 "bad bv_extract indices: hi = "
5251 "TheoryBitvector::newBVExtractExpr:"
5252 "inputs must have type BITVECTOR:\n e = " +
5255 getEM()->newRatExpr(hi),
5256 getEM()->newRatExpr(low)).mkOp(), e);
5264 "TheoryBitvector::newBVSubExpr:"
5265 "inputs must have type BITVECTOR:\n t1 = " +
5268 "TheoryBitvector::newBVSubExpr"
5269 "inputs must have same length:\n t1 = " + t1.
toString()
5278 " TheoryBitvector::newBVPlusExpr:"
5279 "bvplus length must be a positive integer: "+
5282 "TheoryBitvector::newBVPlusExpr:"
5283 "inputs must have type BITVECTOR:\n t1 = " +
5287 "TheoryBitvector::newBVPlusExpr:"
5288 "inputs must have type BITVECTOR:\n t1 = " +
5297 const vector<Expr>& k)
5300 " TheoryBitvector::newBVPlusExpr:"
5301 "bvplus length must be a positive integer: "+
5304 " TheoryBitvector::newBVPlusExpr:"
5305 " size of input vector must be greater than 0: ");
5306 for(
unsigned int i=0; i<k.size(); ++i) {
5308 "TheoryBitvector::newBVPlusExpr:"
5309 "inputs must have type BITVECTOR:\n t1 = " +
5318 const vector<Expr>& k)
5320 vector<Expr> newKids;
5321 for (
unsigned i = 0; i < k.size(); ++i) {
5322 newKids.push_back(
pad(bvLength, k[i]));
5334 "TheoryBitvector::getBitvectorTypeParam: wrong kind: " +
5343 "TheoryBitvector::getTypePredType:\n tp = "+tp.
toString());
5351 "TheoryBitvector::getTypePredType:\n tp = "+tp.
toString());
5359 "TheoryBitvector::getBoolExtractIndex: wrong kind" +
5368 "TheoryBitvector::getSXIndex: wrong kind\n"+e.
toString());
5380 "TheoryBitvector::getBVIndex: wrong kind\n"+e.
toString());
5390 "TheoryBitvector::getFixedLeftShiftParam: wrong kind" +
5399 "TheoryBitvector::getFixedRightShiftParam: wrong kind" +
5408 "TheoryBitvector::getExtractLow: wrong kind" +
5417 "TheoryBitvector::getExtractHi: wrong kind" +
5426 "TheoryBitvector::getBVPlusParam: wrong kind" +
5434 "TheoryBitvector::getBVMultParam: wrong kind " +
5453 return bvc->getValue(i);
5477 "TheoryBitvector::computeBVConst:"
5478 "input must be a BITVECTOR CONST: " + e.
toString());
5498 "TheoryBitvector::computeBVConst:"
5499 "input must be a BITVECTOR CONST: " + e.
toString());
5525 std::string::reverse_iterator i = bvconst.rbegin();
5526 std::string::reverse_iterator iend = bvconst.rend();
5528 "TheoryBitvector::newBVConstExpr:"
5529 "# of subterms must be at least 2");
5531 for(;i != iend; ++i) {
5532 TRACE(
"bitvector",
"BVConstExpr: bit ", *i,
"");
5539 DebugAssert(
false,
"BVConstExpr: bad binary bit-vector: "
5551 TRACE(
"bitvector",
"BVConstExpr(vector<bool>): arg. size = ", bvconst.size(),
5558 std::vector<bool>::const_iterator i =
d_bvconst.begin();
5559 std::vector<bool>::const_iterator iend =
d_bvconst.end();
5560 size_t hash_value = 0;
5562 for (;i != iend; i++)
5574 vector<Expr> operatorStack;
5575 vector<Expr> operandStack;
5576 vector<int> childStack;
5579 operatorStack.push_back(e);
5580 childStack.push_back(0);
5582 while (!operatorStack.empty()) {
5583 DebugAssert(operatorStack.size() == childStack.size(),
"Invariant violated");
5585 if (childStack.back() < operatorStack.back().arity()) {
5587 e2 = operatorStack.back()[childStack.back()++];
5590 operandStack.push_back(
trueExpr());
5594 if (itccCache !=
theoryCore()->tccCache().end()) {
5595 operandStack.push_back((*itccCache).second);
5598 if (e2.
arity() == 0) {
5599 operandStack.push_back(
trueExpr());
5602 operatorStack.push_back(e2);
5603 childStack.push_back(0);
5607 operandStack.push_back(
getTCC(e2));
5612 e2 = operatorStack.back();
5613 operatorStack.pop_back();
5614 childStack.pop_back();
5615 vector<Expr> children;
5616 vector<Expr>::iterator childStart = operandStack.end() - (e2.
arity());
5617 children.insert(children.begin(), childStart, operandStack.end());
5618 operandStack.erase(childStart, operandStack.end());
5619 tcc = (children.size() == 0) ?
trueExpr() :
5620 (children.size() == 1) ? children[0] :
5636 operandStack.push_back(tcc);
5640 DebugAssert(childStack.empty(),
"Invariant violated");
5641 DebugAssert(operandStack.size() == 1,
"Expected single operand left");
5642 return operandStack.back();