00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029 #define _CVC3_TRUSTED_
00030
00031 #include "bitvector_theorem_producer.h"
00032 #include "common_proof_rules.h"
00033 #include "theory_core.h"
00034 #include "theory_bitvector.h"
00035
00036 using namespace std;
00037 using namespace CVC3;
00038
00039
00040
00041
00042
00043 BitvectorProofRules*
00044 TheoryBitvector::createProofRules() {
00045 return new BitvectorTheoremProducer(this);
00046 }
00047
00048
00049 BitvectorTheoremProducer::BitvectorTheoremProducer(TheoryBitvector* theoryBV)
00050 : TheoremProducer(theoryBV->theoryCore()->getTM()),
00051 d_theoryBitvector(theoryBV) {
00052
00053 vector<bool> bits(1);
00054 bits[0]=false;
00055 d_bvZero = d_theoryBitvector->newBVConstExpr(bits);
00056 bits[0]=true;
00057 d_bvOne = d_theoryBitvector->newBVConstExpr(bits);
00058 }
00059
00060
00061
00062
00063
00064
00065 Theorem BitvectorTheoremProducer::bitvectorFalseRule(const Theorem& thm) {
00066 if(CHECK_PROOFS) {
00067 const Expr e = thm.getExpr();
00068 CHECK_SOUND(e.isIff() && e[0].isIff(),
00069 "TheoryBitvector::bitvectorFalseRule: "
00070 "premise must be a iff theorem:\n e = "
00071 +e.toString());
00072 CHECK_SOUND(e[1].isFalse(),
00073 "TheoryBitvector::bitvectorFalseRule: "
00074 "premise must be iff Theorem, with False as the RHS:\n e = "
00075 +e.toString());
00076 CHECK_SOUND(e[0][0].getOpKind() == BOOLEXTRACT &&
00077 e[0][1].getOpKind() == BOOLEXTRACT,
00078 "TheoryBitvector::bitvectorFalseRule: "
00079 "premise must be iff Theorem, with False as the RHS:\n e = "
00080 +e.toString());
00081 CHECK_SOUND(d_theoryBitvector->getBoolExtractIndex(e[0][0]) ==
00082 d_theoryBitvector->getBoolExtractIndex(e[0][1]),
00083 "TheoryBitvector::bitvectorFalseRule: "
00084 "premise must be iff Theorem, with False as the RHS:\n e = "
00085 +e.toString());
00086 }
00087 const Expr& e = thm.getExpr();
00088 const Expr& t1 = e[0][0][0];
00089 const Expr& t2 = e[0][1][0];
00090
00091 Proof pf;
00092 if(withProof())
00093 pf = newPf("bitvector_false_rule", e, thm.getProof());
00094 return newRWTheorem(t1.eqExpr(t2), e[1], thm.getAssumptionsRef(), pf);
00095 }
00096
00097
00098
00099
00100
00101
00102
00103 Theorem BitvectorTheoremProducer::bitvectorTrueRule(const Theorem& thm) {
00104 if(CHECK_PROOFS) {
00105 const Expr e = thm.getExpr();
00106 CHECK_SOUND(e.isIff() && e[0].isIff(),
00107 "TheoryBitvector::bitvectorFalseRule: "
00108 "premise must be a iff theorem:\n e = "
00109 +e.toString());
00110 CHECK_SOUND(e[1].isTrue(),
00111 "TheoryBitvector::bitvectorFalseRule: "
00112 "premise must be iff Theorem, with False as the RHS:\n e = "
00113 +e.toString());
00114 CHECK_SOUND(e[0][0].getKind() == NOT &&
00115 e[0][0][0].getOpKind() == BOOLEXTRACT &&
00116 e[0][1].getOpKind() == BOOLEXTRACT,
00117 "TheoryBitvector::bitvectorFalseRule: "
00118 "premise must be iff Theorem, with False as the RHS:\n e = "
00119 +e.toString());
00120 CHECK_SOUND(d_theoryBitvector->getBoolExtractIndex(e[0][0][0]) ==
00121 d_theoryBitvector->getBoolExtractIndex(e[0][1]),
00122 "TheoryBitvector::bitvectorFalseRule: "
00123 "premise must be iff Theorem, with False as the RHS:\n e = "
00124 +e.toString());
00125 }
00126 const Expr& e = thm.getExpr();
00127
00128
00129 const Expr& t1 = e[0][0][0][0];
00130 const Expr& t2 = e[0][1][0];
00131
00132 Proof pf;
00133 if(withProof())
00134 pf = newPf("bitvector_true_rule", e, thm.getProof());
00135 return newRWTheorem(t1.eqExpr(t2).negate(), e[1], thm.getAssumptionsRef(), pf);
00136 }
00137
00138
00139
00140
00141 Theorem BitvectorTheoremProducer::bitBlastEqnRule(const Expr& e, const Expr& f)
00142 {
00143 if(CHECK_PROOFS) {
00144 CHECK_SOUND(e.isEq(),
00145 "TheoryBitvector::bitBlastEqnRule: "
00146 "premise must be a rewrite theorem:\n e = "
00147 +e.toString());
00148 const Expr& lhs = e[0];
00149 const Expr& rhs = e[1];
00150 const Type& leftType = lhs.getType();
00151 const Type& rightType = rhs.getType();
00152 CHECK_SOUND(BITVECTOR == leftType.getExpr().getOpKind() &&
00153 BITVECTOR == rightType.getExpr().getOpKind(),
00154 "TheoryBitvector::bitBlastEqnRule: "
00155 "lhs & rhs must be bitvectors:\n e ="
00156 +e.toString());
00157 int lhsLength = d_theoryBitvector->BVSize(lhs);
00158 int rhsLength = d_theoryBitvector->BVSize(rhs);
00159 CHECK_SOUND(lhsLength == rhsLength,
00160 "TheoryBitvector::bitBlastEqnRule: "
00161 "lhs & rhs must be bitvectors of same bvLength.\n size(lhs) = "
00162 + int2string(lhsLength)
00163 +"\n size(rhs) = "
00164 + int2string(rhsLength)
00165 +"\n e = "+e.toString());
00166 int bvLength = d_theoryBitvector->BVSize(leftType.getExpr());
00167 CHECK_SOUND(f.isAnd(),
00168 "TheoryBitvector::bitBlastEqnRule: "
00169 "consequence of the rule must be an AND.\n f = "
00170 +f.toString());
00171 CHECK_SOUND(bvLength == f.arity(),
00172 "TheoryBitvector::bitBlastEqnRule: "
00173 "the arity of the consequence AND must "
00174 "equal the bvLength of the bitvector:\n f = "
00175 +f.toString()+"\n bvLength = "+ int2string(bvLength));
00176 for (int i=0; i < bvLength; ++i) {
00177 const Expr& conjunct = f[i];
00178 CHECK_SOUND(conjunct.isIff() && 2 == conjunct.arity(),
00179 "TheoryBitvector::bitBlastEqnRule: "
00180 "each conjunct in consequent must be an IFF.\n f = "
00181 +f.toString());
00182 const Expr& leftExtract = conjunct[0];
00183 const Expr& rightExtract = conjunct[1];
00184 CHECK_SOUND(BOOLEXTRACT == leftExtract.getOpKind(),
00185 "TheoryBitvector::bitBlastEqnRule: "
00186 "each conjunct in consequent must be boolextract.\n"
00187 " f["+int2string(i)+"] = "+conjunct.toString());
00188 CHECK_SOUND(BOOLEXTRACT == rightExtract.getOpKind(),
00189 "TheoryBitvector::bitBlastEqnRule: "
00190 "each conjunct in consequent must be boolextract.\n"
00191 " f["+int2string(i)+"] = "+conjunct.toString());
00192 const Expr& leftBV = leftExtract[0];
00193 const Expr& rightBV = rightExtract[0];
00194 CHECK_SOUND(leftBV == lhs && rightBV == rhs,
00195 "TheoryBitvector::bitBlastEqnRule: each boolextract"
00196 " must be applied to the correct bitvector.\n conjunct = "
00197 +conjunct.toString()
00198 +"\n leftBV = "+ leftBV.toString()
00199 +"\n lhs = "+ lhs.toString()
00200 +"\n rightBV = "+rightBV.toString()
00201 +"\n rhs = "+rhs.toString());
00202 int leftBitPosition =
00203 d_theoryBitvector->getBoolExtractIndex(leftExtract);
00204 int rightBitPosition =
00205 d_theoryBitvector->getBoolExtractIndex(rightExtract);
00206 CHECK_SOUND(leftBitPosition == i && rightBitPosition == i,
00207 "TheoryBitvector::bitBlastEqnRule: "
00208 "boolextract positions must match i= "+int2string(i)
00209 +"\n conjunct = "+conjunct.toString());
00210 }
00211 }
00212
00213 Proof pf;
00214 if(withProof())
00215 pf = newPf("bit_blast_equations", e, f);
00216 return newRWTheorem(e, f, Assumptions::emptyAssump(), pf);
00217 }
00218
00219
00220
00221
00222
00223
00224 Theorem BitvectorTheoremProducer::bitBlastDisEqnRule(const Theorem& notE,
00225 const Expr& f){
00226
00227 TRACE("bitvector", "input to bitBlastDisEqnRule(", notE.toString(), ")");
00228 DebugAssert(notE.getExpr().isNot() && (notE.getExpr())[0].isEq(),
00229 "TheoryBitvector::bitBlastDisEqnRule:"
00230 "expecting an equation" + notE.getExpr().toString());
00231
00232 const Expr& e = (notE.getExpr())[0];
00233 if(CHECK_PROOFS) {
00234 CHECK_SOUND(e.isEq(),
00235 "TheoryBitvector::bitBlastDisEqnRule:"
00236 "premise must be a rewrite theorem" + e.toString());
00237 const Expr& lhs = e[0];
00238 const Expr& rhs = e[1];
00239 const Type& leftType = lhs.getType();
00240 const Type& rightType = rhs.getType();
00241 CHECK_SOUND(BITVECTOR == leftType.getExpr().getOpKind() &&
00242 BITVECTOR == rightType.getExpr().getOpKind(),
00243 "TheoryBitvector::bitBlastDisEqnRule:"
00244 "lhs & rhs must be bitvectors" + e.toString());
00245 CHECK_SOUND(d_theoryBitvector->BVSize(leftType.getExpr()) ==
00246 d_theoryBitvector->BVSize(rightType.getExpr()),
00247 "TheoryBitvector::bitBlastDisEqnRule:"
00248 "lhs & rhs must be bitvectors of same bvLength");
00249 int bvLength = d_theoryBitvector->BVSize(leftType.getExpr());
00250 CHECK_SOUND(f.isOr(),
00251 "TheoryBitvector::bitBlastDisEqnRule:"
00252 "consequence of the rule must be an OR" + f.toString());
00253 CHECK_SOUND(bvLength == f.arity(),
00254 "TheoryBitvector::bitBlastDisEqnRule:"
00255 "the arity of the consequence OR must be"
00256 "equal to the bvLength of the bitvector" +
00257 f.toString() + int2string(bvLength));
00258 for(int i=0; i <bvLength; i++) {
00259 const Expr& disjunct = f[i];
00260 CHECK_SOUND(disjunct.isIff() &&
00261 2 == disjunct.arity() && disjunct[0].isNot(),
00262 "TheoryBitvector::bitBlastDisEqnRule:"
00263 "each conjunct in consequent must be an Iff"+f.toString());
00264 const Expr& leftExtract = (disjunct[0])[0];
00265 const Expr& rightExtract = disjunct[1];
00266 CHECK_SOUND(BOOLEXTRACT == leftExtract.getOpKind(),
00267 "TheoryBitvector::bitBlastDisEqnRule:"
00268 "each disjunct in consequent must be boolextract" +
00269 disjunct.toString());
00270 CHECK_SOUND(BOOLEXTRACT == rightExtract.getOpKind(),
00271 "TheoryBitvector::bitBlastDisEqnRule:"
00272 "each conjunct in consequent must be boolextract" +
00273 disjunct.toString());
00274 const Expr& leftBV = leftExtract[0];
00275 const Expr& rightBV = rightExtract[0];
00276 CHECK_SOUND(leftBV == lhs && rightBV == rhs,
00277 "TheoryBitvector::bitBlastDisEqnRule:"
00278 "each boolextract must be applied to the correct bitvector"+
00279 disjunct.toString() + leftBV.toString() + lhs.toString() +
00280 rightBV.toString() + rhs.toString());
00281 int leftBitPosition =
00282 d_theoryBitvector->getBoolExtractIndex(leftExtract);
00283 int rightBitPosition =
00284 d_theoryBitvector->getBoolExtractIndex(rightExtract);
00285 CHECK_SOUND(leftBitPosition == i && rightBitPosition == i,
00286 "TheoryBitvector::bitBlastDisEqnRule:"
00287 "boolextract positions must match" + disjunct.toString());
00288 }
00289 }
00290
00291 Proof pf;
00292 if(withProof())
00293 pf = newPf("bit_blast_disequations", notE.getExpr(), f, notE.getProof());
00294 return newTheorem(f, notE.getAssumptionsRef(), pf);
00295 }
00296
00297
00298
00299
00300
00301
00302
00303 Theorem
00304 BitvectorTheoremProducer::padBVLTRule(const Expr& e, int len) {
00305 if(CHECK_PROOFS) {
00306 CHECK_SOUND((BVLT == e.getOpKind() || BVLE == e.getOpKind()) &&
00307 e.arity()==2,
00308 "BitvectorTheoremProducer::padBVLTRule: "
00309 "input must e be a BVLT/BVLE: e = " + e.toString());
00310 CHECK_SOUND(BITVECTOR==e[0].getType().getExpr().getOpKind() &&
00311 BITVECTOR==e[1].getType().getExpr().getOpKind(),
00312 "BitvectorTheoremProducer::padBVLTRule: "
00313 "for BVMULT terms e[0],e[1] must be a BV: " + e.toString());
00314 CHECK_SOUND(0<len,
00315 "BitvectorTheoremProducer::padBVLTRule: "
00316 "input len must be >=0 and an integer: len = " +
00317 int2string(len));
00318 }
00319 Expr e0 = pad(len, e[0]);
00320 Expr e1 = pad(len, e[1]);
00321 int kind = e.getOpKind();
00322
00323 Expr output;
00324 if(kind == BVLT)
00325 output = d_theoryBitvector->newBVLTExpr(e0,e1);
00326 else
00327 output = d_theoryBitvector->newBVLEExpr(e0,e1);
00328
00329 Proof pf;
00330 if(withProof())
00331 pf = newPf("pad_bvlt_rule", e);
00332 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
00333 return result;
00334 }
00335
00336
00337 Theorem
00338 BitvectorTheoremProducer::signExtendRule(const Expr& e) {
00339 if(CHECK_PROOFS) {
00340 CHECK_SOUND(BITVECTOR==e.getType().getExpr().getOpKind(),
00341 "input must be a bitvector. \n e = " + e.toString());
00342 CHECK_SOUND(SX == e.getOpKind(),
00343 "input must be SX(e).\n e = " + e.toString());
00344 CHECK_SOUND(SX != e[0].getOpKind(),
00345 "input cannot have nested SX.\n e = " + e.toString());
00346 }
00347 Expr input0 = e[0];
00348
00349 while(SX == input0.getOpKind())
00350 input0 = input0[0];
00351
00352 int bvLength = d_theoryBitvector->BVSize(e);
00353 int bvLength0 = d_theoryBitvector->BVSize(input0);
00354
00355 Expr output;
00356 if(bvLength0 == bvLength) {
00357 output = input0;
00358 } else if(bvLength0 < bvLength) {
00359 std::vector<Expr> k;
00360 int c = bvLength - bvLength0;
00361 Expr topBit =
00362 d_theoryBitvector->newBVExtractExpr(input0,bvLength0-1,bvLength0-1);
00363 while(c--)
00364 k.push_back(topBit);
00365 k.push_back(input0);
00366 output = d_theoryBitvector->newConcatExpr(k);
00367 } else
00368 output = d_theoryBitvector->newBVExtractExpr(input0, bvLength-1, 0);
00369
00370 Proof pf;
00371 if(withProof())
00372 pf = newPf("sign_extend_rule", e);
00373 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
00374 return result;
00375 }
00376
00377
00378 Theorem
00379 BitvectorTheoremProducer::bitExtractSXRule(const Expr& e, int i) {
00380
00381
00382 Theorem thm = signExtendRule(e);
00383 Expr e_i = d_theoryBitvector->newBoolExtractExpr(e,i);
00384 Expr newE_i = d_theoryBitvector->newBoolExtractExpr(thm.getRHS(),i);
00385
00386 Proof pf;
00387 if(withProof())
00388 pf = newPf("bitExtract_SX_rule",e,rat(i));
00389 Theorem result(newRWTheorem(e_i,newE_i,Assumptions::emptyAssump(),pf));
00390 return result;
00391 }
00392
00393
00394
00395 Theorem
00396 BitvectorTheoremProducer::padBVSLTRule(const Expr& e, int len) {
00397 if(CHECK_PROOFS) {
00398 CHECK_SOUND((BVSLT == e.getOpKind() || BVSLE == e.getOpKind()) &&
00399 e.arity()==2,
00400 "BitvectorTheoremProducer::padBVSLTRule: "
00401 "input must e be a BVSLT/BVSLE: e = " + e.toString());
00402 CHECK_SOUND(BITVECTOR==e[0].getType().getExpr().getOpKind() &&
00403 BITVECTOR==e[1].getType().getExpr().getOpKind(),
00404 "BitvectorTheoremProducer::padBVSLTRule: "
00405 "for BVMULT terms e[0],e[1] must be a BV: " + e.toString());
00406 CHECK_SOUND(0<=len,
00407 "BitvectorTheoremProducer::padBVSLTRule: "
00408 "input len must be >=0 and an integer: len = " +
00409 int2string(len));
00410 }
00411 Expr e0 = d_theoryBitvector->newSXExpr(e[0], len);
00412 Expr e1 = d_theoryBitvector->newSXExpr(e[1], len);
00413 int kind = e.getOpKind();
00414
00415 Expr output;
00416 if(kind == BVSLT)
00417 output = d_theoryBitvector->newBVSLTExpr(e0,e1);
00418 else
00419 output = d_theoryBitvector->newBVSLEExpr(e0,e1);
00420
00421 Proof pf;
00422 if(withProof())
00423 pf = newPf("pad_bvslt_rule", e);
00424 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
00425 return result;
00426 }
00427
00428
00429
00430
00431
00432
00433
00434
00435 Theorem
00436 BitvectorTheoremProducer::signBVLTRule(const Expr& e,
00437 const Theorem& topBit0,
00438 const Theorem& topBit1){
00439 if(CHECK_PROOFS) {
00440 CHECK_SOUND((BVSLT == e.getOpKind() || BVSLE == e.getOpKind()) &&
00441 e.arity()==2,
00442 "BitvectorTheoremProducer::signedBVLTRule: "
00443 "input must e be a BVSLT/BVSLE: e = " + e.toString());
00444 CHECK_SOUND(BITVECTOR==e[0].getType().getExpr().getOpKind() &&
00445 BITVECTOR==e[1].getType().getExpr().getOpKind(),
00446 "BitvectorTheoremProducer::signedBVLTRule: "
00447 "for BVMULT terms e[0],e[1] must be a BV: " + e.toString());
00448 }
00449 const Expr e0 = e[0];
00450 const Expr e1 = e[1];
00451 int e0len = d_theoryBitvector->BVSize(e0);
00452 int e1len = d_theoryBitvector->BVSize(e1);
00453
00454 if(CHECK_PROOFS) {
00455 const Expr e0ext =
00456 d_theoryBitvector->newBVExtractExpr(e0,e0len-1,e0len-1);
00457 const Expr e1ext =
00458 d_theoryBitvector->newBVExtractExpr(e1,e1len-1,e1len-1);
00459 CHECK_SOUND(e0ext == topBit0.getLHS(),
00460 "BitvectorTheoremProducer::signedBVLTRule: "
00461 "topBit0.getLHS() is the un-rewritten form of MSB of e0\n"
00462 "topBit0 is screwed up: topBit0 = " +
00463 topBit0.getExpr().toString());
00464 CHECK_SOUND(e1ext == topBit1.getLHS(),
00465 "BitvectorTheoremProducer::signedBVLTRule: "
00466 "topBit1.getLHS() is the un-rewritten form of MSB of e1\n"
00467 "topBit1 is screwed up: topBit1 = " +
00468 topBit1.getExpr().toString());
00469 CHECK_SOUND(e0len == e1len,
00470 "BitvectorTheoremProducer::signedBVLTRule: "
00471 "both e[0] and e[1] must have the same length\n. e =" +
00472 e.toString());
00473 }
00474 const Expr MSB0 = topBit0.getRHS();
00475 const Expr MSB1 = topBit1.getRHS();
00476
00477 int eKind = e.getOpKind();
00478 Expr output;
00479
00480
00481
00482
00483
00484
00485
00486 Rational b0 = -1;
00487 Rational b1 = -1;
00488 if(MSB0.getKind() == BVCONST) b0 = d_theoryBitvector->computeBVConst(MSB0);
00489 if(MSB1.getKind() == BVCONST) b1 = d_theoryBitvector->computeBVConst(MSB1);
00490
00491
00492 const Expr tExpr = d_theoryBitvector->trueExpr();
00493 const Expr fExpr = d_theoryBitvector->falseExpr();
00494 const Expr MSB0isZero = MSB0.eqExpr(bvZero());
00495 const Expr MSB0isOne = MSB0.eqExpr(bvOne());
00496 const Expr MSB1isZero = MSB1.eqExpr(bvZero());
00497 const Expr MSB1isOne = MSB1.eqExpr(bvOne());
00498
00499
00500
00501
00502 if(e0len == 1) {
00503 if(b0==0 && b1==0)
00504 output = eKind==BVSLT ? fExpr : tExpr;
00505 else if(b0==0 && b1==1)
00506 output = fExpr;
00507 else if(b0==1 && b1==0)
00508 output = tExpr;
00509 else if(b0==1 && b1==1)
00510 output = eKind==BVSLT ? fExpr : tExpr;
00511 else if(b0==0 && b1==-1)
00512 output = eKind==BVSLT ? fExpr : MSB1isZero;
00513 else if(b0==1 && b1==-1)
00514 output = eKind==BVSLT ? MSB1isZero : tExpr;
00515 else if(b0==-1 && b1==0)
00516 output = eKind==BVSLT ? MSB0isOne : tExpr;
00517 else if(b0==-1 && b1==1)
00518 output = eKind==BVSLT ? fExpr : MSB0isOne;
00519 else
00520
00521 output =
00522 eKind==BVSLT ?
00523 MSB0isOne.andExpr(MSB1isZero) :
00524 MSB0isOne.orExpr(MSB1isZero);
00525 } else {
00526
00527 Expr newE0 = d_theoryBitvector->newBVExtractExpr(e0,e0len-2,0);
00528 Expr newE1 = d_theoryBitvector->newBVExtractExpr(e1,e1len-2,0);
00529 Expr newBVLT =
00530 eKind==BVSLT ?
00531 d_theoryBitvector->newBVLTExpr(newE0,newE1):
00532 d_theoryBitvector->newBVLEExpr(newE0,newE1);
00533
00534
00535
00536
00537
00538
00539
00540 if(-1 != b0 && -1 !=b1) {
00541
00542 if(b0 == 1 && b1 == 0)
00543 output = tExpr;
00544
00545 else if(b0 == 0 && b1 == 1)
00546 output = fExpr;
00547
00548 else {
00549 output = newBVLT;
00550 }
00551 }
00552 else if(-1 != b0 && -1 == b1) {
00553
00554
00555
00556
00557
00558
00559
00560 output =
00561 (b0==0) ?
00562
00563 MSB1isZero.andExpr(newBVLT) :
00564
00565 MSB1isZero.orExpr(MSB1isOne.andExpr(newBVLT));
00566 }
00567 else if(-1 == b0 && -1 != b1) {
00568
00569
00570
00571
00572
00573
00574
00575 output =
00576 (b1==0) ?
00577
00578 MSB0isOne.orExpr(MSB0isZero.andExpr(newBVLT)) :
00579
00580 MSB0isOne.andExpr(newBVLT);
00581 } else {
00582
00583
00584
00585 Expr k0 = MSB0isOne.andExpr(MSB1isZero);
00586
00587
00588 Expr k1 = MSB0.eqExpr(MSB1);
00589
00590
00591
00592 output = k0.orExpr(k1.andExpr(newBVLT));
00593 }
00594 }
00595
00596 Proof pf;
00597 if(withProof())
00598 pf = newPf("sign_bvlt_rule", e);
00599 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00600 }
00601
00602
00603
00604
00605 Theorem BitvectorTheoremProducer::notBVEQ1Rule(const Expr& e)
00606 {
00607 if(CHECK_PROOFS) {
00608 CHECK_SOUND(e.getKind() == NOT,
00609 "BitvectorTheoremProducer::notBVEQ1Rule: "
00610 "input kind must be a NOT:\n e = " + e.toString());
00611 CHECK_SOUND(e[0].getOpKind() == EQ,
00612 "BitvectorTheoremProducer::notBVEQ1Rule: "
00613 "e[0] must be EQ: \n e = " + e.toString());
00614 CHECK_SOUND(d_theoryBitvector->BVSize(e[0][0]) == 1,
00615 "BitvectorTheoremProducer::notBVEQ1Rule: "
00616 "BVSize(e[0][0]) must be 1: \n e = " + e.toString());
00617 }
00618 Expr output = e[0][0].eqExpr(d_theoryBitvector->newBVNegExpr(e[0][1]));
00619
00620 Proof pf;
00621 if(withProof())
00622 pf = newPf("not_eq1_rule", e);
00623 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00624 }
00625
00626
00627
00628
00629
00630 Theorem BitvectorTheoremProducer::notBVLTRule(const Expr& e) {
00631 if(CHECK_PROOFS) {
00632 CHECK_SOUND(e.getKind() == NOT,
00633 "BitvectorTheoremProducer::notBVLTRule: "
00634 "input kind must be a NOT:\n e = " + e.toString());
00635 CHECK_SOUND(e[0].getOpKind() == BVLT ||
00636 e[0].getOpKind() == BVLE,
00637 "BitvectorTheoremProducer::notBVLTRule: "
00638 "e[0] must be BVLT or BVLE: \n e = " + e.toString());
00639 }
00640 Expr output;
00641
00642 const Expr& e00 = e[0][0];
00643 const Expr& e01 = e[0][1];
00644 if(BVLT == e[0].getOpKind())
00645 output = d_theoryBitvector->newBVLEExpr(e01,e00);
00646 else
00647 output = d_theoryBitvector->newBVLTExpr(e01,e00);
00648
00649 Proof pf;
00650 if(withProof())
00651 pf = newPf("not_bvlt_rule", e);
00652 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00653 }
00654
00655
00656
00657 Theorem BitvectorTheoremProducer::lhsEqRhsIneqn(const Expr& e, int kind) {
00658 if(CHECK_PROOFS) {
00659 CHECK_SOUND(BVLT == e.getOpKind() || BVLE == e.getOpKind(),
00660 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
00661 "input kind must be BVLT or BVLE: e = " + e.toString());
00662 CHECK_SOUND(kind == e.getOpKind(),
00663 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
00664 "input kind must match e.getOpKind(): "
00665 "\n e = " + e.toString());
00666 CHECK_SOUND((e.arity()==2) && (e[0]==e[1]),
00667 "BitvectorTheoremProducer::lhsEqRhsIneqn: "
00668 "input arity must be 2, and e[0] must be equal to e[1]: "
00669 "\ne = " + e.toString());
00670 }
00671 Expr output;
00672 if(kind == BVLT)
00673 output = d_theoryBitvector->falseExpr();
00674 else
00675 output = d_theoryBitvector->trueExpr();
00676
00677 Proof pf;
00678 if(withProof())
00679 pf = newPf("lhs_eq_rhs_ineqn", e);
00680 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00681 }
00682
00683
00684
00685 Theorem BitvectorTheoremProducer::zeroLeq(const Expr& e) {
00686 if(CHECK_PROOFS) {
00687 CHECK_SOUND(BVLE == e.getOpKind(),
00688 "BitvectorTheoremProducer::zeroLeq: "
00689 "input kind must be BVLE: e = " + e.toString());
00690 CHECK_SOUND(e.arity()==2 && e[0].getOpKind() == BVCONST &&
00691 d_theoryBitvector->computeBVConst(e[0]) == 0,
00692 "BitvectorTheoremProducer::zeroLeq: "
00693 "unexpected input: e = " + e.toString());
00694 }
00695 Proof pf;
00696 if(withProof())
00697 pf = newPf("zeroLeq", e);
00698 return newRWTheorem(e, d_theoryBitvector->trueExpr(), Assumptions::emptyAssump(), pf);
00699 }
00700
00701
00702
00703 Theorem BitvectorTheoremProducer::bvConstIneqn(const Expr& e, int kind) {
00704 if(CHECK_PROOFS) {
00705 CHECK_SOUND(BVLT == e.getOpKind() || BVLE == e.getOpKind(),
00706 "BitvectorTheoremProducer::bvConstIneqn: "
00707 "input kind must be BVLT or BVLE: e = " + e.toString());
00708 CHECK_SOUND(kind == e.getOpKind(),
00709 "BitvectorTheoremProducer::bvConstIneqn: "
00710 "input kind must match e.getOpKind(): "
00711 "\n e = " + e.toString());
00712 CHECK_SOUND((e.arity()==2),
00713 "BitvectorTheoremProducer::bvConstIneqn: "
00714 "input arity must be 2: \ne = " + e.toString());
00715 CHECK_SOUND(BVCONST == e[0].getKind() && BVCONST == e[1].getKind(),
00716 "BitvectorTheoremProducer::bvConstIneqn: "
00717 "e[0] and e[1] must both be constants:\n e = " +
00718 e.toString());
00719 }
00720
00721 int e0len = d_theoryBitvector->BVSize(e[0]);
00722 int e1len = d_theoryBitvector->BVSize(e[1]);
00723 if(CHECK_PROOFS)
00724 CHECK_SOUND(e0len == e1len,
00725 "BitvectorTheoremProducer::bvConstIneqn: "
00726 "e[0] and e[1] must have the same bvLength:\ne = " +
00727 e.toString());
00728
00729 Rational lhsVal = d_theoryBitvector->computeBVConst(e[0]);
00730 Rational rhsVal = d_theoryBitvector->computeBVConst(e[1]);
00731 Expr output;
00732
00733 if(BVLT == kind) {
00734 if(lhsVal < rhsVal)
00735 output = d_theoryBitvector->trueExpr();
00736 else
00737 output = d_theoryBitvector->falseExpr();
00738 } else {
00739 if(lhsVal <= rhsVal)
00740 output = d_theoryBitvector->trueExpr();
00741 else
00742 output = d_theoryBitvector->falseExpr();
00743 }
00744
00745 Proof pf;
00746 if(withProof())
00747 pf = newPf("bv_const_ineqn", e);
00748 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00749 }
00750
00751
00752
00753
00754
00755
00756
00757
00758
00759
00760
00761 Theorem BitvectorTheoremProducer::generalIneqn(const Expr& e,
00762 const Theorem& lhs_i,
00763 const Theorem& rhs_i,
00764 int kind) {
00765 if(CHECK_PROOFS) {
00766 CHECK_SOUND(BVLT == e.getOpKind() || BVLE == e.getOpKind(),
00767 "BitvectorTheoremProducer::generalIneqn: "
00768 "input kind must be BVLT or BVLE: e = " + e.toString());
00769 CHECK_SOUND(kind == e.getOpKind(),
00770 "BitvectorTheoremProducer::generalIneqn: "
00771 "input kind must match e.getOpKind(): "
00772 "\n e = " + e.toString());
00773 CHECK_SOUND((e.arity()==2),
00774 "BitvectorTheoremProducer::generalIneqn: "
00775 "input arity must be 2: \ne = " + e.toString());
00776 CHECK_SOUND(lhs_i.isRewrite() && rhs_i.isRewrite(),
00777 "BitvectorTheoremProducer::generalIneqn: "
00778 "lhs_i and rhs_i must be rewrite theorems: "
00779 "\nlhs_i = " + lhs_i.toString() +
00780 "\nrhs_i = " + rhs_i.toString());
00781 }
00782
00783 int e0len = d_theoryBitvector->BVSize(e[0]);
00784 int e1len = d_theoryBitvector->BVSize(e[1]);
00785 const Expr& e0_iBit = lhs_i.getLHS();
00786 const Expr& e1_iBit = rhs_i.getLHS();
00787 if(CHECK_PROOFS) {
00788 CHECK_SOUND(BOOLEXTRACT == e0_iBit.getOpKind() &&
00789 BOOLEXTRACT == e1_iBit.getOpKind(),
00790 "BitvectorTheoremProducer::generalIneqn: "
00791 "lhs_i.getRHS() and rhs_i.getRHS() must be BOOLEXTRACTs:"
00792 "\nlhs_i = " + lhs_i.toString() +
00793 "\nrhs_i = " + rhs_i.toString());
00794 CHECK_SOUND(e[0] == e0_iBit[0],
00795 "BitvectorTheoremProducer::generalIneqn: "
00796 "e[0] must be equal to LHS of lhs_i: \nlhs_i = " +
00797 lhs_i.toString() + "\n e[0] = " + e[0].toString());
00798 CHECK_SOUND(e[1] == e1_iBit[0],
00799 "BitvectorTheoremProducer::generalIneqn: "
00800 "e[1] must be equal to LHS of rhs_i: \nrhs_i = " +
00801 rhs_i.toString() + "\n e[1] = " + e[1].toString());
00802 CHECK_SOUND(e0len == e1len,
00803 "BitvectorTheoremProducer::generalIneqn: "
00804 "e[0] and e[1] must have the same bvLength:\ne = " +
00805 e.toString());
00806 int e0_iBitIndex =
00807 d_theoryBitvector->getBoolExtractIndex(e0_iBit);
00808 int e1_iBitIndex =
00809 d_theoryBitvector->getBoolExtractIndex(e1_iBit);
00810 CHECK_SOUND(e0_iBitIndex == e1_iBitIndex &&
00811 e0_iBitIndex == e0len-1,
00812 "BitvectorTheoremProducer::generalIneqn: "
00813 "e0_iBit & e1_iBit must have same extract index: "
00814 "\ne0_iBit = " + e0_iBit.toString() +
00815 "\ne1_iBit = " + e1_iBit.toString());
00816 }
00817
00818 const Expr& b1 = lhs_i.getRHS();
00819 const Expr& b2 = rhs_i.getRHS();
00820 const Expr& trueExpression = d_theoryBitvector->trueExpr();
00821 const Expr& falseExpression = d_theoryBitvector->falseExpr();
00822
00823 if(CHECK_PROOFS) {
00824 CHECK_SOUND(b1.getType().isBool(),
00825 "BitvectorTheoremProducer::generalIneqn: "
00826 "b1 must be a boolean type: "
00827 "\n b1 = " + b1.toString());
00828 CHECK_SOUND(b2.getType().isBool(),
00829 "BitvectorTheoremProducer::generalIneqn: "
00830 "b2 must be boolean type: "
00831 "\n b2 = " + b2.toString());
00832 }
00833
00834 Expr output;
00835
00836 if (b1.isFalse() && b2.isTrue())
00837 output = trueExpression;
00838 else if (b1.isTrue() && b2.isFalse())
00839 output = falseExpression;
00840 else if (e0len==1) {
00841
00842 if (kind==BVLE && (b1.isFalse() || b2.isTrue()))
00843 output = trueExpression;
00844 else if (kind==BVLT && (b2.isFalse() || b1.isTrue()))
00845 output = falseExpression;
00846 }
00847
00848
00849 if (output.isNull()) {
00850
00851
00852 if (kind == BVLT || e0len > 1) {
00853 output = (!b1) && b2;
00854 }
00855 else {
00856 output = (!b1) || b2;
00857 }
00858
00859 if(e0len > 1) {
00860
00861 Expr e0_extract =
00862 d_theoryBitvector->newBVExtractExpr(e[0],e0len-2,0);
00863
00864 Expr e1_extract =
00865 d_theoryBitvector->newBVExtractExpr(e[1],e1len-2,0);
00866
00867 Expr a;
00868 if(kind==BVLT)
00869
00870 a = d_theoryBitvector->newBVLTExpr(e0_extract,e1_extract);
00871 else
00872
00873 a = d_theoryBitvector->newBVLEExpr(e0_extract,e1_extract);
00874
00875
00876 output = output || (b1.iffExpr(b2) && a);
00877 }
00878 }
00879
00880 Proof pf;
00881 if(withProof())
00882 pf = newPf("general_ineqn", e);
00883 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
00884 }
00885
00886
00887
00888
00889
00890
00891
00892
00893
00894 Theorem BitvectorTheoremProducer::bitExtractAllToConstEq(vector<Theorem>& thms)
00895 {
00896 if (CHECK_PROOFS) {
00897 CHECK_SOUND(thms.size() > 0, "Expected size > 0");
00898 unsigned i;
00899 for(i = 0; i < thms.size(); ++i) {
00900 Expr e = thms[i].getExpr();
00901 CHECK_SOUND(e.getKind() == IFF && e.arity() == 2 && e[1].isBoolConst(),
00902 "Unexpected structure");
00903 CHECK_SOUND(e[0].getOpKind() == BOOLEXTRACT &&
00904 e[0].arity() == 1 &&
00905 e[0][0] == thms[0].getExpr()[0][0] &&
00906 unsigned(d_theoryBitvector->getBoolExtractIndex(e[0])) == i,
00907 "Unexpected structure");
00908 }
00909 }
00910 Expr lhs = thms[0].getExpr()[0][0];
00911 vector<bool> bits;
00912 for (unsigned i = 0; i < thms.size(); ++i) {
00913 bits.push_back(thms[i].getExpr()[1].isTrue() ? true : false);
00914 }
00915 Expr rhs = d_theoryBitvector->newBVConstExpr(bits);
00916
00917 Assumptions a(thms);
00918 Proof pf;
00919 if (withProof())
00920 pf = newPf("bit_extract_all_to_const_eq");
00921 return newRWTheorem(lhs, rhs, a, pf);
00922 }
00923
00924
00925
00926 Theorem BitvectorTheoremProducer::bitExtractToExtract(const Theorem& thm) {
00927 const Expr& e = thm.getExpr();
00928 if(CHECK_PROOFS) {
00929 CHECK_SOUND((e.isNot() && e[0].getOpKind() == BOOLEXTRACT)
00930 || (e.getOpKind() == BOOLEXTRACT),
00931 "BitvectorTheoremProducer::bitExtractToExtract:\n e = "
00932 +e.toString());
00933 }
00934 bool negative = e.isNot();
00935 const Expr& boolExtract = negative? e[0] : e;
00936 int i = d_theoryBitvector->getBoolExtractIndex(boolExtract);
00937 Expr lhs = d_theoryBitvector->newBVExtractExpr(boolExtract[0], i, i);
00938
00939 Proof pf;
00940 if(withProof())
00941 pf = newPf("bit_extract_to_extract", e, thm.getProof());
00942 return newRWTheorem(lhs, negative? bvZero() : bvOne(), thm.getAssumptionsRef(), pf);
00943 }
00944
00945
00946
00947 Theorem BitvectorTheoremProducer::bitExtractRewrite(const Expr& x) {
00948 if(CHECK_PROOFS) {
00949 CHECK_SOUND(x.getOpKind() == BOOLEXTRACT,
00950 "BitvectorTheoremProducer::bitExtractRewrite: x = "
00951 +x.toString());
00952 }
00953
00954 int i = d_theoryBitvector->getBoolExtractIndex(x);
00955 const Expr& t = x[0];
00956 int bvLength = d_theoryBitvector->BVSize(t);
00957
00958 if(CHECK_PROOFS) {
00959 CHECK_SOUND(0<=i && i<bvLength,
00960 "BitvectorTheoremProducer::bitExtractRewrite:"
00961 "\n bvLength = "
00962 + int2string(bvLength)
00963 +"\n i = "+ int2string(i)
00964 +"\n x = "+ x.toString());
00965 }
00966 Proof pf;
00967 if(withProof())
00968 pf = newPf("bit_extract_rewrite", x);
00969 Expr res = d_theoryBitvector->newBVExtractExpr(t, i, i);
00970 res = d_theoryBitvector->newBoolExtractExpr(res, 0);
00971 return newRWTheorem(x, res, Assumptions::emptyAssump(), pf);
00972 }
00973
00974
00975
00976 Theorem BitvectorTheoremProducer::bitExtractConstant(const Expr & x, int i)
00977 {
00978 TRACE("bitvector", "bitExtractConstant(", x, ", "+ int2string(i) +" ) {");
00979 if(CHECK_PROOFS) {
00980
00981 CHECK_SOUND(BVCONST == x.getKind(),
00982 "BitvectorTheoremProducer::bitExtractConstant:"
00983 "the bitvector must be a constant.");
00984
00985 CHECK_SOUND(0 <= i && (unsigned)i < d_theoryBitvector->getBVConstSize(x),
00986 "BitvectorTheoremProducer::bitExtractConstant:"
00987 "illegal extraction attempted on the bitvector x = "
00988 + x.toString()
00989 + "\nat the position i = "
00990 + int2string(i));
00991 }
00992
00993 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
00994
00995
00996
00997
00998 Expr output;
00999 if(!d_theoryBitvector->getBVConstValue(x, i))
01000 output = d_theoryBitvector->falseExpr();
01001 else
01002 output = d_theoryBitvector->trueExpr();
01003
01004 Proof pf;
01005 if(withProof()) pf = newPf("bit_extract_constant", x, rat(i));
01006 Theorem result(newRWTheorem(bitExtract,output,Assumptions::emptyAssump(),pf));
01007 TRACE("bitvector", "bitExtractConstant => ", result, " }");
01008 return result;
01009 }
01010
01011
01012
01013
01014
01015
01016 Theorem BitvectorTheoremProducer::bitExtractConcatenation(const Expr & x,
01017 int i)
01018 {
01019 TRACE("bitvector", "bitExtractConcatenation(",
01020 x.toString(), ", "+ int2string(i) + " ) {");
01021 Type type = d_theoryBitvector->getBaseType(x);
01022 if(CHECK_PROOFS) {
01023
01024 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01025 "BitvectorTheoremProducer::bitExtractConcatenation: "
01026 "term must be bitvector:\n x = "+x.toString());
01027 CHECK_SOUND(CONCAT == x.getOpKind() && x.arity() >= 2,
01028 "BitvectorTheoremProducer::bitExtractConcatenation: "
01029 "the bitvector must be a concat:\n x = " + x.toString());
01030 }
01031
01032
01033 int bvLength = d_theoryBitvector->BVSize(x);
01034 if(CHECK_PROOFS) {
01035 CHECK_SOUND(0 <= i && i < bvLength,
01036 "BitvectorTheoremProducer::bitExtractNot:"
01037 "illegal boolean extraction was attempted at position i = "
01038 + int2string(i)
01039 + "\non bitvector x = " + x.toString()
01040 + "\nwhose bvLength is = " +
01041 int2string(bvLength));
01042 }
01043
01044
01045 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01046
01047 int numOfKids = x.arity();
01048 int lenOfKidsSeen = 0;
01049 Expr bitExtractKid;
01050 for(int count = numOfKids-1; count >= 0; --count) {
01051 int bvLengthOfKid = d_theoryBitvector->BVSize(x[count]);
01052 if(lenOfKidsSeen <= i && i < bvLengthOfKid + lenOfKidsSeen) {
01053 bitExtractKid =
01054 d_theoryBitvector->newBoolExtractExpr(x[count], i - lenOfKidsSeen);
01055 break;
01056 }
01057 lenOfKidsSeen += bvLengthOfKid;
01058 }
01059 DebugAssert(!bitExtractKid.isNull(),
01060 "BitvectorTheoremProducer::bitExtractConcatenation: "
01061 "something's broken...");
01062
01063 Proof pf;
01064 if(withProof())
01065 pf = newPf("bit_extract_concatenation", x, rat(i));
01066 Theorem result(newRWTheorem(bitExtract, bitExtractKid, Assumptions::emptyAssump(), pf));
01067 TRACE("bitvector", "bitExtractConcatenation => ", result, " }");
01068 return result;
01069 }
01070
01071
01072
01073 Theorem BitvectorTheoremProducer::bitExtractConstBVMult(const Expr& t, int i)
01074 {
01075 TRACE("bitvector", "input to bitExtractConstBVMult(", t.toString(), ")");
01076 TRACE("bitvector", "input to bitExtractConstBVMult(", int2string(i), ")");
01077
01078 Type type = t.getType();
01079 int bvLength = d_theoryBitvector->BVSize(t);
01080 if(CHECK_PROOFS) {
01081 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01082 "BitvectorTheoremProducer::bitExtractConstBVMult:"
01083 "the term must be a bitvector: " + t.toString());
01084 CHECK_SOUND(BVMULT == t.getOpKind() && 2 == t.arity(),
01085 "BitvectorTheoremProducer::bitExtractConstBVMult:"
01086 "the term must be a MULT of arity 2: " + t.toString());
01087 CHECK_SOUND(d_theoryBitvector->BVSize(t[0]) == bvLength &&
01088 d_theoryBitvector->BVSize(t[1]) == bvLength,
01089 "BitvectorTheoremProducer::bitExtractConstBVMult:"
01090 "Expected inputs of same length");
01091 CHECK_SOUND(0 <= i && i < bvLength,
01092 "BitvectorTheoremProducer::bitExtractNot:"
01093 "illegal boolean extraction was attempted at position i = "
01094 + int2string(i)
01095 + "\non bitvector x = " + t.toString()
01096 + "\nwhose bvLength is = " +
01097 int2string(bvLength));
01098 CHECK_SOUND(BVCONST == t[0].getKind(),
01099 "BitvectorTheoremProducer::bitExtractConstBVMult:"
01100 "illegal BVMULT expression" + t.toString());
01101 }
01102
01103 std::vector<Expr> k;
01104 for(int j=0; j < bvLength; ++j)
01105 if (d_theoryBitvector->getBVConstValue(t[0], j)) {
01106 Expr leftshiftTerm =
01107 d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t[1], j);
01108 k.push_back(leftshiftTerm);
01109 }
01110
01111 Expr mult;
01112
01113 switch(k.size()) {
01114 case 0:
01115
01116 mult = d_theoryBitvector->newBVZeroString(bvLength);
01117 break;
01118 case 1:
01119 mult = k[0];
01120 break;
01121 default:
01122 mult = d_theoryBitvector->newBVPlusExpr(bvLength, k);
01123 break;
01124 }
01125 Expr output = d_theoryBitvector->newBoolExtractExpr(mult, i);
01126
01127
01128 const Expr bitExtract =
01129 d_theoryBitvector->newBoolExtractExpr(t, i);
01130
01131 Proof pf;
01132 if(withProof()) pf = newPf("bit_extract_const_bvmult", t, rat(i));
01133 const Theorem result = newRWTheorem(bitExtract,output,Assumptions::emptyAssump(),pf);
01134 TRACE("bitvector",
01135 "output of bitExtract_const_bvmult(", result, ")");
01136 return result;
01137 }
01138
01139
01140 Theorem BitvectorTheoremProducer::bitExtractBVMult(const Expr& t, int i)
01141 {
01142 TRACE("bitvector", "input to bitExtractBVMult(", t.toString(), ")");
01143 TRACE("bitvector", "input to bitExtractBVMult(", int2string(i), ")");
01144
01145 Type type = t.getType();
01146 int bvLength= d_theoryBitvector->BVSize(t);
01147 if(CHECK_PROOFS) {
01148 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01149 "BitvectorTheoremProducer::bitExtractBVMult:"
01150 "the term must be a bitvector" + t.toString());
01151 CHECK_SOUND(BVMULT == t.getOpKind() && 2 == t.arity(),
01152 "BitvectorTheoremProducer::bitExtractBVMult:"
01153 "the term must be a bitvector" + t.toString());
01154 CHECK_SOUND(d_theoryBitvector->BVSize(t[0]) == bvLength &&
01155 d_theoryBitvector->BVSize(t[1]) == bvLength,
01156 "BitvectorTheoremProducer::bitExtractConstBVMult:"
01157 "Expected inputs of same length");
01158 CHECK_SOUND(0 <= i && i < bvLength,
01159 "BitvectorTheoremProducer::bitExtractNot:"
01160 "illegal boolean extraction was attempted at position i = "
01161 + int2string(i)
01162 + "\non bitvector t = " + t.toString()
01163 + "\nwhose Length is = " +
01164 int2string(bvLength));
01165 CHECK_SOUND(BVCONST != t[0].getOpKind(),
01166 "BitvectorTheoremProducer::bitExtractBVMult:"
01167 "illegal BVMULT expression" + t.toString());
01168 }
01169 Expr trueExpression = d_theoryBitvector->trueExpr();
01170 std::vector<Expr> k;
01171 for(int j=bvLength-1; j >= 0; j--) {
01172 Expr ext = d_theoryBitvector->newBVExtractExpr(t[0],j,j);
01173 Expr cond = ext.eqExpr(d_theoryBitvector->newBVOneString(1));
01174 Expr leftshiftTerm = d_theoryBitvector->newFixedConstWidthLeftShiftExpr(t[1], j);
01175 Expr zeroString = d_theoryBitvector->newBVZeroString(bvLength);
01176 Expr iteTerm = cond.iteExpr(leftshiftTerm, zeroString);
01177 k.push_back(iteTerm);
01178 }
01179
01180 if(CHECK_PROOFS)
01181 CHECK_SOUND(k.size() > 0,
01182 "BitvectorTheoremProducer::bitExtractBVMult:"
01183 "size of output vector must be > 0");
01184 Expr mult;
01185 if (k.size() > 1)
01186 mult = d_theoryBitvector->newBVPlusExpr(bvLength, k);
01187 else
01188 mult = k[0];
01189 Expr output = d_theoryBitvector->newBoolExtractExpr(mult, i);
01190
01191
01192 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(t, i);
01193
01194 Proof pf;
01195 if(withProof()) pf = newPf("bit_extract_bvmult", t, rat(i));
01196 const Theorem result = newRWTheorem(bitExtract,output,Assumptions::emptyAssump(),pf);
01197 TRACE("bitvector","output of bitExtract_bvmult(", result, ")");
01198 return result;
01199 }
01200
01201
01202
01203
01204
01205 Theorem BitvectorTheoremProducer::bitExtractExtraction(const Expr & x, int i)
01206 {
01207 TRACE("bitvector", "input to bitExtractExtraction(", x.toString(), ")");
01208 TRACE("bitvector", "input to bitExtractExtraction(", int2string(i), ")");
01209
01210 Type type = x.getType();
01211 if(CHECK_PROOFS) {
01212
01213 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01214 "BitvectorTheoremProducer::bitExtract-Extraction:"
01215 "term must be bitvector.");
01216 CHECK_SOUND(EXTRACT == x.getOpKind() && 1 == x.arity(),
01217 "BitvectorTheoremProducer::bitExtract-Extraction:"
01218 "the bitvector must be an extract." + x.toString());
01219
01220 int bvLength= d_theoryBitvector->BVSize(type.getExpr());
01221 CHECK_SOUND(0 <= i && i < bvLength,
01222 "BitvectorTheoremProducer::bitExtractNot:"
01223 "illegal boolean extraction was attempted at position i = "
01224 + int2string(i)
01225 + "\non bitvector t = " + x.toString()
01226 + "\nwhose Length is = " +
01227 int2string(bvLength));
01228 int extractLeft = d_theoryBitvector->getExtractHi(x);
01229 int extractRight = d_theoryBitvector->getExtractLow(x);
01230 CHECK_SOUND(extractLeft >= extractRight && extractLeft >= 0,
01231 "BitvectorTheoremProducer::bitExtract-Extraction:"
01232 "illegal boolean extraction was attempted." + int2string(i) +
01233 int2string(extractLeft) + int2string(extractRight));
01234 CHECK_SOUND(0 <= i && i < extractLeft-extractRight+1,
01235 "BitvectorTheoremProducer::bitExtract-Extraction:"
01236 "illegal boolean extraction was attempted." + int2string(i) +
01237 int2string(extractLeft) + int2string(extractRight));
01238 }
01239
01240 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01241 const Expr bitExtractExtraction =
01242 d_theoryBitvector->newBoolExtractExpr(x[0], i +
01243 d_theoryBitvector->getExtractLow(x));
01244
01245 Proof pf;
01246 if(withProof()) pf = newPf("bit_extract_extraction", x, rat(i));
01247 Theorem result(newRWTheorem(bitExtract, bitExtractExtraction, Assumptions::emptyAssump(), pf));
01248 TRACE("bitvector",
01249 "output of bitExtractExtraction(", result, ")");
01250 return result;
01251 }
01252
01253 Theorem
01254 BitvectorTheoremProducer::
01255 bitExtractBVPlus(const std::vector<Theorem>& t1BitExtractThms,
01256 const std::vector<Theorem>& t2BitExtractThms,
01257 const Expr& bvPlusTerm, int bitPos)
01258 {
01259 TRACE("bitvector","input to bitExtractBVPlus(", bvPlusTerm.toString(), ")");
01260 TRACE("bitvector","input to bitExtractBVPlus(", int2string(bitPos), ")");
01261
01262 if(CHECK_PROOFS) {
01263 CHECK_SOUND(BVPLUS == bvPlusTerm.getOpKind() && 2 == bvPlusTerm.arity(), "BitvectorTheoremProducer::bitExtractBVPlus: illegal bitvector fed to the function." + bvPlusTerm.toString());
01264 CHECK_SOUND(d_theoryBitvector->getBVPlusParam(bvPlusTerm) >= 0, "BitvectorTheoremProducer::bitExtractBVPlus: illegal bitvector fed to the function." + bvPlusTerm.toString());
01265 CHECK_SOUND(bitPos+1 == (int)t1BitExtractThms.size() && bitPos+1 == (int)t2BitExtractThms.size(), "BitvectorTheoremProducer::bitExtractBVPlus: illegal bitvector fed to the function." + int2string(bitPos));
01266 const Expr& t1 = bvPlusTerm[0];
01267 const Expr& t2 = bvPlusTerm[1];
01268 std::vector<Theorem>::const_iterator i = t1BitExtractThms.begin();
01269 std::vector<Theorem>::const_iterator iend = t1BitExtractThms.end();
01270 std::vector<Theorem>::const_iterator j = t2BitExtractThms.begin();
01271 for(; i !=iend; ++i, ++j) {
01272 const Expr& t1Expr = i->getLHS();
01273 const Expr& t2Expr = j->getLHS();
01274 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());
01275 }
01276 }
01277 const Expr lhs = d_theoryBitvector->newBoolExtractExpr(bvPlusTerm, bitPos);
01278 Expr rhs;
01279 const Expr& t1_iBit = (t1BitExtractThms[bitPos]).getRHS();
01280 const Expr& t2_iBit = (t2BitExtractThms[bitPos]).getRHS();
01281 if(0 != bitPos) {
01282 const Expr carry_iBit = computeCarry(t1BitExtractThms, t2BitExtractThms, bitPos);
01283
01284
01285
01286
01287 rhs = t1_iBit.iffExpr(t2_iBit).iffExpr(carry_iBit);
01288
01289
01290
01291 } else
01292
01293 rhs = !(t1_iBit.iffExpr(t2_iBit));
01294
01295 Proof pf;
01296 if(withProof())
01297 pf = newPf("bit_extract_BVPlus_rule",bvPlusTerm,rat(bitPos));
01298 Theorem result = newRWTheorem(lhs, rhs, Assumptions::emptyAssump(), pf);
01299 TRACE("bitvector","output of bitExtractBVPlus(", result, ")");
01300 return result;
01301 }
01302
01303 Expr
01304 BitvectorTheoremProducer::computeCarry(const std::vector<Theorem>& t1BitExtractThms,
01305 const std::vector<Theorem>& t2BitExtractThms,
01306 int i){
01307 vector<Expr> carry;
01308 int bitPos = i;
01309 DebugAssert(bitPos >= 0,
01310 "computeCarry: negative bitExtract_Pos is illegal");
01311 if(0 == bitPos) {
01312 const Expr& t1Thm = t1BitExtractThms[bitPos].getRHS();
01313 const Expr& t2Thm = t2BitExtractThms[bitPos].getRHS();
01314 carry.push_back(t1Thm.andExpr(t2Thm));
01315 }
01316 else {
01317 const Expr& t1Thm = t1BitExtractThms[bitPos-1].getRHS();
01318 const Expr& t2Thm = t2BitExtractThms[bitPos-1].getRHS();
01319 const Expr iMinusOneTerm = t1Thm.andExpr(t2Thm);
01320 carry.push_back(iMinusOneTerm);
01321
01322 const Expr iMinusOneCarry =
01323 computeCarry(t1BitExtractThms,t2BitExtractThms,bitPos-1);
01324 const Expr secondTerm = t1Thm.andExpr(iMinusOneCarry);
01325 carry.push_back(secondTerm);
01326
01327 const Expr thirdTerm = t2Thm.andExpr(iMinusOneCarry);
01328
01329 carry.push_back(thirdTerm);
01330 }
01331 return orExpr(carry);
01332 }
01333
01334 Theorem
01335 BitvectorTheoremProducer::
01336 bitExtractBVPlusPreComputed(const Theorem& t1_i,
01337 const Theorem& t2_i,
01338 const Expr& bvPlusTerm,
01339 int bitPos,
01340 int precomputedFlag)
01341 {
01342 DebugAssert(0 != precomputedFlag,
01343 "precomputedFlag cannot be 0");
01344 TRACE("bitvector","input to bitExtractBVPlus(", bvPlusTerm.toString(), ")");
01345 TRACE("bitvector","input to bitExtractBVPlus(", int2string(bitPos), ")");
01346
01347 if(CHECK_PROOFS) {
01348 CHECK_SOUND(BVPLUS == bvPlusTerm.getOpKind() && 2 == bvPlusTerm.arity(),
01349 "BitvectorTheoremProducer::bitExtractBVPlus:"
01350 "illegal bitvector fed to the function." +
01351 bvPlusTerm.toString());
01352 CHECK_SOUND(d_theoryBitvector->getBVPlusParam(bvPlusTerm) >= 0,
01353 "BitvectorTheoremProducer::bitExtractBVPlus:"
01354 "illegal bitvector fed to the function." +
01355 bvPlusTerm.toString());
01356 const Expr& t1 = bvPlusTerm[0];
01357 const Expr& t2 = bvPlusTerm[1];
01358 CHECK_SOUND(t1_i.getLHS()[0] == t1 &&
01359 t2_i.getLHS()[0] == t2,
01360 "BitvectorTheoremProducer::bitExtractBVPlus:"
01361 "illegal theorems fed to the function. Theorem1 = " +
01362 t1_i.toString() + "\nTheorem2 = " + t2_i.toString());
01363 CHECK_SOUND(t1_i.getLHS().getOpKind() == BOOLEXTRACT &&
01364 t2_i.getLHS().getOpKind() == BOOLEXTRACT,
01365 "BitvectorTheoremProducer::bitExtractBVPlus:"
01366 "illegal theorems fed to the function. Theorem1 = " +
01367 t1_i.toString() + "\nTheorem2 = " + t2_i.toString());
01368 CHECK_SOUND(d_theoryBitvector->getBoolExtractIndex(t1_i.getLHS()) == bitPos &&
01369 d_theoryBitvector->getBoolExtractIndex(t2_i.getLHS()) == bitPos,
01370 "BitvectorTheoremProducer::bitExtractBVPlus:"
01371 "illegal theorems fed to the function. Theorem1 = " +
01372 t1_i.toString() + "\nTheorem2 = " + t2_i.toString());
01373 }
01374 const Expr lhs =
01375 d_theoryBitvector->newBoolExtractExpr(bvPlusTerm, bitPos);
01376 Expr rhs;
01377 const Expr& t1_iBit = t1_i.getRHS();
01378 const Expr& t2_iBit = t2_i.getRHS();
01379
01380 const Expr carry_iBit = computeCarryPreComputed(t1_i, t2_i, bitPos, precomputedFlag);
01381
01382 if(0 != bitPos) {
01383
01384
01385
01386
01387 rhs = t1_iBit.iffExpr(t2_iBit).iffExpr(carry_iBit);
01388
01389 } else
01390
01391 rhs = !(t1_iBit.iffExpr(t2_iBit));
01392
01393 Proof pf;
01394 if(withProof())
01395 pf = newPf("bit_extract_BVPlus_precomputed_rule",bvPlusTerm,rat(bitPos));
01396 Theorem result = newRWTheorem(lhs, rhs, Assumptions::emptyAssump(), pf);
01397 TRACE("bitvector","output of bitExtractBVPlus(", result, ")");
01398 return result;
01399 }
01400
01401
01402
01403 Expr
01404 BitvectorTheoremProducer::
01405 computeCarryPreComputed(const Theorem& t1_i,
01406 const Theorem& t2_i,
01407 int bitPos, int preComputed){
01408 DebugAssert(1 == preComputed ||
01409 2 == preComputed,
01410 "cannot happen");
01411 Expr carryout;
01412 Expr carryin;
01413 DebugAssert(bitPos >= 0,
01414 "computeCarry: negative bitExtract_Pos is illegal");
01415
01416 const Expr& t1Thm = t1_i.getRHS();
01417 const Expr& t2Thm = t2_i.getRHS();
01418 Expr x = t1Thm.andExpr(t2Thm);
01419 const Expr& t1 = t1_i.getLHS()[0];
01420 const Expr& t2 = t2_i.getLHS()[0];
01421 Expr t1Andt2 = t1.andExpr(t2);
01422 Expr index = t1Andt2.andExpr(rat(bitPos));
01423
01424 if(0 == bitPos) {
01425 if(1 == preComputed)
01426 d_theoryBitvector->d_bvPlusCarryCacheLeftBV.insert(index,x);
01427 else
01428 d_theoryBitvector->d_bvPlusCarryCacheRightBV.insert(index,x);
01429 carryout = x;
01430
01431 }
01432 else {
01433 if(1 == preComputed) {
01434 Expr indexMinusOne = t1Andt2.andExpr(rat(bitPos-1));
01435 if(d_theoryBitvector->d_bvPlusCarryCacheLeftBV.find(indexMinusOne) ==
01436 d_theoryBitvector->d_bvPlusCarryCacheLeftBV.end())
01437 DebugAssert(false,
01438 "this should not happen");
01439 carryin =
01440 (d_theoryBitvector->d_bvPlusCarryCacheLeftBV).find(indexMinusOne)->second;
01441 Expr secondTerm = t1Thm.andExpr(carryin);
01442 Expr thirdTerm = t2Thm.andExpr(carryin);
01443
01444 carryout = (x.orExpr(secondTerm)).orExpr(thirdTerm);
01445 d_theoryBitvector->d_bvPlusCarryCacheLeftBV.insert(index,carryout);
01446 }
01447 else {
01448 Expr indexMinusOne = t1Andt2.andExpr(rat(bitPos-1));
01449 if(d_theoryBitvector->d_bvPlusCarryCacheRightBV.find(indexMinusOne) ==
01450 d_theoryBitvector->d_bvPlusCarryCacheRightBV.end())
01451 DebugAssert(false,
01452 "this should not happen");
01453 carryin =
01454 (d_theoryBitvector->d_bvPlusCarryCacheRightBV).find(indexMinusOne)->second;
01455
01456 Expr secondTerm = t1Thm.andExpr(carryin);
01457 Expr thirdTerm = t2Thm.andExpr(carryin);
01458
01459 carryout = (x.orExpr(secondTerm)).orExpr(thirdTerm);
01460 d_theoryBitvector->d_bvPlusCarryCacheRightBV.insert(index,carryout);
01461 }
01462 }
01463
01464 return carryin;
01465 }
01466
01467 Theorem
01468 BitvectorTheoremProducer::
01469 zeroPaddingRule(const Expr& e, int i) {
01470 if(CHECK_PROOFS) {
01471 CHECK_SOUND(BITVECTOR == e.getType().getExpr().getOpKind(),
01472 "BitvectorTheoremProducer::zeroPaddingRule:"
01473 "Wrong Input: Input must be a bitvector. But the input is: " +
01474 e.toString());
01475 }
01476
01477 int bvLength =
01478 d_theoryBitvector->BVSize(d_theoryBitvector->getBaseType(e).getExpr());
01479
01480 if(CHECK_PROOFS) {
01481 CHECK_SOUND(0 <= i && i >= bvLength,
01482 "BitvectorTheoremProducer::zeroPaddingRule:"
01483 "bitPosition of extraction must be greater than bvLength" +
01484 int2string(i) + "bvLength:" + int2string(bvLength));
01485 }
01486 const Expr boolExtractExpr = d_theoryBitvector->newBoolExtractExpr(e, i);
01487
01488 Proof pf;
01489 if(withProof())
01490 pf = newPf("zeropadding_rule", e, rat(i));
01491 return newRWTheorem(boolExtractExpr, d_theoryBitvector->falseExpr(), Assumptions::emptyAssump(), pf);
01492 }
01493
01494 Theorem
01495 BitvectorTheoremProducer::
01496 bvPlusAssociativityRule(const Expr& bvPlusTerm)
01497 {
01498 TRACE("bitvector",
01499 "input to bvPlusAssociativityRule(", bvPlusTerm.toString(), ")");
01500
01501 Type type = bvPlusTerm.getType();
01502 if(CHECK_PROOFS) {
01503 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01504 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
01505 "term must be BITVECTOR type.");
01506 CHECK_SOUND(BVPLUS == bvPlusTerm.getOpKind(),
01507 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
01508 "term must have the kind BVPLUS.");
01509 CHECK_SOUND(2 < bvPlusTerm.arity(),
01510 "BitvectorTheoremProducer::bvPlusAssociativityRule:"
01511 "term must have arity() greater than 2 for associativity.");
01512 }
01513 std::vector<Expr> BVPlusTerms0;
01514 std::vector<Expr>::const_iterator j = (bvPlusTerm.getKids()).begin();
01515 std::vector<Expr>::const_iterator jend = (bvPlusTerm.getKids()).end();
01516
01517 j++;
01518 BVPlusTerms0.insert(BVPlusTerms0.end(), j, jend);
01519 int bvLength = d_theoryBitvector->BVSize(bvPlusTerm);
01520 const Expr bvplus0 = d_theoryBitvector->newBVPlusExpr(bvLength,
01521 BVPlusTerms0);
01522
01523 std::vector<Expr> BVPlusTerms1;
01524 BVPlusTerms1.push_back(*((bvPlusTerm.getKids()).begin()));
01525 BVPlusTerms1.push_back(bvplus0);
01526 const Expr bvplusOutput = d_theoryBitvector->newBVPlusExpr(bvLength,
01527 BVPlusTerms1);
01528
01529 Proof pf;
01530 if(withProof()) pf = newPf("bv_plus_associativityrule", bvPlusTerm);
01531 const Theorem result(newRWTheorem(bvPlusTerm, bvplusOutput, Assumptions::emptyAssump(), pf));
01532 TRACE("bitvector",
01533 "output of bvPlusAssociativityRule(", result, ")");
01534 return result;
01535 }
01536
01537
01538 Theorem BitvectorTheoremProducer::bitExtractNot(const Expr & x,
01539 int i) {
01540 TRACE("bitvector", "input to bitExtractNot(", x.toString(), ")");
01541 TRACE("bitvector", "input to bitExtractNot(", int2string(i), ")");
01542
01543 Type type = x.getType();
01544 if(CHECK_PROOFS) {
01545
01546 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01547 "BitvectorTheoremProducer::bitExtractNot:"
01548 "term must be bitvector.");
01549 CHECK_SOUND(BVNEG == x.getOpKind() && 1 == x.arity(),
01550 "BitvectorTheoremProducer::bitExtractNot:"
01551 "the bitvector must be an bitwise negation." + x.toString());
01552
01553 int bvLength= d_theoryBitvector->BVSize(type.getExpr());
01554 CHECK_SOUND(0 <= i && i < bvLength,
01555 "BitvectorTheoremProducer::bitExtractNot:"
01556 "illegal boolean extraction was attempted at position i = "
01557 + int2string(i)
01558 + "\non bitvector x = " + x.toString()
01559 + "\nwhose Length is = " +
01560 int2string(bvLength));
01561 }
01562
01563 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01564 const Expr bitNegTerm = d_theoryBitvector->newBoolExtractExpr(x[0], i);
01565
01566 Proof pf;
01567 if(withProof()) pf = newPf("bit_extract_bitwiseneg", x, rat(i));
01568 const Theorem result(newRWTheorem(bitExtract,!bitNegTerm,Assumptions::emptyAssump(),pf));
01569 TRACE("bitvector","output of bitExtractNot(", result, ")");
01570 return result;
01571 }
01572
01573
01574 Theorem BitvectorTheoremProducer::bitExtractBitwise(const Expr & x,
01575 int i, int kind)
01576 {
01577 TRACE("bitvector", "bitExtractBitwise(", x, ", "+ int2string(i)+") {");
01578 Type type = x.getType();
01579 if(CHECK_PROOFS) {
01580 CHECK_SOUND(kind == BVAND || kind == BVOR || kind == BVXOR,
01581 "BitvectorTheoremProducer::bitExtractBitwise: kind = "
01582 +d_theoryBitvector->getEM()->getKindName(kind));
01583
01584 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01585 "BitvectorTheoremProducer::bitExtractBitwise: "
01586 "term must be bitvector.\n x = "+x.toString()
01587 +" : "+type.toString());
01588 CHECK_SOUND(x.getOpKind() == kind && 2 <= x.arity(),
01589 "BitvectorTheoremProducer::bitExtractBitwise: "
01590 "kind does not match.\n x = "
01591 + x.toString());
01592
01593 int size = d_theoryBitvector->BVSize(x);
01594 CHECK_SOUND(0 <= i && i < size,
01595 "BitvectorTheoremProducer::bitExtractBitwise: "
01596 "illegal boolean extraction was attempted.\n i = "
01597 + int2string(i) + "\n size = "+ int2string(size));
01598 }
01599
01600 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01601 vector<Expr> kids;
01602 for(Expr::iterator j=x.begin(), jend=x.end(); j!=jend; ++j) {
01603 kids.push_back(d_theoryBitvector->newBoolExtractExpr(*j, i));
01604 }
01605
01606 int resKind = kind == BVAND ? AND :
01607 kind == BVOR ? OR : XOR;
01608 Expr rhs = Expr(resKind, kids);
01609
01610 Proof pf;
01611 if(withProof()) pf = newPf("bit_extract_bitwise", x, rat(i));
01612 const Theorem result(newRWTheorem(bitExtract, rhs, Assumptions::emptyAssump(), pf));
01613 TRACE("bitvector", "bitExtractBitwise => ", result.toString(), " }");
01614 return result;
01615 }
01616
01617
01618 Theorem BitvectorTheoremProducer::bitExtractFixedLeftShift(const Expr & x,
01619 int i) {
01620 TRACE("bitvector", "input to bitExtractFixedleftshift(", x.toString(), ")");
01621 TRACE("bitvector", "input to bitExtractFixedleftshift(", int2string(i), ")");
01622
01623 Type type = x.getType();
01624 if(CHECK_PROOFS) {
01625
01626 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01627 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
01628 "term must be bitvector.");
01629 CHECK_SOUND((x.getOpKind() == LEFTSHIFT ||
01630 x.getOpKind() == CONST_WIDTH_LEFTSHIFT) && 1 == x.arity(),
01631 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
01632 "the bitvector must be a bitwise LEFTSHIFT." +
01633 x.toString());
01634 CHECK_SOUND(d_theoryBitvector->getFixedLeftShiftParam(x) >= 0,
01635 "BitvectorTheoremProducer::bitExtractFixedleftshift:"
01636 "the bitvector must be a bitwise LEFTSHIFT." +
01637 x.toString());
01638
01639 int bvLength= d_theoryBitvector->BVSize(type.getExpr());
01640 CHECK_SOUND(0 <= i && i < bvLength,
01641 "BitvectorTheoremProducer::bitExtractNot:"
01642 "illegal boolean extraction was attempted at position i = "
01643 + int2string(i)
01644 + "\non bitvector x = " + x.toString()
01645 + "\nwhose bvLength is = " +
01646 int2string(bvLength));
01647 }
01648
01649 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01650 int shiftLength = d_theoryBitvector->getFixedLeftShiftParam(x);
01651 Expr output;
01652 if(0 <= i && i < shiftLength)
01653 output = d_theoryBitvector->falseExpr();
01654 else
01655 output =
01656 d_theoryBitvector->newBoolExtractExpr(x[0], i-shiftLength);
01657
01658 Proof pf;
01659 if(withProof())
01660 pf = newPf("bit_extract_bitwisefixedleftshift", x,rat(i));
01661 const Theorem result = newRWTheorem(bitExtract, output, Assumptions::emptyAssump(), pf);
01662 TRACE("bitvector",
01663 "output of bitExtractFixedleftshift(", result, ")");
01664 return result;
01665 }
01666
01667 Theorem BitvectorTheoremProducer::bitExtractFixedRightShift(const Expr & x,
01668 int i) {
01669 TRACE("bitvector", "input to bitExtractFixedRightShift(", x.toString(), ")");
01670 TRACE("bitvector", "input to bitExtractFixedRightShift(", int2string(i), ")");
01671
01672 Type type = x.getType();
01673 if(CHECK_PROOFS) {
01674
01675 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01676 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
01677 "term must be bitvector.");
01678 CHECK_SOUND(RIGHTSHIFT == x.getOpKind() && 1 == x.arity(),
01679 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
01680 "the bitvector must be an bitwise RIGHTSHIFT." +
01681 x.toString());
01682 CHECK_SOUND(d_theoryBitvector->getFixedRightShiftParam(x) >= 0,
01683 "BitvectorTheoremProducer::bitExtractFixedRightShift:"
01684 "the bitvector must be an bitwise RIGHTSHIFT." +
01685 x.toString());
01686 }
01687
01688 int bvLength = d_theoryBitvector->BVSize(x);
01689 if(CHECK_PROOFS)
01690 CHECK_SOUND(0 <= i && i < bvLength,
01691 "BitvectorTheoremProducer::bitExtractNot:"
01692 "illegal boolean extraction was attempted at position i = "
01693 + int2string(i)
01694 + "\non bitvector t = " + x.toString()
01695 + "\nwhose Length is = " +
01696 int2string(bvLength));
01697
01698
01699 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01700 int shiftLength = d_theoryBitvector->getFixedRightShiftParam(x);
01701 Expr output;
01702 if(bvLength > i && i > bvLength-shiftLength-1)
01703 output = d_theoryBitvector->falseExpr();
01704 else
01705 output =
01706 d_theoryBitvector->newBoolExtractExpr(x[0], i);
01707
01708 Proof pf;
01709 if(withProof())
01710 pf = newPf("bit_extract_bitwiseFixedRightShift", x,rat(i));
01711 const Theorem result = newRWTheorem(bitExtract, output, Assumptions::emptyAssump(), pf);
01712 TRACE("bitvector",
01713 "output of bitExtractFixedRightShift(", result, ")");
01714 return result;
01715 }
01716
01717
01718
01719
01720 Theorem BitvectorTheoremProducer::bitExtractBVSHL(const Expr & x, int i)
01721 {
01722 Type type = x.getType();
01723 int bvLength= d_theoryBitvector->BVSize(x);
01724 if(CHECK_PROOFS) {
01725
01726 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01727 "BitvectorTheoremProducer::bitExtractBVSHL:"
01728 "term must be bitvector.");
01729 CHECK_SOUND(x.getOpKind() == BVSHL && 2 == x.arity(),
01730 "BitvectorTheoremProducer::bitExtractBVSHL:"
01731 "the bitvector must be a BVSHL." +
01732 x.toString());
01733
01734 CHECK_SOUND(0 <= i && i < bvLength,
01735 "BitvectorTheoremProducer::bitExtractBVSHL:"
01736 "illegal boolean extraction was attempted at position i = "
01737 + int2string(i)
01738 + "\non bitvector x = " + x.toString()
01739 + "\nwhose bvLength is = " +
01740 int2string(bvLength));
01741 }
01742
01743 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01744
01745 const Expr& term = x[0];
01746 const Expr& shift = x[1];
01747
01748 vector<Expr> kids;
01749
01750 for (int j = 0; j <= i; ++j) {
01751 Expr eq = shift.eqExpr(d_theoryBitvector->newBVConstExpr(j, bvLength));
01752 Expr ext = d_theoryBitvector->newBoolExtractExpr(term, i-j);
01753 kids.push_back(eq && ext);
01754 }
01755
01756 Expr output;
01757 if (kids.size() == 1) {
01758 output = kids[0];
01759 }
01760 else {
01761 output = Expr(OR, kids);
01762 }
01763
01764 Proof pf;
01765 if(withProof())
01766 pf = newPf("bit_extract_bvshl", x, rat(i));
01767 return newRWTheorem(bitExtract, output, Assumptions::emptyAssump(), pf);
01768 }
01769
01770
01771
01772
01773
01774 Theorem BitvectorTheoremProducer::bitExtractBVLSHR(const Expr & x, int i)
01775 {
01776 Type type = x.getType();
01777 int bvLength= d_theoryBitvector->BVSize(x);
01778 if(CHECK_PROOFS) {
01779
01780 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01781 "BitvectorTheoremProducer::bitExtractBVSHL:"
01782 "term must be bitvector.");
01783 CHECK_SOUND(x.getOpKind() == BVLSHR && 2 == x.arity(),
01784 "BitvectorTheoremProducer::bitExtractBVSHL:"
01785 "the bitvector must be a BVSHL." +
01786 x.toString());
01787
01788 CHECK_SOUND(0 <= i && i < bvLength,
01789 "BitvectorTheoremProducer::bitExtractBVSHL:"
01790 "illegal boolean extraction was attempted at position i = "
01791 + int2string(i)
01792 + "\non bitvector x = " + x.toString()
01793 + "\nwhose bvLength is = " +
01794 int2string(bvLength));
01795 }
01796
01797 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01798
01799 const Expr& term = x[0];
01800 const Expr& shift = x[1];
01801
01802 vector<Expr> kids;
01803
01804 for (int j = 0; j <= bvLength-1-i; ++j) {
01805 Expr eq = shift.eqExpr(d_theoryBitvector->newBVConstExpr(j, bvLength));
01806 Expr ext = d_theoryBitvector->newBoolExtractExpr(term, i+j);
01807 kids.push_back(eq && ext);
01808 }
01809
01810 Expr output;
01811 if (kids.size() == 1) {
01812 output = kids[0];
01813 }
01814 else {
01815 output = Expr(OR, kids);
01816 }
01817
01818 Proof pf;
01819 if(withProof())
01820 pf = newPf("bit_extract_bvlshr", x, rat(i));
01821 return newRWTheorem(bitExtract, output, Assumptions::emptyAssump(), pf);
01822 }
01823
01824
01825
01826
01827
01828 Theorem BitvectorTheoremProducer::bitExtractBVASHR(const Expr & x, int i)
01829 {
01830 Type type = x.getType();
01831 int bvLength= d_theoryBitvector->BVSize(x);
01832 if(CHECK_PROOFS) {
01833
01834 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
01835 "BitvectorTheoremProducer::bitExtractBVSHL:"
01836 "term must be bitvector.");
01837 CHECK_SOUND(x.getOpKind() == BVASHR && 2 == x.arity(),
01838 "BitvectorTheoremProducer::bitExtractBVSHL:"
01839 "the bitvector must be a BVSHL." +
01840 x.toString());
01841
01842 CHECK_SOUND(0 <= i && i < bvLength,
01843 "BitvectorTheoremProducer::bitExtractBVSHL:"
01844 "illegal boolean extraction was attempted at position i = "
01845 + int2string(i)
01846 + "\non bitvector x = " + x.toString()
01847 + "\nwhose bvLength is = " +
01848 int2string(bvLength));
01849 }
01850
01851 const Expr bitExtract = d_theoryBitvector->newBoolExtractExpr(x, i);
01852
01853 const Expr& term = x[0];
01854 const Expr& shift = x[1];
01855
01856 vector<Expr> kids;
01857 int j = 0;
01858 for (; j < bvLength-1-i; ++j) {
01859 Expr eq = shift.eqExpr(d_theoryBitvector->newBVConstExpr(j, bvLength));
01860 Expr ext = d_theoryBitvector->newBoolExtractExpr(term, i+j);
01861 kids.push_back(eq && ext);
01862 }
01863 Expr tmp = d_theoryBitvector->newBVConstExpr(j, bvLength);
01864 tmp = d_theoryBitvector->newBVLEExpr(tmp, shift);
01865 Expr ext = d_theoryBitvector->newBoolExtractExpr(term, bvLength-1);
01866 kids.push_back(tmp && ext);
01867
01868 Expr output;
01869 if (kids.size() == 1) {
01870 output = kids[0];
01871 }
01872 else {
01873 output = Expr(OR, kids);
01874 }
01875
01876 Proof pf;
01877 if(withProof())
01878 pf = newPf("bit_extract_bvashr", x, rat(i));
01879 return newRWTheorem(bitExtract, output, Assumptions::emptyAssump(), pf);
01880 }
01881
01882
01883
01884 static bool constantKids(const Expr& e) {
01885 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
01886 if(i->getOpKind() != BVCONST) return false;
01887 return true;
01888 }
01889
01890
01891
01892 Theorem BitvectorTheoremProducer::eqConst(const Expr& e) {
01893 if(CHECK_PROOFS) {
01894
01895 CHECK_SOUND(e.isEq(),
01896 "BitvectorTheoremProducer::eqConst: e = "+e.toString());
01897 CHECK_SOUND(constantKids(e),
01898 "BitvectorTheoremProducer::eqConst: e = "+e.toString());
01899 }
01900 Proof pf;
01901 if(withProof())
01902 pf = newPf("bitvector_eq_const", e);
01903 Expr res((e[0]==e[1])? d_theoryBitvector->trueExpr() :
01904 d_theoryBitvector->falseExpr());
01905 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01906 }
01907
01908
01909
01910 Theorem BitvectorTheoremProducer::eqToBits(const Theorem& eq) {
01911 if(CHECK_PROOFS) {
01912 CHECK_SOUND(eq.isRewrite(),
01913 "BitvectorTheoremProducer::eqToBits: eq = "+eq.toString());
01914 }
01915
01916 const Expr& lhs = eq.getLHS();
01917 const Expr& rhs = eq.getRHS();
01918
01919 if(CHECK_PROOFS) {
01920 CHECK_SOUND(d_theoryBitvector->getBaseType(lhs).getExpr().getOpKind() == BITVECTOR,
01921 "BitvectorTheoremProducer::eqToBits: eq = "+eq.toString());
01922 CHECK_SOUND(d_theoryBitvector->BVSize(lhs)
01923 == d_theoryBitvector->BVSize(rhs),
01924 "BitvectorTheoremProducer::eqToBits: eq = "+eq.toString());
01925 }
01926
01927 int i=0, size=d_theoryBitvector->BVSize(lhs);
01928 vector<Expr> bitEqs;
01929 for(; i<size; i++) {
01930 Expr l = d_theoryBitvector->newBVExtractExpr(lhs, i, i);
01931 Expr r = d_theoryBitvector->newBVExtractExpr(rhs, i, i);
01932 bitEqs.push_back(l.eqExpr(r));
01933 }
01934 Expr res = andExpr(bitEqs);
01935 Proof pf;
01936 if(withProof())
01937 pf = newPf("eq_to_bits", eq.getExpr(), eq.getProof());
01938 return newTheorem(res, eq.getAssumptionsRef(), pf);
01939 }
01940
01941
01942
01943 Theorem BitvectorTheoremProducer::leftShiftToConcat(const Expr& e) {
01944 if(CHECK_PROOFS) {
01945
01946 CHECK_SOUND(e.getOpKind() == LEFTSHIFT && e.arity() == 1,
01947 "BitvectorTheoremProducer::leftShiftConst: e = "+e.toString());
01948 CHECK_SOUND(d_theoryBitvector->getFixedLeftShiftParam(e) >= 0,
01949 "BitvectorTheoremProducer::leftShiftConst: e = "+e.toString());
01950 }
01951 const Expr& e0 = e[0];
01952 Expr res(e0);
01953 int shiftSize=d_theoryBitvector->getFixedLeftShiftParam(e);
01954
01955 if (shiftSize != 0) {
01956 Expr padding = d_theoryBitvector->newBVConstExpr(Rational(0), shiftSize);
01957 res = d_theoryBitvector->newConcatExpr(e0, padding);
01958 }
01959
01960 Proof pf;
01961 if(withProof())
01962 pf = newPf("leftshift_to_concat", e);
01963 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01964 }
01965
01966
01967 Theorem BitvectorTheoremProducer::constWidthLeftShiftToConcat(const Expr& e) {
01968 if(CHECK_PROOFS) {
01969
01970 CHECK_SOUND(e.getOpKind() == CONST_WIDTH_LEFTSHIFT && e.arity() == 1,
01971 "BitvectorTheoremProducer::leftShiftConst: e = "+e.toString());
01972 CHECK_SOUND(d_theoryBitvector->getFixedLeftShiftParam(e) >= 0,
01973 "BitvectorTheoremProducer::leftShiftConst: e = "+e.toString());
01974 }
01975 const Expr& e0 = e[0];
01976 Expr res;
01977
01978 int shiftSize=d_theoryBitvector->getFixedLeftShiftParam(e);
01979 if (shiftSize == 0)
01980 res = e0;
01981 else {
01982 int bvLength = d_theoryBitvector->BVSize(e);
01983 if (shiftSize >= bvLength)
01984 res = d_theoryBitvector->newBVConstExpr(Rational(0), bvLength);
01985 else {
01986 Expr padding = d_theoryBitvector->newBVConstExpr(Rational(0), shiftSize);
01987 res = d_theoryBitvector->newBVExtractExpr(e0, bvLength-shiftSize-1, 0);
01988 res = d_theoryBitvector->newConcatExpr(res, padding);
01989 }
01990 }
01991
01992 Proof pf;
01993 if(withProof())
01994 pf = newPf("constWidthLeftShift_to_concat", e);
01995 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
01996 }
01997
01998
01999
02000 Theorem BitvectorTheoremProducer::rightShiftToConcat(const Expr& e) {
02001 if(CHECK_PROOFS) {
02002 CHECK_SOUND(e.getOpKind() == RIGHTSHIFT && e.arity() == 1,
02003 "BitvectorTheoremProducer::rightShiftConst: e = "+e.toString());
02004 CHECK_SOUND(d_theoryBitvector->getFixedRightShiftParam(e) >= 0,
02005 "BitvectorTheoremProducer::rightShiftConst: e = "+e.toString());
02006 }
02007 int bvLength = d_theoryBitvector->BVSize(e[0]);
02008
02009 int shiftSize=d_theoryBitvector->getFixedRightShiftParam(e);
02010
02011 Expr output;
02012 if (shiftSize == 0) output = e[0];
02013 if (shiftSize >= bvLength)
02014 output = d_theoryBitvector->newBVZeroString(bvLength);
02015 else {
02016 Expr padding = d_theoryBitvector->newBVZeroString(shiftSize);
02017 Expr out0 = d_theoryBitvector->newBVExtractExpr(e[0],bvLength-1,shiftSize);
02018 output = d_theoryBitvector->newConcatExpr(padding,out0);
02019 }
02020
02021 DebugAssert(bvLength == d_theoryBitvector->BVSize(output),
02022 "BitvectorTheoremProducer::rightShiftConst: e = "+e.toString());
02023
02024 Proof pf;
02025 if(withProof())
02026 pf = newPf("rightshift_to_concat", e);
02027 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02028 }
02029
02030
02031
02032 Theorem BitvectorTheoremProducer::bvshlToConcat(const Expr& e) {
02033 if(CHECK_PROOFS) {
02034
02035 CHECK_SOUND(e.getOpKind() == BVSHL && e.arity() == 2,
02036 "BitvectorTheoremProducer::bvshlToConcat: e = "+e.toString());
02037 CHECK_SOUND(e[1].getOpKind() == BVCONST,
02038 "BitvectorTheoremProducer::bvshlToConcat: e = "+e.toString());
02039 }
02040 const Expr& e0 = e[0];
02041 Expr res;
02042
02043 Rational shiftSize=d_theoryBitvector->computeBVConst(e[1]);
02044 if (shiftSize == 0) res = e0;
02045 else {
02046 int bvLength = d_theoryBitvector->BVSize(e);
02047 if (shiftSize >= bvLength)
02048 res = d_theoryBitvector->newBVConstExpr(Rational(0), bvLength);
02049 else {
02050 Expr padding = d_theoryBitvector->newBVConstExpr(Rational(0), shiftSize.getInt());
02051 res = d_theoryBitvector->newBVExtractExpr(e0, bvLength-shiftSize.getInt()-1, 0);
02052 res = d_theoryBitvector->newConcatExpr(res, padding);
02053 }
02054 }
02055
02056 Proof pf;
02057 if(withProof())
02058 pf = newPf("bvshl_to_concat");
02059 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02060 }
02061
02062
02063
02064
02065
02066
02067 Theorem BitvectorTheoremProducer::bvshlSplit(const Expr &e)
02068 {
02069 Type type = e.getType();
02070 int bvLength= d_theoryBitvector->BVSize(e);
02071 if(CHECK_PROOFS) {
02072
02073 CHECK_SOUND(BITVECTOR == type.getExpr().getOpKind(),
02074 "BitvectorTheoremProducer::bitExtractBVSHL:"
02075 "term must be bitvector.");
02076 CHECK_SOUND(e.getOpKind() == BVSHL && 2 == e.arity(),
02077 "BitvectorTheoremProducer::bitExtractBVSHL:"
02078 "the bitvector must be a BVSHL." +
02079 e.toString());
02080 }
02081
02082 const Expr& term = e[0];
02083 const Expr& shift = e[1];
02084
02085 Expr newExpr = d_theoryBitvector->newBVZeroString(bvLength);
02086 Expr eq, tmp;
02087
02088 for (int i = bvLength-1; i > 0; --i) {
02089 eq = shift.eqExpr(d_theoryBitvector->newBVConstExpr(i, bvLength));
02090 tmp = d_theoryBitvector->newBVExtractExpr(term, bvLength-i-1, 0);
02091 tmp = d_theoryBitvector->newConcatExpr(tmp, d_theoryBitvector->newBVZeroString(i));
02092 newExpr = eq.iteExpr(tmp, newExpr);
02093 }
02094
02095 eq = shift.eqExpr(d_theoryBitvector->newBVZeroString(bvLength));
02096 newExpr = eq.iteExpr(term, newExpr);
02097
02098 Proof pf;
02099 if(withProof())
02100 pf = newPf("bvshl_split", e);
02101 return newRWTheorem(e, newExpr, Assumptions::emptyAssump(), pf);
02102 }
02103
02104
02105
02106 Theorem BitvectorTheoremProducer::bvlshrToConcat(const Expr& e)
02107 {
02108 if(CHECK_PROOFS) {
02109 CHECK_SOUND(e.getOpKind() == BVLSHR && e.arity() == 2,
02110 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.toString());
02111 CHECK_SOUND(e[1].getOpKind() == BVCONST,
02112 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.toString());
02113 }
02114 int bvLength = d_theoryBitvector->BVSize(e);
02115
02116 Rational shiftSize=d_theoryBitvector->computeBVConst(e[1]);
02117
02118 Expr output;
02119 if (shiftSize == 0) output = e[0];
02120 else if(shiftSize >= bvLength)
02121 output = d_theoryBitvector->newBVZeroString(bvLength);
02122 else {
02123 Expr padding = d_theoryBitvector->newBVZeroString(shiftSize.getInt());
02124 Expr out0 = d_theoryBitvector->newBVExtractExpr(e[0],bvLength-1,shiftSize.getInt());
02125 output = d_theoryBitvector->newConcatExpr(padding,out0);
02126 }
02127
02128 Proof pf;
02129 if(withProof())
02130 pf = newPf("bvlshr_to_concat", e);
02131 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02132 }
02133
02134 Theorem BitvectorTheoremProducer::bvShiftZero(const Expr& e)
02135 {
02136 if(CHECK_PROOFS) {
02137 int kind = e.getOpKind();
02138 CHECK_SOUND((kind == BVLSHR || kind == BVSHL || kind == BVASHR || kind == LEFTSHIFT || kind == CONST_WIDTH_LEFTSHIFT || kind == RIGHTSHIFT)
02139 && e.arity() == 2, "BitvectorTheoremProducer::bvShiftZero: e = "+e.toString());
02140 CHECK_SOUND(e[0].getOpKind() == BVCONST && d_theoryBitvector->computeBVConst(e[0]) == 0, "BitvectorTheoremProducer::bvShiftZero: e = "+e.toString());
02141 }
02142
02143 int bvLength = d_theoryBitvector->BVSize(e);
02144 Expr output = d_theoryBitvector->newBVZeroString(bvLength);
02145
02146 Proof pf;
02147 if(withProof())
02148 pf = newPf("shift_zero", e);
02149
02150 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02151 }
02152
02153
02154 Theorem BitvectorTheoremProducer::bvashrToConcat(const Expr& e)
02155 {
02156 if(CHECK_PROOFS) {
02157 CHECK_SOUND(e.getOpKind() == BVASHR && e.arity() == 2,
02158 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.toString());
02159 CHECK_SOUND(e[1].getOpKind() == BVCONST,
02160 "BitvectorTheoremProducer::bvlshrToConcat: e = "+e.toString());
02161 }
02162 int bvLength = d_theoryBitvector->BVSize(e);
02163
02164 Rational shiftSize=d_theoryBitvector->computeBVConst(e[1]);
02165
02166 Expr output;
02167 if (shiftSize > 0) {
02168 if (shiftSize >= bvLength) shiftSize = bvLength - 1;
02169 Expr out0 = d_theoryBitvector->newBVExtractExpr(e[0],bvLength-1,shiftSize.getInt());
02170 output = d_theoryBitvector->newSXExpr(out0, bvLength);
02171 } else output = e[0];
02172
02173 Proof pf;
02174 if(withProof())
02175 pf = newPf("bvashr_to_concat", e);
02176 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02177 }
02178
02179
02180 Theorem BitvectorTheoremProducer::rewriteXNOR(const Expr& e)
02181 {
02182 if (CHECK_PROOFS) {
02183 CHECK_SOUND(e.getKind() == BVXNOR && e.arity() == 2,
02184 "Bad call to rewriteXNOR");
02185 }
02186 Expr res = d_theoryBitvector->newBVNegExpr(e[0]);
02187 res = d_theoryBitvector->newBVXorExpr(res, e[1]);
02188 Proof pf;
02189 if (withProof())
02190 pf = newPf("rewriteXNOR", e);
02191 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02192 }
02193
02194
02195 Theorem BitvectorTheoremProducer::rewriteNAND(const Expr& e)
02196 {
02197 if (CHECK_PROOFS) {
02198 CHECK_SOUND(e.getKind() == BVNAND && e.arity() == 2,
02199 "Bad call to rewriteNAND");
02200 }
02201 Expr andExpr = d_theoryBitvector->newBVAndExpr(e[0], e[1]);
02202 Proof pf;
02203 if (withProof())
02204 pf = newPf("rewriteNAND", e);
02205 return newRWTheorem(e, d_theoryBitvector->newBVNegExpr(andExpr),
02206 Assumptions::emptyAssump(), pf);
02207 }
02208
02209
02210 Theorem BitvectorTheoremProducer::rewriteNOR(const Expr& e)
02211 {
02212 if (CHECK_PROOFS) {
02213 CHECK_SOUND(e.getKind() == BVNOR && e.arity() == 2,
02214 "Bad call to rewriteNOR");
02215 }
02216 Expr orExpr = d_theoryBitvector->newBVOrExpr(e[0], e[1]);
02217 Proof pf;
02218 if (withProof())
02219 pf = newPf("rewriteNOR", e);
02220 return newRWTheorem(e, d_theoryBitvector->newBVNegExpr(orExpr),
02221 Assumptions::emptyAssump(), pf);
02222 }
02223
02224
02225 Theorem BitvectorTheoremProducer::rewriteBVCOMP(const Expr& e)
02226 {
02227 if (CHECK_PROOFS) {
02228 CHECK_SOUND(e.getKind() == BVCOMP && e.arity() == 2,
02229 "Bad call to rewriteBVCOMP");
02230 }
02231 Expr res = e[0].eqExpr(e[1]).iteExpr(d_theoryBitvector->newBVOneString(1),
02232 d_theoryBitvector->newBVZeroString(1));
02233 Proof pf;
02234 if (withProof())
02235 pf = newPf("rewriteBVCOMP");
02236 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02237 }
02238
02239
02240 Theorem BitvectorTheoremProducer::rewriteBVSub(const Expr& e)
02241 {
02242 if (CHECK_PROOFS) {
02243 CHECK_SOUND(e.getKind() == BVSUB && e.arity() == 2 &&
02244 d_theoryBitvector->BVSize(e[0]) ==
02245 d_theoryBitvector->BVSize(e[1]),
02246 "Bad call to rewriteBVSub");
02247 }
02248 int bvsize = d_theoryBitvector->BVSize(e[0]);
02249 vector<Expr> k;
02250 k.push_back(e[0]);
02251 k.push_back(d_theoryBitvector->newBVUminusExpr(e[1]));
02252 Expr new_expr = d_theoryBitvector->newBVPlusExpr(bvsize, k);
02253
02254 ExprMap<Rational> sumHashMap;
02255 Rational known_term;
02256 getPlusTerms(new_expr, known_term, sumHashMap);
02257 new_expr = buildPlusTerm(bvsize, known_term, sumHashMap);
02258
02259
02260 Proof pf;
02261 if (withProof())
02262 pf = newPf("rewriteBVSub", e);
02263 return newRWTheorem(e, new_expr, Assumptions::emptyAssump(), pf);
02264 }
02265
02266
02267
02268
02269 Theorem BitvectorTheoremProducer::constMultToPlus(const Expr& e) {
02270 DebugAssert(false,
02271 "BitvectorTheoremProducer::constMultToPlus: this rule does not work\n");
02272 if(CHECK_PROOFS) {
02273 CHECK_SOUND(e.getOpKind() == BVMULT && e.arity() == 2
02274 && e[0].isRational() && e[0].getRational().isInteger(),
02275 "BitvectorTheoremProducer::constMultToPlus:\n e = "
02276 +e.toString());
02277 }
02278
02279 Rational k = e[0].getRational();
02280 const Expr& t = e[1];
02281 int resLength = d_theoryBitvector->BVSize(e);
02282 string coeffBinary = abs(k).toString(2);
02283 int len = coeffBinary.length();
02284 Expr res;
02285 if(k == 0) {
02286
02287 vector<bool> bits;
02288 int len = resLength;
02289 for(int i=0; i<len; ++i) bits.push_back(false);
02290 res = d_theoryBitvector->newBVConstExpr(bits);
02291 } else {
02292
02293 vector<Expr> kids;
02294 for(int i=0; i<len; ++i) {
02295 if(coeffBinary[i] == '1')
02296 kids.push_back(d_theoryBitvector->newFixedLeftShiftExpr(t, (len-1)-i));
02297 }
02298 res = (kids.size() == 1)? kids[0]
02299 : d_theoryBitvector->newBVPlusExpr(resLength, kids);
02300
02301 if(k < 0) {
02302 vector<Expr> kk;
02303 kk.push_back(d_theoryBitvector->newBVNegExpr(res));
02304 kk.push_back(rat(1));
02305 res = d_theoryBitvector->newBVPlusExpr(resLength, kk);
02306 }
02307 }
02308
02309 Proof pf;
02310 if(withProof())
02311 pf = newPf("const_mult_to_plus", e);
02312 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02313 }
02314
02315
02316 Theorem
02317 BitvectorTheoremProducer::bvplusZeroConcatRule(const Expr& e) {
02318 if(CHECK_PROOFS) {
02319 CHECK_SOUND(e.getOpKind()==CONCAT && e.arity()==2,
02320 "BitvectorTheoremProducer::bvplusZeroConcatRule: e = "
02321 +e.toString());
02322 CHECK_SOUND(e[0].getKind()==BVCONST && e[1].getOpKind()==BVPLUS
02323 && d_theoryBitvector->computeBVConst(e[0])==0,
02324 "BitvectorTheoremProducer::bvplusZeroConcatRule: e = "
02325 +e.toString());
02326 }
02327
02328 int constSize = d_theoryBitvector->BVSize(e[0]);
02329 const Expr& bvplus = e[1];
02330 int bvplusSize = d_theoryBitvector->getBVPlusParam(bvplus);
02331
02332
02333 int maxKidSize(0);
02334 for(Expr::iterator i=bvplus.begin(), iend=bvplus.end(); i!=iend; ++i) {
02335 int size(d_theoryBitvector->BVSize(*i));
02336
02337 if(i->getOpKind()==CONCAT && i->arity()>=2
02338 && (*i)[0].getKind()==BVCONST && d_theoryBitvector->computeBVConst((*i)[0])==0)
02339 size -= d_theoryBitvector->BVSize((*i)[0]);
02340 if(size > maxKidSize) maxKidSize = size;
02341 }
02342 int numKids = bvplus.arity();
02343
02344 int log2 = 0;
02345 for(int i=1; i < numKids; i *=2, log2++);
02346 if(log2+maxKidSize > bvplusSize) {
02347
02348 TRACE("bv 0@+", "bvplusZeroConcatRule(", e, "): skipped");
02349 return d_theoryBitvector->reflexivityRule(e);
02350 }
02351
02352 Expr res(d_theoryBitvector->newBVPlusExpr(bvplusSize+constSize,
02353 bvplus.getKids()));
02354
02355 Proof pf;
02356 if(withProof())
02357 pf = newPf("bvplus_zero_concat", e);
02358 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02359 }
02360
02361
02362
02363
02364 Theorem BitvectorTheoremProducer::extractConst(const Expr& e) {
02365 if(CHECK_PROOFS) {
02366
02367 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity() == 1,
02368 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
02369 CHECK_SOUND(constantKids(e),
02370 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
02371 }
02372
02373 int hi = d_theoryBitvector->getExtractHi(e);
02374 int low = d_theoryBitvector->getExtractLow(e);
02375 const Expr& e0 = e[0];
02376
02377 if(CHECK_PROOFS) {
02378 CHECK_SOUND(0 <= low && low <= hi,
02379 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
02380 CHECK_SOUND((unsigned)hi < d_theoryBitvector->getBVConstSize(e0),
02381 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
02382 }
02383 vector<bool> res;
02384
02385 for(int bit=low; bit <= hi; bit++)
02386 res.push_back(d_theoryBitvector->getBVConstValue(e0, bit));
02387
02388 Proof pf;
02389 if(withProof())
02390 pf = newPf("extract_const", e);
02391 return newRWTheorem(e, d_theoryBitvector->newBVConstExpr(res), Assumptions::emptyAssump(), pf);
02392 }
02393
02394
02395 Theorem
02396 BitvectorTheoremProducer::extractWhole(const Expr& e) {
02397 if(CHECK_PROOFS) {
02398 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity() == 1,
02399 "BitvectorTheoremProducer::extractWhole: e = "+e.toString());
02400 }
02401
02402 int hi = d_theoryBitvector->getExtractHi(e);
02403 int low = d_theoryBitvector->getExtractLow(e);
02404 const Expr& e0 = e[0];
02405
02406 if(CHECK_PROOFS) {
02407 CHECK_SOUND(low ==0 && hi == d_theoryBitvector->BVSize(e0) - 1,
02408 "BitvectorTheoremProducer::extractWhole: e = "+e.toString()
02409 +"\n BVSize(e) = "+ int2string(d_theoryBitvector->BVSize(e0)));
02410 }
02411 Proof pf;
02412 if(withProof())
02413 pf = newPf("extract_whole", e);
02414 return newRWTheorem(e, e0, Assumptions::emptyAssump(), pf);
02415 }
02416
02417
02418
02419 Theorem
02420 BitvectorTheoremProducer::extractExtract(const Expr& e) {
02421 if(CHECK_PROOFS) {
02422 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity() == 1,
02423 "BitvectorTheoremProducer::extractExtract: e = "+e.toString());
02424 }
02425
02426 int hi = d_theoryBitvector->getExtractHi(e);
02427 int low = d_theoryBitvector->getExtractLow(e);
02428 const Expr& e0 = e[0];
02429
02430 if(CHECK_PROOFS) {
02431
02432 CHECK_SOUND(0 <= low && low <= hi,
02433 "BitvectorTheoremProducer::extractExtract: e = "+e.toString());
02434
02435 CHECK_SOUND(e0.getOpKind() == EXTRACT && e0.arity() == 1,
02436 "BitvectorTheoremProducer::extractExtract: e0 = "
02437 +e0.toString());
02438 }
02439
02440 int hi0 = d_theoryBitvector->getExtractHi(e0);
02441 int low0 = d_theoryBitvector->getExtractLow(e0);
02442 const Expr& e00 = e0[0];
02443
02444 if(CHECK_PROOFS) {
02445
02446 CHECK_SOUND((0 <= low) && (low <= hi) && (hi <= hi0-low0),
02447 "BitvectorTheoremProducer::extractExtract:\n"
02448 " [hi:low][hi0:low0] = ["+ int2string(hi0)+":"+ int2string(low0)
02449 +"]["+ int2string(hi) + ":" + int2string(low)
02450 +"]\n e = "+e.toString());
02451 }
02452
02453 Expr res = d_theoryBitvector->newBVExtractExpr(e00, hi+low0, low+low0);
02454
02455 Proof pf;
02456 if(withProof())
02457 pf = newPf("extract_extract", e);
02458 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02459 }
02460
02461
02462
02463 Theorem
02464 BitvectorTheoremProducer::extractConcat(const Expr& e) {
02465 TRACE("bitvector rules", "extractConcat(", e, ") {");
02466 if(CHECK_PROOFS) {
02467 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity() == 1,
02468 "BitvectorTheoremProducer::extractConcat: e = "+e.toString());
02469 }
02470
02471 int hi = d_theoryBitvector->getExtractHi(e);
02472 int low = d_theoryBitvector->getExtractLow(e);
02473 const Expr& e0 = e[0];
02474
02475 if(CHECK_PROOFS) {
02476
02477 CHECK_SOUND(0 <= low && low <= hi,
02478 "BitvectorTheoremProducer::extractConcat: e = "+e.toString());
02479 CHECK_SOUND(hi < d_theoryBitvector->BVSize(e0),
02480 "BitvectorTheoremProducer::extractConcat: e = "+e.toString()
02481 +"\n BVSize(e0) = "+ int2string(d_theoryBitvector->BVSize(e0)));
02482
02483 CHECK_SOUND(e0.getOpKind() == CONCAT,
02484 "BitvectorTheoremProducer::extractConcat: e0 = "
02485 +e0.toString());
02486 }
02487
02488 vector<Expr> kids;
02489 int width(d_theoryBitvector->BVSize(e0));
02490 TRACE("bitvector rules", "extractConcat: width=", width, "");
02491 for(Expr::iterator i=e0.begin(), iend=e0.end(); i!=iend && width>low; ++i) {
02492 TRACE("bitvector rules", "extractConcat: *i=", *i, "");
02493 int w(d_theoryBitvector->BVSize(*i));
02494 int newWidth = width-w;
02495 int l(0), h(0);
02496 TRACE("bitvector rules", "extractConcat: w=", w, "");
02497 TRACE("bitvector rules", "extractConcat: newWidth=", newWidth, "");
02498 if(width > hi) {
02499 if(hi >= newWidth) {
02500 h = hi-newWidth;
02501 l = (newWidth <= low)? low-newWidth : 0;
02502 TRACE("bitvector rules", "extractConcat[newWidth<=hi<width]: h=",
02503 h, ", l="+ int2string(l));
02504 kids.push_back(d_theoryBitvector->newBVExtractExpr(*i, h, l));
02505 }
02506 } else if(width > low) {
02507
02508 h = w-1;
02509 l = (newWidth <= low)? low-newWidth : 0;
02510 TRACE("bitvector rules", "extractConcat[low<width<=hi]: h=",
02511 h, ", l="+ int2string(l));
02512 kids.push_back(d_theoryBitvector->newBVExtractExpr(*i, h, l));
02513 }
02514 width=newWidth;
02515 TRACE("bitvector rules", "extractConcat: width=", width, "");
02516 }
02517 Expr res = (kids.size()==1)? kids[0]
02518 : d_theoryBitvector->newConcatExpr(kids);
02519 Proof pf;
02520 if(withProof())
02521 pf = newPf("extract_concat", e);
02522 Theorem thm(newRWTheorem(e, res, Assumptions::emptyAssump(), pf));
02523 TRACE("bitvector rules", "extractConcat => ", thm.getExpr(), " }");
02524 return thm;
02525 }
02526
02527
02528
02529
02530 Theorem
02531 BitvectorTheoremProducer::extractBitwise(const Expr& e, int kind,
02532 const string& pfName) {
02533 if(CHECK_PROOFS) {
02534 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity() == 1,
02535 "BitvectorTheoremProducer::"+pfName+": e = "+e.toString());
02536 CHECK_SOUND(kind == BVAND || kind == BVOR ||
02537 kind == BVNEG || kind == BVXOR ||
02538 kind == BVXNOR,
02539 "BitvectorTheoremProducer::"+pfName+": kind = "
02540 +d_theoryBitvector->getEM()->getKindName(kind));
02541 }
02542
02543 int hi = d_theoryBitvector->getExtractHi(e);
02544 int low = d_theoryBitvector->getExtractLow(e);
02545 const Expr& e0 = e[0];
02546
02547 if(CHECK_PROOFS) {
02548
02549 CHECK_SOUND(0 <= low && low <= hi,
02550 "BitvectorTheoremProducer::"+pfName+": e = "+e.toString());
02551
02552 CHECK_SOUND(e0.getOpKind() == kind,
02553 "BitvectorTheoremProducer::"+pfName+": e0 = "
02554 +e0.toString());
02555 }
02556
02557 vector<Expr> kids;
02558 for(Expr::iterator i=e0.begin(), iend=e0.end(); i!=iend; ++i) {
02559 kids.push_back(d_theoryBitvector->newBVExtractExpr(*i, hi, low));
02560 }
02561 Expr res = Expr(e0.getOp(), kids);
02562 Proof pf;
02563 if(withProof())
02564 pf = newPf(pfName, e);
02565 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02566 }
02567
02568
02569 Theorem
02570 BitvectorTheoremProducer::extractAnd(const Expr& e) {
02571 return extractBitwise(e, BVAND, "extract_and");
02572 }
02573
02574
02575
02576 Theorem
02577 BitvectorTheoremProducer::extractOr(const Expr& e) {
02578 return extractBitwise(e, BVOR, "extract_or");
02579 }
02580
02581
02582
02583 Theorem
02584 BitvectorTheoremProducer::extractNeg(const Expr& e) {
02585 return extractBitwise(e, BVNEG, "extract_neg");
02586 }
02587
02588
02589 Theorem
02590 BitvectorTheoremProducer::iteExtractRule(const Expr& e) {
02591 if(CHECK_PROOFS) {
02592 CHECK_SOUND(e.getOpKind() == EXTRACT && e.arity()==1,
02593 "BitvectorTheoremProducer::iteExtractRule: "
02594 "input must be an bitvector EXTRACT expr:\n"+
02595 e.toString());
02596 }
02597 int hi = d_theoryBitvector->getExtractHi(e);
02598 int low = d_theoryBitvector->getExtractLow(e);
02599
02600 if(CHECK_PROOFS) {
02601 CHECK_SOUND(e[0].getKind() == ITE &&
02602 e[0].arity()==3 &&
02603 BITVECTOR == e[0].getType().getExpr().getOpKind(),
02604 "BitvectorTheoremProducer::iteExtractRule: "
02605 "input must be an bitvector EXTRACT expr over an ITE:\n" +
02606 e.toString());
02607 CHECK_SOUND(hi >= low && d_theoryBitvector->BVSize(e[0]) >= hi-low,
02608 "BitvectorTheoremProducer::iteExtractRule: "
02609 "i should be greater than j in e[i:j] = "
02610 +e.toString());
02611 }
02612 const Expr ite = e[0];
02613 Expr cond = ite[0];
02614 Expr e1 = d_theoryBitvector->newBVExtractExpr(ite[1],hi,low);
02615 Expr e2 = d_theoryBitvector->newBVExtractExpr(ite[2],hi,low);
02616 Expr output = Expr(CVC3::ITE,cond,e1,e2);
02617
02618 Proof pf;
02619 if(withProof())
02620 pf = newPf("ite_extract_rule", e);
02621 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02622 }
02623
02624
02625 Theorem
02626 BitvectorTheoremProducer::iteBVnegRule(const Expr& e) {
02627 if(CHECK_PROOFS) {
02628 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity()==1,
02629 "BitvectorTheoremProducer::itebvnegrule: "
02630 "input must be an bitvector EXTRACT expr:\n"+
02631 e.toString());
02632 }
02633 if(CHECK_PROOFS) {
02634 CHECK_SOUND(e[0].getKind() == ITE &&
02635 e[0].arity()==3 &&
02636 BITVECTOR == e[0].getType().getExpr().getOpKind(),
02637 "BitvectorTheoremProducer::itebvnegrule: "
02638 "input must be an bitvector EXTRACT expr over an ITE:\n" +
02639 e.toString());
02640 }
02641 const Expr ite = e[0];
02642 Expr cond = ite[0];
02643 Expr e1 = d_theoryBitvector->newBVNegExpr(ite[1]);
02644 Expr e2 = d_theoryBitvector->newBVNegExpr(ite[2]);
02645 Expr output = Expr(CVC3::ITE,cond,e1,e2);
02646
02647 Proof pf;
02648 if(withProof())
02649 pf = newPf("ite_bvneg_rule", e);
02650 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02651 }
02652
02653
02654 Theorem BitvectorTheoremProducer::negConst(const Expr& e) {
02655 if(CHECK_PROOFS) {
02656
02657 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02658 "BitvectorTheoremProducer::negConst: e = "+e.toString());
02659 CHECK_SOUND(constantKids(e),
02660 "BitvectorTheoremProducer::negConst: e = "+e.toString());
02661 }
02662 const Expr& e0 = e[0];
02663 vector<bool> res;
02664
02665 for(int bit=0, size=d_theoryBitvector->getBVConstSize(e0); bit<size; bit++)
02666 res.push_back(!d_theoryBitvector->getBVConstValue(e0, bit));
02667
02668 Proof pf;
02669 if(withProof())
02670 pf = newPf("bitneg_const", e);
02671 return newRWTheorem(e, d_theoryBitvector->newBVConstExpr(res), Assumptions::emptyAssump(), pf);
02672 }
02673
02674
02675
02676 Theorem
02677 BitvectorTheoremProducer::negConcat(const Expr& e) {
02678 if(CHECK_PROOFS) {
02679
02680 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02681 "BitvectorTheoremProducer::negConcat: e = "+e.toString());
02682 CHECK_SOUND(e[0].getOpKind() == CONCAT,
02683 "BitvectorTheoremProducer::negConcat: e = "+e.toString());
02684 }
02685
02686 const Expr& e0 = e[0];
02687
02688 vector<Expr> kids;
02689 for(Expr::iterator i=e0.begin(), iend=e0.end(); i!=iend; ++i)
02690 kids.push_back(d_theoryBitvector->newBVNegExpr(*i));
02691
02692 Expr res = d_theoryBitvector->newConcatExpr(kids);
02693
02694 Proof pf;
02695 if(withProof())
02696 pf = newPf("bitneg_concat", e);
02697 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02698 }
02699
02700
02701 Theorem
02702 BitvectorTheoremProducer::negNeg(const Expr& e) {
02703 if(CHECK_PROOFS) {
02704 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02705 "BitvectorTheoremProducer::negNeg: e = "+e.toString());
02706 CHECK_SOUND(e[0].getOpKind() == BVNEG && e[0].arity() == 1,
02707 "BitvectorTheoremProducer::negNeg: e = "+e.toString());
02708 }
02709
02710 Proof pf;
02711 if(withProof())
02712 pf = newPf("bitneg_neg", e);
02713 return newRWTheorem(e, e[0][0], Assumptions::emptyAssump(), pf);
02714 }
02715
02716
02717
02718 Theorem BitvectorTheoremProducer::negElim(const Expr& e)
02719 {
02720 if(CHECK_PROOFS) {
02721 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02722 "BitvectorTheoremProducer::negNeg: e = "+e.toString());
02723 }
02724
02725 int bv_size = d_theoryBitvector->BVSize(e[0]);
02726 Rational modulus = pow(Rational(bv_size), Rational(2));
02727 Expr minus_one = d_theoryBitvector->newBVConstExpr(modulus-1, bv_size);
02728
02729 vector<Expr> bvplusTerms;
02730 bvplusTerms.push_back(minus_one);
02731 bvplusTerms.push_back(d_theoryBitvector->newBVMultExpr(bv_size, minus_one, e[0]));
02732 Expr res = d_theoryBitvector->newBVPlusExpr(bv_size, bvplusTerms);
02733
02734 Proof pf;
02735 if(withProof())
02736 pf = newPf("bitneg_elim", e);
02737 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02738 }
02739
02740
02741
02742 Theorem
02743 BitvectorTheoremProducer::negBVand(const Expr& e) {
02744 if(CHECK_PROOFS) {
02745 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02746 "BitvectorTheoremProducer::negBVand: e = "+e.toString());
02747 CHECK_SOUND(e[0].getOpKind() == BVAND,
02748 "BitvectorTheoremProducer::negBVand: e = "+e.toString());
02749 }
02750 Expr output;
02751 std::vector<Expr> negated;
02752 for(Expr::iterator i = e[0].begin(),iend=e[0].end();i!=iend;++i)
02753 negated.push_back(d_theoryBitvector->newBVNegExpr(*i));
02754 output = d_theoryBitvector->newBVOrExpr(negated);
02755
02756 Proof pf;
02757 if(withProof())
02758 pf = newPf("bitneg_and", e);
02759 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02760 }
02761
02762
02763
02764 Theorem
02765 BitvectorTheoremProducer::negBVor(const Expr& e) {
02766 if(CHECK_PROOFS) {
02767 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1,
02768 "BitvectorTheoremProducer::negBVor: e = "+e.toString());
02769 CHECK_SOUND(e[0].getOpKind() == BVOR,
02770 "BitvectorTheoremProducer::negBVor: e = "+e.toString());
02771 }
02772
02773 Expr output;
02774 std::vector<Expr> negated;
02775 for(Expr::iterator i = e[0].begin(),iend=e[0].end();i!=iend;++i)
02776 negated.push_back(d_theoryBitvector->newBVNegExpr(*i));
02777 output = d_theoryBitvector->newBVAndExpr(negated);
02778
02779 Proof pf;
02780 if(withProof())
02781 pf = newPf("bitneg_or", e);
02782 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02783 }
02784
02785
02786
02787 Theorem
02788 BitvectorTheoremProducer::negBVxor(const Expr& e) {
02789 if(CHECK_PROOFS) {
02790 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1 && e[0].arity() > 0,
02791 "BitvectorTheoremProducer::negBVxor: e = "+e.toString());
02792 CHECK_SOUND(e[0].getOpKind() == BVXOR,
02793 "BitvectorTheoremProducer::negBVxor: e = "+e.toString());
02794 }
02795
02796 Expr output;
02797 std::vector<Expr> children;
02798 Expr::iterator i = e[0].begin(), iend = e[0].end();
02799 children.push_back(d_theoryBitvector->newBVNegExpr(*i));
02800 ++i;
02801 for(; i!=iend; ++i)
02802 children.push_back(*i);
02803 output = d_theoryBitvector->newBVXorExpr(children);
02804
02805 Proof pf;
02806 if(withProof())
02807 pf = newPf("bitneg_xor", e);
02808 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02809 }
02810
02811
02812
02813 Theorem
02814 BitvectorTheoremProducer::negBVxnor(const Expr& e) {
02815 if(CHECK_PROOFS) {
02816 CHECK_SOUND(e.getOpKind() == BVNEG && e.arity() == 1 && e[0].arity() > 0,
02817 "BitvectorTheoremProducer::negBVxor: e = "+e.toString());
02818 CHECK_SOUND(e[0].getOpKind() == BVXNOR,
02819 "BitvectorTheoremProducer::negBVxor: e = "+e.toString());
02820 }
02821
02822 Expr t2 = e[0][1];
02823 if (e[0].arity() > 2) {
02824 std::vector<Expr> children;
02825 Expr::iterator i = e[0].begin(), iend = e[0].end();
02826 ++i;
02827 for(; i!=iend; ++i)
02828 children.push_back(*i);
02829 t2 = d_theoryBitvector->newBVXnorExpr(children);
02830 }
02831 Expr output = d_theoryBitvector->newBVXorExpr(e[0][0], t2);
02832
02833 Proof pf;
02834 if(withProof())
02835 pf = newPf("bitneg_xnor", e);
02836 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
02837 }
02838
02839
02840
02841 Theorem BitvectorTheoremProducer::bitwiseConst(const Expr& e,
02842 const vector<int>& idxs,
02843 int kind)
02844 {
02845 if(CHECK_PROOFS) {
02846
02847 CHECK_SOUND(e.getOpKind() == kind,
02848 "BitvectorTheoremProducer::bitwiseConst: e = "+e.toString());
02849 CHECK_SOUND(e.getOpKind() == BVAND ||
02850 e.getOpKind() == BVOR ||
02851 e.getOpKind() == BVXOR, "Expected AND, OR, or XOR");
02852 CHECK_SOUND(idxs.size() >= 2, "BitvectorTheoremProducer::bitwiseConst():\n e = "
02853 +e.toString());
02854 for(size_t i=0; i<idxs.size(); ++i) {
02855 CHECK_SOUND(idxs[i] < e.arity(),
02856 "BitvectorTheoremProducer::bitwiseConst: idxs["
02857 +int2string(i)+"]="+int2string(idxs[i])
02858 +", e.arity() = "+int2string(e.arity())
02859 +"\n e = "+e.toString());
02860 CHECK_SOUND(e[idxs[i]].getKind() == BVCONST,
02861 "BitvectorTheoremProducer::bitwiseConst: e = "+e.toString());
02862 }
02863 }
02864
02865 vector<bool> bits;
02866 int size = d_theoryBitvector->BVSize(e);
02867 for(int bit=0; bit<size; bit++) {
02868 bits.push_back(kind == BVAND);
02869 }
02870
02871 vector<Expr> kids(1);
02872 size_t ii(0);
02873 int idx(idxs[0]);
02874 for(int i=0, iend=e.arity(); i<iend; ++i) {
02875 const Expr& ei = e[i];
02876 if(i == idx) {
02877 if(CHECK_PROOFS) {
02878 CHECK_SOUND(ei.getKind() == BVCONST,
02879 "BitvectorTheoremProducer::bitwiseConst: e["
02880 +int2string(i)+"] = "+ei.toString());
02881 CHECK_SOUND(d_theoryBitvector->getBVConstSize(ei) == (unsigned)size,
02882 "BitvectorTheoremProducer::bitwiseConst: e["
02883 +int2string(i)+"] = "+ei.toString());
02884 }
02885
02886 for(int bit=0; bit<size; bit++)
02887 bits[bit] =
02888 kind == BVAND ? (bits[bit] && d_theoryBitvector->getBVConstValue(ei, bit)) :
02889 kind == BVOR ? (bits[bit] || d_theoryBitvector->getBVConstValue(ei, bit)) :
02890 bits[bit] != d_theoryBitvector->getBVConstValue(ei, bit);
02891
02892 if (ii < idxs.size() - 1)
02893 idx = idxs[++ii];
02894 else
02895 idx = e.arity();
02896 }
02897 else
02898 kids.push_back(ei);
02899 }
02900
02901 kids[0] = d_theoryBitvector->newBVConstExpr(bits);
02902
02903 Expr res = (kids.size() == 1) ? kids[0] :
02904 kind == BVAND ? d_theoryBitvector->newBVAndExpr(kids) :
02905 kind == BVOR ? d_theoryBitvector->newBVOrExpr(kids) :
02906 d_theoryBitvector->newBVXorExpr(kids);
02907
02908 Proof pf;
02909 if(withProof()) {
02910
02911 vector<Expr> indices;
02912 for(size_t i=0, iend=idxs.size(); i<iend; ++i)
02913 indices.push_back(rat(idxs[i]));
02914 pf = newPf("bitwise_const", e, Expr(RAW_LIST, indices));
02915 }
02916 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02917 }
02918
02919
02920
02921 Theorem BitvectorTheoremProducer::bitwiseConcat(const Expr& e, int kind)
02922 {
02923 if(CHECK_PROOFS) {
02924 CHECK_SOUND(e.getOpKind() == kind,
02925 "BitvectorTheoremProducer::bitwiseConcat: e = "+e.toString());
02926 }
02927
02928 int arity = e.arity();
02929 int idx;
02930 for (idx = 0; idx < arity; ++idx) {
02931 if (e[idx].getOpKind() == CONCAT) break;
02932 }
02933 if (idx == arity)
02934 return d_theoryBitvector->reflexivityRule(e);
02935
02936 const Expr& ei = e[idx];
02937
02938
02939 vector<Expr> concatKids;
02940
02941 int hi=d_theoryBitvector->BVSize(e)-1;
02942 int low=hi-d_theoryBitvector->BVSize(ei[0])+1;
02943
02944 for(int i=0, iend=ei.arity(); i<iend; ++i) {
02945
02946 vector<Expr> kids;
02947 for(int j=0; j<arity; ++j) {
02948 if(j==idx)
02949 kids.push_back(ei[i]);
02950 else
02951 kids.push_back(d_theoryBitvector->newBVExtractExpr(e[j], hi, low));
02952 }
02953 concatKids.push_back(Expr(kind, kids));
02954 if(i+1<iend) {
02955 int newHi = low-1;
02956 low = low - d_theoryBitvector->BVSize(ei[i+1]);
02957 hi = newHi;
02958 }
02959 }
02960 Expr res = d_theoryBitvector->newConcatExpr(concatKids);
02961 Proof pf;
02962 if(withProof())
02963 pf = newPf("bitwise_concat", e, rat(idx));
02964 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
02965 }
02966
02967
02968
02969 Theorem BitvectorTheoremProducer::bitwiseFlatten(const Expr& e, int kind)
02970 {
02971 if(CHECK_PROOFS) {
02972 CHECK_SOUND(e.getOpKind() == kind && e.arity()>=2,
02973 "BitvectorTheoremProducer::bitwiseFlatten: e = "+e.toString());
02974 CHECK_SOUND(e.getOpKind() == BVAND ||
02975 e.getOpKind() == BVOR ||
02976 e.getOpKind() == BVXOR, "Expected AND, OR, or XOR");
02977 }
02978 int bvLength = d_theoryBitvector->BVSize(e);
02979
02980
02981 vector<Expr> flattenkids;
02982 for(Expr::iterator i = e.begin(),iend=e.end();i!=iend; ++i) {
02983 if(i->getOpKind() == kind)
02984 flattenkids.insert(flattenkids.end(),
02985 i->getKids().begin(),i->getKids().end());
02986 else
02987 flattenkids.push_back(*i);
02988 }
02989
02990
02991 Expr output;
02992 int flag;
02993 ExprMap<int> likeTerms;
02994 vector<Expr>::iterator j = flattenkids.begin();
02995 vector<Expr>::iterator jend = flattenkids.end();
02996 bool negate = false;
02997
02998 for(; output.isNull() && j != flattenkids.end(); ++j) {
02999 Expr t = *j;
03000 if (kind == BVXOR && t.getOpKind() == BVNEG) {
03001 negate = !negate;
03002 t = t[0];
03003 }
03004
03005 flag = sameKidCheck(t, likeTerms);
03006 switch(flag) {
03007 case 0:
03008
03009 break;
03010 case 1:
03011
03012 if (kind == BVXOR) {
03013
03014 likeTerms.erase(t);
03015 }
03016 break;
03017 case -1:
03018
03019 if (kind == BVAND)
03020 output = d_theoryBitvector->newBVZeroString(bvLength);
03021 else if (kind == BVOR)
03022 output = d_theoryBitvector->newBVOneString(bvLength);
03023 else {
03024 DebugAssert(false, "Shouldn't be possible");
03025 }
03026 break;
03027 default:
03028 DebugAssert(false,
03029 "control should not reach here");
03030 break;
03031 }
03032 }
03033
03034 if (output.isNull()) {
03035 vector<Expr> outputkids;
03036 ExprMap<int>::iterator it = likeTerms.begin();
03037 for(; it != likeTerms.end(); ++it) {
03038 outputkids.push_back((*it).first);
03039 }
03040 if(CHECK_PROOFS) {
03041 CHECK_SOUND(kind == BVXOR || outputkids.size() > 0,
03042 "TheoryBitvector:bitwiseFlatten: fatal error");
03043 }
03044 if (outputkids.size() == 0) {
03045 outputkids.push_back(d_theoryBitvector->newBVZeroString(bvLength));
03046 }
03047 if (negate) {
03048 outputkids[0] = d_theoryBitvector->newBVNegExpr(outputkids[0]);
03049 }
03050 if (outputkids.size() == 1) {
03051 output = outputkids[0];
03052 }
03053 else {
03054 output = Expr(kind, outputkids);
03055 }
03056 }
03057
03058 Proof pf;
03059 if(withProof())
03060 pf = newPf("bitwise_flatten", e);
03061 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
03062 }
03063
03064
03065
03066
03067 Theorem BitvectorTheoremProducer::bitwiseConstElim(const Expr& e,
03068 int idx, int kind)
03069 {
03070 if(CHECK_PROOFS) {
03071 CHECK_SOUND(e.getOpKind() == kind,
03072 "BitvectorTheoremProducer::bitwiseConstElim: e = "+e.toString());
03073 CHECK_SOUND(e.getOpKind() == BVAND ||
03074 e.getOpKind() == BVOR ||
03075 e.getOpKind() == BVXOR, "Expected AND, OR, or XOR");
03076 CHECK_SOUND(idx < e.arity() && e.arity() > 1,
03077 "BitvectorTheoremProducer::bitwiseConstElim: e = "+e.toString()
03078 +"\n idx = "+int2string(idx)
03079 +"\n e.arity() = "+int2string(e.arity()));
03080 CHECK_SOUND(e[idx].getOpKind() == BVCONST,
03081 "BitvectorTheoremProducer::bitwiseConstElim: e["+int2string(idx)
03082 +"] = "+e[idx].toString());
03083 }
03084
03085 int bvLength = d_theoryBitvector->BVSize(e);
03086 Expr output;
03087 vector<Expr> kids;
03088 for (int i = 0; i < e.arity(); ++i) {
03089 if (i == idx) continue;
03090 kids.push_back(e[i]);
03091 }
03092 if (kids.size() == 1) output = kids[0];
03093 else output = Expr(kind, kids);
03094
03095 const Expr& c = e[idx];
03096 int i=d_theoryBitvector->getBVConstSize(c)-1;
03097 bool curVal = d_theoryBitvector->getBVConstValue(c, i);
03098 int hi = bvLength-1;
03099 Expr term;
03100 vector<Expr> concatTerms;
03101
03102 for(--i; i >= 0; --i) {
03103 if (d_theoryBitvector->getBVConstValue(c,i) != curVal) {
03104 if (kind == BVAND && curVal == false) {
03105 term = d_theoryBitvector->newBVZeroString(hi-i);
03106 }
03107 else if (kind == BVOR && curVal == true) {
03108 term = d_theoryBitvector->newBVOneString(hi-i);
03109 }
03110 else {
03111 term = d_theoryBitvector->newBVExtractExpr(output, hi, i+1);
03112 if (kind == BVXOR && curVal == true) {
03113 term = d_theoryBitvector->newBVNegExpr(term);
03114 }
03115 }
03116 concatTerms.push_back(term);
03117 curVal = !curVal;
03118 hi = i;
03119 }
03120 }
03121
03122 if (kind == BVAND && curVal == false) {
03123 term = d_theoryBitvector->newBVZeroString(hi+1);
03124 }
03125 else if (kind == BVOR && curVal == true) {
03126 term = d_theoryBitvector->newBVOneString(hi+1);
03127 }
03128 else {
03129 if (hi < bvLength-1) {
03130 term = d_theoryBitvector->newBVExtractExpr(output, hi, 0);
03131 }
03132 else term = output;
03133 if (kind == BVXOR && curVal == true) {
03134 term = d_theoryBitvector->newBVNegExpr(term);
03135 }
03136 }
03137 concatTerms.push_back(term);
03138 if (concatTerms.size() == 1) {
03139 output = concatTerms[0];
03140 }
03141 else {
03142 output = d_theoryBitvector->newConcatExpr(concatTerms);
03143 }
03144
03145 Proof pf;
03146 if(withProof())
03147 pf = newPf("bitwise_zero", e, rat(idx));
03148 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
03149 }
03150
03151
03152
03153
03154
03155
03156
03157
03158
03159 int BitvectorTheoremProducer::sameKidCheck(const Expr& e,
03160 ExprMap<int>& likeTerms) {
03161
03162 int flag = 0;
03163
03164
03165 ExprMap<int>::iterator it = likeTerms.find(e);
03166
03167
03168 if(it==likeTerms.end()) {
03169 switch(e.getOpKind()) {
03170 case BVNEG: {
03171 ExprMap<int>::iterator it0 = likeTerms.find(e[0]);
03172 if(it0!=likeTerms.end())
03173 flag = -1;
03174 break;
03175 }
03176 default: {
03177 Expr bvNeg = d_theoryBitvector->newBVNegExpr(e);
03178 ExprMap<int>::iterator negIt = likeTerms.find(bvNeg);
03179 if(negIt!=likeTerms.end())
03180 flag=-1;
03181 break;
03182 }
03183 }
03184 if (flag == 0) likeTerms[e] = 1;
03185 return flag;
03186 }
03187
03188
03189 return 1;
03190 }
03191
03192
03193
03194 Theorem BitvectorTheoremProducer::concatConst(const Expr& e) {
03195 if(CHECK_PROOFS) {
03196
03197 CHECK_SOUND(e.getOpKind() == CONCAT,
03198 "BitvectorTheoremProducer::concatConst: e = "+e.toString());
03199 CHECK_SOUND(constantKids(e),
03200 "BitvectorTheoremProducer::concatConst: e = "+e.toString());
03201 }
03202 vector<bool> res;
03203 for(int i=e.arity()-1; i >= 0; --i) {
03204 for(int bit=0, size=d_theoryBitvector->getBVConstSize(e[i]); bit < size; bit++)
03205 res.push_back(d_theoryBitvector->getBVConstValue(e[i], bit));
03206 }
03207 Proof pf;
03208 if(withProof())
03209 pf = newPf("concat_const", e);
03210 return newRWTheorem(e, d_theoryBitvector->newBVConstExpr(res), Assumptions::emptyAssump(), pf);
03211 }
03212
03213
03214
03215 Theorem
03216 BitvectorTheoremProducer::concatFlatten(const Expr& e) {
03217 if(CHECK_PROOFS) {
03218 CHECK_SOUND(e.getOpKind() == CONCAT && e.arity() >= 2,
03219 "BitvectorTheoremProducer::concatFlatten: e = "+e.toString());
03220 }
03221
03222 vector<Expr> kids;
03223 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
03224 if(i->getOpKind() == CONCAT)
03225 kids.insert(kids.end(), i->getKids().begin(), i->getKids().end());
03226 else
03227 kids.push_back(*i);
03228 }
03229 Proof pf;
03230 if(withProof())
03231 pf = newPf("concat_flatten", e);
03232 return newRWTheorem(e, Expr(e.getOp(), kids), Assumptions::emptyAssump(), pf);
03233 }
03234
03235
03236
03237 Theorem
03238 BitvectorTheoremProducer::concatMergeExtract(const Expr& e) {
03239 if(CHECK_PROOFS) {
03240 CHECK_SOUND(e.getOpKind() == CONCAT && e.arity() >= 2,
03241 "BitvectorTheoremProducer::concatMergeExtract: e = "
03242 +e.toString());
03243 CHECK_SOUND(e[0].getOpKind() == EXTRACT,
03244 "BitvectorTheoremProducer::concatMergeExtract: e = "
03245 +e.toString());
03246 CHECK_SOUND(d_theoryBitvector->getExtractHi(e[0]) >= d_theoryBitvector->getExtractLow(e[0]),
03247 "BitvectorTheoremProducer::concatMergeExtract: e = "
03248 +e.toString());
03249 }
03250
03251 const Expr& base = e[0][0];
03252
03253 if(CHECK_PROOFS) {
03254
03255 int low = d_theoryBitvector->getExtractLow(e[0]);
03256 for(int i=1, iend=e.arity(); i<iend; ++i) {
03257 const Expr& ei = e[i];
03258 CHECK_SOUND(ei.getOpKind() == EXTRACT && ei[0] == base,
03259 "BitvectorTheoremProducer::concatMergeExtract: e["
03260 +int2string(i)+"] = "+ei.toString()
03261 +"\n base = "+base.toString());
03262 CHECK_SOUND(d_theoryBitvector->getExtractHi(ei) >= d_theoryBitvector->getExtractLow(ei),
03263 "BitvectorTheoremProducer::concatMergeExtract: e["
03264 +int2string(i)+"] = "+e.toString());
03265
03266 int newHi = d_theoryBitvector->getExtractHi(ei);
03267
03268 CHECK_SOUND(0 <= newHi && newHi == low-1,
03269 "BitvectorTheoremProducer::concatMergeExtract:\n e["
03270 +int2string(i-1)+"] = "+e[i-1].toString()
03271 +"\n e["+int2string(i)+"] = "+ei.toString());
03272 low = d_theoryBitvector->getExtractLow(ei);
03273 }
03274 }
03275
03276 int hi = d_theoryBitvector->getExtractHi(e[0]);
03277 int low = d_theoryBitvector->getExtractLow(e[e.arity()-1]);
03278 Expr res = d_theoryBitvector->newBVExtractExpr(base, hi, low);
03279
03280 Proof pf;
03281 if(withProof())
03282 pf = newPf("concat_merge_extract", e);
03283 return newRWTheorem(e, res, Assumptions::emptyAssump(), pf);
03284 }
03285
03286
03287
03288
03289 Theorem BitvectorTheoremProducer::bvplusConst(const Expr& e) {
03290 if(CHECK_PROOFS) {
03291
03292 CHECK_SOUND(e.getOpKind() == BVPLUS,
03293 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
03294 CHECK_SOUND(constantKids(e),
03295 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
03296 CHECK_SOUND(d_theoryBitvector->getBVPlusParam(e) > 0,
03297 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
03298 }
03299
03300
03301 Rational acc(0);
03302 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
03303 Rational x = d_theoryBitvector->computeBVConst(*i);
03304 TRACE("bitvector rewrite", "bvplusConst: x(", *i, ") = "+x.toString());
03305 acc += x;
03306 TRACE("bitvector rewrite", "bvplusConst: acc = ", acc, "");
03307 }
03308
03309 int resSize = d_theoryBitvector->getBVPlusParam(e);
03310 vector<bool> res(resSize);
03311 for(int i=0; i<resSize; i++) {
03312 res[i] = (mod(acc, 2) == 1);
03313 TRACE("bitvector rewrite", "bvplusConst: acc = ", acc, "");
03314 TRACE("bitvector rewrite", "bvplusConst: res["+int2string(i)+"] = ",
03315 res[i], "");
03316 acc = floor(acc/2);
03317 }
03318
03319 Proof pf;
03320 if(withProof())
03321 pf = newPf("bvplus_const", e);
03322 return newRWTheorem(e, d_theoryBitvector->newBVConstExpr(res), Assumptions::emptyAssump(), pf);
03323 }
03324
03325
03326
03327
03328 Theorem BitvectorTheoremProducer::bvmultConst(const Expr& e) {
03329 if(CHECK_PROOFS) {
03330
03331 CHECK_SOUND(e.getOpKind() == BVMULT,
03332 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
03333 CHECK_SOUND(constantKids(e),
03334 "BitvectorTheoremProducer::extractConst: e = "+e.toString());
03335 }
03336 Rational c = d_theoryBitvector->computeBVConst(e[0]);
03337
03338 Rational x = d_theoryBitvector->computeBVConst(e[1]) * c;
03339
03340
03341 int resSize = d_theoryBitvector->BVSize(e.getType().getExpr());
03342 vector<bool> res(resSize);
03343 for(int i=0; i<resSize; i++) {
03344 res[i] = (mod(x, 2) == 1);
03345 x = floor(x/2);
03346 }
03347
03348 Proof pf;
03349 if(withProof())
03350 pf = newPf("bvmult_const", e);
03351 return newRWTheorem(e, d_theoryBitvector->newBVConstExpr(res), Assumptions::emptyAssump(), pf);
03352 }
03353
03354 Theorem
03355 BitvectorTheoremProducer::zeroCoeffBVMult(const Expr& e) {
03356 if(CHECK_PROOFS) {
03357 CHECK_SOUND(e.getOpKind() == BVMULT && e.arity() == 2,
03358 "BitvectorTheoremProducer::zeroCoeffBVMult: e = "+e.toString());
03359 CHECK_SOUND(BVCONST == e[0].getKind(),
03360 "BitvectorTheoremProducer::zeroCoeffBVMult: e = "+e.toString());
03361 Rational c = d_theoryBitvector->computeBVConst(e[0]);
03362 CHECK_SOUND(0 == c,
03363 "BitvectorTheoremProducer::zeroCoeffBVMult:"
03364 "coeff must be zero:\n e = " +e.toString());
03365 }
03366 int size = d_theoryBitvector->BVSize(e);
03367 Expr output = d_theoryBitvector->newBVZeroString(size);
03368
03369 Proof pf;
03370 if(withProof())
03371 pf = newPf("zerocoeff_bvmult", e);
03372 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03373 return result;
03374 }
03375
03376 Theorem
03377 BitvectorTheoremProducer::oneCoeffBVMult(const Expr& e) {
03378 if(CHECK_PROOFS) {
03379 CHECK_SOUND(e.getOpKind() == BVMULT && e.arity() == 2,
03380 "BitvectorTheoremProducer::oneCoeffBVMult: e = "
03381 +e.toString());
03382 CHECK_SOUND(BVCONST == e[0].getKind(),
03383 "BitvectorTheoremProducer::oneCoeffBVMult: e = "
03384 +e.toString());
03385 Rational c = d_theoryBitvector->computeBVConst(e[0]);
03386 CHECK_SOUND(1 == c,
03387 "BitvectorTheoremProducer::oneCoeffBVMult:"
03388 "coeff must be one:\n e = " +e.toString());
03389 }
03390 int size = d_theoryBitvector->BVSize(e);
03391 Expr output = pad(size,e);
03392
03393 Proof pf;
03394 if(withProof())
03395 pf = newPf("onecoeff_bvmult", e);
03396 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03397 return result;
03398 }
03399
03400
03401 Theorem
03402 BitvectorTheoremProducer::flipBVMult(const Expr& e) {
03403 if(CHECK_PROOFS) {
03404 CHECK_SOUND(e.arity()==2 && BVMULT == e.getOpKind(),
03405 "BVMULT must have exactly 2 kids: " + e.toString());
03406 }
03407 int len = d_theoryBitvector->BVSize(e);
03408 Expr output = d_theoryBitvector->newBVMultExpr(len,e[1],e[0]);
03409
03410 Proof pf;
03411 if(withProof())
03412 pf = newPf("flip_bvmult", e);
03413 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03414 return result;
03415 }
03416
03417
03418
03419
03420
03421
03422 Expr
03423 BitvectorTheoremProducer::pad(int len, const Expr& e) {
03424 DebugAssert(len > 0,
03425 "TheoryBitvector::pad:"
03426 "padding bvLength must be a non-negative integer: "+
03427 int2string(len));
03428 DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
03429 "TheoryBitvector::newBVPlusExpr:"
03430 "input must be a BITVECTOR: " + e.toString());
03431
03432 int size = d_theoryBitvector->BVSize(e);
03433 Expr res;
03434 if(size == len)
03435 res = e;
03436 else if (len < size)
03437 res = d_theoryBitvector->newBVExtractExpr(e,len-1,0);
03438 else {
03439
03440 Expr zero = d_theoryBitvector->newBVZeroString(len-size);
03441 res = d_theoryBitvector->newConcatExpr(zero,e);
03442 }
03443 return res;
03444 }
03445
03446
03447 Theorem
03448 BitvectorTheoremProducer::padBVPlus(const Expr& e) {
03449 if(CHECK_PROOFS) {
03450 CHECK_SOUND(BVPLUS == e.getOpKind() && e.arity()>1,
03451 "BitvectorTheoremProducer::padBVPlus: "
03452 "input must be a BVPLUS: " + e.toString());
03453 }
03454 int len = d_theoryBitvector->BVSize(e);
03455 vector<Expr> kids;
03456 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
03457 if(i->getOpKind() == BVMULT) {
03458 Expr e0 = pad(len, (*i)[0]);
03459 Expr e1 = pad(len, (*i)[1]);
03460 Expr out = d_theoryBitvector->newBVMultExpr(len,e0,e1);
03461 kids.push_back(out);
03462 }
03463 else
03464 kids.push_back(pad(len, *i));
03465 }
03466
03467 Expr output = d_theoryBitvector->newBVPlusExpr(len, kids);
03468
03469 Proof pf;
03470 if(withProof())
03471 pf = newPf("pad_bvplus", e);
03472 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03473 return result;
03474 }
03475
03476
03477 Theorem
03478 BitvectorTheoremProducer::padBVMult(const Expr& e) {
03479 if(CHECK_PROOFS) {
03480 CHECK_SOUND(BVMULT == e.getOpKind() && e.arity()==2,
03481 "BitvectorTheoremProducer::padBVMult: "
03482 "input must be a BVMULT: " + e.toString());
03483 CHECK_SOUND(BITVECTOR==e[0].getType().getExpr().getOpKind() &&
03484 BITVECTOR==e[1].getType().getExpr().getOpKind(),
03485 "for BVMULT terms e[0],e[1] must be a BV: " + e.toString());
03486 }
03487 int len = d_theoryBitvector->BVSize(e);
03488 Expr e0 = pad(len, e[0]);
03489 Expr e1 = pad(len, e[1]);
03490
03491 Expr output = d_theoryBitvector->newBVMultExpr(len,e0,e1);
03492
03493 Proof pf;
03494 if(withProof())
03495 pf = newPf("pad_bvmult", e);
03496 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03497 return result;
03498 }
03499
03500
03501 Theorem
03502 BitvectorTheoremProducer::bvConstMultAssocRule(const Expr& e) {
03503 if(CHECK_PROOFS) {
03504 CHECK_SOUND(BVMULT == e.getOpKind() && e.arity() == 2,
03505 "BitvectorTheoremProducer::bvConstMultAssocRule: "
03506 "input must be a BVMULT: " + e.toString());
03507 CHECK_SOUND(BVMULT == e[1].getOpKind(),
03508 "BitvectorTheoremProducer::bvConstMultAssocRule: "
03509 "e[1] must be a BVMULT:\n e= " + e.toString());
03510 CHECK_SOUND(BVCONST == e[0].getKind() &&
03511 BVCONST == e[1][0].getKind(),
03512 "BitvectorTheoremProducer::bvConstMultAssocRule: "
03513 "e[0] & e[1][0] must be a BVCONST:\n e = " + e.toString());
03514 }
03515 int len = d_theoryBitvector->BVSize(e);
03516 int len0 = d_theoryBitvector->BVSize(e[0]);
03517 int len10 = d_theoryBitvector->BVSize(e[1][0]);
03518 int len11 = d_theoryBitvector->BVSize(e[1][1]);
03519 if(CHECK_PROOFS) {
03520 CHECK_SOUND(len == len0 && len0 == len10 && len0 == len11,
03521 "BitvectorTheoremProducer::bvConstMultAssocRule: "
03522 "kids of BVMULT must be equibvLength: ");
03523 }
03524 Rational e0 = d_theoryBitvector->computeBVConst(e[0]);
03525 Rational e10 = d_theoryBitvector->computeBVConst(e[1][0]);
03526 Expr c = d_theoryBitvector->newBVConstExpr(e0*e10, len);
03527 Expr output = d_theoryBitvector->newBVMultExpr(len, c, e[1][1]);
03528
03529 Proof pf;
03530 if(withProof())
03531 pf = newPf("bvconstmult_assoc_rule", e);
03532 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03533 return result;
03534 }
03535
03536
03537
03538
03539 Theorem
03540 BitvectorTheoremProducer::bvMultAssocRule(const Expr& e) {
03541 if(CHECK_PROOFS) {
03542 CHECK_SOUND(BVMULT == e.getOpKind() && e.arity() == 2,
03543 "BitvectorTheoremProducer::bvMultAssocRule: "
03544 "input must be a BVMULT: " + e.toString());
03545 CHECK_SOUND(BVMULT == e[0].getOpKind() ||
03546 BVMULT == e[1].getOpKind(),
03547 "BitvectorTheoremProducer::bvMultAssocRule: "
03548 "e[0] or e[1] must be a BVMULT:\n e= " + e.toString());
03549 CHECK_SOUND(!(BVCONST == e[0].getOpKind() &&
03550 BVCONST == e[1][0].getOpKind()),
03551 "BitvectorTheoremProducer::bvMultAssocRule: "
03552 "e[0] & e[1][0] cannot be a BVCONST:\n e = " +
03553 e.toString());
03554 }
03555 int len = d_theoryBitvector->BVSize(e);
03556 int len0 = d_theoryBitvector->BVSize(e[0]);
03557 int len1 = d_theoryBitvector->BVSize(e[1]);
03558 if(CHECK_PROOFS)
03559 CHECK_SOUND(len == len0 && len0 == len1,
03560 "BitvectorTheoremProducer::bvMultAssocRule: "
03561 "kids of BVMULT must be equibvLength: ");
03562 Expr e0, e1;
03563 e0 = e[0];
03564 e1 = e[1];
03565
03566 std::vector<Expr> outputkids;
03567 if(BVMULT == e[0].getOpKind() && BVMULT != e[1].getOpKind()) {
03568 outputkids.push_back(e0[0]);
03569 outputkids.push_back(e0[1]);
03570 outputkids.push_back(e1);
03571
03572 } else if(BVMULT != e[0].getOpKind() && BVMULT == e[1].getOpKind()) {
03573 outputkids.push_back(e1[0]);
03574 outputkids.push_back(e1[1]);
03575 outputkids.push_back(e0);
03576 } else {
03577
03578 outputkids.push_back(e0[0]);
03579 outputkids.push_back(e0[1]);
03580 outputkids.push_back(e1[0]);
03581 outputkids.push_back(e1[1]);
03582 }
03583 sort(outputkids.begin(),outputkids.end());
03584
03585 Expr output;
03586 switch(outputkids.size()) {
03587 case 3: {
03588 Expr out1 =
03589 d_theoryBitvector->newBVMultExpr(len, outputkids[1],outputkids[2]);
03590 output =
03591 d_theoryBitvector->newBVMultExpr(len, outputkids[0], out1);
03592 break;
03593 }
03594 case 4: {
03595 Expr out0 =
03596 d_theoryBitvector->newBVMultExpr(len, outputkids[0], outputkids[1]);
03597 Expr out1 =
03598 d_theoryBitvector->newBVMultExpr(len, outputkids[2], outputkids[3]);
03599 output =
03600 d_theoryBitvector->newBVMultExpr(len, out0, out1);
03601 break;
03602 }
03603 }
03604
03605 Proof pf;
03606 if(withProof())
03607 pf = newPf("bvmult_assoc_rule", e);
03608 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03609 return result;
03610 }
03611
03612
03613 Theorem
03614 BitvectorTheoremProducer::bvMultDistRule(const Expr& e) {
03615 if(CHECK_PROOFS) {
03616 CHECK_SOUND(BVMULT == e.getOpKind() && e.arity() == 2,
03617 "BitvectorTheoremProducer::bvMultDistRule: "
03618 "input must be a BVMULT: " + e.toString());
03619 CHECK_SOUND(BVPLUS == e[1].getOpKind(),
03620 "BitvectorTheoremProducer::bvMultDistRule: "
03621 "input must be of the form a*(t1+...+tn): " + e.toString());
03622 }
03623 int bvLength= d_theoryBitvector->BVSize(e);
03624 int e0len = d_theoryBitvector->BVSize(e[0]);
03625 int e1len = d_theoryBitvector->BVSize(e[1]);
03626 if(CHECK_PROOFS) {
03627 CHECK_SOUND(bvLength== e0len && e0len == e1len,
03628 "BitvectorTheoremProducer::bvMultDistRule: "
03629 "all subterms must of equal bvLength: " + e.toString());
03630 }
03631 const Expr& e0 = e[0];
03632 const Expr& e1 = e[1];
03633
03634 std::vector<Expr> v;
03635 Expr::iterator i = e1.begin();
03636 Expr::iterator iend = e1.end();
03637 for(;i != iend; ++i) {
03638 Expr s = d_theoryBitvector->newBVMultExpr(bvLength, e0, *i);
03639 v.push_back(s);
03640 }
03641 Expr output = d_theoryBitvector->newBVPlusExpr(bvLength,v);
03642
03643 Proof pf;
03644 if(withProof())
03645 pf = newPf("bvmult_distributivity_rule", e);
03646 Theorem result(newRWTheorem(e,output,Assumptions::emptyAssump(),pf));
03647 return result;
03648 }
03649
03650
03651
03652
03653 Theorem
03654 BitvectorTheoremProducer::flattenBVPlus(const Expr& e) {
03655 if(CHECK_PROOFS) {
03656 CHECK_SOUND(e.getOpKind() == BVPLUS && e.arity() >= 2,
03657 "BitvectorTheoremProducer::flattenBVPlus: e = "+e.toString());
03658 }
03659 int bvLength= d_theoryBitvector->BVSize(e);
03660 const int numOfKids = e.arity();
03661
03662 if(CHECK_PROOFS) {
03663 for(int i=0; i<numOfKids; ++i)
03664 CHECK_SOUND(d_theoryBitvector->BVSize(e[i]) == bvLength,
03665 "BitvectorTheoremProducer::flattenBVPlus: "
03666 "summands must be of the same bvLength as BVPLUS:\n e = "
03667 +e.toString());
03668 }
03669
03670
03671
03672 std::vector<Expr> v;
03673 for(int i = 0; i < numOfKids; ++i) {
03674 if(e[i].getOpKind() == BVPLUS) {
03675 const Expr& bvplusKid = e[i];
03676 const int bvplusArity = bvplusKid.arity();
03677 for(int j=0; j < bvplusArity; ++j)
03678 v.push_back(bvplusKid[j]);
03679 } else
03680 v.push_back(e[i]);
03681 }
03682 Expr eprime = d_theoryBitvector->newBVPlusExpr(bvLength, v);
03683
03684 Proof pf;
03685 if(withProof())
03686 pf = newPf("flatten_bvplus", e);
03687 return newRWTheorem(e, eprime, Assumptions::emptyAssump(), pf);
03688 }
03689
03690 void
03691 BitvectorTheoremProducer::collectOneTermOfPlus(const Rational & coefficient,
03692 const Expr& term,
03693 ExprMap<Rational> & likeTerms,
03694 Rational & plusConstant)
03695 {
03696 ExprMap<Rational>::iterator it = likeTerms.find(term);
03697
03698 if(it!=likeTerms.end())
03699 likeTerms[term] += coefficient;
03700 else {
03701
03702 bool foundNegated= false;
03703 if (!likeTerms.empty()) {
03704 Expr negTerm = d_theoryBitvector->newBVNegExpr(term);
03705 negTerm = d_theoryBitvector->pushNegationRec(term).getRHS();
03706 it = likeTerms.find(negTerm);
03707 if (it!= likeTerms.end()) {
03708 foundNegated = true;
03709
03710
03711 likeTerms[negTerm] += -coefficient;
03712 plusConstant+= -1;
03713 }
03714 }
03715 if (!foundNegated)
03716
03717 likeTerms[term] = coefficient;
03718 }
03719 }
03720
03721 void
03722 BitvectorTheoremProducer::collectLikeTermsOfPlus(const Expr& e,
03723 ExprMap<Rational> & likeTerms,
03724 Rational & plusConstant) {
03725 likeTerms.clear();
03726 Expr::iterator i = e.begin();
03727 Expr::iterator iend = e.end();
03728 plusConstant= 0;
03729
03730 for(; i!=iend; ++i) {
03731 const Expr s = *i;
03732 switch(s.getOpKind()) {
03733 case BVMULT: {
03734
03735 if (s[0].getKind() == BVCONST) {
03736 Rational coefficient= d_theoryBitvector->computeBVConst(s[0]);
03737 const Expr& var = s[1];
03738 collectOneTermOfPlus(coefficient, var, likeTerms, plusConstant);
03739 }
03740 else {
03741 if(CHECK_PROOFS) {
03742 CHECK_SOUND(BVCONST != s[1].getKind(),
03743 "TheoryBitvector::combineLikeTerms: "
03744 "Unexpected MULT syntax:\n\n s = " + s.toString()
03745 +"\n\n in e = "+e.toString());
03746 }
03747 collectOneTermOfPlus(1, s, likeTerms, plusConstant);
03748 }
03749 break;
03750 }
03751 case BVUMINUS:
03752 collectOneTermOfPlus(-1, s[0], likeTerms, plusConstant);
03753 break;
03754 case BVCONST:
03755 plusConstant += d_theoryBitvector->computeBVConst(s);
03756 break;
03757 default:
03758
03759 collectOneTermOfPlus(1, s, likeTerms, plusConstant);
03760 break;
03761 }
03762 }
03763 }
03764
03765 static Rational boundedModulo(const Rational & value, const Rational & modulo,
03766 const Rational & lowerBound) {
03767 Rational ret = mod(value, modulo);
03768 if(ret == 0)
03769 return ret;
03770
03771 if (ret< lowerBound)
03772 ret+= modulo;
03773 else {
03774
03775 Rational end= modulo+lowerBound;
03776 if (ret >= end)
03777 ret-= modulo;
03778 }
03779 return ret;
03780 }
03781
03782 void
03783 BitvectorTheoremProducer::
03784 createNewPlusCollection(const Expr & e,
03785 const ExprMap<Rational> & likeTerms,
03786 Rational & plusConstant,
03787 std::vector<Expr> & result) {
03788 int bvplusLength= d_theoryBitvector->BVSize(e);
03789
03790 Rational power2(1);
03791 for(int i=0; i<bvplusLength; i += 1) power2 *= 2;
03792
03793 ExprMap<Rational>::const_iterator j = likeTerms.begin();
03794 ExprMap<Rational>::const_iterator jend = likeTerms.end();
03795 for(; j!=jend; ++j) {
03796
03797
03798
03799 Rational coefficient = boundedModulo(j->second, power2, -power2/2+1);
03800 if(coefficient == 0)
03801 continue;
03802 Expr multiplicand = j->first;
03803 Expr monomial;
03804 if (coefficient<0) {
03805
03806
03807 multiplicand = d_theoryBitvector->newBVNegExpr(multiplicand);
03808 multiplicand = d_theoryBitvector->pushNegationRec(multiplicand).getRHS();
03809 coefficient= coefficient*-1;
03810 plusConstant +=coefficient;
03811 }
03812 if(coefficient == 1)
03813 monomial = multiplicand;
03814 else {
03815 Expr coeffExpr =
03816 d_theoryBitvector->newBVConstExpr(coefficient, bvplusLength);
03817 monomial =
03818 d_theoryBitvector->newBVMultExpr(bvplusLength, coeffExpr,multiplicand);
03819 }
03820 if(CHECK_PROOFS) {
03821 CHECK_SOUND(BITVECTOR==monomial.getType().getExpr().getOpKind(),
03822 "TheoryBitvector::combineLikeTerms:"
03823 "each monomial must be a bitvector:\n"
03824 "monomial = " + monomial.toString());
03825 CHECK_SOUND(bvplusLength == d_theoryBitvector->BVSize(monomial),
03826 "TheoryBitvector::combineLikeTerms:"
03827 "bvLength of each monomial must be the same as e:\n"
03828 "monomial = " + monomial.toString() + "\n e = " + e.toString());
03829 }
03830 result.push_back(monomial);
03831 }
03832
03833 plusConstant = boundedModulo(plusConstant, power2, 0);
03834
03835
03836 if(plusConstant != 0) {
03837 const Expr c =
03838 d_theoryBitvector->newBVConstExpr(plusConstant, bvplusLength);
03839 result.push_back(c);
03840 }
03841 }
03842
03843 Expr
03844 BitvectorTheoremProducer::sumNormalizedElements(int bvplusLength,
03845 const std::vector<Expr>&items){
03846
03847
03848 switch(items.size()) {
03849 case 0:
03850
03851 return d_theoryBitvector->newBVZeroString(bvplusLength);
03852
03853 case 1:
03854
03855 return items[0];
03856
03857 default:
03858
03859 return d_theoryBitvector->newBVPlusExpr(bvplusLength, items);
03860 }
03861 }
03862
03863 Theorem
03864 BitvectorTheoremProducer::combineLikeTermsRule(const Expr& e) {
03865 TRACE("bitvector rewrite", "combineLikeTermsRule(",e.toString(), ") {");
03866 if(CHECK_PROOFS) {
03867 CHECK_SOUND(BVPLUS == e.getOpKind() && e.arity()>=2,
03868 "TheoryBitvector::combineLikeTerms: "
03869 "input must be a BVPLUS term:\n e = " + e.toString());
03870 int bvplusLength = d_theoryBitvector->BVSize(e);
03871 Expr::iterator i = e.begin();
03872 Expr::iterator iend = e.end();
03873 for(;i!=iend;++i) {
03874 const Expr& s = *i;
03875 if(s.getOpKind() == BVPLUS) {
03876 CHECK_SOUND(s.getOpKind() != BVPLUS,
03877 "TheoryBitvector::combineLikeTerms: "
03878 "BVPLUS must be flattened:\n e = " + e.toString());
03879 }
03880
03881 int bvLength= d_theoryBitvector->BVSize(s);
03882
03883 CHECK_SOUND(bvLength==bvplusLength,
03884 "TheoryBitvector::combineLikeTerms: "
03885 "BVPLUS must be padded:\n e = " + e.toString());
03886
03887 if(s.getOpKind()==BVMULT) {
03888 int s0len = d_theoryBitvector->BVSize(s[0]);
03889 int s1len = d_theoryBitvector->BVSize(s[1]);
03890 CHECK_SOUND(bvplusLength == s0len && s0len== s1len,
03891 "all monoms must have the samebvLength "
03892 "as the bvplus term: " + e.toString());
03893 }
03894 }
03895 }
03896 int bvplusLength = d_theoryBitvector->BVSize(e);
03897 ExprMap<Rational> likeTerms;
03898 Rational theConstant(0);
03899 collectLikeTermsOfPlus(e, likeTerms, theConstant);
03900
03901 std::vector<Expr> collection;
03902 createNewPlusCollection(e, likeTerms, theConstant, collection);
03903
03904 Expr output= sumNormalizedElements(bvplusLength, collection);
03905
03906 TRACE("bitvector rewrite",
03907 "combineLikeTermsRule =>",output.toString(), "}");
03908 Proof pf;
03909 if(withProof())
03910 pf=newPf("bvplus_combine_like_terms", e);
03911 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
03912 }
03913
03914 Theorem
03915 BitvectorTheoremProducer::lhsMinusRhsRule(const Expr& e) {
03916 if(CHECK_PROOFS) {
03917 CHECK_SOUND(EQ == e.getKind() && e.arity() == 2,
03918 "BitvectorTheoremProducer::lhsMinusRhsRule: "
03919 "input must be an EQ: e = " +e.toString());
03920 CHECK_SOUND(BVPLUS == e[0].getOpKind() ||
03921 BVPLUS == e[1].getOpKind(),
03922 "BitvectorTheoremProducer::lhsMinusRhsRule: "
03923 "atleast one of the input subterms must be BVPLUS:"
03924 "e = " +e.toString());
03925 int bvLength0 = d_theoryBitvector->BVSize(e[0]);
03926 int bvLength1 = d_theoryBitvector->BVSize(e[1]);
03927 CHECK_SOUND(bvLength0 == bvLength1,
03928 "BitvectorTheoremProducer::lhsMinusRhsRule: "
03929 "both sides of EQ must be same Length. e = " +e.toString());
03930 for(Expr::iterator i=e[0].begin(),iend=e[0].end();i!=iend;++i) {
03931 int bvLength= d_theoryBitvector->BVSize(*i);
03932 CHECK_SOUND(bvLength0 == bvLength,
03933 "BitvectorTheoremProducer::lhsMinusRhsRule: "
03934 "all subterms of e[0] must be of same Length."
03935 "e = " +e.toString());
03936 }
03937 for(Expr::iterator i=e[1].begin(),iend=e[1].end();i!=iend;++i) {
03938 int bvLength= d_theoryBitvector->BVSize(*i);
03939 CHECK_SOUND(bvLength1 == bvLength,
03940 "BitvectorTheoremProducer::lhsMinusRhsRule: "
03941 "all subterms of e[1] must be of same Length."
03942 "e = " +e.toString());
03943 }
03944 }
03945 Expr output;
03946 int bvLength = d_theoryBitvector->BVSize(e[0]);
03947 std::vector<Expr> k;
03948
03949
03950 Expr zeroStr = d_theoryBitvector->newBVZeroString(bvLength);
03951
03952 if(e[0] == e[1])
03953 output = Expr(EQ, zeroStr, zeroStr);
03954 else {
03955
03956 std::vector<Expr> e0K = e[0].getKids();
03957 std::vector<Expr> e1K = e[1].getKids();
03958 for(vector<Expr>::iterator i=e0K.begin(),iend=e0K.end();i!=iend;++i){
03959 for(vector<Expr>::iterator j=e1K.begin(),jend=e1K.end();j!=jend;++j){
03960 if(*i == *j) {
03961 e0K.erase(i);
03962 e1K.erase(j);
03963 break;
03964 }
03965 }
03966 }
03967 Expr newLhs = d_theoryBitvector->newBVPlusExpr(bvLength, e0K);
03968 k.push_back(newLhs);
03969 Expr newRhs = d_theoryBitvector->newBVPlusExpr(bvLength, e1K);
03970
03971 Expr uminus = d_theoryBitvector->newBVUminusExpr(newRhs);
03972
03973 k.push_back(uminus);
03974
03975 Expr lhsMinusRhs = d_theoryBitvector->newBVPlusExpr(bvLength,k);
03976
03977 output = Expr(EQ, lhsMinusRhs, zeroStr);
03978 }
03979
03980 Proof pf;
03981 if(withProof())
03982 pf = newPf("lhs_minus_rhs_rule", e);
03983 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
03984 }
03985
03986
03987 Theorem
03988 BitvectorTheoremProducer::bvuminusToBVPlus(const Expr& e) {
03989 if(CHECK_PROOFS) {
03990 CHECK_SOUND(BVUMINUS == e.getOpKind(),
03991 "BitvectorTheoremProducer::bvuminusBitBlastRule: "
03992 "input must be bvuminus: e = " + e.toString());
03993 }
03994 int bvLength = d_theoryBitvector->BVSize(e);
03995 std::vector<Expr> k;
03996 Expr negE0 = d_theoryBitvector->newBVNegExpr(e[0]);
03997 k.push_back(negE0);
03998 Expr plusOne = d_theoryBitvector->newBVConstExpr(1, bvLength);
03999 k.push_back(plusOne);
04000
04001 Expr output = d_theoryBitvector->newBVPlusExpr(bvLength, k);
04002 Proof pf;
04003 if(withProof())
04004 pf = newPf("bvuminus_bitblast_rule", e);
04005 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04006 }
04007
04008
04009 Theorem
04010 BitvectorTheoremProducer::bvuminusBVConst(const Expr& e) {
04011 if(CHECK_PROOFS) {
04012 CHECK_SOUND(BVUMINUS == e.getOpKind() &&
04013 BVCONST == e[0].getKind(),
04014 "BitvectorTheoremProducer::bvuminusBVConst: "
04015 "e should be bvuminus, e[0] should be bvconst: e = " +
04016 e.toString());
04017 }
04018 Expr output;
04019 int e0Length = d_theoryBitvector->BVSize(e[0]);
04020
04021 if(d_theoryBitvector->computeBVConst(e[0]) == 0)
04022 output = e[0];
04023 else {
04024
04025 Rational x = d_theoryBitvector->computeNegBVConst(e[0]);
04026 output = d_theoryBitvector->newBVConstExpr(x, e0Length);
04027 }
04028
04029 Proof pf;
04030 if(withProof())
04031 pf = newPf("bvuminus_bvconst_rule", e);
04032 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04033 }
04034
04035
04036 Theorem
04037 BitvectorTheoremProducer::bvuminusBVMult(const Expr& e) {
04038 if(CHECK_PROOFS) {
04039 CHECK_SOUND(BVUMINUS == e.getOpKind(),
04040 "BitvectorTheoremProducer::bvuminusBVMult: "
04041 "e should be bvuminus: e =" + e.toString());
04042 CHECK_SOUND(BVMULT == e[0].getOpKind(),
04043 "Bitvectortheoremproducer::bvuminusBVMult: "
04044 "in input expression e = " + e.toString() +
04045 "\ne[0] should be bvmult: e[0] = " + e[0].toString());
04046 CHECK_SOUND(BVCONST == e[0][0].getKind(),
04047 "Bitvectortheoremproducer::bvuminusBVMult: "
04048 "in input expression e = " + e.toString() +
04049 "\ne[0][0] should be bvconst: e[0][0] = " + e[0][0].toString());
04050 int bvLength = d_theoryBitvector->BVSize(e);
04051 int e0Length = d_theoryBitvector->BVSize(e[0]);
04052 int e00Length = d_theoryBitvector->BVSize(e[0][0]);
04053 CHECK_SOUND(bvLength == e0Length && e0Length == e00Length,
04054 "Bitvectortheoremproducer::bvuminusBVMult: "
04055 "in input expression e = " + e.toString() +
04056 "\nLengths of all subexprs must be equal: e = " + e.toString());
04057 }
04058
04059 Expr output;
04060 int e0Length = d_theoryBitvector->BVSize(e[0]);
04061
04062 Rational coeff = d_theoryBitvector->computeNegBVConst(e[0][0]);
04063 if(0 == coeff)
04064
04065 output = d_theoryBitvector->newBVZeroString(e0Length);
04066 else if (1 == coeff)
04067
04068 output = e[0][1];
04069 else {
04070
04071 Expr newcoeff = d_theoryBitvector->newBVConstExpr(coeff, e0Length);
04072 output = d_theoryBitvector->newBVMultExpr(e0Length, newcoeff, e[0][1]);
04073 }
04074
04075 Proof pf;
04076 if(withProof())
04077 pf = newPf("bvuminus_bvmult_rule", e);
04078 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04079 }
04080
04081
04082 Theorem
04083 BitvectorTheoremProducer::bvuminusBVUminus(const Expr& e) {
04084 if(CHECK_PROOFS) {
04085 CHECK_SOUND(BVUMINUS == e.getOpKind(),
04086 "BitvectorTheoremProducer::bvuminusBVUminus: "
04087 "e should be bvuminus: e =" + e.toString());
04088 CHECK_SOUND(BVUMINUS == e[0].getOpKind(),
04089 "Bitvectortheoremproducer::bvuminusBVUminus: "
04090 "in input expression e = " + e.toString() +
04091 "\ne[0] should be bvmult: e[0] = " + e[0].toString());
04092 }
04093 Expr output;
04094
04095 output = e[0][0];
04096 Proof pf;
04097 if(withProof())
04098 pf = newPf("bvuminus_bvuminus_rule", e);
04099 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04100 }
04101
04102
04103 Theorem
04104 BitvectorTheoremProducer::bvuminusVar(const Expr& e) {
04105 if(CHECK_PROOFS) {
04106 CHECK_SOUND(BVUMINUS == e.getOpKind(),
04107 "BitvectorTheoremProducer::bvuminusVar: "
04108 "e should be bvuminus: e =" + e.toString());
04109 }
04110 Expr output;
04111 std::vector<bool> res;
04112 int e0Length = d_theoryBitvector->BVSize(e[0]);
04113 for(int i=0; i<e0Length; ++i) {
04114 res.push_back(true);
04115 }
04116 Expr coeff = d_theoryBitvector->newBVConstExpr(res);
04117 output = d_theoryBitvector->newBVMultExpr(e0Length, coeff, e[0]);
04118
04119 Proof pf;
04120 if(withProof())
04121 pf = newPf("bvuminus_var_rule", e);
04122 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04123 }
04124
04125
04126 Theorem
04127 BitvectorTheoremProducer::bvmultBVUminus(const Expr& e) {
04128 if(CHECK_PROOFS) {
04129 CHECK_SOUND(BVUMINUS == e.getOpKind(),
04130 "BitvectorTheoremProducer::bvmultBVUminus: "
04131 "e should be bvuminus: e =" + e.toString());
04132 CHECK_SOUND(BVMULT == e[0].getOpKind() &&
04133 BVCONST == e[0][0].getKind() &&
04134 BVUMINUS == e[0][1].getOpKind(),
04135 "Bitvectortheoremproducer::bvmultBVUminus: "
04136 "in input expression e = " + e.toString() +
04137 "\ne[0] has to be bvmult"
04138 "e[0][1] must be bvuminus: e[0] = " + e[0].toString());
04139 int bvLength = d_theoryBitvector->BVSize(e);
04140 int e00Length = d_theoryBitvector->BVSize(e[0][0]);
04141 int e01Length = d_theoryBitvector->BVSize(e[0][1]);
04142 CHECK_SOUND(bvLength == e00Length && e00Length == e01Length,
04143 "Bitvectortheoremproducer::bvmultBVUminus: "
04144 "in input expression e = " + e.toString() +
04145 "\nLengths of all subexprs must be equal.");
04146 }
04147 Expr output;
04148 int bvLength = d_theoryBitvector->BVSize(e);
04149 const Expr& coeff = e[0][0];
04150 Rational negatedcoeff = d_theoryBitvector->computeNegBVConst(coeff);
04151 const Expr& e010 = e[0][1][0];
04152
04153 if(0 == negatedcoeff)
04154
04155 output = d_theoryBitvector->newBVZeroString(bvLength);
04156 else if (1 == negatedcoeff)
04157
04158 output = e010;
04159 else {
04160
04161 Expr newcoeff = d_theoryBitvector->newBVConstExpr(negatedcoeff, bvLength);
04162 output = d_theoryBitvector->newBVMultExpr(bvLength, newcoeff, e010);
04163 }
04164
04165 Proof pf;
04166 if(withProof())
04167 pf = newPf("bvmult_bvuminus_rule", e);
04168 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04169 }
04170
04171
04172 Theorem
04173 BitvectorTheoremProducer::bvuminusBVPlus(const Expr& e) {
04174
04175
04176
04177
04178
04179
04180
04181
04182
04183
04184
04185
04186
04187
04188
04189
04190
04191
04192
04193
04194
04195
04196
04197
04198
04199
04200
04201 Proof pf;
04202 if(withProof())
04203 pf = newPf("bvminus_bvplus_rule", e);
04204 return newRWTheorem(e, e, Assumptions::emptyAssump(), pf);
04205 }
04206
04207 Theorem
04208 BitvectorTheoremProducer::extractBVMult(const Expr& e) {
04209 if(CHECK_PROOFS) {
04210 CHECK_SOUND(e.getOpKind() == EXTRACT &&
04211 e[0].getOpKind() == BVMULT &&
04212 e[0].arity() == 2,
04213 "BitvectorTheoremProducer::extractBVMult: "
04214 "input must be an EXTRACT over BVMULT:\n e = "+e.toString());
04215 }
04216 const Expr& bvmult = e[0];
04217 int bvmultLen = d_theoryBitvector->BVSize(bvmult);
04218 int extractHi = d_theoryBitvector->getExtractHi(e);
04219 int extractLow = d_theoryBitvector->getExtractLow(e);
04220
04221 if(CHECK_PROOFS) {
04222 CHECK_SOUND(bvmultLen > extractHi,
04223 "BitvectorTheoremProducer::extractBVMult: "
04224 "bvmult Length must be greater than extract Length:\n e = "
04225 +e.toString());
04226 }
04227
04228 Expr output = d_theoryBitvector->newBVMultPadExpr(extractHi+1, bvmult[0],
04229 bvmult[1]);
04230 if(extractLow > 0)
04231 output=d_theoryBitvector->newBVExtractExpr(output, extractHi, extractLow);
04232
04233 Proof pf;
04234 if(withProof())
04235 pf = newPf("extract_bvmult_rule", e);
04236 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04237 }
04238
04239 Theorem
04240 BitvectorTheoremProducer::extractBVPlus(const Expr& e) {
04241 if(CHECK_PROOFS) {
04242 CHECK_SOUND(e.getOpKind() == EXTRACT && e[0].getOpKind() == BVPLUS,
04243 "BitvectorTheoremProducer::extractBVPlus: "
04244 "input must be an EXTRACT over BVPLUS:\n e = "+e.toString());
04245 }
04246 const Expr& bvplus = e[0];
04247 int bvplusLen = d_theoryBitvector->BVSize(bvplus);
04248 int extractHi = d_theoryBitvector->getExtractHi(e);
04249 int extractLow = d_theoryBitvector->getExtractLow(e);
04250
04251 if(CHECK_PROOFS) {
04252 CHECK_SOUND(bvplusLen > extractHi,
04253 "BitvectorTheoremProducer::extractBVPlus: "
04254 "bvplus Length must be greater than extract bvLength:\n e = "
04255 +e.toString());
04256 }
04257
04258
04259 if(bvplusLen == extractHi+1)
04260 return d_theoryBitvector->reflexivityRule(e);
04261
04262
04263 Expr output(d_theoryBitvector->newBVPlusPadExpr(extractHi+1, bvplus.getKids()));
04264 if(extractLow > 0)
04265 output=d_theoryBitvector->newBVExtractExpr(output, extractHi, extractLow);
04266
04267 Proof pf;
04268 if(withProof())
04269 pf = newPf("extract_bvplus_rule", e);
04270 return newRWTheorem(e, output, Assumptions::emptyAssump(), pf);
04271 }
04272
04273
04274
04275 Theorem
04276 BitvectorTheoremProducer::typePredBit(const Expr& e) {
04277 if(CHECK_PROOFS) {
04278 CHECK_SOUND(d_theoryBitvector->getBaseType(e).getExpr().getOpKind() == BITVECTOR,
04279 "BitvectorTheoremProducer::typePredBit: e = "+e.toString());
04280 CHECK_SOUND(d_theoryBitvector->BVSize(e) == 1,
04281 "BitvectorTheoremProducer::typePredBit: e = "+e.toString());
04282 }
04283
04284 Proof pf;
04285 if(withProof())
04286 pf=newPf("type_pred_bit", e);
04287 return newTheorem(e.eqExpr(bvZero()) || e.eqExpr(bvOne()), Assumptions::emptyAssump(), pf);
04288 }
04289
04290
04291
04292 Theorem
04293 BitvectorTheoremProducer::expandTypePred(const Theorem& tp) {
04294 Expr tpExpr = tp.getExpr();
04295 if(CHECK_PROOFS) {
04296 CHECK_SOUND(tpExpr.getOpKind() == BVTYPEPRED ||
04297 (tpExpr.getKind() == NOT && tpExpr[0].getOpKind() == BVTYPEPRED),
04298 "BitvectorTheoremProducer::expandTypePred: "
04299 "Expected BV_TYPE_PRED wrapper:\n tp = "
04300 +tpExpr.toString());
04301 }
04302 Expr res;
04303 if(tpExpr.getKind() == NOT)
04304 res = d_theoryBitvector->falseExpr();
04305 else {
04306 Type t(d_theoryBitvector->getTypePredType(tpExpr));
04307 const Expr& e(d_theoryBitvector->getTypePredExpr(tpExpr));
04308 int size(d_theoryBitvector->getBitvectorTypeParam(t));
04309
04310
04311 if(size >= 2) {
04312 vector<Expr> kids;
04313 for(int i=0; i<size; i++) {
04314 Expr bit(d_theoryBitvector->newBVExtractExpr(e, i, i));
04315 kids.push_back(bit.eqExpr(bvZero()) || bit.eqExpr(bvOne()));
04316 }
04317 res = andExpr(kids);
04318 } else {
04319 res = (e.eqExpr(bvZero()) || e.eqExpr(bvOne()));
04320 }
04321 }
04322 Proof pf;
04323 if(withProof())
04324 pf = newPf("expand_type_pred", tp.getExpr(), tp.getProof());
04325
04326 return newTheorem(res, tp.getAssumptionsRef(), pf);
04327 }
04328
04329
04330
04331
04332
04333
04334
04335
04336
04337
04338
04339
04340
04341
04342 Theorem BitvectorTheoremProducer::MarkNonSolvableEq( const Expr& e)
04343 {
04344
04345 int bv_size = d_theoryBitvector->BVSize(e[0]);
04346 Expr bv_zero( d_theoryBitvector->newBVZeroString(bv_size));
04347
04348 if (CHECK_PROOFS)
04349 CHECK_SOUND( e.isEq() &&
04350 ( e[0] == bv_zero || e[1] == bv_zero ),
04351 "MarkNonSolvableEq: input must be a canonized equation" + e.toString());
04352 if( e[1] == bv_zero )
04353 {
04354 Expr expr_res= Expr(EQ, e[1], e[0]);
04355 Proof pf= newPf("mark non solvable eq");
04356 Theorem th_res= newRWTheorem( e, expr_res, Assumptions::emptyAssump(), pf);
04357 return th_res;
04358 }
04359 else
04360 {
04361 return d_theoryBitvector->reflexivityRule(e);
04362 }
04363
04364
04365 }
04366
04367
04368
04369
04370 Theorem BitvectorTheoremProducer::isolate_var(const Expr& e)
04371 {
04372 int bv_size = d_theoryBitvector->BVSize(e[0]);
04373 Expr bv_zero(d_theoryBitvector->newBVZeroString(bv_size));
04374
04375 if (CHECK_PROOFS) {
04376 CHECK_SOUND(e.isEq() && e[1] == bv_zero && e[0].getOpKind() != BVCONST,
04377 "isolate_var: input must be an equation with lhs non-cosnt and rhs must be zero" + e.toString());
04378 }
04379
04380
04381
04382 Rational modulus = pow(Rational(bv_size), Rational(2));
04383 Expr res_expr;
04384 Expr lhs = e[0];
04385
04386 switch (lhs.getOpKind()) {
04387 case BVMULT:
04388
04389 if( lhs[0].getOpKind() == BVCONST )
04390 {
04391 DebugAssert(lhs[1].getOpKind() != BVCONST &&
04392 lhs[1].getOpKind() != BVPLUS, "Should have been canonized");
04393 DebugAssert(d_theoryBitvector->computeBVConst(lhs[0]) % 2 == 0,
04394 "Expected even coeff");
04395 }
04396 res_expr = e;
04397 break;
04398 case BVPLUS:
04399 {
04400 int e_kid_arity = lhs.arity();
04401 bool foundUnitCoeff = false;
04402 Expr new_lhs, new_rhs, new_coeff;
04403 vector<Expr> newKids;
04404 Rational tmp, const_term = 0;
04405 for( int i = 0; i < e_kid_arity; ++i)
04406 {
04407
04408 Expr e_sub_kid = lhs[i];
04409 switch (e_sub_kid.getOpKind()) {
04410 case BVCONST:
04411 DebugAssert(const_term == 0, "Expected only one constant");
04412 const_term = ((modulus-1) * d_theoryBitvector->computeBVConst(e_sub_kid)) % modulus;
04413 newKids.push_back(d_theoryBitvector->newBVConstExpr(const_term, bv_size));
04414 break;
04415 case BVMULT:
04416 if( e_sub_kid[0].getOpKind() == BVCONST )
04417 {
04418 DebugAssert(e_sub_kid.arity() == 2, "Expected arity 2 BVMULT");
04419 tmp = d_theoryBitvector->computeBVConst(e_sub_kid[0]);
04420 DebugAssert(tmp != 1, "Expected coeff other than 1");
04421 tmp = (tmp * (modulus-1)) % modulus;
04422 new_coeff = d_theoryBitvector->newBVConstExpr(tmp, bv_size);
04423 newKids.push_back(d_theoryBitvector->newBVMultExpr(bv_size, new_coeff, e_sub_kid[1]));
04424 }
04425 else {
04426 new_coeff = d_theoryBitvector->newBVConstExpr(modulus-1, bv_size);
04427 newKids.push_back(d_theoryBitvector->newBVMultExpr(bv_size, new_coeff, e_sub_kid));
04428 }
04429 break;
04430 default:
04431 if (!foundUnitCoeff) {
04432 foundUnitCoeff = true;
04433 new_lhs = e_sub_kid;
04434 }
04435 else {
04436 new_coeff = d_theoryBitvector->newBVConstExpr(modulus-1, bv_size);
04437 newKids.push_back(d_theoryBitvector->newBVMultExpr(bv_size, new_coeff, e_sub_kid));
04438 }
04439 break;
04440 }
04441 }
04442 if (foundUnitCoeff) {
04443 DebugAssert(newKids.size() > 0, "Expected non-empty kids");
04444 Expr new_rhs;
04445 if (newKids.size() == 1) {
04446 new_rhs = newKids[0];
04447 }
04448 else {
04449 new_rhs = d_theoryBitvector->newBVPlusExpr(bv_size, newKids);
04450 }
04451 res_expr = Expr(EQ, new_lhs, new_rhs);
04452 }
04453 else {
04454 res_expr = e;
04455 }
04456 break;
04457 }
04458 default:
04459 res_expr = e;
04460 break;
04461 }
04462 Proof pf= newPf("isolate var");
04463
04464
04465 DebugAssert(e == res_expr || (res_expr.isEq() && d_theoryBitvector->isLeaf(res_expr[0]) &&
04466 !d_theoryBitvector->isLeafIn(res_expr[0], res_expr[1])),
04467 "Expected no change or solved form");
04468
04469 return newRWTheorem(e, res_expr, Assumptions::emptyAssump(), pf);
04470 }
04471
04472
04473
04474
04475
04476
04477
04478
04479
04480
04481
04482
04483
04484
04485
04486
04487
04488
04489
04490
04491
04492
04493
04494
04495
04496
04497
04498
04499
04500
04501
04502
04503
04504
04505
04506
04507
04508
04509
04510
04511
04512
04513
04514
04515
04516
04517
04518
04519
04520
04521
04522
04523
04524
04525
04526
04527
04528
04529
04530
04531
04532
04533
04534
04535
04536
04537
04538
04539
04540
04541
04542
04543
04544
04545
04546
04547
04548
04549
04550
04551
04552
04553
04554
04555
04556
04557
04558
04559
04560
04561
04562
04563
04564
04565
04566
04567
04568
04569
04570
04571
04572
04573
04574
04575
04576
04577
04578
04579
04580
04581
04582
04583
04584
04585
04586
04587
04588
04589
04590
04591
04592
04593
04594
04595
04596
04597
04598
04599
04600
04601
04602
04603
04604
04605
04606
04607
04608
04609
04610
04611
04612
04613
04614
04615
04616
04617
04618 Theorem BitvectorTheoremProducer::BVMult_order_subterms( const Expr& e )
04619 {
04620 if (CHECK_PROOFS)
04621 CHECK_SOUND(e.getOpKind() == BVMULT,
04622 "BitvectorTheoremProducer::BVMult_order_vars: input must be a BVMULT expression" + e.toString());
04623
04624
04625 int bv_size= d_theoryBitvector->BVSize(e);
04626 Expr new_expr;
04627 vector<Expr> vars;
04628
04629
04630
04631 bool hasConst = false;
04632 if (e[0].getOpKind() == BVCONST) {
04633 d_theoryBitvector->extract_vars(e[1], vars);
04634 hasConst = true;
04635 }
04636 else {
04637 d_theoryBitvector->extract_vars(e, vars);
04638 }
04639
04640 int vars_size = vars.size();
04641 ExprMap<int> vars_map;
04642
04643 for( int i=0; i < vars_size; ++i)
04644 {
04645
04646
04647 if( vars_map.count( vars[i] ) == 0)
04648 vars_map[ vars[i] ] = 1;
04649 else
04650 vars_map[ vars[i] ] = vars_map[ vars[i] ] + 1;
04651 }
04652
04653
04654
04655 ExprMap<int>::iterator j = vars_map.begin();
04656 new_expr = (*j).first;
04657 if ((*j).second != 1) {
04658 for(int k=1; k < (*j).second; ++k) {
04659 new_expr = d_theoryBitvector->newBVMultExpr( bv_size, (*j).first, new_expr);
04660 }
04661 }
04662
04663 for( ++j; j != vars_map.end(); ++j) {
04664 new_expr = d_theoryBitvector->newBVMultExpr( bv_size, (*j).first, new_expr);
04665 if ((*j).second != 1) {
04666 for(int k=1; k < (*j).second; ++k) {
04667 new_expr = d_theoryBitvector->newBVMultExpr( bv_size, (*j).first, new_expr);
04668 }
04669 }
04670 }
04671
04672 Proof pf;
04673 if (withProof()) pf = newPf("BVMult_order_subterms");
04674
04675 if (hasConst) {
04676 new_expr = d_theoryBitvector->newBVMultExpr( bv_size, e[0], new_expr);
04677 }
04678
04679 Theorem result = newRWTheorem( e, new_expr, Assumptions::emptyAssump(), pf);
04680 return result;
04681 }
04682
04683
04684
04685
04686 Theorem BitvectorTheoremProducer::liftConcatBVMult(const Expr& e)
04687 {
04688 if (CHECK_PROOFS) {
04689 CHECK_SOUND(e.getOpKind() == BVMULT,
04690 "BitvectorTheoremProducer::liftConcatBVMult: input must be a BVMULT expression" + e.toString());
04691 }
04692 int bv_size = d_theoryBitvector->BVSize( e );
04693 vector<Expr> kids;
04694 int idx = -1;
04695 bool first = false;
04696 int i = 0;
04697 for (; i< e.arity(); ++i) {
04698 const Expr& kid = e[i];
04699 if (idx == -1 &&
04700 kid.getOpKind() == CONCAT) {
04701 if (kid[kid.arity()-1].getKind() == BVCONST) {
04702 idx = i;
04703 }
04704 else if (kid[0].getKind() == BVCONST &&
04705 d_theoryBitvector->computeBVConst(kid[0]) != 0) {
04706 idx = i;
04707 first = true;
04708 }
04709 else kids.push_back(kid);
04710 }
04711 else kids.push_back(kid);
04712 }
04713 if (idx == -1) return d_theoryBitvector->reflexivityRule(e);
04714
04715 Expr concatHi, concatLo;
04716
04717 if (first) {
04718
04719 if (e[idx].arity() == 2) {
04720 concatLo = e[idx][1];
04721 }
04722 else {
04723 vector<Expr> concatKids;
04724 for (i = 1; i < e[idx].arity(); ++i) {
04725 concatKids.push_back(e[idx][i]);
04726 }
04727 concatLo = d_theoryBitvector->newConcatExpr(concatKids);
04728 }
04729 concatHi = e[idx][0];
04730 }
04731 else {
04732
04733 vector<Expr> concatKids = e[idx].getKids();
04734 concatLo = concatKids.back();
04735 concatKids.pop_back();
04736 if (concatKids.size() == 1) {
04737 concatHi = concatKids[0];
04738 }
04739 else {
04740 concatHi = d_theoryBitvector->newConcatExpr(concatKids);
04741 }
04742 }
04743
04744 int n = d_theoryBitvector->BVSize(concatLo);
04745 kids.push_back(concatLo);
04746 Expr bvMult1 = d_theoryBitvector->newBVMultPadExpr(bv_size, kids);
04747 kids.pop_back();
04748 kids.push_back(concatHi);
04749 Expr bvMult2 = d_theoryBitvector->newBVMultPadExpr(bv_size-n,kids);
04750 Expr newLowConcat = d_theoryBitvector->newBVZeroString(n);
04751 Expr newConcat = d_theoryBitvector->newConcatExpr(bvMult2, newLowConcat);
04752 Expr res_expr = d_theoryBitvector->newBVPlusExpr(bv_size, bvMult1, newConcat);
04753
04754 Proof pf;
04755 if (withProof()) pf = newPf("liftConcatBVMult");
04756 return newRWTheorem(e, res_expr, Assumptions::emptyAssump(), pf);
04757 }
04758
04759
04760
04761
04762
04763
04764
04765
04766
04767
04768
04769 Theorem BitvectorTheoremProducer::canonBVMult( const Expr& e )
04770 {
04771 TRACE("canonBVMult", "canonBVMult: {\n ", e.toString(), " --");
04772 if (CHECK_PROOFS)
04773 CHECK_SOUND(e.getOpKind() == BVMULT,
04774 "BitvectorTheoremProducer::canonBVMult: input must be a BVMULT expression" + e.toString());
04775
04776
04777 int expr_arity = e.arity();
04778 int bv_size= d_theoryBitvector->BVSize(e);
04779 Theorem result;
04780 std::vector<Expr> mult_vars;
04781 Rational temp_coeff = 1;
04782 Expr new_expr;
04783 Expr no_minus_kid;
04784 Expr new_prod;
04785 Rational modulus = pow(Rational(bv_size), Rational(2));
04786
04787
04788
04789 for( int i = 0; i < expr_arity; ++i) {
04790 if (e[i].getOpKind() == BVUMINUS) {
04791 temp_coeff = (temp_coeff * (modulus-1)) % modulus;
04792 no_minus_kid = e[i][0];
04793 } else no_minus_kid = e[i];
04794
04795 switch (no_minus_kid.getOpKind()) {
04796
04797 case BVCONST: {
04798
04799 temp_coeff *= d_theoryBitvector->computeBVConst( no_minus_kid );
04800 temp_coeff = temp_coeff % modulus;
04801 break;
04802 }
04803
04804 case BVMULT: {
04805 if (no_minus_kid[0].getOpKind() == BVCONST) {
04806
04807 temp_coeff *= d_theoryBitvector->computeBVConst(no_minus_kid[0]);
04808 temp_coeff = temp_coeff % modulus;
04809 DebugAssert(no_minus_kid[1].getOpKind() != BVCONST &&
04810 no_minus_kid[1].getOpKind() != BVPLUS &&
04811 no_minus_kid[1].getOpKind() != BVUMINUS,
04812 "Expected canonized subterm");
04813
04814 if (!new_prod.isNull()) {
04815
04816 new_prod = d_theoryBitvector->newBVMultExpr( bv_size, new_prod, no_minus_kid[1]);
04817 }
04818 else
04819 {
04820 new_prod = no_minus_kid[1];
04821 }
04822 }
04823 else {
04824 if (!new_prod.isNull()) {
04825
04826 new_prod = d_theoryBitvector->newBVMultExpr( bv_size, new_prod, no_minus_kid);
04827 }
04828 else
04829 {
04830 new_prod = no_minus_kid;
04831 }
04832 }
04833 break;
04834 }
04835
04836 case BVPLUS: {
04837 result = distributive_rule( e );
04838 TRACE("canonBVMult", "--> ", result.getRHS().toString(), "\n}");
04839 return result;
04840 }
04841
04842 default:
04843 if (!new_prod.isNull()) {
04844
04845 new_prod = d_theoryBitvector->newBVMultExpr( bv_size, new_prod, no_minus_kid);
04846 }
04847 else
04848 {
04849 new_prod = no_minus_kid;
04850 }
04851 }
04852 }
04853
04854
04855 if (temp_coeff == 0 || new_prod.isNull()) {
04856
04857 new_expr = d_theoryBitvector->newBVConstExpr(temp_coeff, bv_size);
04858 }
04859 else {
04860 if (new_prod.getOpKind() == BVMULT) {
04861 new_prod = BVMult_order_subterms(new_prod).getRHS();
04862 }
04863 ExprMap<Rational> sumHashMap;
04864 Rational known_term;
04865 Expr coeff_expr = d_theoryBitvector->newBVConstExpr(temp_coeff, bv_size);
04866 new_expr = d_theoryBitvector->newBVMultExpr(bv_size, coeff_expr, new_prod);
04867 getPlusTerms(new_expr, known_term, sumHashMap);
04868 new_expr = buildPlusTerm(bv_size, known_term, sumHashMap);
04869 }
04870
04871 Proof pf;
04872 if (withProof()) pf = newPf("canonBVMult");
04873 result = newRWTheorem(e, new_expr, Assumptions::emptyAssump(), pf);
04874 TRACE("canonBVMult", "--> ", new_expr.toString(), "\n}");
04875
04876 return result;
04877 }
04878
04879
04880
04881 Theorem BitvectorTheoremProducer::distributive_rule( const Expr& e )
04882 {
04883 if (CHECK_PROOFS)
04884 CHECK_SOUND(e.getOpKind() == BVMULT,
04885 "BitvectorTheoremProducer::distributive_rule: input must be a BVMULT expression" + e.toString());
04886
04887 int bv_size= d_theoryBitvector->BVSize(e);
04888
04889
04890
04891
04892 vector<Expr> e0_kids, e1_kids, result_kids;
04893
04894 if (e[0].getOpKind() == BVPLUS) {
04895 e0_kids = e[0].getKids();
04896 }
04897 else e0_kids.push_back(e[0]);
04898
04899 if (e[1].getOpKind() == BVPLUS) {
04900 e1_kids = e[1].getKids();
04901 }
04902 else e1_kids.push_back(e[1]);
04903
04904 unsigned e0_kids_size = e0_kids.size();
04905 unsigned e1_kids_size = e1_kids.size();
04906 for( unsigned i = 0; i < e0_kids_size; ++i) {
04907 for( unsigned j = 0; j < e1_kids_size; ++j) {
04908 Expr sum_term = d_theoryBitvector->newBVMultExpr ( bv_size, e0_kids[i], e1_kids[j] );
04909 result_kids.push_back( sum_term );
04910 }
04911 }
04912 Expr result_sum = d_theoryBitvector->newBVPlusExpr ( bv_size, result_kids);
04913 Proof pf;
04914 if (withProof()) pf = newPf("distributive rule");
04915 Theorem result = newRWTheorem( e, result_sum, Assumptions::emptyAssump(), pf);
04916 return result;
04917 }
04918
04919
04920
04921
04922
04923 Theorem BitvectorTheoremProducer::liftConcatBVPlus(const Expr& e)
04924 {
04925 if (CHECK_PROOFS) {
04926 CHECK_SOUND(e.getOpKind() == BVPLUS,
04927 "BitvectorTheoremProducer::liftConcatBVPlus: input must be a BVPLUS expression" + e.toString());
04928 }
04929 int bv_size = d_theoryBitvector->BVSize( e );
04930 vector<Expr> kids;
04931 int i = 0;
04932 Rational c = 0;
04933
04934 if (e[0].getOpKind() == BVCONST) {
04935 ++i;
04936 c = d_theoryBitvector->computeBVConst(e[0]);
04937 }
04938
04939 int chopSize = bv_size;
04940
04941 bool nonzero = false;
04942 bool nonconst = false;
04943 Expr term;
04944
04945 for (; i< e.arity(); ++i) {
04946 const Expr& kid = e[i];
04947 if (kid.getOpKind() != CONCAT) {
04948 return d_theoryBitvector->reflexivityRule(e);
04949 }
04950 Expr last = kid[kid.arity()-1];
04951 int size = d_theoryBitvector->BVSize(last);
04952
04953
04954
04955
04956 if (last.getOpKind() != BVCONST) {
04957 if (nonzero || size > chopSize) {
04958 return d_theoryBitvector->reflexivityRule(e);
04959 }
04960 nonzero = true;
04961 nonconst = true;
04962 chopSize = size;
04963 term = last;
04964 continue;
04965 }
04966
04967
04968
04969
04970 if (d_theoryBitvector->computeBVConst(last) == 0) {
04971 if (size >= chopSize) continue;
04972 if (nonconst) return d_theoryBitvector->reflexivityRule(e);
04973 chopSize = size;
04974 continue;
04975 }
04976
04977
04978
04979 if (nonzero) return d_theoryBitvector->reflexivityRule(e);
04980 nonzero = true;
04981 if (size < chopSize) chopSize = size;
04982 term = last;
04983 }
04984
04985
04986 if (nonzero) {
04987 if (c != 0) {
04988 Rational modulus = pow(Rational(chopSize), Rational(2));
04989 if ((c % modulus) != 0) {
04990 return d_theoryBitvector->reflexivityRule(e);
04991 }
04992 }
04993 }
04994 else if (c == 0) {
04995 term = d_theoryBitvector->newBVZeroString(chopSize);
04996 }
04997 else {
04998 term = d_theoryBitvector->newBVExtractExpr(e[0], chopSize-1, 0);
04999 }
05000
05001 vector<Expr> newKids;
05002 for (i = 0; i < e.arity(); ++i) {
05003 newKids.push_back(d_theoryBitvector->newBVExtractExpr(e[i], bv_size-1, chopSize));
05004 }
05005
05006 Expr bvPlus = d_theoryBitvector->newBVPlusExpr(bv_size-chopSize, newKids);
05007 if (d_theoryBitvector->BVSize(term) > chopSize) {
05008 term = d_theoryBitvector->newBVExtractExpr(term, chopSize-1, 0);
05009 }
05010
05011 Expr res_expr = d_theoryBitvector->newConcatExpr(bvPlus, term);
05012
05013 Proof pf;
05014 if (withProof()) pf = newPf("liftConcatBVPlus");
05015 return newRWTheorem(e, res_expr, Assumptions::emptyAssump(), pf);
05016 }
05017
05018
05019 void BitvectorTheoremProducer::getPlusTerms(const Expr& e, Rational& known_term,
05020 ExprMap<Rational>& sumHashMap)
05021 {
05022 int bv_size = d_theoryBitvector->BVSize( e );
05023 Rational modulus = pow(Rational(bv_size), Rational(2));
05024 unsigned i;
05025 vector<Expr> plusTerms;
05026 vector<Rational> coeffs;
05027
05028 plusTerms.push_back(e);
05029 coeffs.push_back(1);
05030 known_term = 0;
05031
05032 for(i = 0; i < plusTerms.size(); ++i) {
05033 Expr kid = plusTerms[i];
05034 int kidSize = d_theoryBitvector->BVSize(kid);
05035 DebugAssert(kidSize <= bv_size, "Expected kid no wider than bv_size");
05036 Rational coeff = coeffs[i];
05037 if (coeff == 0) continue;
05038
05039 switch (kid.getOpKind()) {
05040
05041 case BVCONST:
05042 known_term += coeff * d_theoryBitvector->computeBVConst( kid );
05043 known_term = known_term % modulus;
05044 break;
05045
05046 case BVUMINUS:
05047 DebugAssert(kidSize == bv_size, "Unexpected size for uminus");
05048 plusTerms.push_back(plusTerms[i][0]);
05049 coeffs.push_back((coeff * (modulus - 1)) % modulus);
05050 break;
05051
05052 case BVNEG:
05053 if (kidSize < bv_size) {
05054 Rational m2 = pow(Rational(kidSize), Rational(2));
05055 known_term += coeff * (m2-1);
05056 }
05057 else {
05058 known_term += coeff * (modulus-1);
05059 }
05060 known_term = known_term % modulus;
05061 plusTerms.push_back(plusTerms[i][0]);
05062 coeffs.push_back((coeff * (modulus-1)) % modulus);
05063 break;
05064
05065 case BVMULT:
05066 if (kidSize < bv_size) {
05067 int shift = 0;
05068 Rational tcoeff = coeff;
05069 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
05070 if (shift + kidSize < bv_size) {
05071
05072
05073 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
05074 break;
05075 }
05076 }
05077
05078 if( kid[0].getOpKind() == BVCONST )
05079 {
05080 DebugAssert(kid.arity() == 2, "Expected arity 2 BVMULT");
05081 plusTerms.push_back(kid[1]);
05082 coeffs.push_back((coeff * d_theoryBitvector->computeBVConst(kid[0])) % modulus);
05083 }
05084 else
05085 {
05086 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
05087 }
05088 break;
05089
05090 case BVPLUS: {
05091 if (kidSize < bv_size) {
05092 int shift = 0;
05093 Rational tcoeff = coeff;
05094 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
05095 if (shift + kidSize < bv_size) {
05096
05097
05098 sumHashMap[ kid ] = sumHashMap[ kid ] + coeff;
05099 break;
05100 }
05101 }
05102
05103 int kid_arity = kid.arity();
05104 for(int j = 0; j < kid_arity; ++j) {
05105 plusTerms.push_back(kid[j]);
05106 coeffs.push_back(coeff);
05107 }
05108 break;
05109 }
05110
05111 case CONCAT: {
05112
05113 int n = d_theoryBitvector->BVSize(kid);
05114 Rational concatConst;
05115 for (int j = 0; j < kid.arity(); ++j) {
05116 const Expr& concatKid = kid[j];
05117 n -= d_theoryBitvector->BVSize(concatKid);
05118 concatConst = pow(Rational(n), Rational(2)) * coeff;
05119 plusTerms.push_back(concatKid);
05120 coeffs.push_back(concatConst % modulus);
05121 }
05122 break;
05123 }
05124
05125 case EXTRACT: {
05126
05127 if (false && kidSize < bv_size) {
05128
05129 const Expr& ext_kid = kid[0];
05130 int size = d_theoryBitvector->BVSize(ext_kid);
05131 int extractLeft = d_theoryBitvector->getExtractHi(kid);
05132 if (extractLeft < size-1) {
05133 int shift = 0;
05134 Rational tcoeff = coeff;
05135 for (; tcoeff % 2 == 0; ++shift, tcoeff = tcoeff / 2);
05136 if (shift + kidSize >= bv_size) {
05137 int bitsToAdd = bv_size - kidSize;
05138 extractLeft += bitsToAdd;
05139 if (extractLeft > size - 1) extractLeft = size - 1;
05140 int extractRight = d_theoryBitvector->getExtractLow(kid);
05141 if (extractLeft == size-1 && extractRight == 0) {
05142 plusTerms.push_back(ext_kid);
05143 coeffs.push_back(coeff);
05144 }
05145 else {
05146 plusTerms.push_back(d_theoryBitvector->newBVExtractExpr(ext_kid, extractLeft, extractRight));
05147 coeffs.push_back(coeff);
05148 }
05149 break;
05150 }
05151 }
05152 else {
05153 DebugAssert(d_theoryBitvector->getExtractLow(kid) != 0,
05154 "Unexpected extract bounds");
05155 }
05156 }
05157
05158 }
05159
05160 default:
05161 sumHashMap[ kid] = sumHashMap[ kid] + coeff;
05162 break;
05163 }
05164 }
05165 }
05166
05167
05168 Expr BitvectorTheoremProducer::chopConcat(int bv_size, Rational c,
05169 vector<Expr>& concatKids)
05170 {
05171 int chopSize = bv_size;
05172
05173 bool nonzero = false;
05174 bool nonconst = false;
05175 Expr term, kid, last;
05176 int size;
05177 unsigned i;
05178
05179 for (i = 0; i< concatKids.size(); ++i) {
05180 kid = concatKids[i];
05181 if (kid.getOpKind() != CONCAT) return Expr();
05182
05183 last = kid[kid.arity()-1];
05184 size = d_theoryBitvector->BVSize(last);
05185
05186
05187
05188
05189 if (last.getOpKind() != BVCONST) {
05190 if (nonzero || size > chopSize) return Expr();
05191 nonzero = true;
05192 nonconst = true;
05193 chopSize = size;
05194 term = last;
05195 continue;
05196 }
05197
05198
05199
05200
05201 if (d_theoryBitvector->computeBVConst(last) == 0) {
05202 if (size >= chopSize) continue;
05203 if (nonconst) return Expr();
05204 chopSize = size;
05205 continue;
05206 }
05207
05208
05209
05210 if (nonzero) return Expr();
05211 nonzero = true;
05212 if (size < chopSize) chopSize = size;
05213 term = last;
05214 }
05215
05216 Rational modulus = pow(Rational(chopSize), Rational(2));
05217
05218
05219 if (nonzero) {
05220 if (c != 0) {
05221 if ((c % modulus) != 0) return Expr();
05222 c = c / modulus;
05223 }
05224 }
05225 else if (c == 0) {
05226 term = d_theoryBitvector->newBVZeroString(chopSize);
05227 }
05228 else {
05229 Rational value = c % modulus;
05230 term = d_theoryBitvector->newBVConstExpr(value, chopSize);
05231 c = c - value;
05232 c = c / modulus;
05233 }
05234
05235
05236 for (i = 0; i < concatKids.size(); ++i) {
05237 kid = concatKids[i];
05238 vector<Expr> kids = kid.getKids();
05239 last = kids.back();
05240 kids.pop_back();
05241 size = d_theoryBitvector->BVSize(last);
05242
05243 if (size != chopSize) {
05244 DebugAssert(size > chopSize, "Expected last to be wider than chopSize");
05245 DebugAssert(last.getOpKind() == BVCONST, "Expected last kind = BVCONST");
05246 Rational value = d_theoryBitvector->computeBVConst(last);
05247 if (value != 0) {
05248 value = value - (value % modulus);
05249 value = value / modulus;
05250 }
05251 kids.push_back(d_theoryBitvector->newBVConstExpr(value, size - chopSize));
05252 }
05253 DebugAssert(kids.size() > 0, "Expected size > 0");
05254 if (kids.size() == 1) {
05255 concatKids[i] = kids[0];
05256 }
05257 else {
05258 concatKids[i] = d_theoryBitvector->newConcatExpr(kids);
05259 }
05260 }
05261
05262 if (d_theoryBitvector->BVSize(term) > chopSize) {
05263 DebugAssert(term.getOpKind() == BVCONST, "Expected BVCONST");
05264 Rational value = d_theoryBitvector->computeBVConst(term);
05265 DebugAssert(value != 0, "Expected 0");
05266 value = value % modulus;
05267 term = d_theoryBitvector->newBVConstExpr(value, chopSize);
05268 }
05269
05270 Expr bvPlus = chopConcat(bv_size-chopSize, c, concatKids);
05271 if (!bvPlus.isNull()) {
05272 DebugAssert(bvPlus.getOpKind() == CONCAT, "Expected CONCAT");
05273 vector<Expr> kids = bvPlus.getKids();
05274 kids.push_back(term);
05275 return d_theoryBitvector->newConcatExpr(kids);
05276 }
05277
05278 vector<Expr> newKids;
05279 if (c != 0) {
05280 newKids.push_back(d_theoryBitvector->newBVConstExpr(c, bv_size - chopSize));
05281 }
05282 for (i = 0; i < concatKids.size(); ++i) {
05283 newKids.push_back(concatKids[i]);
05284 }
05285 DebugAssert(newKids.size() > 1, "Expected more than one kid");
05286 bvPlus = d_theoryBitvector->newBVPlusExpr(bv_size-chopSize, newKids);
05287
05288
05289 ExprMap<Rational> sumHashMap;
05290 Rational known_term;
05291 getPlusTerms(bvPlus, known_term, sumHashMap);
05292 bvPlus = buildPlusTerm(bv_size-chopSize, known_term, sumHashMap);
05293 return d_theoryBitvector->newConcatExpr(bvPlus, term);
05294 }
05295
05296
05297 Expr BitvectorTheoremProducer::buildPlusTerm(int bv_size,
05298 Rational& known_term,
05299 ExprMap<Rational>& sumHashMap)
05300 {
05301
05302 Rational modulus = pow(Rational(bv_size), Rational(2));
05303 Rational coeff, pos;
05304 Rational tmask, tcoeff, marked = 0;
05305 int nbits, lg;
05306 ExprMap<Rational>::iterator j = sumHashMap.begin();
05307 vector<Expr> multKids, concatKids;
05308 unsigned i;
05309 for(; j != sumHashMap.end(); ++j) {
05310 coeff = mod((*j).second, modulus);
05311 Expr term = (*j).first;
05312 nbits = d_theoryBitvector->BVSize(term);
05313
05314
05315 if (coeff == 1 && nbits == bv_size) {
05316 if (nbits == 1 && known_term == 1) {
05317
05318 multKids.push_back(d_theoryBitvector->newBVNegExpr(term));
05319 known_term = 0;
05320 }
05321 else {
05322 multKids.push_back(term);
05323 }
05324 continue;
05325 }
05326
05327 while (coeff != 0) {
05328
05329 for (pos = coeff, lg = 0; pos % 2 == 0; pos = pos / 2, ++lg);
05330 pos = pow(Rational(lg), Rational(2));
05331
05332 Expr concatTerm;
05333
05334
05335 Rational tmodulus = modulus;
05336 if (nbits+lg < bv_size) tmodulus = pow(Rational(nbits+lg), Rational(2));
05337 Rational tcoeff = coeff % tmodulus;
05338
05339 if (tcoeff == pos) {
05340 coeff -= tcoeff;
05341 concatTerm = term;
05342 }
05343 else if (((tcoeff + pos) % tmodulus) == 0) {
05344 coeff = (coeff + pos) % modulus;
05345
05346 concatTerm = d_theoryBitvector->newBVNegExpr(term);
05347 known_term += pos;
05348 if (nbits + lg < bv_size) {
05349 known_term += (modulus - tmodulus);
05350 }
05351 if (pos == 1 && nbits == bv_size) {
05352 multKids.push_back(concatTerm);
05353 continue;
05354 }
05355 }
05356 else {
05357
05358 if (nbits + lg > bv_size) {
05359
05360 int diff = nbits + lg - bv_size;
05361 int high, low;
05362 if (term.getOpKind() == EXTRACT) {
05363
05364 high = d_theoryBitvector->getExtractHi(term) - diff;
05365 low = d_theoryBitvector->getExtractLow(term);
05366 term = term[0];
05367 }
05368 else {
05369 high = nbits - 1 - diff;
05370 low = 0;
05371 }
05372 term = d_theoryBitvector->newBVExtractExpr(term, high, low);
05373 }
05374 nbits = bv_size - lg;
05375 coeff = coeff / pos;
05376 Expr new_coeff = d_theoryBitvector->newBVConstExpr(coeff, nbits);
05377 term = d_theoryBitvector->newBVMultPadExpr(nbits, new_coeff, term);
05378 coeff = 0;
05379 if (lg == 0) {
05380 multKids.push_back(term);
05381 continue;
05382 }
05383 concatTerm = term;
05384 }
05385
05386
05387 bool found = false;
05388 Expr t;
05389 vector<Expr> tmp;
05390 int bits, size, k, t_arity;
05391 for (i = 0; i < concatKids.size(); ++i) {
05392 t = concatKids[i];
05393 DebugAssert(t.getOpKind() == CONCAT, "Expected CONCAT");
05394 bits = bv_size;
05395 t_arity = t.arity();
05396 for (k = 0; k < t_arity; ++k) {
05397 if (k > 0 && bits < lg + nbits) break;
05398 size = d_theoryBitvector->BVSize(t[k]);
05399 if (bits - size <= lg) {
05400 if (t[k].getOpKind() == BVCONST) {
05401 found = true;
05402 }
05403 break;
05404 }
05405 else {
05406 tmp.push_back(t[k]);
05407 bits -= size;
05408 }
05409 }
05410 if (found) break;
05411 tmp.clear();
05412 }
05413 if (!found) {
05414 bits = bv_size;
05415 size = bv_size;
05416 k = t_arity = 0;
05417 }
05418 if (lg + nbits < bits) {
05419 tmp.push_back(d_theoryBitvector->newBVZeroString(bits-(lg+nbits)));
05420 }
05421 if (lg + nbits > bits) {
05422 bool negate = false;
05423 if (concatTerm.getOpKind() == BVNEG) {
05424
05425 negate = true;
05426 concatTerm = concatTerm[0];
05427 }
05428 DebugAssert(!found || k == 0,
05429 "Too big only OK for first child");
05430
05431 int diff = lg + nbits - bits;
05432 int high, low;
05433 if (concatTerm.getOpKind() == EXTRACT) {
05434
05435 high = d_theoryBitvector->getExtractHi(concatTerm) - diff;
05436 low = d_theoryBitvector->getExtractLow(concatTerm);
05437 concatTerm = concatTerm[0];
05438 }
05439 else {
05440 high = nbits - 1 - diff;
05441 low = 0;
05442 }
05443 concatTerm = d_theoryBitvector->newBVExtractExpr(concatTerm, high, low);
05444 if (negate) {
05445 concatTerm = d_theoryBitvector->newBVNegExpr(concatTerm);
05446 }
05447 }
05448 tmp.push_back(concatTerm);
05449 bits -= size;
05450 if (lg > bits) {
05451 tmp.push_back(d_theoryBitvector->newBVZeroString(lg-bits));
05452 }
05453 for (++k; k < t_arity; ++k) {
05454 tmp.push_back(t[k]);
05455 }
05456
05457 if (tmp.size() == 1) {
05458 DebugAssert(!found, "Invariant violated");
05459 multKids.push_back(tmp[0]);
05460 }
05461 else if (found) {
05462
05463 concatKids[i] = d_theoryBitvector->newConcatExpr(tmp);
05464 }
05465 else {
05466
05467 concatKids.push_back(d_theoryBitvector->newConcatExpr(tmp));
05468 }
05469 }
05470 }
05471
05472 known_term = known_term % modulus;
05473
05474
05475 if (known_term != 0 && !concatKids.empty()) {
05476 vector<Expr> tmp;
05477 for (i = 0; i < concatKids.size(); ++i) {
05478 Expr t = concatKids[i];
05479 DebugAssert(t.getOpKind() == CONCAT, "Expected CONCAT");
05480 int bits = bv_size;
05481 int size;
05482 bool anyChanged = false;
05483 for (int k = 0; k < t.arity(); ++k) {
05484 size = d_theoryBitvector->BVSize(t[k]);
05485 bool changed = false;
05486 if (known_term != 0 && t[k].getOpKind() == BVCONST) {
05487 Rational high = pow(Rational(bits), Rational(2));
05488 Rational partConst = known_term % high;
05489 if (partConst != 0) {
05490 Rational low = pow(Rational(bits - size), Rational(2));
05491 partConst = partConst - (partConst % low);
05492 if (partConst != 0) {
05493 anyChanged = changed = true;
05494 tmp.push_back(d_theoryBitvector->newBVConstExpr(partConst / low, size));
05495 known_term -= partConst;
05496 }
05497 }
05498 }
05499 if (!changed) {
05500 tmp.push_back(t[k]);
05501 }
05502 bits -= size;
05503 }
05504 if (anyChanged) {
05505 concatKids[i] = d_theoryBitvector->newConcatExpr(tmp);
05506 if (known_term == 0) break;
05507 }
05508 tmp.clear();
05509 }
05510 }
05511
05512
05513 Expr expr_result;
05514
05515
05516 if (multKids.size() == 0 &&
05517 (concatKids.size() > 1 ||
05518 (concatKids.size() == 1 && known_term != 0))) {
05519 expr_result = chopConcat(bv_size, known_term, concatKids);
05520 if (!expr_result.isNull()) return expr_result;
05521 }
05522
05523 if (known_term == 0) {
05524 for (i = 0; i < concatKids.size(); ++i) {
05525 multKids.push_back(concatKids[i]);
05526 }
05527 if (multKids.size() == 0) {
05528 expr_result = d_theoryBitvector->newBVConstExpr( Rational(0), bv_size);
05529 }
05530 else if (multKids.size() == 1) {
05531 expr_result = multKids[0];
05532 }
05533 else {
05534 expr_result = d_theoryBitvector->newBVPlusExpr( bv_size, multKids);
05535 }
05536 }
05537 else {
05538 vector<Expr> sumKids;
05539 sumKids.push_back( d_theoryBitvector->newBVConstExpr( known_term, bv_size));
05540 for (i = 0; i < multKids.size(); ++i) {
05541 sumKids.push_back(multKids[i]);
05542 }
05543 for (i = 0; i < concatKids.size(); ++i) {
05544 sumKids.push_back(concatKids[i]);
05545 }
05546 if (sumKids.size() == 1) {
05547 expr_result = sumKids[0];
05548 }
05549 else {
05550 expr_result = d_theoryBitvector->newBVPlusExpr( bv_size, sumKids);
05551 }
05552 }
05553 return expr_result;
05554 }
05555
05556
05557
05558 Theorem BitvectorTheoremProducer::canonBVPlus( const Expr& e )
05559 {
05560 TRACE("canonBVPlus", "canonBVPlus: {\n ", e.toString(), " --");
05561
05562 if (CHECK_PROOFS)
05563 CHECK_SOUND(e.getOpKind() == BVPLUS,
05564 "BitvectorTheoremProducer::canonBVPlus: input must be a BVPLUS expression" + e.toString());
05565
05566
05567
05568 ExprMap<Rational> sumHashMap;
05569 int bv_size = d_theoryBitvector->BVSize( e );
05570 Rational known_term;
05571
05572
05573 getPlusTerms(e, known_term, sumHashMap);
05574
05575
05576 Expr expr_result = buildPlusTerm(bv_size, known_term, sumHashMap);
05577
05578 Proof pf;
05579 if (withProof()) pf = newPf("canonBVPlus");
05580 Theorem result = newRWTheorem( e, expr_result, Assumptions::emptyAssump(), pf);
05581 TRACE("canonBVPlus", "--> ", expr_result.toString(), "\n}");
05582 return result;
05583 }
05584
05585
05586 Theorem BitvectorTheoremProducer::canonBVUMinus( const Expr& e )
05587 {
05588 if (CHECK_PROOFS)
05589 CHECK_SOUND(e.getOpKind() == BVUMINUS,
05590 "BitvectorTheoremProducer::canonBVUMinus: input must be a BVUMINUS expression" + e.toString());
05591
05592 int bv_size = d_theoryBitvector->BVSize(e);
05593 Rational modulus = pow(Rational(bv_size), Rational(2));
05594 Expr coeff = d_theoryBitvector->newBVConstExpr(modulus-1, bv_size);
05595 Expr res_expr = d_theoryBitvector->newBVMultExpr(bv_size, coeff, e[0]);
05596 Proof pf;
05597 if (withProof()) pf = newPf("canonBVUMinus");
05598 return newRWTheorem(e, res_expr, Assumptions::emptyAssump(), pf);
05599 }
05600
05601
05602
05603
05604
05605
05606
05607
05608 Theorem BitvectorTheoremProducer::processExtract(const Theorem& e, bool& solvedForm)
05609 {
05610 Expr expr = e.getExpr();
05611
05612 if (CHECK_PROOFS) {
05613 CHECK_SOUND(expr.getOpKind() == EQ && expr[0].getOpKind() == EXTRACT,
05614 "BitvectorTheoremProducer::processExtract: invalid input");
05615 CHECK_SOUND(d_theoryBitvector->BVSize(expr[0]) == d_theoryBitvector->BVSize(expr[1]),
05616 "Expected same size");
05617 }
05618
05619 Expr ext = expr[0];
05620 Expr lhs;
05621 Expr rhs = expr[1];
05622 Expr child = ext[0];
05623 int size = d_theoryBitvector->BVSize(child);
05624 int high = d_theoryBitvector->getExtractHi(ext);
05625 int low = d_theoryBitvector->getExtractLow(ext);
05626
05627 DebugAssert(d_theoryBitvector->isLeaf(child), "Expected leaf");
05628 solvedForm = !d_theoryBitvector->isLeafIn(child, rhs);
05629
05630 vector<Expr> terms;
05631 vector<Expr> boundVars;
05632 if (high < size-1) {
05633 terms.push_back(d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(size-1-high)));
05634 boundVars.push_back(terms.back());
05635 }
05636 if (solvedForm) terms.push_back(rhs);
05637 else {
05638 lhs = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(high-low+1));
05639 terms.push_back(lhs);
05640 boundVars.push_back(lhs);
05641 }
05642 if (low > 0) {
05643 terms.push_back(d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(low)));
05644 boundVars.push_back(terms.back());
05645 }
05646 DebugAssert(terms.size() > 1, "Expected at least two terms");
05647 Expr result = child.eqExpr(d_theoryBitvector->newConcatExpr(terms));
05648 if (!solvedForm) result = result && lhs.eqExpr(rhs);
05649 result = d_theoryBitvector->getEM()->newClosureExpr(EXISTS, boundVars, result);
05650 Assumptions a(e);
05651 Proof pf;
05652 if (withProof()) pf = newPf("processExtract");
05653 return newTheorem(result, a, pf);
05654 }
05655
05656 bool BitvectorTheoremProducer::okToSplit(const Expr& e)
05657 {
05658 if (d_theoryBitvector->isLeaf(e)) return true;
05659 switch (e.getOpKind()) {
05660 case BVCONST:
05661 case EXTRACT:
05662 case BVAND:
05663 case BVOR:
05664 case BVXOR:
05665 case BVNEG:
05666 return true;
05667 case BVSHL:
05668 case BVLSHR:
05669 case BVASHR:
05670 case BVPLUS:
05671 case BVMULT:
05672 case BVUDIV:
05673 case BVSDIV:
05674 case BVUREM:
05675 case BVSREM:
05676 case BVSMOD:
05677 return false;
05678 default:
05679 FatalAssert(false, "unexpected kind in okToSplit");
05680 break;
05681 }
05682 return false;
05683 }
05684
05685
05686
05687
05688
05689
05690
05691 Theorem BitvectorTheoremProducer::canonBVEQ( const Expr& e, int maxEffort )
05692 {
05693 TRACE("canonBVEQ", "canonBVEQ: {\n ", e.toString(), " --");
05694 DebugAssert(maxEffort == 3 || maxEffort == 5 || maxEffort == 6,
05695 "Unexpected value for maxEffort");
05696 if(CHECK_PROOFS) {
05697 CHECK_SOUND( e.getOpKind() == EQ,
05698 "BitvectorTheoremProducer::canonBVEQ: expression must be an equation");
05699 CHECK_SOUND(BITVECTOR==e[0].getType().getExpr().getOpKind(),
05700 "input must be a bitvector eqn. \n e = " + e.toString());
05701 }
05702
05703 Expr lhs = e[0];
05704 Expr rhs = e[1];
05705 int bv_size = d_theoryBitvector->BVSize( lhs );
05706
05707
05708 if (lhs.getOpKind() == CONCAT || rhs.getOpKind() == CONCAT) {
05709 Expr::iterator lit, rit;
05710 int lsize, rsize;
05711 if (lhs.getOpKind() == CONCAT) {
05712 lit = e[0].begin();
05713 }
05714 else {
05715 lit = e.begin();
05716 }
05717 if (rhs.getOpKind() == CONCAT) {
05718 rit = e[1].begin();
05719 }
05720 else {
05721 rit = e.begin();
05722 ++rit;
05723 }
05724 int splitSize;
05725 lsize = d_theoryBitvector->BVSize(*lit);
05726 rsize = d_theoryBitvector->BVSize(*rit);
05727 while (true) {
05728 DebugAssert(lsize <= bv_size && rsize <= bv_size, "invariant violated");
05729 if (lsize < rsize) {
05730 if (okToSplit(*rit)) {
05731 splitSize = lsize;
05732 break;
05733 }
05734 else {
05735 ++lit;
05736 lsize += d_theoryBitvector->BVSize(*lit);
05737 }
05738 }
05739 else if (lsize > rsize) {
05740 if (okToSplit(*lit)) {
05741 splitSize = rsize;
05742 break;
05743 }
05744 else {
05745 ++rit;
05746 rsize += d_theoryBitvector->BVSize(*rit);
05747 }
05748 }
05749 else {
05750 splitSize = lsize;
05751 break;
05752 }
05753 }
05754 if (splitSize != bv_size) {
05755 Proof pf;
05756 if (withProof()) pf = newPf("canonBVEQ");
05757 Expr tmp = d_theoryBitvector->newBVExtractExpr(lhs, bv_size-1, bv_size-splitSize);
05758 tmp = tmp.eqExpr(d_theoryBitvector->newBVExtractExpr(rhs, bv_size-1, bv_size-splitSize));
05759 Expr expr_result = d_theoryBitvector->newBVExtractExpr(lhs, bv_size-splitSize-1, 0);
05760 expr_result = expr_result.eqExpr(d_theoryBitvector->newBVExtractExpr(rhs, bv_size-splitSize-1, 0));
05761 expr_result = tmp && expr_result;
05762 TRACE("canonBVEQ", "--> ", expr_result.toString(), "\n}");
05763 return newRWTheorem( e, expr_result, Assumptions::emptyAssump(), pf);
05764 }
05765 }
05766
05767 rhs = d_theoryBitvector->newBVUminusExpr(rhs);
05768 ExprMap<Rational> sumHashMap;
05769 Rational modulus = pow(Rational(bv_size), Rational(2));
05770 Rational known_term;
05771
05772 getPlusTerms(d_theoryBitvector->newBVPlusExpr(bv_size, lhs, rhs), known_term, sumHashMap);
05773
05774
05775
05776
05777
05778
05779
05780
05781
05782
05783
05784
05785
05786
05787 Rational coeff, foundCoeff = 1;
05788 ExprMap<Rational>::iterator j = sumHashMap.begin();
05789 ExprMap<Rational>::iterator fixCoeff = j;
05790 Expr xor_leaf, leaf, foundterm;
05791 unsigned xor_idx=0, xor_size=0;
05792 int priority, size, foundpriority = 7;
05793 bool isExtract;
05794 for(; j != sumHashMap.end(); ++j) {
05795 Expr t = (*j).first;
05796 coeff = (*j).second;
05797 size = d_theoryBitvector->BVSize(t);
05798 if (j == fixCoeff) {
05799 coeff = (*j).second = mod(coeff, modulus);
05800 ++fixCoeff;
05801 }
05802 if (coeff == 0) continue;
05803
05804 priority = 7;
05805 isExtract = false;
05806 if (coeff % 2 == 1) {
05807 if (d_theoryBitvector->isLeaf(t)) {
05808 if (size == bv_size) {
05809 leaf = t; priority = 1;
05810 } else if (size > bv_size) {
05811 isExtract = true;
05812 leaf = t; priority = 3;
05813 } else {
05814 leaf = t; priority = 4;
05815 }
05816 } else if (t.getOpKind() == EXTRACT &&
05817 d_theoryBitvector->isLeaf(t[0])) {
05818 isExtract = true;
05819 if (size >= bv_size) {
05820 leaf = t[0]; priority = 3;
05821 } else {
05822 leaf = t[0]; priority = 4;
05823 }
05824 } else if (t.getOpKind() == BVXOR && size == bv_size) {
05825 if (foundpriority == 2) continue;
05826 xor_idx = 0;
05827 xor_size = t.arity();
05828 for (xor_idx = 0; xor_idx < xor_size; ++xor_idx) {
05829 if (!d_theoryBitvector->isLeaf(t[xor_idx])) {
05830 continue;
05831 }
05832 unsigned l = 0;
05833 for (; l < xor_size; ++l) {
05834 if (l == xor_idx) continue;
05835 if (d_theoryBitvector->isLeafIn(t[xor_idx], t[l])) break;
05836 }
05837 if (l < xor_size) continue;
05838 break;
05839 }
05840 if (xor_idx < xor_size) {
05841 leaf = t[xor_idx];
05842 xor_leaf = leaf;
05843 priority = 2;
05844 }
05845 else {
05846 leaf = t; priority = 6;
05847 }
05848 }
05849 else {
05850 leaf = t; priority = 6;
05851 }
05852 } else if (maxEffort >= 5) {
05853 if (d_theoryBitvector->isLeaf(t)) {
05854 leaf = t; priority = 5;
05855 } else if (t.getOpKind() == EXTRACT &&
05856 d_theoryBitvector->isLeaf(t[0])) {
05857 isExtract = true;
05858 leaf = t[0]; priority = 5;
05859 }
05860 }
05861
05862 if (priority < foundpriority) {
05863 if (priority < 6) {
05864 ExprMap<Rational>::iterator k = sumHashMap.begin();
05865 while (k != sumHashMap.end()) {
05866 if (j == k) {
05867 ++k; continue;
05868 }
05869 if (k == fixCoeff) {
05870 (*k).second = mod((*k).second, modulus);
05871 ++fixCoeff;
05872 }
05873 if ((*k).second == 0) {
05874 ++k; continue;
05875 }
05876 if (!isExtract && d_theoryBitvector->isLeafIn(leaf, (*k).first)) {
05877 if (priority == 2) {
05878
05879 for (++xor_idx; xor_idx < xor_size; ++xor_idx) {
05880 if (!d_theoryBitvector->isLeaf(t[xor_idx])) {
05881 continue;
05882 }
05883 unsigned l = 0;
05884 for (; l < xor_size; ++l) {
05885 if (l == xor_idx) continue;
05886 if (d_theoryBitvector->isLeafIn(t[xor_idx], t[l])) break;
05887 }
05888 if (l < xor_size) continue;
05889 break;
05890 }
05891 if (xor_idx < xor_size) {
05892
05893 leaf = t[xor_idx];
05894 xor_leaf = leaf;
05895 k = sumHashMap.begin();
05896 continue;
05897 }
05898 }
05899
05900 break;
05901 }
05902 ++k;
05903 }
05904 if (k == sumHashMap.end()) {
05905 foundpriority = priority;
05906 foundterm = t;
05907 if (coeff == 1 || priority == 5) foundCoeff = 1;
05908 else foundCoeff = d_theoryBitvector->multiplicative_inverse(coeff, bv_size);
05909 if (priority == 1) break;
05910 }
05911 }
05912 if (foundpriority > 6 && priority != 5) {
05913 foundpriority = 6;
05914 foundterm = t;
05915 if (coeff == 1) foundCoeff = 1;
05916 else foundCoeff = d_theoryBitvector->multiplicative_inverse(coeff, bv_size);
05917 }
05918 }
05919 }
05920
05921 bool solving = (foundpriority <= maxEffort);
05922
05923 if (foundpriority == 7) {
05924
05925 if (known_term % 2 == 1) {
05926 Proof pf;
05927 if (withProof()) pf = newPf("canonBVEQ");
05928 TRACE("canonBVEQ", "--> ", d_theoryBitvector->falseExpr().toString(), "\n}");
05929 return newRWTheorem(e, d_theoryBitvector->falseExpr(), Assumptions::emptyAssump(), pf);
05930 }
05931 else foundCoeff = foundCoeff / Rational(2);
05932 if (bv_size > 1) {
05933 bv_size = bv_size - 1;
05934 modulus = pow(Rational(bv_size), Rational(2));
05935 }
05936 }
05937 else if (!solving && (e[1] == d_theoryBitvector->newBVZeroString(bv_size))) {
05938
05939
05940 TRACE("canonBVEQ", "--> ", e, "\n}");
05941 return newReflTheorem(e);
05942 }
05943
05944 Rational solveCoeff = 0;
05945
05946
05947 if (solving || foundCoeff != 1) {
05948 known_term = (known_term * foundCoeff) % modulus;
05949 if (solving && known_term != 0)
05950 known_term = modulus - known_term;
05951 for(j = sumHashMap.begin(); j != sumHashMap.end(); ++j) {
05952 coeff = (*j).second;
05953 if (coeff == 0) continue;
05954 (*j).second = (coeff * foundCoeff) % modulus;
05955 if (solving) {
05956 if ((*j).first == foundterm) {
05957
05958 solveCoeff = (*j).second;
05959 (*j).second = 0;
05960 }
05961 else {
05962 (*j).second = modulus - (*j).second;
05963 }
05964 }
05965 }
05966 }
05967
05968
05969 Expr plusTerm = buildPlusTerm(bv_size, known_term, sumHashMap);
05970
05971 Expr new_lhs, new_rhs, expr_result;
05972
05973 if (solving) {
05974 DebugAssert(solveCoeff != 0, "Expected solveCoeff != 0");
05975 if (foundpriority == 6 && d_theoryBitvector->BVSize(foundterm) < bv_size) {
05976
05977 foundterm = d_theoryBitvector->pad(bv_size, foundterm);
05978 }
05979 switch (foundpriority) {
05980 case 1:
05981
05982
05983 case 6:
05984
05985
05986 DebugAssert(solveCoeff == 1, "Expected coeff = 1");
05987 new_lhs = foundterm;
05988 new_rhs = plusTerm;
05989 break;
05990 case 2: {
05991
05992 DebugAssert(solveCoeff == 1, "Expected coeff = 1");
05993 vector<Expr> rhsTerms;
05994 rhsTerms.push_back(plusTerm);
05995 for (unsigned l = 0; l < xor_size; ++l) {
05996 if (l == xor_idx) continue;
05997 rhsTerms.push_back(foundterm[l]);
05998 }
05999 new_lhs = xor_leaf;
06000 new_rhs = d_theoryBitvector->newBVXorExpr(rhsTerms);
06001 break;
06002 }
06003 case 3:
06004
06005
06006 DebugAssert(solveCoeff == 1, "Expected coeff = 1");
06007 if (d_theoryBitvector->BVSize(foundterm) > bv_size) {
06008 if (foundterm.getOpKind() == EXTRACT) {
06009 int diff = d_theoryBitvector->BVSize(foundterm) - bv_size;
06010 int high = d_theoryBitvector->getExtractHi(foundterm);
06011 int low = d_theoryBitvector->getExtractLow(foundterm);
06012 foundterm = d_theoryBitvector->newBVExtractExpr(foundterm[0], high - diff, low);
06013 }
06014 else {
06015 foundterm = d_theoryBitvector->newBVExtractExpr(foundterm, bv_size-1, 0);
06016 }
06017 }
06018 new_lhs = foundterm;
06019 new_rhs = plusTerm;
06020 break;
06021 case 4: {
06022
06023
06024 DebugAssert(solveCoeff == 1, "Expected coeff = 1");
06025 int foundtermsize = d_theoryBitvector->BVSize(foundterm);
06026 DebugAssert(foundtermsize < bv_size, "Expected undersized term");
06027 new_rhs = d_theoryBitvector->newBVExtractExpr(plusTerm, foundtermsize-1, 0);
06028 expr_result = foundterm.eqExpr(new_rhs);
06029 new_rhs = d_theoryBitvector->newBVExtractExpr(plusTerm, bv_size-1, foundtermsize);
06030 new_lhs = d_theoryBitvector->newBVZeroString(bv_size - foundtermsize);
06031 expr_result = expr_result && new_lhs.eqExpr(new_rhs);
06032 break;
06033 }
06034 case 5: {
06035
06036
06037 int lg = 0;
06038 for (; solveCoeff % 2 == 0; solveCoeff = solveCoeff / 2, ++lg);
06039 new_lhs = d_theoryBitvector->newBVConstExpr(solveCoeff, bv_size-lg);
06040 new_lhs = d_theoryBitvector->newBVMultPadExpr(bv_size-lg, new_lhs, foundterm);
06041 new_rhs = d_theoryBitvector->newBVExtractExpr(plusTerm, bv_size-1, lg);
06042 expr_result = new_lhs.eqExpr(new_rhs);
06043 new_lhs = d_theoryBitvector->newBVZeroString(lg);
06044 new_rhs = d_theoryBitvector->newBVExtractExpr(plusTerm, lg - 1, 0);
06045 expr_result = expr_result && new_lhs.eqExpr(new_rhs);
06046 break;
06047 }
06048 default:
06049 FatalAssert(false, "Expected priority < 7");
06050 break;
06051 }
06052 }
06053 else {
06054 new_lhs = plusTerm;
06055 new_rhs = d_theoryBitvector->newBVZeroString(bv_size);
06056 }
06057
06058 if (expr_result.isNull()) {
06059 if ( new_lhs == new_rhs) {
06060 expr_result = d_theoryBitvector->trueExpr();
06061 }
06062 else if ( new_lhs >= new_rhs) {
06063 expr_result = Expr(EQ, new_lhs, new_rhs);
06064 }
06065 else {
06066 expr_result = Expr(EQ, new_rhs, new_lhs);
06067 }
06068 }
06069
06070 Proof pf;
06071 if (withProof()) pf = newPf("canonBVEQ");
06072 TRACE("canonBVEQ", "--> ", expr_result.toString(), "\n}");
06073 Theorem result = newRWTheorem( e, expr_result, Assumptions::emptyAssump(), pf);
06074 return result;
06075 }
06076
06077
06078
06079
06080 Theorem BitvectorTheoremProducer::zeroExtendRule(const Expr& e) {
06081 if(CHECK_PROOFS) {
06082 CHECK_SOUND(BITVECTOR==e.getType().getExpr().getOpKind(),
06083 "input must be a bitvector. \n e = " + e.toString());
06084 CHECK_SOUND(BVZEROEXTEND == e.getOpKind(),
06085 "input must be BVZEROEXTEND(e).\n e = " + e.toString());
06086 }
06087
06088 int extendLen = d_theoryBitvector->getBVIndex(e);
06089 Expr res;
06090 if (extendLen == 0) {
06091 res = e[0];
06092 }
06093 else {
06094 Expr extend = d_theoryBitvector->newBVZeroString(extendLen);
06095 res = d_theoryBitvector->newConcatExpr(extend, e[0]);
06096 }
06097
06098 Proof pf;
06099 if(withProof())
06100 pf = newPf("zero_extend_rule");
06101 Theorem result(newRWTheorem(e, res, Assumptions::emptyAssump(), pf));
06102 return result;
06103 }
06104
06105
06106
06107
06108 Theorem BitvectorTheoremProducer::repeatRule(const Expr& e) {
06109 if(CHECK_PROOFS) {
06110 CHECK_SOUND(BITVECTOR==e.getType().getExpr().getOpKind(),
06111 "input must be a bitvector. \n e = " + e.toString());
06112 CHECK_SOUND(BVREPEAT == e.getOpKind(),
06113 "input must be BVREPEAT(e).\n e = " + e.toString());
06114 CHECK_SOUND(d_theoryBitvector->getBVIndex(e) > 0,
06115 "Expected positive repeat value");
06116 }
06117
06118 int repeatVal = d_theoryBitvector->getBVIndex(e);
06119 Expr res;
06120 if (repeatVal == 1) {
06121 res = e[0];
06122 }
06123 else {
06124 vector<Expr> kids;
06125 for (int i = 0; i < repeatVal; ++i) {
06126 kids.push_back(e[0]);
06127 }
06128 res = d_theoryBitvector->newConcatExpr(kids);
06129 }
06130
06131 Proof pf;
06132 if(withProof())
06133 pf = newPf("repeat_rule");
06134 Theorem result(newRWTheorem(e, res, Assumptions::emptyAssump(), pf));
06135 return result;
06136 }
06137
06138
06139
06140
06141 Theorem BitvectorTheoremProducer::rotlRule(const Expr& e) {
06142 if(CHECK_PROOFS) {
06143 CHECK_SOUND(BITVECTOR==e.getType().getExpr().getOpKind(),
06144 "input must be a bitvector. \n e = " + e.toString());
06145 CHECK_SOUND(BVROTL == e.getOpKind(),
06146 "input must be BVROTL(e).\n e = " + e.toString());
06147 }
06148
06149 int bvsize = d_theoryBitvector->BVSize(e);
06150 int rotation = d_theoryBitvector->getBVIndex(e);
06151 rotation = rotation % bvsize;
06152 Expr res;
06153 if (rotation == 0) {
06154 res = e[0];
06155 }
06156 else {
06157 Expr hi = d_theoryBitvector->newBVExtractExpr(e[0],bvsize-1-rotation,0);
06158 Expr low = d_theoryBitvector->newBVExtractExpr(e[0],bvsize-1, bvsize-rotation);
06159 res = d_theoryBitvector->newConcatExpr(hi, low);
06160 }
06161
06162 Proof pf;
06163 if(withProof())
06164 pf = newPf("rotl_rule");
06165 Theorem result(newRWTheorem(e, res, Assumptions::emptyAssump(), pf));
06166 return result;
06167 }
06168
06169
06170
06171
06172 Theorem BitvectorTheoremProducer::rotrRule(const Expr& e) {
06173 if(CHECK_PROOFS) {
06174 CHECK_SOUND(BITVECTOR==e.getType().getExpr().getOpKind(),
06175 "input must be a bitvector. \n e = " + e.toString());
06176 CHECK_SOUND(BVROTR == e.getOpKind(),
06177 "input must be BVROTR(e).\n e = " + e.toString());
06178 }
06179
06180 int bvsize = d_theoryBitvector->BVSize(e);
06181 int rotation = d_theoryBitvector->getBVIndex(e);
06182 rotation = rotation % bvsize;
06183 Expr res;
06184 if (rotation == 0) {
06185 res = e[0];
06186 }
06187 else {
06188 Expr hi = d_theoryBitvector->newBVExtractExpr(e[0],rotation-1,0);
06189 Expr low = d_theoryBitvector->newBVExtractExpr(e[0],bvsize-1, rotation);
06190 res = d_theoryBitvector->newConcatExpr(hi, low);
06191 }
06192
06193 Proof pf;
06194 if(withProof())
06195 pf = newPf("rotr_rule");
06196 Theorem result(newRWTheorem(e, res, Assumptions::emptyAssump(), pf));
06197 return result;
06198 }
06199
06200 Theorem BitvectorTheoremProducer::bvURemConst(const Expr& remExpr) {
06201 const Expr& a = remExpr[0];
06202 const Expr& b = remExpr[1];
06203 int size = d_theoryBitvector->BVSize(remExpr);
06204
06205 Rational a_value = d_theoryBitvector->computeBVConst(a);
06206 Rational b_value = d_theoryBitvector->computeBVConst(b);
06207
06208 Expr rem;
06209
06210 if (b_value != 0) {
06211 Rational rem_value = a_value - floor(a_value / b_value)*b_value;
06212 rem = d_theoryBitvector->newBVConstExpr(rem_value, size);
06213 } else {
06214 static int div_by_zero_count = 0;
06215 div_by_zero_count ++;
06216 char var_name[10000];
06217 sprintf(var_name, "mod_by_zero_const_%d", div_by_zero_count);
06218 rem = d_theoryBitvector->newVar(var_name, remExpr.getType());
06219 }
06220
06221 Proof pf;
06222 if (withProof())
06223 pf = newPf("bvUDivConst");
06224
06225 return newRWTheorem(remExpr, rem, Assumptions::emptyAssump(), pf);
06226 }
06227
06228 Theorem BitvectorTheoremProducer::bvURemRewrite(const Expr& remExpr) {
06229 Expr a = remExpr[0];
06230 Expr b = remExpr[1];
06231 int size = d_theoryBitvector->BVSize(remExpr);
06232 Expr div = d_theoryBitvector->newBVUDivExpr(a, b);
06233
06234 Expr rem = d_theoryBitvector->newBVSubExpr(a, d_theoryBitvector->newBVMultExpr(size, div, b));
06235 Proof pf;
06236 if (withProof())
06237 pf = newPf("bvURemRewrite", remExpr);
06238 return newRWTheorem(remExpr, rem, Assumptions::emptyAssump(), pf);
06239 }
06240
06241
06242 Theorem BitvectorTheoremProducer::bvUDivConst(const Expr& divExpr)
06243 {
06244 const Expr& a = divExpr[0];
06245 const Expr& b = divExpr[1];
06246 int size = d_theoryBitvector->BVSize(divExpr);
06247
06248 Rational a_value = d_theoryBitvector->computeBVConst(a);
06249 Rational b_value = d_theoryBitvector->computeBVConst(b);
06250
06251 Expr div;
06252
06253 if (b_value != 0) {
06254 Rational div_value = floor(a_value / b_value);
06255 div = d_theoryBitvector->newBVConstExpr(div_value, size);
06256 } else {
06257 static int div_by_zero_count = 0;
06258 div_by_zero_count ++;
06259 char var_name[10000];
06260 sprintf(var_name, "div_by_zero_const_%d", div_by_zero_count);
06261 div = d_theoryBitvector->newVar(var_name, divExpr.getType());
06262 }
06263
06264 Proof pf;
06265 if (withProof())
06266 pf = newPf("bvUDivConst");
06267
06268 return newRWTheorem(divExpr, div, Assumptions::emptyAssump(), pf);
06269 }
06270
06271 Theorem BitvectorTheoremProducer::bvUDivTheorem(const Expr& divExpr)
06272 {
06273 int size = d_theoryBitvector->BVSize(divExpr);
06274
06275 if(CHECK_PROOFS) {
06276 CHECK_SOUND(BITVECTOR == divExpr.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + divExpr.toString());
06277 CHECK_SOUND(BVUDIV == divExpr.getOpKind(),"input must be BVUDIV(e).\n e = " + divExpr.toString());
06278 }
06279
06280 const Expr a = divExpr[0];
06281 const Expr b = divExpr[1];
06282
06283
06284 Type type = divExpr.getType();
06285 Expr div = d_theoryBitvector->getEM()->newBoundVarExpr(type);
06286 Expr mod = d_theoryBitvector->getEM()->newBoundVarExpr(type);
06287 vector<Expr> boundVars;
06288 boundVars.push_back(div);
06289 boundVars.push_back(mod);
06290
06291 vector<Expr> assertions;
06292 Expr pad = d_theoryBitvector->newBVConstExpr(Rational(0), size);
06293 Expr a_expanded = d_theoryBitvector->newConcatExpr(pad, a);
06294 Expr b_expanded = d_theoryBitvector->newConcatExpr(pad, b);
06295 Expr div_expanded = d_theoryBitvector->newConcatExpr(pad, div);
06296 Expr mod_expanded = d_theoryBitvector->newConcatExpr(pad, mod);
06297 assertions.push_back(a_expanded.eqExpr(
06298 d_theoryBitvector->newBVPlusExpr(2*size,
06299 d_theoryBitvector->newBVMultExpr(2*size, b_expanded, div_expanded),
06300 mod_expanded
06301 )
06302 )
06303 );
06304 assertions.push_back(d_theoryBitvector->newBVLTExpr(mod, b));
06305
06306 Expr non_zero_div = andExpr(assertions);
06307
06308 Expr complete_div = (b.eqExpr(d_theoryBitvector->newBVConstExpr(Rational(0), size))).negate().impExpr(non_zero_div);
06309
06310 complete_div = divExpr.eqExpr(div).andExpr(complete_div);
06311
06312 Expr result = d_theoryBitvector->getEM()->newClosureExpr(EXISTS, boundVars, complete_div);
06313
06314
06315 Proof pf;
06316 if (withProof())
06317 pf = newPf("bvUDiv");
06318
06319
06320 return newTheorem(result, Assumptions::emptyAssump(), pf);
06321 }
06322
06323 Theorem BitvectorTheoremProducer::bitblastBVMult(const std::vector<Theorem>& a_bits, const std::vector<Theorem>& b_bits,
06324 const Expr& a_times_b, std::vector<Theorem>& output_bits)
06325 {
06326 if(CHECK_PROOFS) {
06327 CHECK_SOUND(a_times_b.arity() == 2, "must be a binary multiplication");
06328 CHECK_SOUND(BITVECTOR == a_times_b.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + a_times_b.toString());
06329 CHECK_SOUND(BVMULT == a_times_b.getOpKind(),"input must be BVMULT(e).\n e = " + a_times_b.toString());
06330 CHECK_SOUND(a_bits.size() == b_bits.size(), "given bit expansions of different size");
06331 CHECK_SOUND((int) a_bits.size() <= d_theoryBitvector->BVSize(a_times_b), "the expansion is bigger than the multiplier");
06332 }
06333
06334 int size = a_bits.size();
06335 Expr falseExpr = d_theoryBitvector->falseExpr();
06336
06337
06338
06339
06340
06341
06342
06343
06344
06345
06346
06347
06348
06349
06350
06351
06352
06353
06354
06355
06356
06357
06358
06359
06360 vector<Expr> sum_bits;
06361 vector<Expr> carry_bits;
06362
06363
06364 int a_bit, b_bit;
06365 for (a_bit = size - 1; a_bit >= 0 && a_bits[a_bit].getRHS() == falseExpr; a_bit --);
06366 for (b_bit = size - 1; b_bit >= 0 && b_bits[b_bit].getRHS() == falseExpr; b_bit --);
06367
06368
06369
06370 int new_size = size;
06371 if (a_bit + b_bit + 2 < new_size) new_size = a_bit + b_bit + 2;
06372
06373
06374 for (int i = 0; i < new_size; i ++) {
06375 sum_bits.push_back(a_bits[i].getRHS().andExpr(b_bits[0].getRHS()));
06376 carry_bits.push_back(d_theoryBitvector->falseExpr());
06377 }
06378
06379
06380 Expr carry = d_theoryBitvector->falseExpr();
06381 for (int row = 1; row < new_size; row ++) {
06382 for (int bit = new_size-1; bit >= row; bit --) {
06383 Expr m = a_bits[bit-row].getRHS().andExpr(b_bits[row].getRHS());
06384 Expr sum = sum_bits[bit].iffExpr(m).iffExpr(carry_bits[bit - 1]);
06385 Expr carry = sum_bits[bit].andExpr(m).orExpr(carry_bits[bit - 1].andExpr(sum_bits[bit].orExpr(m)));
06386 sum_bits[bit] = sum;
06387 carry_bits[bit] = carry;
06388 }
06389
06390 carry = carry.orExpr(carry_bits[new_size - 1]);
06391 }
06392
06393
06394 for (int bit = 0; bit < size; bit ++) {
06395 Proof pf;
06396 if (withProof()) {
06397 pf = newPf("bitblastBVMult", a_times_b, rat(bit));
06398 }
06399 output_bits.push_back(newRWTheorem(d_theoryBitvector->newBoolExtractExpr(a_times_b, bit), bit < new_size ? sum_bits[bit] : falseExpr, Assumptions::emptyAssump(), pf));
06400 }
06401
06402 Theorem carry_thm;
06403 return carry_thm;
06404 }
06405
06406 Theorem BitvectorTheoremProducer::bitblastBVPlus(const std::vector<Theorem>& a_bits, const std::vector<Theorem>& b_bits,
06407 const Expr& a_plus_b, std::vector<Theorem>& output_bits)
06408 {
06409 if(CHECK_PROOFS) {
06410 CHECK_SOUND(a_plus_b.arity() == 2, "must be a binary addition");
06411 CHECK_SOUND(BITVECTOR == a_plus_b.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + a_plus_b.toString());
06412 CHECK_SOUND(BVPLUS == a_plus_b.getOpKind(),"input must be BVPLUS(e).\n e = " + a_plus_b.toString());
06413 CHECK_SOUND(a_bits.size() == b_bits.size(), "given bit expansions of different size");
06414 CHECK_SOUND((int) a_bits.size() <= d_theoryBitvector->BVSize(a_plus_b), "the expansion is bigger than the multiplier");
06415 }
06416
06417 int size = a_bits.size();
06418
06419 if (CHECK_PROOFS) {
06420 Expr a = a_plus_b[0];
06421 for (int bit = 0; bit < size; bit++) {
06422 Theorem bit_i = a_bits[bit];
06423 Expr bit_extract = d_theoryBitvector->newBoolExtractExpr(a, bit);
06424 CHECK_SOUND(bit_extract == bit_i.getLHS(), "not the right bit theorems");
06425 }
06426 Expr b = a_plus_b[1];
06427 for (int bit = 0; bit < size; bit++) {
06428 Theorem bit_i = b_bits[bit];
06429 Expr bit_extract = d_theoryBitvector->newBoolExtractExpr(b, bit);
06430 CHECK_SOUND(bit_extract == bit_i.getLHS(), "not the right bit theorems");
06431 }
06432 }
06433
06434 vector<Expr> sum_bits;
06435
06436 Expr carry = d_theoryBitvector->falseExpr();
06437 for (int i = 0; i < size; i ++)
06438 {
06439 Expr a_i = a_bits[i].getRHS();
06440 Expr b_i = b_bits[i].getRHS();
06441 sum_bits.push_back(a_i.iffExpr(b_i).iffExpr(carry));
06442 carry = a_i.andExpr(b_i).orExpr(carry.andExpr(a_i.orExpr(b_i)));
06443 }
06444
06445
06446 for (int bit = 0; bit < size; bit ++) {
06447 Proof pf;
06448 if (withProof()) {
06449 pf = newPf("bitblastBVPlus", a_plus_b, rat(bit));
06450 }
06451 output_bits.push_back(newRWTheorem(d_theoryBitvector->newBoolExtractExpr(a_plus_b, bit), sum_bits[bit], Assumptions::emptyAssump(), pf));
06452 }
06453
06454 Theorem carry_thm;
06455 return carry_thm;
06456 }
06457
06458
06459
06460
06461 Theorem BitvectorTheoremProducer::bvSDivRewrite(const Expr& sDivExpr)
06462 {
06463 if(CHECK_PROOFS) {
06464 CHECK_SOUND(BITVECTOR == sDivExpr.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + sDivExpr.toString());
06465 CHECK_SOUND(BVSDIV == sDivExpr.getOpKind(),"input must be BVSDIV(e).\n e = " + sDivExpr.toString());
06466 }
06467
06468 int m = d_theoryBitvector->BVSize(sDivExpr);
06469
06470 Proof pf;
06471 if (withProof()) pf = newPf("bvSDivRewrite", sDivExpr);
06472
06473
06474
06475
06476
06477
06478
06479
06480
06481
06482
06483
06484 Expr s = sDivExpr[0];
06485 Expr t = sDivExpr[1];
06486
06487 Expr s_neg = d_theoryBitvector->newBVUminusExpr(s);
06488 Expr t_neg = d_theoryBitvector->newBVUminusExpr(t);
06489
06490 Expr msb_s = d_theoryBitvector->newBVExtractExpr(s, m-1, m-1);
06491 Expr msb_t = d_theoryBitvector->newBVExtractExpr(t, m-1, m-1);
06492
06493 Expr bit0 = d_theoryBitvector->newBVConstExpr(Rational(0), 1);
06494 Expr bit1 = d_theoryBitvector->newBVConstExpr(Rational(1), 1);
06495
06496 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0));
06497 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0));
06498 Expr cond3 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit1));
06499
06500 Expr result = cond1.iteExpr(
06501 d_theoryBitvector->newBVUDivExpr(s, t),
06502 cond2.iteExpr(
06503 d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVUDivExpr(s_neg, t)),
06504 cond3.iteExpr(
06505 d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVUDivExpr(s, t_neg)),
06506 d_theoryBitvector->newBVUDivExpr(s_neg, t_neg)
06507 )
06508 )
06509 );
06510
06511 return newRWTheorem(sDivExpr, result, Assumptions::emptyAssump(), pf);
06512 }
06513
06514
06515
06516
06517 Theorem BitvectorTheoremProducer::bvSRemRewrite(const Expr& sRemExpr)
06518 {
06519 if(CHECK_PROOFS) {
06520 CHECK_SOUND(BITVECTOR == sRemExpr.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + sRemExpr.toString());
06521 CHECK_SOUND(BVSREM == sRemExpr.getOpKind(),"input must be BVSDIV(e).\n e = " + sRemExpr.toString());
06522 }
06523
06524 int m = d_theoryBitvector->BVSize(sRemExpr);
06525
06526 Proof pf;
06527 if (withProof()) pf = newPf("bvSRemRewrite", sRemExpr);
06528
06529
06530
06531
06532
06533
06534
06535
06536
06537
06538
06539
06540 Expr s = sRemExpr[0];
06541 Expr t = sRemExpr[1];
06542
06543 Expr s_neg = d_theoryBitvector->newBVUminusExpr(s);
06544 Expr t_neg = d_theoryBitvector->newBVUminusExpr(t);
06545
06546 Expr msb_s = d_theoryBitvector->newBVExtractExpr(s, m-1, m-1);
06547 Expr msb_t = d_theoryBitvector->newBVExtractExpr(t, m-1, m-1);
06548
06549 Expr bit0 = d_theoryBitvector->newBVConstExpr(Rational(0), 1);
06550 Expr bit1 = d_theoryBitvector->newBVConstExpr(Rational(1), 1);
06551
06552 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0));
06553 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0));
06554 Expr cond3 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit1));
06555
06556 Expr result = cond1.iteExpr(
06557 d_theoryBitvector->newBVURemExpr(s, t),
06558 cond2.iteExpr(
06559 d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVURemExpr(s_neg, t)),
06560 cond3.iteExpr(
06561 d_theoryBitvector->newBVURemExpr(s, t_neg),
06562 d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVURemExpr(s_neg, t_neg))
06563 )
06564 )
06565 );
06566
06567 return newRWTheorem(sRemExpr, result, Assumptions::emptyAssump(), pf);
06568 }
06569
06570
06571
06572
06573 Theorem BitvectorTheoremProducer::bvSModRewrite(const Expr& sModExpr)
06574 {
06575 if(CHECK_PROOFS) {
06576 CHECK_SOUND(BITVECTOR == sModExpr.getType().getExpr().getOpKind(), "input must be a bitvector. \n e = " + sModExpr.toString());
06577 CHECK_SOUND(BVSMOD == sModExpr.getOpKind(),"input must be BVSDIV(e).\n e = " + sModExpr.toString());
06578 }
06579
06580 int m = d_theoryBitvector->BVSize(sModExpr);
06581
06582 Proof pf;
06583 if (withProof()) pf = newPf("bvSModRewrite", sModExpr);
06584
06585
06586
06587
06588
06589
06590
06591
06592
06593
06594
06595
06596 Expr s = sModExpr[0];
06597 Expr t = sModExpr[1];
06598
06599 Expr s_neg = d_theoryBitvector->newBVUminusExpr(s);
06600 Expr t_neg = d_theoryBitvector->newBVUminusExpr(t);
06601
06602 Expr msb_s = d_theoryBitvector->newBVExtractExpr(s, m-1, m-1);
06603 Expr msb_t = d_theoryBitvector->newBVExtractExpr(t, m-1, m-1);
06604
06605 Expr bit0 = d_theoryBitvector->newBVConstExpr(Rational(0), 1);
06606 Expr bit1 = d_theoryBitvector->newBVConstExpr(Rational(1), 1);
06607
06608 Expr cond1 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit0));
06609 Expr cond2 = msb_s.eqExpr(bit1).andExpr(msb_t.eqExpr(bit0));
06610 Expr cond3 = msb_s.eqExpr(bit0).andExpr(msb_t.eqExpr(bit1));
06611
06612 Expr result = cond1.iteExpr(
06613 d_theoryBitvector->newBVURemExpr(s, t),
06614 cond2.iteExpr(
06615 d_theoryBitvector->newBVPlusExpr(m, d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVURemExpr(s_neg, t)), t),
06616 cond3.iteExpr(
06617 d_theoryBitvector->newBVPlusExpr(m, d_theoryBitvector->newBVURemExpr(s, t_neg), t),
06618 d_theoryBitvector->newBVUminusExpr(d_theoryBitvector->newBVURemExpr(s_neg, t_neg))
06619 )
06620 )
06621 );
06622
06623 return newRWTheorem(sModExpr, result, Assumptions::emptyAssump(), pf);
06624 }
06625
06626 Theorem BitvectorTheoremProducer::zeroBVOR(const Expr& orEqZero)
06627 {
06628 if(CHECK_PROOFS) {
06629 CHECK_SOUND(orEqZero.isEq(), "input must be an equality. \n e = " + orEqZero.toString());
06630 CHECK_SOUND(orEqZero[0].getKind() == BVOR, "left-hand side must be a bitwise or. \n e = " + orEqZero.toString());
06631 CHECK_SOUND(orEqZero[1].getKind() == BVCONST, "right-hand side must be a constant or. \n e = " + orEqZero.toString());
06632 CHECK_SOUND(d_theoryBitvector->computeBVConst(orEqZero[1]) == 0, "right-hand side must be 0. \n e = " + orEqZero.toString());
06633 }
06634
06635 vector<Expr> conjuncts;
06636
06637 for (int disjunct = 0; disjunct < orEqZero[0].arity(); disjunct ++)
06638 conjuncts.push_back(orEqZero[0][disjunct].eqExpr(orEqZero[1]));
06639
06640 Expr result = andExpr(conjuncts);
06641
06642 Proof pf;
06643 if (withProof()) pf = newPf("zeroBVOR", orEqZero);
06644
06645 return newRWTheorem(orEqZero, result, Assumptions::emptyAssump(), pf);
06646 }
06647
06648 Theorem BitvectorTheoremProducer::oneBVAND(const Expr& andEqOne)
06649 {
06650 if(CHECK_PROOFS) {
06651 CHECK_SOUND(andEqOne.isEq(), "input must be an equality. \n e = " + andEqOne.toString());
06652 CHECK_SOUND(andEqOne[0].getKind() == BVAND, "left-hand side must be a bitwise and. \n e = " + andEqOne.toString());
06653 CHECK_SOUND(andEqOne[1].getKind() == BVCONST, "right-hand side must be a constant or. \n e = " + andEqOne.toString());
06654 CHECK_SOUND(d_theoryBitvector->computeBVConst(andEqOne[1]) == pow(d_theoryBitvector->BVSize(andEqOne[1]), 2) - 1, "right-hand side must be 1^n. \n e = " + andEqOne.toString());
06655 }
06656
06657 vector<Expr> conjuncts;
06658
06659 for (int conjunct = 0; conjunct < andEqOne[0].arity(); conjunct ++)
06660 conjuncts.push_back(andEqOne[0][conjunct].eqExpr(andEqOne[1]));
06661
06662 Expr result = andExpr(conjuncts);
06663
06664 Proof pf;
06665 if (withProof()) pf = newPf("oneBVAND", andEqOne);
06666
06667 return newRWTheorem(andEqOne, result, Assumptions::emptyAssump(), pf);
06668 }
06669
06670 Theorem BitvectorTheoremProducer::constEq(const Expr& eq)
06671 {
06672 if(CHECK_PROOFS) {
06673 CHECK_SOUND(eq.isEq(), "input must be an equality. \n e = " + eq.toString());
06674 CHECK_SOUND(eq[0].getKind() == BVCONST, "left-hand side must be a constant. \n e = " + eq.toString());
06675 CHECK_SOUND(eq[1].getKind() == BVCONST, "right-hand side must be a constant. \n e = " + eq.toString());
06676 }
06677
06678 Expr result = eq[0] == eq[1] ? d_theoryBitvector->trueExpr() : d_theoryBitvector->falseExpr();
06679
06680 Proof pf;
06681 if (withProof()) pf = newPf("constEq", eq);
06682
06683 return newRWTheorem(eq, result, Assumptions::emptyAssump(), pf);
06684 }
06685
06686 bool BitvectorTheoremProducer::solveExtractOverlapApplies(const Expr& eq)
06687 {
06688
06689 if (eq[0].getOpKind() != EXTRACT) return false;
06690 if (eq[1].getOpKind() != EXTRACT) return false;
06691
06692 if (eq[0][0] != eq[1][0]) return false;
06693
06694 int i = d_theoryBitvector->getExtractHi(eq[0]);
06695 int j = d_theoryBitvector->getExtractLow(eq[0]);
06696 int k = d_theoryBitvector->getExtractHi(eq[1]);
06697 int l = d_theoryBitvector->getExtractLow(eq[1]);
06698
06699
06700
06701 if (i == k) return false;
06702 else if (i > k)
06703 return (k >= j && j > l);
06704 else
06705 return (i >= l && l > j);
06706 }
06707
06708 Theorem BitvectorTheoremProducer::solveExtractOverlap(const Expr& eq)
06709 {
06710 Expr res;
06711
06712 if (CHECK_PROOFS)
06713 CHECK_SOUND(solveExtractOverlapApplies(eq), "solveExtractOvelap does not apply to " + eq.toString());
06714
06715
06716 Expr lhs = eq[0];
06717 Expr rhs = eq[1];
06718
06719
06720 int i = d_theoryBitvector->getExtractHi(lhs);
06721 int j = d_theoryBitvector->getExtractLow(lhs);
06722 int k = d_theoryBitvector->getExtractHi(rhs);
06723 int l = d_theoryBitvector->getExtractLow(rhs);
06724
06725
06726 if (i > k)
06727 {
06728 vector<Expr> terms;
06729 vector<Expr> boundVars;
06730
06731
06732 Expr x = lhs[0];
06733 int x_size = d_theoryBitvector->BVSize(x);
06734
06735
06736 if (i < x_size - 1) {
06737 Expr x_begin = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(x_size - i - 1));
06738 terms.push_back(x_begin);
06739 boundVars.push_back(x_begin);
06740 }
06741
06742 if (2*k + 1 <= i + j)
06743 {
06744
06745
06746
06747
06748
06749 int o_size = k - j + 1;
06750 bool no_rest = (2*k + 1 == i + j);
06751
06752
06753 Expr a = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(o_size));
06754 boundVars.push_back(a);
06755 terms.push_back(a);
06756
06757 if (no_rest) {
06758
06759 terms.push_back(a);
06760 terms.push_back(a);
06761 } else {
06762
06763 Expr b = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(i - k - o_size));
06764 boundVars.push_back(b);
06765 terms.push_back(b);
06766 terms.push_back(a);
06767 terms.push_back(b);
06768 terms.push_back(a);
06769 }
06770 }
06771 else
06772 {
06773
06774
06775
06776
06777 int o_size = k - j + 1;
06778 int r_size = i - k;
06779
06780 int d = gcd(Rational(o_size), Rational(r_size)).getInt();
06781
06782 int different_pieces = r_size / d;
06783
06784 for (int p = 0; p < different_pieces; p ++) {
06785 Expr piece = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(d));
06786 boundVars.push_back(piece);
06787 terms.push_back(piece);
06788 }
06789
06790 int other_pieces = (o_size + r_size) / d;
06791 for (int p = 0; p < other_pieces; p ++)
06792 terms.push_back(terms[terms.size() - different_pieces]);
06793 }
06794
06795
06796 if (l > 0) {
06797 Expr x_end = d_theoryBitvector->getEM()->newBoundVarExpr(d_theoryBitvector->newBitvectorType(l));
06798 terms.push_back(x_end);
06799 boundVars.push_back(x_end);
06800 }
06801
06802 res = x.eqExpr(d_theoryBitvector->newConcatExpr(terms));
06803 res = d_theoryBitvector->getEM()->newClosureExpr(EXISTS, boundVars, res);
06804
06805 } else
06806
06807 res = solveExtractOverlap(rhs.eqExpr(lhs)).getRHS();
06808
06809 Proof pf;
06810 if (withProof()) pf = newPf("solveExtractOverlap", eq);
06811
06812 return newTheorem(eq.iffExpr(res), Assumptions::emptyAssump(), pf);
06813 }
06814