CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_bitvector.cpp 00004 * 00005 * Author: Vijay Ganesh. 00006 * 00007 * Created: Wed May 5 16:16:59 PST 2004 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 00022 #include "theory_bitvector.h" 00023 #include "bitvector_proof_rules.h" 00024 #include "bitvector_exception.h" 00025 #include "typecheck_exception.h" 00026 #include "parser_exception.h" 00027 #include "smtlib_exception.h" 00028 #include "bitvector_expr_value.h" 00029 #include "command_line_flags.h" 00030 00031 00032 #define HASH_VALUE_ZERO 380 00033 #define HASH_VALUE_ONE 450 00034 00035 00036 using namespace std; 00037 using namespace CVC3; 00038 00039 00040 /////////////////////////////////////////////////////////////////////////////// 00041 // TheoryBitvector Private Methods // 00042 /////////////////////////////////////////////////////////////////////////////// 00043 00044 00045 int TheoryBitvector::BVSize(const Expr& e) 00046 { 00047 Type tp(getBaseType(e)); 00048 DebugAssert(tp.getExpr().getOpKind() == BITVECTOR, 00049 "BVSize: e = "+e.toString()); 00050 return getBitvectorTypeParam(tp); 00051 } 00052 00053 00054 //! Converts e into a BITVECTOR of length 'len' 00055 /*! 00056 * \param len is the desired length of the resulting bitvector 00057 * \param e is the original bitvector of arbitrary length 00058 */ 00059 Expr TheoryBitvector::pad(int len, const Expr& e) 00060 { 00061 DebugAssert(len >=0, 00062 "TheoryBitvector::newBVPlusExpr:" 00063 "padding length must be a non-negative integer: "+ 00064 int2string(len)); 00065 DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(), 00066 "TheoryBitvector::newBVPlusExpr:" 00067 "input must be a BITVECTOR: " + e.toString()); 00068 00069 int size = BVSize(e); 00070 Expr res; 00071 if(size == len) 00072 res = e; 00073 else if (len < size) 00074 res = newBVExtractExpr(e,len-1,0); 00075 else { 00076 // size < len 00077 Expr zero = newBVZeroString(len-size); 00078 res = newConcatExpr(zero,e); 00079 } 00080 return res; 00081 } 00082 00083 00084 // Bit-blasting methods 00085 00086 00087 //! accepts a bitvector equation t1 = t2. 00088 /*! \return a rewrite theorem which is a conjunction of equivalences 00089 * over the bits of t1,t2 respectively. 00090 */ 00091 Theorem TheoryBitvector::bitBlastEqn(const Expr& e) 00092 { 00093 TRACE("bitvector", "bitBlastEqn(", e.toString(), ") {"); 00094 d_bvBitBlastEq++; 00095 00096 DebugAssert(e.isEq(), 00097 "TheoryBitvector::bitBlastEqn:" 00098 "expecting an equation" + e.toString()); 00099 const Expr& leftBV = e[0]; 00100 const Expr& rightBV = e[1]; 00101 IF_DEBUG(const Type& leftType = getBaseType(leftBV);) 00102 IF_DEBUG(const Type& rightType = getBaseType(rightBV);) 00103 DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() && 00104 BITVECTOR == rightType.getExpr().getOpKind(), 00105 "TheoryBitvector::bitBlastEqn:" 00106 "lhs & rhs must be bitvectors"); 00107 DebugAssert(BVSize(leftBV) == BVSize(rightBV), 00108 "TheoryBitvector::bitBlastEqn:\n e = " 00109 +e.toString()); 00110 00111 Theorem result = reflexivityRule(e); 00112 Theorem bitBlastLeftThm; 00113 Theorem bitBlastRightThm; 00114 std::vector<Theorem> substThms; 00115 std::vector<Theorem> leftBVrightBVThms; 00116 int bvLength = BVSize(leftBV); 00117 int bitPosition = 0; 00118 Theorem thm0; 00119 00120 for(; bitPosition < bvLength; ++bitPosition) { 00121 //bitBlastLeftThm is the theorem 'leftBV[bitPosition] <==> phi' 00122 bitBlastLeftThm = bitBlastTerm(leftBV, bitPosition); 00123 //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta' 00124 bitBlastRightThm = bitBlastTerm(rightBV, bitPosition); 00125 //collect the two theorems created above in the vector 00126 //leftBVrightBVthms. 00127 leftBVrightBVThms.push_back(bitBlastLeftThm); 00128 leftBVrightBVThms.push_back(bitBlastRightThm); 00129 //construct (leftBV[bitPosition] <==> rightBV[bitPosition]) 00130 //<====> phi <==> theta 00131 //and store in the vector substThms. 00132 Theorem thm = substitutivityRule(IFF, leftBVrightBVThms); 00133 thm = transitivityRule(thm, rewriteBoolean(thm.getRHS())); 00134 leftBVrightBVThms.clear(); 00135 substThms.push_back(thm); 00136 //if phi <==> theta is false, then stop bitblasting. immediately 00137 //exit and return false. 00138 if(thm.getRHS().isFalse()) 00139 return transitivityRule(result, 00140 d_rules->bitvectorFalseRule(thm)); 00141 } 00142 // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====> 00143 // AND_0^bvLength(phi <==> theta) 00144 Theorem thm = substitutivityRule(AND, substThms); 00145 // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====> 00146 // rewriteBoolean(AND_0^bvLength(phi <==> theta)) 00147 thm = transitivityRule(thm, rewriteBoolean(thm.getRHS())); 00148 //call trusted rule for bitblasting equations. 00149 result = d_rules->bitBlastEqnRule(e, thm.getLHS()); 00150 result = transitivityRule(result, thm); 00151 TRACE("bitvector", "bitBlastEqn => ", result.toString(), " }"); 00152 return result; 00153 } 00154 00155 00156 //! accepts a bitvector equation t1 != t2. 00157 /*! \return a rewrite theorem which is a conjunction of 00158 * (dis)-equivalences over the bits of t1,t2 respectively. 00159 * 00160 * A separate rule for disequations for efficiency sake. Obvious 00161 * implementation using rule for equations and rule for NOT, is not 00162 * efficient. 00163 */ 00164 Theorem TheoryBitvector::bitBlastDisEqn(const Theorem& notE) 00165 { 00166 TRACE("bitvector", "bitBlastDisEqn(", notE, ") {"); 00167 IF_DEBUG(debugger.counter("bit-blasted diseq")++); 00168 //stat counter 00169 d_bvBitBlastDiseq++; 00170 00171 DebugAssert(notE.getExpr().isNot() && (notE.getExpr())[0].isEq(), 00172 "TheoryBitvector::bitBlastDisEqn:" 00173 "expecting an equation" + notE.getExpr().toString()); 00174 //e is the equation 00175 const Expr& e = (notE.getExpr())[0]; 00176 const Expr& leftBV = e[0]; 00177 const Expr& rightBV = e[1]; 00178 IF_DEBUG(Type leftType = leftBV.getType()); 00179 IF_DEBUG(debugger.counter("bit-blasted diseq bits")+= 00180 BVSize(leftBV)); 00181 IF_DEBUG(Type rightType = rightBV.getType()); 00182 DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() && 00183 BITVECTOR == rightType.getExpr().getOpKind(), 00184 "TheoryBitvector::bitBlastDisEqn:" 00185 "lhs & rhs must be bitvectors"); 00186 DebugAssert(BVSize(leftBV) == BVSize(rightBV), 00187 "TheoryBitvector::bitBlastDisEqn: e = " 00188 +e.toString()); 00189 Theorem bitBlastLeftThm; 00190 Theorem bitBlastRightThm; 00191 std::vector<Theorem> substThms; 00192 std::vector<Theorem> leftBVrightBVThms; 00193 int bvLength = BVSize(leftBV); 00194 int bitPosition = 0; 00195 for(; bitPosition < bvLength; bitPosition = bitPosition+1) { 00196 //bitBlastLeftThm is the theorem '~leftBV[bitPosition] <==> ~phi' 00197 bitBlastLeftThm = 00198 getCommonRules()->iffContrapositive(bitBlastTerm(leftBV, bitPosition)); 00199 //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta' 00200 bitBlastRightThm = bitBlastTerm(rightBV, bitPosition); 00201 //collect the two theorems created above in the vector leftBVrightBVthms. 00202 leftBVrightBVThms.push_back(bitBlastLeftThm); 00203 leftBVrightBVThms.push_back(bitBlastRightThm); 00204 //construct (~leftBV[bitPosition] <==> rightBV[bitPosition]) 00205 //<====> ~phi <==> theta 00206 //and store in the vector substThms. 00207 //recall that (p <=/=> q) is same as (~p <==> q) 00208 Theorem thm = substitutivityRule(IFF, leftBVrightBVThms); 00209 thm = transitivityRule(thm, rewriteBoolean(thm.getRHS())); 00210 leftBVrightBVThms.clear(); 00211 substThms.push_back(thm); 00212 00213 //if phi <==> theta is the True theorem, then stop bitblasting. immediately 00214 //exit and return t1!=t2 <=> true. 00215 if(thm.getRHS().isTrue()) 00216 return d_rules->bitvectorTrueRule(thm); 00217 } 00218 00219 // OR_0^bvLength(~leftBV[bitPosition] <==> rightBV[bitPosition]) <====> 00220 // OR_0^bvLength(~phi <==> theta) 00221 Theorem thm1 = substitutivityRule(OR, substThms); 00222 // Call trusted rule for bitblasting disequations. 00223 Theorem result = d_rules->bitBlastDisEqnRule(notE, thm1.getLHS()); 00224 Theorem thm2 = transitivityRule(thm1, rewriteBoolean(thm1.getRHS())); 00225 result = iffMP(result, thm2); 00226 TRACE("bitvector", "bitBlastDisEqn => ", result.toString(), " }"); 00227 return result; 00228 } 00229 00230 00231 /*! \param e has the form e1 pred e2, where pred is < or <=. 00232 * 00233 * if e1,e2 are constants, determine bv2int(e1) pred bv2int(e2). 00234 * 00235 * most significant bit of ei is denoted by msb(ei) 00236 * 00237 * \return \f$(msb(e1)\ pred\ msb(e2)) \vee 00238 * (msb(e1)=msb(e2) \wedge e1[n-2:0]\ pred\ e2[n-2:0])\f$ 00239 */ 00240 Theorem TheoryBitvector::bitBlastIneqn(const Expr& e) 00241 { 00242 TRACE("bitvector", "bitBlastIneqn(", e.toString(), ") {"); 00243 00244 DebugAssert(BVLT == e.getOpKind() || 00245 BVLE == e.getOpKind(), 00246 "TheoryBitvector::bitBlastIneqn: " 00247 "input e must be BVLT/BVLE: e = " + e.toString()); 00248 DebugAssert(e.arity() == 2, 00249 "TheoryBitvector::bitBlastIneqn: " 00250 "arity of e must be 2: e = " + e.toString()); 00251 Expr lhs = e[0]; 00252 Expr rhs = e[1]; 00253 int e0len = BVSize(lhs); 00254 DebugAssert(e0len == BVSize(rhs), "Expected sizes to match"); 00255 00256 int kind = e.getOpKind(); 00257 Theorem res; 00258 if(lhs == rhs) { 00259 res = d_rules->lhsEqRhsIneqn(e, kind); 00260 } 00261 else if (lhs.getKind() == BVCONST && rhs.getKind() == BVCONST) { 00262 res = d_rules->bvConstIneqn(e, kind); 00263 } else { 00264 Theorem lhs_i = bitBlastTerm(lhs, e0len-1); 00265 Theorem rhs_i = bitBlastTerm(rhs, e0len-1); 00266 res = d_rules->generalIneqn(e, lhs_i, rhs_i, kind); 00267 00268 //check if output is TRUE or FALSE theorem, and then simply return 00269 Theorem output = rewriteBoolean(res.getRHS()); 00270 if (output.getRHS().isBoolConst()) { 00271 res = transitivityRule(res, output); 00272 } 00273 else if (e0len > 1) { 00274 // Copy by value, since 'res' will be changing 00275 Expr resRHS = res.getRHS(); 00276 // resRHS is of the form (\alpha or (\beta and \gamma)) 00277 // where \gamma is an inequality 00278 DebugAssert(resRHS.getKind() == OR && resRHS.arity() == 2 && 00279 resRHS[1].getKind() == AND && resRHS[1].arity() == 2, 00280 "Unexpected structure"); 00281 00282 vector<unsigned> changed; 00283 vector<Theorem> thms; 00284 00285 // \gamma <=> \gamma' 00286 Theorem thm = bitBlastIneqn(resRHS[1][1]); 00287 00288 // (\beta and \gamma) <=> (\beta and \gamma') 00289 changed.push_back(1); 00290 thms.push_back(thm); 00291 thm = substitutivityRule(resRHS[1], changed, thms); 00292 00293 // (\alpha or (\beta and \gamma)) <=> (\alpha or (\beta and \gamma')) 00294 // 'changed' is the same, only update thms[0] 00295 thms[0] = thm; 00296 thm = substitutivityRule(resRHS, changed, thms); 00297 res = transitivityRule(res, thm); 00298 /* 00299 00300 //resRHS can be of the form (\beta and \gamma) or 00301 //resRHS can be of the form (\alpha or \gamma) or 00302 //resRHS can be of the form (\gamma) 00303 // Our mission is to bitblast \gamma and insert it back to the formula 00304 switch(resRHS.getOpKind()) { 00305 case OR: 00306 if(resRHS[1].isAnd()) { // (\alpha or (\beta and \gamma)) 00307 break; 00308 } 00309 // (\alpha or \gamma) - fall through (same as the AND case) 00310 case AND: { // (\beta and \gamma) 00311 changed.push_back(1); 00312 gamma = resRHS[1]; 00313 // \gamma <=> \gamma' 00314 gammaThm = rewriteBV(gamma,2); 00315 //\gamma' <=> \gamma" 00316 Theorem thm3 = bitBlastIneqn(gammaThm.getRHS()); 00317 //Theorem thm3 = bitBlastIneqn(gamma); 00318 //\gamma <=> \gamma' <=> \gamma" 00319 thm3 = transitivityRule(gammaThm, thm3); 00320 thms.push_back(thm3); 00321 // (\beta and \gamma) <=> (\beta and \gamma") 00322 thm3 = substitutivityRule(resRHS,changed,thms); 00323 res = transitivityRule(res, thm3); 00324 break; 00325 } 00326 default: // (\gamma) 00327 IF_DEBUG(gamma = resRHS;) 00328 // \gamma <=> \gamma' 00329 gammaThm = rewriteBV(resRHS,2); 00330 //\gamma' <=> \gamma" 00331 Theorem thm3 = bitBlastIneqn(gammaThm.getRHS()); 00332 //Theorem thm3 = bitBlastIneqn(gamma); 00333 //\gamma <=> \gamma' <=> \gamma" 00334 thm3 = transitivityRule(gammaThm, thm3); 00335 res = transitivityRule(res, thm3); 00336 break; 00337 } 00338 00339 DebugAssert(kind == gamma.getOpKind(), 00340 "TheoryBitvector::bitBlastIneqn: " 00341 "gamma must be a BVLT/BVLE. gamma = " + 00342 gamma.toString()); 00343 */ 00344 } 00345 } 00346 TRACE("bitvector", "bitBlastIneqn => ", res.toString(), " }"); 00347 return res; 00348 } 00349 00350 00351 /*! The invariant maintained by this function is: accepts a bitvector 00352 * term, t,and a bitPosition, i. returns a formula over the set of 00353 * propositional variables defined using BOOLEXTRACT of bitvector 00354 * variables in t at the position i. 00355 * 00356 * \return Theorem(BOOLEXTRACT(t, bitPosition) <=> phi), where phi is 00357 * a Boolean formula over the individual bits of bit-vector variables. 00358 */ 00359 Theorem TheoryBitvector::bitBlastTerm(const Expr& t, int bitPosition) 00360 { 00361 TRACE("bitvector", "bitBlastTerm(", t, ", " + int2string(bitPosition) + ") {"); 00362 00363 IF_DEBUG(Type type = t.getType();) 00364 DebugAssert(BITVECTOR == type.getExpr().getOpKind(), "TheoryBitvector::bitBlastTerm: The type of input to bitBlastTerm must be BITVECTOR.\n t = " +t.toString()); 00365 DebugAssert(bitPosition >= 0, "TheoryBitvector::bitBlastTerm: illegal bitExtraction attempted.\n bitPosition = " + int2string(bitPosition)); 00366 00367 Theorem result; 00368 00369 // Check the cache 00370 Expr t_i = newBoolExtractExpr(t, bitPosition); 00371 CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(t_i); 00372 if (it != d_bitvecCache.end()) { 00373 result = (*it).second; 00374 TRACE("bitvector", "bitBlastTerm[cached] => ", result, " }"); 00375 DebugAssert(t_i == result.getLHS(), "TheoryBitvector::bitBlastTerm: created wrong theorem" + result.toString() + t_i.toString()); 00376 return result; 00377 } 00378 00379 // Construct the theorem t[bitPosition] <=> \theta_i and put it into 00380 // d_bitvecCache 00381 switch(t.getOpKind()) { 00382 case BVCONST: 00383 result = d_rules->bitExtractConstant(t, bitPosition); 00384 break; 00385 case CONCAT: 00386 { 00387 Theorem thm = d_rules->bitExtractConcatenation(t, bitPosition); 00388 const Expr& boolExtractTerm = thm.getRHS(); 00389 DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be bool_extract"); 00390 const Expr& term = boolExtractTerm[0]; 00391 int bitPos = getBoolExtractIndex(boolExtractTerm); 00392 TRACE("bitvector", "term for bitblastTerm recursion:(", term.toString(), ")"); 00393 result = transitivityRule(thm, bitBlastTerm(term, bitPos)); 00394 break; 00395 } 00396 case EXTRACT: 00397 { 00398 Theorem thm = d_rules->bitExtractExtraction(t, bitPosition); 00399 const Expr& boolExtractTerm = thm.getRHS(); 00400 DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be bool_extract"); 00401 const Expr& term = boolExtractTerm[0]; 00402 int bitPos = getBoolExtractIndex(boolExtractTerm); 00403 TRACE("bitvector", "term for bitblastTerm recursion:(", term, ")"); 00404 result = transitivityRule(thm, bitBlastTerm(term, bitPos)); 00405 break; 00406 } 00407 case CONST_WIDTH_LEFTSHIFT: 00408 { 00409 result = d_rules->bitExtractFixedLeftShift(t, bitPosition); 00410 const Expr& extractTerm = result.getRHS(); 00411 if(BOOLEXTRACT == extractTerm.getOpKind()) 00412 result = transitivityRule(result, bitBlastTerm(extractTerm[0], getBoolExtractIndex(extractTerm))); 00413 break; 00414 } 00415 case BVSHL: 00416 { 00417 // BOOLEXTRACT(bvshl(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR 00418 // ((x = 1) AND BOOLEXTRACT(t,i-1)) OR ... 00419 // ((x = i) AND BOOLEXTRACT(t,0)) 00420 Theorem thm = d_rules->bitExtractBVSHL(t, bitPosition); 00421 // bitblast the equations and extractions 00422 vector<Theorem> thms, thms0; 00423 int bvsize = BVSize(t); 00424 for (int i = 0; i <= bitPosition; ++i) { 00425 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize)))); 00426 thms0.push_back(bitBlastTerm(t[0], bitPosition-i)); 00427 thms.push_back(substitutivityRule(AND, thms0)); 00428 thms0.clear(); 00429 } 00430 // Put it all together 00431 if (thms.size() == 1) { 00432 result = transitivityRule(thm, thms[0]); 00433 } 00434 else { 00435 Theorem thm2 = substitutivityRule(OR, thms); 00436 result = transitivityRule(thm, thm2); 00437 } 00438 break; 00439 } 00440 case BVLSHR: 00441 { 00442 // BOOLEXTRACT(bvlshr(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR 00443 // ((x = 1) AND BOOLEXTRACT(t,i+1)) OR ... 00444 // ((x = n-1-i) AND BOOLEXTRACT(t,n-1)) 00445 Theorem thm = d_rules->bitExtractBVLSHR(t, bitPosition); 00446 // bitblast the equations and extractions 00447 vector<Theorem> thms, thms0; 00448 int bvsize = BVSize(t); 00449 for (int i = 0; i <= bvsize-1-bitPosition; ++i) { 00450 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize)))); 00451 thms0.push_back(bitBlastTerm(t[0], bitPosition+i)); 00452 thms.push_back(substitutivityRule(AND, thms0)); 00453 thms0.clear(); 00454 } 00455 // Put it all together 00456 if (thms.size() == 1) { 00457 result = transitivityRule(thm, thms[0]); 00458 } 00459 else { 00460 Theorem thm2 = substitutivityRule(OR, thms); 00461 result = transitivityRule(thm, thm2); 00462 } 00463 break; 00464 } 00465 case BVASHR: 00466 { 00467 // BOOLEXTRACT(bvlshr(t,x),i) <=> ((x = 0) AND BOOLEXTRACT(t,i)) OR 00468 // ((x = 1) AND BOOLEXTRACT(t,i+1)) OR ... 00469 // ((x >= n-1-i) AND BOOLEXTRACT(t,n-1)) 00470 Theorem thm = d_rules->bitExtractBVASHR(t, bitPosition); 00471 // bitblast the equations and extractions 00472 vector<Theorem> thms, thms0; 00473 int bvsize = BVSize(t); 00474 int i = 0; 00475 for (; i < bvsize-1-bitPosition; ++i) { 00476 thms0.push_back(bitBlastEqn(t[1].eqExpr(newBVConstExpr(i, bvsize)))); 00477 thms0.push_back(bitBlastTerm(t[0], bitPosition+i)); 00478 thms.push_back(substitutivityRule(AND, thms0)); 00479 thms0.clear(); 00480 } 00481 Expr leExpr = newBVLEExpr(newBVConstExpr(i, bvsize), t[1]); 00482 thms0.push_back(bitBlastIneqn(leExpr)); 00483 thms0.push_back(bitBlastTerm(t[0], bvsize-1)); 00484 thms.push_back(substitutivityRule(AND, thms0)); 00485 // Put it all together 00486 if (thms.size() == 1) { 00487 result = transitivityRule(thm, thms[0]); 00488 } 00489 else { 00490 Theorem thm2 = substitutivityRule(OR, thms); 00491 result = transitivityRule(thm, thm2); 00492 } 00493 break; 00494 } 00495 case BVOR: 00496 case BVAND: 00497 case BVXOR: 00498 { 00499 int kind = t.getOpKind(); 00500 int resKind = (kind == BVOR) ? OR : 00501 kind == BVAND ? AND : XOR; 00502 Theorem thm = d_rules->bitExtractBitwise(t, bitPosition, kind); 00503 const Expr& phi = thm.getRHS(); 00504 DebugAssert(phi.getOpKind() == resKind && phi.arity() == t.arity(), "TheoryBitvector::bitBlastTerm: recursion:\n phi = " + phi.toString() + "\n t = " + t.toString()); 00505 vector<Theorem> substThms; 00506 for(Expr::iterator i=phi.begin(), iend=phi.end(); i!=iend; ++i) { 00507 DebugAssert(i->getOpKind() == BOOLEXTRACT, "Expected BOOLEXTRACT"); 00508 substThms.push_back(bitBlastTerm((*i)[0], getBoolExtractIndex(*i))); 00509 } 00510 result = transitivityRule(thm, substitutivityRule(resKind, substThms)); 00511 break; 00512 } 00513 case BVNEG: 00514 { 00515 Theorem thm = d_rules->bitExtractNot(t, bitPosition); 00516 const Expr& extractTerm = thm.getRHS(); 00517 DebugAssert(NOT == extractTerm.getKind(), "TheoryBitvector::bitBlastTerm: recursion: term must be NOT"); 00518 const Expr& term0 = extractTerm[0]; 00519 DebugAssert(BOOLEXTRACT == term0.getOpKind(), "TheoryBitvector::bitBlastTerm: recursion:(terms must be BOOL-EXTRACT"); 00520 int bitPos0 = getBoolExtractIndex(term0); 00521 std::vector<Theorem> res; 00522 res.push_back(bitBlastTerm(term0[0], bitPos0)); 00523 result = transitivityRule(thm, substitutivityRule(NOT, res)); 00524 break; 00525 } 00526 case BVPLUS: 00527 { 00528 Theorem thm_binary; 00529 if(t.arity() > 2) thm_binary = d_rules->bvPlusAssociativityRule(t); 00530 else thm_binary = reflexivityRule(t); 00531 00532 Expr bvPlusTerm = thm_binary.getRHS(); 00533 00534 // Get the bits of the right multiplicand 00535 Expr b = bvPlusTerm[1]; 00536 vector<Theorem> b_bits(bitPosition + 1); 00537 for (int bit = bitPosition; bit >= 0; -- bit) 00538 b_bits[bit] = bitBlastTerm(b, bit); 00539 00540 // The output of the bit-blasting 00541 vector<Theorem> output_bits; 00542 00543 // Get the bits of the left multiplicand 00544 Expr a = bvPlusTerm[0]; 00545 vector<Theorem> a_bits(bitPosition + 1); 00546 for (int bit = bitPosition; bit >= 0; -- bit) 00547 a_bits[bit] = bitBlastTerm(a, bit); 00548 00549 // Bit-blast them and get all the output bits (of this size) 00550 d_rules->bitblastBVPlus(a_bits, b_bits, bvPlusTerm, output_bits); 00551 00552 // Simplify all the resulting bit expressions and add them to the bit-blasting cache 00553 Theorem thm; 00554 for (int bit = 0; bit <= bitPosition; bit ++) 00555 { 00556 thm = output_bits[bit]; 00557 00558 Expr original_boolextract = newBoolExtractExpr(t, bit); 00559 Expr boolextract = thm.getLHS(); 00560 Expr bitblasted = thm.getRHS(); 00561 00562 CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(boolextract); 00563 if (it != d_bitvecCache.end()) 00564 continue; 00565 00566 thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.getRHS())); 00567 if (boolextract != original_boolextract) 00568 thm = d_bitvecCache[original_boolextract] = transitivityRule(substitutivityRule(original_boolextract, thm_binary), thm); 00569 } 00570 00571 // We are returning the last theorem 00572 return thm; 00573 00574 break; 00575 } 00576 case BVMULT: { 00577 00578 Theorem thm; 00579 00580 bool a_is_const = (BVCONST == t[0].getKind()); 00581 00582 // If a constant, rewrite using addition 00583 if (a_is_const) { 00584 thm = d_rules->bitExtractConstBVMult(t, bitPosition); 00585 const Expr& boolExtractTerm = thm.getRHS(); 00586 const Expr& term = boolExtractTerm[0]; 00587 result = transitivityRule(thm, bitBlastTerm(term, bitPosition)); 00588 break; 00589 } 00590 00591 // Get the bits ot the right multiplicant 00592 Expr b = t[1]; 00593 vector<Theorem> b_bits(bitPosition + 1); 00594 for (int bit = bitPosition; bit >= 0; -- bit) 00595 b_bits[bit] = bitBlastTerm(b, bit); 00596 00597 // The output of the bitblasting 00598 vector<Theorem> output_bits; 00599 00600 // Get the bits of the left multiplicant 00601 Expr a = t[0]; 00602 vector<Theorem> a_bits(bitPosition + 1); 00603 for (int bit = bitPosition; bit >= 0; -- bit) 00604 a_bits[bit] = bitBlastTerm(a, bit); 00605 00606 // Bitblast them and get all the output bits (of this size) 00607 d_rules->bitblastBVMult(a_bits, b_bits, t, output_bits); 00608 00609 // Simplify all the resulting bit expressions and add them to the bitblasting cache 00610 for (int bit = 0; bit <= bitPosition; bit ++) 00611 { 00612 thm = output_bits[bit]; 00613 00614 Expr boolextract = thm.getLHS(); 00615 Expr bitblasted = thm.getRHS(); 00616 00617 CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(boolextract); 00618 if (it != d_bitvecCache.end()) 00619 continue; 00620 00621 thm = d_bitvecCache[boolextract] = transitivityRule(thm, rewriteBoolean(thm.getRHS())); 00622 // not allowed to use simplify in bitblasting 00623 //theoryCore()->simplify(thm.getRHS())); 00624 } 00625 00626 // We are returning the last theorem 00627 return thm; 00628 00629 break; 00630 } 00631 // case BVMULT: { 00632 // 00633 // Theorem thm; 00634 // if(BVCONST == t[0].getKind()) 00635 // thm = d_rules->bitExtractConstBVMult(t, bitPosition); 00636 // else 00637 // thm = d_rules->bitExtractBVMult(t, bitPosition); 00638 // const Expr& boolExtractTerm = thm.getRHS(); 00639 // const Expr& term = boolExtractTerm[0]; 00640 // result = transitivityRule(thm, bitBlastTerm(term, bitPosition)); 00641 // break; 00642 // } 00643 default: 00644 { 00645 FatalAssert(theoryOf(t.getOpKind()) != this, "Unexpected operator in bitBlastTerm:" + t.toString()); 00646 //we have bitvector variable. check if the expr is indeed a BITVECTOR. 00647 IF_DEBUG(Type type = t.getType();) 00648 DebugAssert(BITVECTOR == (type.getExpr()).getOpKind(), "BitvectorTheoremProducer::bitBlastTerm: the type must be BITVECTOR"); 00649 //check if 0<= i < length of BITVECTOR 00650 IF_DEBUG(int bvLength=BVSize(t);) 00651 DebugAssert(0 <= bitPosition && bitPosition < bvLength, "BitvectorTheoremProducer::bitBlastTerm: the bitextract position must be legal"); 00652 TRACE("bitvector", "bitBlastTerm: blasting variables(", t, ")"); 00653 const Expr bitExtract = newBoolExtractExpr(t, bitPosition); 00654 result = reflexivityRule(bitExtract); 00655 TRACE("bitvector", "bitBlastTerm: blasting variables(", t, ")"); 00656 break; 00657 } 00658 } 00659 DebugAssert(!result.isNull(), "TheoryBitvector::bitBlastTerm()"); 00660 Theorem simpThm = rewriteBoolean(result.getRHS()); 00661 // not allowed to use simplify in bitblasting 00662 // theoryCore()->simplify(result.getRHS()); 00663 result = transitivityRule(result, simpThm); 00664 d_bitvecCache[t_i] = result; 00665 DebugAssert(t_i == result.getLHS(), 00666 "TheoryBitvector::bitBlastTerm: " 00667 "created wrong theorem.\n result = " 00668 +result.toString() 00669 +"\n t_i = "+t_i.toString()); 00670 TRACE("bitvector", "bitBlastTerm => ", result, " }"); 00671 return result; 00672 } 00673 00674 00675 // Rewriting methods 00676 00677 00678 //! Check that all the kids of e are BVCONST 00679 static bool constantKids(const Expr& e) { 00680 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 00681 if(!i->isRational() && i->getKind() != BVCONST) return false; 00682 return true; 00683 } 00684 00685 00686 //! Search for all the BVCONST kids of e, and return their indices in idxs 00687 static void constantKids(const Expr& e, vector<int>& idxs) { 00688 for(int i=0, iend=e.arity(); i<iend; ++i) 00689 if(e[i].getKind() == BVCONST) idxs.push_back(i); 00690 } 00691 00692 00693 // Recursively descend into the expression e, keeping track of whether 00694 // we are under even or odd number of negations ('neg' == true means 00695 // odd, the context is "negative"). 00696 // Produce a proof of e <==> e' or !e <==> e', depending on whether 00697 // neg is false or true, respectively. 00698 // This function must be called only from the pushNegation function 00699 Theorem TheoryBitvector::pushNegationRec(const Expr& e) 00700 { 00701 TRACE("pushNegation", "pushNegationRec(", e,") {"); 00702 DebugAssert(e.getKind() == BVNEG, "Expected BVNEG in pushNegationRec"); 00703 ExprMap<Theorem>::iterator i = d_pushNegCache.find(e); 00704 if(i != d_pushNegCache.end()) { // Found cached result 00705 TRACE("TheoryBitvector::pushNegation", 00706 "pushNegationRec [cached] => ", (*i).second, "}"); 00707 return (*i).second; 00708 } 00709 Theorem res(reflexivityRule(e)); 00710 00711 switch(e[0].getOpKind()) { 00712 case BVCONST: 00713 res = d_rules->negConst(e); 00714 break; 00715 case BVNEG:{ 00716 res = d_rules->negNeg(e); 00717 break; 00718 } 00719 case BVAND: { 00720 //demorgan's laws. 00721 Theorem thm0 = d_rules->negBVand(e); 00722 Expr ee = thm0.getRHS(); 00723 if (ee.arity() == 0) res = thm0; 00724 else { 00725 //process each negated kid 00726 Op op = ee.getOp(); 00727 vector<Theorem> thms; 00728 for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i) 00729 thms.push_back(pushNegationRec(*i)); 00730 res = substitutivityRule(op, thms); 00731 res = transitivityRule(thm0, res); 00732 } 00733 break; 00734 } 00735 case BVOR: { 00736 //demorgan's laws. 00737 Theorem thm0 = d_rules->negBVor(e); 00738 Expr ee = thm0.getRHS(); 00739 if (ee.arity() == 0) res = thm0; 00740 else { 00741 //process each negated kid 00742 Op op = ee.getOp(); 00743 vector<Theorem> thms; 00744 for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i) 00745 thms.push_back(pushNegationRec(*i)); 00746 res = substitutivityRule(op, thms); 00747 res = transitivityRule(thm0, res); 00748 } 00749 break; 00750 } 00751 case BVXOR: { 00752 res = d_rules->negBVxor(e); 00753 Expr ee = res.getRHS(); 00754 00755 // only the first child is negated 00756 Theorem thm0 = pushNegationRec(ee[0]); 00757 if (!thm0.isRefl()) { 00758 thm0 = substitutivityRule(ee, 0, thm0); 00759 res = transitivityRule(res, thm0); 00760 } 00761 break; 00762 } 00763 case BVXNOR: { 00764 res = d_rules->negBVxnor(e); 00765 break; 00766 } 00767 case CONCAT: { 00768 //demorgan's laws. 00769 Theorem thm0 = d_rules->negConcat(e); 00770 Expr ee = thm0.getRHS(); 00771 if (ee.arity() == 0) res = thm0; 00772 else { 00773 //process each negated kid 00774 Op op = ee.getOp(); 00775 vector<Theorem> thms; 00776 for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i) 00777 thms.push_back(pushNegationRec(*i)); 00778 res = substitutivityRule(op, thms); 00779 res = transitivityRule(thm0, res); 00780 } 00781 break; 00782 } 00783 case BVPLUS: 00784 // FIXME: Need to implement the following transformation: 00785 // ~(x+y) <=> ~x+~y+1 00786 // (because ~(x+y)+1= -(x+y) = -x-y = ~x+1+~y+1) 00787 case BVMULT: 00788 // FIXME: Need to implement the following transformation: 00789 // ~(x*y) <=> (~x+1)*y-1 00790 // [ where we prefer x to be constant/AND/OR/NEG and then 00791 // BVPLUS, and only then everything else]. 00792 // (because ~(x*y)+1= -(x+y) = (-x)*y = (~x+1)*y) 00793 default: 00794 res = reflexivityRule(e); 00795 break; 00796 } 00797 TRACE("TheoryBitvector::pushNegation", "pushNegationRec => ", res, "}"); 00798 d_pushNegCache[e] = res; 00799 return res; 00800 } 00801 00802 00803 // We assume that the cache is initially empty 00804 Theorem TheoryBitvector::pushNegation(const Expr& e) { 00805 d_pushNegCache.clear(); 00806 DebugAssert(BVNEG == e.getOpKind(), "Expected BVNEG"); 00807 return pushNegationRec(e); 00808 } 00809 00810 00811 //! Top down simplifier 00812 Theorem TheoryBitvector::simplifyOp(const Expr& e) { 00813 if (e.arity() > 0) { 00814 Expr ee(e); 00815 Theorem thm0; 00816 switch(e.getOpKind()) { 00817 case BVNEG: 00818 thm0 = pushNegation(e); 00819 break; 00820 case EXTRACT: 00821 switch(e[0].getOpKind()) { 00822 case BVPLUS: 00823 thm0 = d_rules->extractBVPlus(e); 00824 break; 00825 case BVMULT: 00826 thm0 = d_rules->extractBVMult(e); 00827 break; 00828 default: 00829 thm0 = reflexivityRule(e); 00830 break; 00831 } 00832 break; 00833 case BVPLUS: 00834 break; 00835 case BVMULT: 00836 // thm0 = d_rules->padBVMult(e); 00837 break; 00838 case CONCAT: // 0bin0_[k] @ BVPLUS(n, args) => BVPLUS(n+k, args) 00839 // if(e.arity()==2 && e[0].getKind()==BVCONST && e[1].getOpKind()==BVPLUS 00840 // && computeBVConst(e[0]) == 0) { 00841 // thm0 = d_rules->bvplusZeroConcatRule(e); 00842 // } 00843 break; 00844 case RIGHTSHIFT: 00845 thm0 = d_rules->rightShiftToConcat(e); 00846 break; 00847 case LEFTSHIFT: 00848 thm0 = d_rules->leftShiftToConcat(e); 00849 break; 00850 case CONST_WIDTH_LEFTSHIFT: 00851 thm0 = d_rules->constWidthLeftShiftToConcat(e); 00852 break; 00853 default: 00854 thm0 = reflexivityRule(e); 00855 break; 00856 } 00857 vector<Theorem> newChildrenThm; 00858 vector<unsigned> changed; 00859 if(thm0.isNull()) thm0 = reflexivityRule(e); 00860 ee = thm0.getRHS(); 00861 int ar = ee.arity(); 00862 for(int k = 0; k < ar; ++k) { 00863 // Recursively simplify the kids 00864 Theorem thm = simplify(ee[k]); 00865 if (thm.getLHS() != thm.getRHS()) { 00866 newChildrenThm.push_back(thm); 00867 changed.push_back(k); 00868 } 00869 } 00870 if(changed.size() > 0) { 00871 Theorem thm1 = substitutivityRule(ee, changed, newChildrenThm); 00872 return transitivityRule(thm0,thm1); 00873 } else 00874 return thm0; 00875 } 00876 return reflexivityRule(e); 00877 } 00878 00879 00880 // Theorem TheoryBitvector::rewriteConst(const Expr& e) 00881 // { 00882 // Theorem result = reflexivityRule(e); 00883 // return result; 00884 // } 00885 00886 00887 Theorem TheoryBitvector::rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n) 00888 { 00889 TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV(", e, ") {"); 00890 00891 if (n <= 0) return reflexivityRule(e); 00892 00893 Theorem res; 00894 00895 if(n >= 2) { 00896 // rewrite children recursively 00897 Theorem thm; 00898 vector<Theorem> thms; 00899 vector<unsigned> changed; 00900 for(int i=0, iend=e.arity(); i<iend; ++i) { 00901 thm = rewriteBV(e[i], cache, n-1); 00902 if(thm.getLHS() != thm.getRHS()) { 00903 thms.push_back(thm); 00904 changed.push_back(i); 00905 } 00906 } 00907 if(changed.size() > 0) { 00908 thm = substitutivityRule(e, changed, thms); 00909 return transitivityRule(thm, rewriteBV(thm.getRHS(), cache)); 00910 } 00911 // else fall through 00912 } 00913 00914 // Check the cache 00915 ExprMap<Theorem>::iterator it = cache.find(e); 00916 if (it != cache.end()) { 00917 res = (*it).second; 00918 TRACE("bitvector rewrite", "TheoryBitvector::rewrite["+int2string(n) 00919 +"][cached] => ", res.getExpr(), " }"); 00920 IF_DEBUG(debugger.counter("bv rewriteBV[n] cache hits")++;) 00921 return res; 00922 } 00923 00924 // Main rewrites 00925 switch(e.getOpKind()) { 00926 case NOT: 00927 switch (e[0].getKind()) { 00928 case BVLT: 00929 case BVLE: 00930 res = d_rules->notBVLTRule(e); 00931 if (!res.isRefl()) { 00932 res = transitivityRule(res, simplify(res.getRHS())); 00933 } 00934 break; 00935 case EQ: 00936 if (BVSize(e[0][0]) == 1) { 00937 res = d_rules->notBVEQ1Rule(e); 00938 res = transitivityRule(res, simplify(res.getRHS())); 00939 break; 00940 } 00941 break; 00942 } 00943 break; 00944 case EQ: 00945 { 00946 // Canonise constant equations to true or false 00947 if (e[0].getKind() == BVCONST && e[1].getKind() == BVCONST) { 00948 res = d_rules->constEq(e); 00949 } else 00950 // If x_1 or x_2 = 0 then both have to be 0 00951 if (e[0].getKind() == BVOR && e[1].getKind() == BVCONST && computeBVConst(e[1]) == 0) { 00952 res = d_rules->zeroBVOR(e); 00953 res = transitivityRule(res, simplify(res.getRHS())); 00954 } 00955 // if x_1 and x_2 = 1 then both have to be 1 00956 else if (e[0].getKind() == BVAND && e[1].getKind() == BVCONST && computeBVConst(e[1]) == pow(BVSize(e[1]), 2) - 1) { 00957 res = d_rules->oneBVAND(e); 00958 res = transitivityRule(res, simplify(res.getRHS())); 00959 } 00960 // Solve 00961 else { 00962 res = d_rules->canonBVEQ(e); 00963 if (!res.isRefl()) { 00964 res = transitivityRule(res, simplify(res.getRHS())); 00965 } 00966 else e.setRewriteNormal(); 00967 } 00968 break; 00969 } 00970 case BVCONST: 00971 { 00972 res = reflexivityRule(e); 00973 break; 00974 } 00975 case CONCAT: { 00976 // First, flatten concatenation 00977 res = d_rules->concatFlatten(e); 00978 TRACE("bitvector rewrite", "rewriteBV (CONCAT): flattened = ", 00979 res.getRHS(), ""); 00980 // Search for adjacent constants and accumulate the vector of 00981 // nested concatenations (@ t1 ... (@ c1 ... ck) ... tn), and the 00982 // indices of constant concatenations in this new expression. 00983 // We'll connect this term to 'e' by inverse of flattenning, and 00984 // rewrite concatenations of constants into bitvector constants. 00985 vector<unsigned> idxs; 00986 vector<Expr> kids; // Kids of the new concatenation 00987 vector<Theorem> thms; // Rewrites of constant concatenations 00988 vector<Expr> nestedKids; // Kids of the current concatenation of constants 00989 // res will be overwritten, using const Expr& may be dangerous 00990 Expr e1 = res.getRHS(); 00991 for(int i=0, iend=e1.arity(); i<iend; ++i) { 00992 TRACE("bitvector rewrite", "rewriteBV: e["+int2string(i)+"]=", 00993 e1[i], ""); 00994 if(e1[i].getKind() == BVCONST) { 00995 // INVARIANT: if it is the first constant in a batch, 00996 // then nestedKids must be empty. 00997 nestedKids.push_back(e1[i]); 00998 TRACE("bitvector rewrite", "rewriteBV: queued up BVCONST: ", 00999 e1[i], ""); 01000 } else { // e1[i] is not a BVCONST 01001 if(nestedKids.size() > 0) { // This is the end of a batch 01002 if(nestedKids.size() >= 2) { // Create a nested const concat 01003 Expr cc = newConcatExpr(nestedKids); 01004 idxs.push_back(kids.size()); 01005 kids.push_back(cc); 01006 thms.push_back(d_rules->concatConst(cc)); 01007 TRACE("bitvector rewrite", "rewriteBV: wrapping ", cc, ""); 01008 } else { // A single constant, add it as it is 01009 TRACE("bitvector rewrite", "rewriteBV: single const ", 01010 nestedKids[0], ""); 01011 kids.push_back(nestedKids[0]); 01012 } 01013 nestedKids.clear(); 01014 } 01015 // Add the current non-constant BV 01016 kids.push_back(e1[i]); 01017 } 01018 } 01019 // Handle the last BVCONST 01020 if(nestedKids.size() > 0) { 01021 if(nestedKids.size() >= 2) { // Create a nested const concat 01022 Expr cc = newConcatExpr(nestedKids); 01023 idxs.push_back(kids.size()); 01024 kids.push_back(cc); 01025 thms.push_back(d_rules->concatConst(cc)); 01026 TRACE("bitvector rewrite", "rewriteBV: wrapping ", cc, ""); 01027 } else { // A single constant, add it as it is 01028 kids.push_back(nestedKids[0]); 01029 TRACE("bitvector rewrite", "rewriteBV: single const ", 01030 nestedKids[0], ""); 01031 } 01032 nestedKids.clear(); 01033 } 01034 // If there are any constants to merge, do the merging 01035 if(idxs.size() > 0) { 01036 // CONCAT with constants groupped 01037 if(kids.size() == 1) { // Special case: all elements are constants 01038 DebugAssert(thms.size() == 1, "TheoryBitvector::rewriteBV:\n" 01039 "case CONCAT: all constants. thms.size() == " 01040 +int2string(thms.size())); 01041 res = transitivityRule(res, thms[0]); 01042 } else { 01043 Expr ee = newConcatExpr(kids); 01044 01045 Theorem constMerge = substitutivityRule(ee, idxs, thms); 01046 // The inverse flattening of ee 01047 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee)); 01048 // Putting it together: Theorem(e==e'), where e' has constants merged 01049 res = transitivityRule(res, unFlatten); 01050 res = transitivityRule(res, constMerge); 01051 } 01052 } 01053 01054 // Now do a similar search for mergeable extractions 01055 idxs.clear(); 01056 thms.clear(); 01057 kids.clear(); 01058 // nestedKids must already be empty 01059 DebugAssert(nestedKids.size() == 0, 01060 "rewriteBV() case CONCAT, end of const merge"); 01061 Expr prevExpr; // Previous base of extraction (initially Null) 01062 // The first and the last bit in the batch of mergeable extractions 01063 int hi(-1), low(-1); 01064 // Refresh e1 01065 e1 = res.getRHS(); 01066 for(int i=0, iend=e1.arity(); i<iend; ++i) { 01067 const Expr& ei = e1[i]; 01068 if(ei.getOpKind() == EXTRACT) { 01069 if(nestedKids.size() > 0 && ei[0] == prevExpr 01070 && (low-1) == getExtractHi(ei)) { 01071 // Continue to accumulate the current batch 01072 nestedKids.push_back(ei); 01073 low = getExtractLow(ei); 01074 } else { // Start a new batch 01075 // First, check if there was a batch before that 01076 if(nestedKids.size() >= 2) { // Create a nested const concat 01077 Expr cc = newConcatExpr(nestedKids); 01078 idxs.push_back(kids.size()); 01079 kids.push_back(cc); 01080 thms.push_back(d_rules->concatMergeExtract(cc)); 01081 nestedKids.clear(); 01082 } else if(nestedKids.size() == 1) { 01083 // A single extraction, add it as it is 01084 kids.push_back(nestedKids[0]); 01085 nestedKids.clear(); 01086 } 01087 // Now, actually start a new batch 01088 nestedKids.push_back(ei); 01089 hi = getExtractHi(ei); 01090 low = getExtractLow(ei); 01091 prevExpr = ei[0]; 01092 } 01093 } else { // e1[i] is not an EXTRACT 01094 if(nestedKids.size() >= 2) { // Create a nested const concat 01095 Expr cc = newConcatExpr(nestedKids); 01096 idxs.push_back(kids.size()); 01097 kids.push_back(cc); 01098 thms.push_back(d_rules->concatMergeExtract(cc)); 01099 } else if(nestedKids.size() == 1) { 01100 // A single extraction, add it as it is 01101 kids.push_back(nestedKids[0]); 01102 } 01103 nestedKids.clear(); 01104 // Add the current non-EXTRACT BV 01105 kids.push_back(ei); 01106 } 01107 } 01108 // Handle the last batch of extractions 01109 if(nestedKids.size() >= 2) { // Create a nested const concat 01110 Expr cc = newConcatExpr(nestedKids); 01111 idxs.push_back(kids.size()); 01112 kids.push_back(cc); 01113 // The extraction may include all the bits, we need to rewrite again 01114 thms.push_back(rewriteBV(d_rules->concatMergeExtract(cc), cache, 1)); 01115 } else if(nestedKids.size() == 1) { 01116 // A single extraction, add it as it is 01117 kids.push_back(nestedKids[0]); 01118 } 01119 // If there are any extractions to merge, do the merging 01120 if(idxs.size() > 0) { 01121 // CONCAT with extractions groupped 01122 if(kids.size() == 1) { // Special case: all elements merge together 01123 DebugAssert(thms.size() == 1, "TheoryBitvector::rewriteBV:\n" 01124 "case CONCAT: all extracts merge. thms.size() == " 01125 +int2string(thms.size())); 01126 res = thms[0]; 01127 } else { 01128 Expr ee = newConcatExpr(kids); 01129 Theorem extractMerge = substitutivityRule(ee, idxs, thms); 01130 // The inverse flattening of ee 01131 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee)); 01132 // Putting it together: Theorem(e==e'), where e' has extractions merged 01133 res = transitivityRule(res, unFlatten); 01134 res = transitivityRule(res, extractMerge); 01135 } 01136 } 01137 // Check for 0bin00 @ BVPLUS(n, ...). Most of the time, this 01138 // case will be handled during the top-down phase 01139 // (simplifyOp()), but not always. 01140 // Expr ee = res.getRHS(); 01141 // if(ee.getOpKind()==CONCAT && ee.arity() == 2 && ee[0].getKind()==BVCONST 01142 // && ee[1].getOpKind()==BVPLUS && computeBVConst(ee[0]) == 0) { 01143 // // Push the concat down through BVPLUS 01144 // Theorem thm = d_rules->bvplusZeroConcatRule(ee); 01145 // if(thm.getLHS()!=thm.getRHS()) { 01146 // thm = transitivityRule(thm, d_rules->padBVPlus(thm.getRHS())); 01147 // // Kids may need to be rewritten again 01148 // res = rewriteBV(transitivityRule(res, thm), cache, 2); 01149 // } 01150 // } 01151 // Since we may have pulled subexpressions from more than one 01152 // level deep, we cannot guarantee that all the new kids are 01153 // fully simplified, and have to call simplify explicitly again. 01154 // Since this is potentially an expensive operation, we try to 01155 // minimize the need for it: 01156 01157 // * check if the result has a find pointer (then kids don't 01158 // need to be simplified), 01159 // * check if any of the kids simplify (if not, don't bother). 01160 // If kids are already simplified, we'll hit the simplifier 01161 // cache. It's only expensive when kids do indeed simplify. 01162 if(theoryCore()->inUpdate() || !res.getRHS().hasFind()) { 01163 Expr ee = res.getRHS(); 01164 vector<Theorem> thms; 01165 vector<unsigned> changed; 01166 for(int i=0, iend=ee.arity(); i<iend; ++i) { 01167 Theorem thm = simplify(ee[i]); 01168 if(thm.getLHS()!=thm.getRHS()) { 01169 thms.push_back(thm); 01170 changed.push_back(i); 01171 } 01172 } 01173 if(changed.size()>0) { 01174 Theorem subst = substitutivityRule(ee, changed, thms); 01175 res = transitivityRule(res, rewriteBV(subst, cache, 1)); 01176 } 01177 } 01178 break; 01179 } 01180 case EXTRACT: { 01181 DebugAssert(e.arity() == 1, "TheoryBitvector::rewriteBV: e = " 01182 +e.toString()); 01183 if(getExtractLow(e) == 0 && getExtractHi(e) == BVSize(e[0])-1) 01184 res = d_rules->extractWhole(e); 01185 else { 01186 switch(e[0].getOpKind()) { 01187 case BVCONST: 01188 res = d_rules->extractConst(e); 01189 break; 01190 case EXTRACT: 01191 res = d_rules->extractExtract(e); 01192 break; 01193 case CONCAT: 01194 // Push extraction through concat, and rewrite the kids 01195 res = rewriteBV(d_rules->extractConcat(e), cache, 2); 01196 break; 01197 case BVNEG: 01198 res = rewriteBV(d_rules->extractNeg(e), cache, 2); 01199 break; 01200 case BVAND: 01201 res = rewriteBV(d_rules->extractAnd(e), cache, 2); 01202 break; 01203 case BVOR: 01204 res = rewriteBV(d_rules->extractOr(e), cache, 2); 01205 break; 01206 case BVXOR: 01207 res = 01208 rewriteBV(d_rules->extractBitwise(e, BVXOR, "extract_bvxor"), cache, 2); 01209 break; 01210 case BVMULT: { 01211 const Expr& bvmult = e[0]; 01212 int hiBit = getExtractHi(e); 01213 int bvmultLen = BVSize(bvmult); 01214 // Applicable if it changes anything 01215 if(hiBit+1 < bvmultLen) { 01216 res = d_rules->extractBVMult(e); 01217 res = rewriteBV(res, cache, 3); 01218 } else 01219 res = reflexivityRule(e); 01220 break; 01221 } 01222 case BVPLUS: { 01223 const Expr& bvplus = e[0]; 01224 int hiBit = getExtractHi(e); 01225 int bvplusLen = BVSize(bvplus); 01226 if(hiBit+1 < bvplusLen) { 01227 res = d_rules->extractBVPlus(e); 01228 } else res = reflexivityRule(e); 01229 break; 01230 } 01231 default: 01232 res = reflexivityRule(e); 01233 break; 01234 } 01235 } 01236 if (!res.isRefl()) { 01237 res = transitivityRule(res, simplify(res.getRHS())); 01238 } 01239 break; 01240 } 01241 case BOOLEXTRACT: { 01242 Expr t(e); 01243 // Normal form: t[0] for 1-bit t, collapse t[i:i][0] into t[i] 01244 if(BVSize(e[0]) > 1) { // transform t[i] to t[i:i][0] and rewrite 01245 res = rewriteBV(d_rules->bitExtractRewrite(e), cache, 2); 01246 t = res.getRHS(); 01247 } 01248 if(t.getOpKind() == BOOLEXTRACT && t[0].getOpKind() == EXTRACT) { 01249 // Collapse t[i:i][0] to t[i] 01250 int low = getExtractLow(t[0]); 01251 if(getExtractHi(t[0]) == low) { 01252 Theorem thm(d_rules->bitExtractRewrite 01253 (newBoolExtractExpr(t[0][0], low))); 01254 thm = symmetryRule(thm); 01255 res = (res.isNull())? thm : transitivityRule(res, thm); 01256 t = res.getRHS()[0]; 01257 // Make sure t in the resulting t[i] is its own find pointer 01258 // (global invariant) 01259 if(t.hasFind()) { 01260 Theorem findThm = find(t); 01261 if(t != findThm.getRHS()) { 01262 vector<Theorem> thms; 01263 thms.push_back(findThm); 01264 thm = substitutivityRule(res.getRHS().getOp(), thms); 01265 res = transitivityRule(res, thm); 01266 } 01267 } 01268 } 01269 } 01270 if(!res.isNull()) t = res.getRHS(); 01271 // Rewrite a constant extraction to TRUE or FALSE 01272 if(t.getOpKind() == BOOLEXTRACT && constantKids(t)) { 01273 Theorem thm = d_rules->bitExtractConstant(t[0], getBoolExtractIndex(t)); 01274 res = (res.isNull())? thm : transitivityRule(res, thm); 01275 } 01276 break; 01277 } 01278 case LEFTSHIFT: 01279 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01280 res = d_rules->bvShiftZero(e); 01281 } else { 01282 res = d_rules->leftShiftToConcat(e); 01283 if (!res.isRefl()) { 01284 res = transitivityRule(res, simplify(res.getRHS())); 01285 } 01286 } 01287 break; 01288 case CONST_WIDTH_LEFTSHIFT: 01289 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01290 res = d_rules->bvShiftZero(e); 01291 } else { 01292 res = d_rules->constWidthLeftShiftToConcat(e); 01293 if (!res.isRefl()) { 01294 res = transitivityRule(res, simplify(res.getRHS())); 01295 } 01296 } 01297 break; 01298 case RIGHTSHIFT: 01299 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01300 res = d_rules->bvShiftZero(e); 01301 } else { 01302 res = d_rules->rightShiftToConcat(e); 01303 if (!res.isRefl()) { 01304 res = transitivityRule(res, simplify(res.getRHS())); 01305 } 01306 } 01307 break; 01308 case BVSHL: 01309 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01310 res = d_rules->bvShiftZero(e); 01311 } else 01312 if (e[1].getKind() == BVCONST) { 01313 res = d_rules->bvshlToConcat(e); 01314 res = transitivityRule(res, simplify(res.getRHS())); 01315 } 01316 // else { 01317 // res = d_rules->bvshlSplit(e); 01318 // res = transitivityRule(res, simplify(res.getRHS())); 01319 // } 01320 break; 01321 case BVLSHR: 01322 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01323 res = d_rules->bvShiftZero(e); 01324 } else 01325 if (e[1].getKind() == BVCONST) { 01326 res = d_rules->bvlshrToConcat(e); 01327 res = transitivityRule(res, simplify(res.getRHS())); 01328 } 01329 break; 01330 case BVASHR: 01331 if (e[0].getKind() == BVCONST && computeBVConst(e[0]) == 0) { 01332 res = d_rules->bvShiftZero(e); 01333 } else 01334 if (e[1].getKind() == BVCONST) { 01335 res = d_rules->bvashrToConcat(e); 01336 res = transitivityRule(res, simplify(res.getRHS())); 01337 } 01338 break; 01339 case SX: { 01340 res = d_rules->signExtendRule(e); 01341 res = transitivityRule(res, simplify(res.getRHS())); 01342 break; 01343 } 01344 01345 case BVZEROEXTEND: 01346 res = d_rules->zeroExtendRule(e); 01347 res = transitivityRule(res, simplify(res.getRHS())); 01348 break; 01349 01350 case BVREPEAT: 01351 res = d_rules->repeatRule(e); 01352 res = transitivityRule(res, simplify(res.getRHS())); 01353 break; 01354 01355 case BVROTL: 01356 res = d_rules->rotlRule(e); 01357 res = transitivityRule(res, simplify(res.getRHS())); 01358 break; 01359 01360 case BVROTR: 01361 res = d_rules->rotrRule(e); 01362 res = transitivityRule(res, simplify(res.getRHS())); 01363 break; 01364 01365 case BVAND: 01366 case BVOR: 01367 case BVXOR: 01368 { 01369 int kind = e.getOpKind(); 01370 // Flatten the bit-wise AND, eliminate duplicates, reorder terms 01371 res = d_rules->bitwiseFlatten(e, kind); 01372 Expr ee = res.getRHS(); 01373 if (ee.getOpKind() != kind) break; 01374 01375 // Search for constant bitvectors 01376 vector<int> idxs; 01377 constantKids(ee, idxs); 01378 int idx = -1; 01379 01380 if(idxs.size() >= 2) { 01381 res = transitivityRule(res, d_rules->bitwiseConst(ee, idxs, kind)); 01382 ee = res.getRHS(); 01383 if (ee.getOpKind() != kind) break; 01384 idx = 0; 01385 } 01386 else if (idxs.size() == 1) { 01387 idx = idxs[0]; 01388 } 01389 01390 if (idx >= 0) { 01391 res = transitivityRule(res, d_rules->bitwiseConstElim(ee, idx, kind)); 01392 ee = res.getRHS(); 01393 if (ee.getOpKind() != kind) break; 01394 } 01395 res = transitivityRule(res, d_rules->bitwiseConcat(ee, kind)); 01396 if (!res.isRefl()) { 01397 res = transitivityRule(res, simplify(res.getRHS())); 01398 } 01399 else { 01400 e.setRewriteNormal(); 01401 } 01402 break; 01403 } 01404 case BVXNOR: { 01405 res = d_rules->rewriteXNOR(e); 01406 res = transitivityRule(res, simplify(res.getRHS())); 01407 break; 01408 } 01409 case BVNEG: { 01410 res = pushNegation(e); 01411 if (!res.isRefl()) { 01412 res = transitivityRule(res, simplify(res.getRHS())); 01413 } 01414 break; 01415 } 01416 case BVNAND: { 01417 res = d_rules->rewriteNAND(e); 01418 res = transitivityRule(res, simplify(res.getRHS())); 01419 break; 01420 } 01421 case BVNOR: { 01422 res = d_rules->rewriteNOR(e); 01423 res = transitivityRule(res, simplify(res.getRHS())); 01424 break; 01425 } 01426 case BVCOMP: { 01427 res = d_rules->rewriteBVCOMP(e); 01428 res = transitivityRule(res, simplify(res.getRHS())); 01429 break; 01430 } 01431 case BVUMINUS: 01432 { 01433 res = d_rules->canonBVUMinus( e ); 01434 res = transitivityRule(res, simplify(res.getRHS())); 01435 break; 01436 } 01437 case BVPLUS: 01438 { 01439 res = d_rules->canonBVPlus(e ); 01440 if (!res.isRefl()) { 01441 res = transitivityRule(res, simplify(res.getRHS())); 01442 } 01443 else e.setRewriteNormal(); 01444 break; 01445 } 01446 case BVSUB: { 01447 res = d_rules->rewriteBVSub(e); 01448 res = transitivityRule(res, simplify(res.getRHS())); 01449 break; 01450 } 01451 case BVMULT: 01452 { 01453 res = d_rules->liftConcatBVMult(e); 01454 if (!res.isRefl()) { 01455 res = transitivityRule(res, simplify(res.getRHS())); 01456 } 01457 else { 01458 res = d_rules->canonBVMult( e ); 01459 if (!res.isRefl()) 01460 res = transitivityRule(res, simplify(res.getRHS())); 01461 else e.setRewriteNormal(); 01462 } 01463 break; 01464 } 01465 01466 case BVUDIV: 01467 { 01468 Expr a = e[0]; 01469 Expr b = e[1]; 01470 01471 // Constant division 01472 if (a.getOpKind() == BVCONST && b.getOpKind() == BVCONST) { 01473 res = d_rules->bvUDivConst(e); 01474 break; 01475 } 01476 01477 if (theoryCore()->okToEnqueue()) 01478 { 01479 // get the full theorem 01480 // e = x/y 01481 // \exists div, mod: e = div & (y != 0 -> ...) 01482 // result is the equality 01483 // assert the additional conjunct 01484 Theorem fullTheorem = d_rules->bvUDivTheorem(e); 01485 // Skolemise the variables 01486 Theorem skolem_div = getCommonRules()->skolemize(fullTheorem); 01487 // Get the rewrite part 01488 res = getCommonRules()->andElim(skolem_div, 0); 01489 // Get the division part 01490 Theorem additionalConstraint = getCommonRules()->andElim(skolem_div, 1); 01491 // Enqueue the division part 01492 enqueueFact(additionalConstraint); 01493 res = transitivityRule(res, simplify(res.getRHS())); 01494 } else { 01495 res = reflexivityRule(e); 01496 } 01497 break; 01498 } 01499 case BVSDIV: 01500 res = d_rules->bvSDivRewrite(e); 01501 res = transitivityRule(res, simplify(res.getRHS())); 01502 break; 01503 case BVUREM: 01504 { 01505 Expr a = e[0]; 01506 Expr b = e[1]; 01507 01508 // Constant division 01509 if (a.getOpKind() == BVCONST && b.getOpKind() == BVCONST) { 01510 res = d_rules->bvURemConst(e); 01511 break; 01512 } 01513 01514 res = d_rules->bvURemRewrite(e); 01515 res = transitivityRule(res, theoryCore()->simplify(res.getRHS())); 01516 01517 break; 01518 } 01519 case BVSREM: 01520 res = d_rules->bvSRemRewrite(e); 01521 res = transitivityRule(res, simplify(res.getRHS())); 01522 break; 01523 case BVSMOD: 01524 res = d_rules->bvSModRewrite(e); 01525 res = transitivityRule(res, simplify(res.getRHS())); 01526 break; 01527 case BVLT: 01528 case BVLE: { 01529 Expr lhs = e[0]; 01530 Expr rhs = e[1]; 01531 if (BVSize(lhs) != BVSize(rhs)) { 01532 res = d_rules->padBVLTRule(e, BVSize(lhs) > BVSize(rhs) ? BVSize(lhs) : BVSize(rhs)); 01533 res = transitivityRule(res, simplify(res.getRHS())); 01534 } 01535 else { 01536 if(lhs == rhs) 01537 res = d_rules->lhsEqRhsIneqn(e, e.getOpKind()); 01538 else if (BVCONST == lhs.getKind() && BVCONST == rhs.getKind()) 01539 res = d_rules->bvConstIneqn(e, e.getOpKind()); 01540 else if (e.getOpKind() == BVLE && BVCONST == lhs.getKind() && computeBVConst(lhs) == 0) 01541 res = d_rules->zeroLeq(e); 01542 } 01543 break; 01544 } 01545 01546 case BVGT: 01547 case BVGE: 01548 FatalAssert(false, "Should be eliminated at parse-time"); 01549 break; 01550 01551 case BVSLT: 01552 case BVSLE:{ 01553 /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of 01554 * e0 and e1 are constants. If they are constants then optimizations 01555 * are done. In general, the following rule is implemented. 01556 * Step1: 01557 * e0 <=(s) e1 01558 * <==> 01559 * pad(e0) <=(s) pad(e1) 01560 * Step2: 01561 * pad(e0) <=(s) pad(e1) 01562 * <==> 01563 * (e0[n-1] AND NOT e1[n-1]) OR 01564 * (e0[n-1] = e1[n-1] AND e0[n-2:0] <= e1[n-2:0]) 01565 */ 01566 int e0len = BVSize(e[0]); 01567 int e1len = BVSize(e[1]); 01568 int bvlength = e0len>=e1len ? e0len : e1len; 01569 //e0 <=(s) e1 <=> signpad(e0) <=(s) signpad(e1) 01570 01571 std::vector<Theorem> thms; 01572 std::vector<unsigned> changed; 01573 01574 //e0 <= e1 <==> pad(e0) <= pad(e1) 01575 Theorem thm = d_rules->padBVSLTRule(e, bvlength); 01576 Expr paddedE = thm.getRHS(); 01577 01578 //the rest of the code simply normalizes pad(e0) and pad(e1) 01579 Theorem thm0 = d_rules->signExtendRule(paddedE[0]); 01580 Expr rhs0 = thm0.getRHS(); 01581 thm0 = transitivityRule(thm0, rewriteBV(rhs0, cache)); 01582 if(thm0.getLHS() != thm0.getRHS()) { 01583 thms.push_back(thm0); 01584 changed.push_back(0); 01585 } 01586 01587 Theorem thm1 = d_rules->signExtendRule(paddedE[1]); 01588 Expr rhs1 = thm1.getRHS(); 01589 thm1 = transitivityRule(thm1, rewriteBV(rhs1, cache)); 01590 if(thm1.getLHS() != thm1.getRHS()) { 01591 thms.push_back(thm1); 01592 changed.push_back(1); 01593 } 01594 01595 if(changed.size() > 0) { 01596 thm0 = substitutivityRule(paddedE,changed,thms); 01597 thm0 = transitivityRule(thm, thm0); 01598 } 01599 else 01600 thm0 = reflexivityRule(e); 01601 01602 //signpad(e0) <= signpad(e1) 01603 Expr thm0RHS = thm0.getRHS(); 01604 DebugAssert(thm0RHS.getOpKind() == BVSLT || 01605 thm0RHS.getOpKind() == BVSLE, 01606 "TheoryBitvector::RewriteBV"); 01607 //signpad(e0)[bvlength-1:bvlength-1] 01608 const Expr MSB0 = newBVExtractExpr(thm0RHS[0],bvlength-1,bvlength-1); 01609 //signpad(e1)[bvlength-1:bvlength-1] 01610 const Expr MSB1 = newBVExtractExpr(thm0RHS[1],bvlength-1,bvlength-1); 01611 //rewritten MSB0 01612 const Theorem topBit0 = rewriteBV(MSB0, cache, 2); 01613 //rewritten MSB1 01614 const Theorem topBit1 = rewriteBV(MSB1, cache, 2); 01615 //compute e0 <=(s) e1 <==> signpad(e0) <=(s) signpad(e1) <==> 01616 //output as given above 01617 thm1 = d_rules->signBVLTRule(thm0RHS, topBit0, topBit1); 01618 thm1 = transitivityRule(thm1,simplify(thm1.getRHS())); 01619 res = transitivityRule(thm0,thm1); 01620 break; 01621 } 01622 case BVSGT: 01623 case BVSGE: 01624 FatalAssert(false, "Should be eliminated at parse-time"); 01625 break; 01626 default: 01627 res = reflexivityRule(e); 01628 break; 01629 } 01630 01631 if (res.isNull()) res = reflexivityRule(e); 01632 01633 // Update cache 01634 cache[e] = res; 01635 01636 TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV => ", 01637 res.getExpr(), " }"); 01638 01639 return res; 01640 } 01641 01642 01643 Theorem TheoryBitvector::rewriteBV(const Expr& e, int n) 01644 { 01645 ExprMap<Theorem> cache; 01646 return rewriteBV(e, cache, n); 01647 } 01648 01649 01650 Theorem TheoryBitvector::rewriteBoolean(const Expr& e) 01651 { 01652 Theorem thm; 01653 switch (e.getKind()) { 01654 case NOT: 01655 if (e[0].isTrue()) 01656 thm = getCommonRules()->rewriteNotTrue(e); 01657 else if (e[0].isFalse()) 01658 thm = getCommonRules()->rewriteNotFalse(e); 01659 else if (e[0].isNot()) 01660 thm = getCommonRules()->rewriteNotNot(e); 01661 break; 01662 case IFF: { 01663 thm = getCommonRules()->rewriteIff(e); 01664 const Expr& rhs = thm.getRHS(); 01665 // The only time we need to rewrite the result (rhs) is when 01666 // e==(FALSE<=>e1) or (e1<=>FALSE), so rhs==!e1. 01667 if (e != rhs && rhs.isNot()) 01668 thm = transitivityRule(thm, rewriteBoolean(rhs)); 01669 break; 01670 } 01671 case AND:{ 01672 std::vector<Theorem> newK; 01673 std::vector<unsigned> changed; 01674 unsigned count(0); 01675 for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) { 01676 Theorem temp = rewriteBoolean(*ii); 01677 if(temp.getLHS() != temp.getRHS()) { 01678 newK.push_back(temp); 01679 changed.push_back(count); 01680 } 01681 } 01682 if(changed.size() > 0) { 01683 Theorem res = substitutivityRule(e,changed,newK); 01684 thm = transitivityRule(res, rewriteAnd(res.getRHS())); 01685 } else 01686 thm = rewriteAnd(e); 01687 } 01688 break; 01689 case OR:{ 01690 std::vector<Theorem> newK; 01691 std::vector<unsigned> changed; 01692 unsigned count(0); 01693 for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) { 01694 Theorem temp = rewriteBoolean(*ii); 01695 if(temp.getLHS() != temp.getRHS()) { 01696 newK.push_back(temp); 01697 changed.push_back(count); 01698 } 01699 } 01700 if(changed.size() > 0) { 01701 Theorem res = substitutivityRule(e,changed,newK); 01702 thm = transitivityRule(res, rewriteOr(res.getRHS())); 01703 } else 01704 thm = rewriteOr(e); 01705 } 01706 break; 01707 01708 default: 01709 break; 01710 } 01711 if(thm.isNull()) thm = reflexivityRule(e); 01712 01713 return thm; 01714 } 01715 01716 01717 /////////////////////////////////////////////////////////////////////////////// 01718 // TheoryBitvector Public Methods // 01719 /////////////////////////////////////////////////////////////////////////////// 01720 TheoryBitvector::TheoryBitvector(TheoryCore* core) 01721 : Theory(core, "Bitvector"), 01722 d_bvDelayEq(core->getStatistics().counter("bv delayed assert eqs")), 01723 d_bvAssertEq(core->getStatistics().counter("bv eager assert eqs")), 01724 d_bvDelayDiseq(core->getStatistics().counter("bv delayed assert diseqs")), 01725 d_bvAssertDiseq(core->getStatistics().counter("bv eager assert diseqs")), 01726 d_bvTypePreds(core->getStatistics().counter("bv type preds enqueued")), 01727 d_bvDelayTypePreds(core->getStatistics().counter("bv type preds delayed")), 01728 d_bvBitBlastEq(core->getStatistics().counter("bv bitblast eqs")), 01729 d_bvBitBlastDiseq(core->getStatistics().counter("bv bitblast diseqs")), 01730 d_bv32Flag(&(core->getFlags()["bv32-flag"].getBool())), 01731 d_bitvecCache(core->getCM()->getCurrentContext()), 01732 d_eq(core->getCM()->getCurrentContext()), 01733 d_eqPending(core->getCM()->getCurrentContext()), 01734 d_eq_index(core->getCM()->getCurrentContext(), 0, 0), 01735 d_bitblast(core->getCM()->getCurrentContext()), 01736 d_bb_index(core->getCM()->getCurrentContext(), 0, 0), 01737 d_sharedSubterms(core->getCM()->getCurrentContext()), 01738 d_sharedSubtermsList(core->getCM()->getCurrentContext()), 01739 d_maxLength(0), 01740 d_index1(core->getCM()->getCurrentContext(), 0, 0), 01741 d_index2(core->getCM()->getCurrentContext(), 0, 0) 01742 // d_solvedEqSet(core->getCM()->getCurrentContext(), 0, 0) 01743 { 01744 getEM()->newKind(BITVECTOR, "_BITVECTOR", true); 01745 getEM()->newKind(BVCONST, "_BVCONST"); 01746 getEM()->newKind(CONCAT, "_CONCAT"); 01747 getEM()->newKind(EXTRACT, "_EXTRACT"); 01748 getEM()->newKind(BOOLEXTRACT, "_BOOLEXTRACT"); 01749 getEM()->newKind(LEFTSHIFT, "_LEFTSHIFT"); 01750 getEM()->newKind(CONST_WIDTH_LEFTSHIFT, "_CONST_WIDTH_LEFTSHIFT"); 01751 getEM()->newKind(RIGHTSHIFT, "_RIGHTSHIFT"); 01752 getEM()->newKind(BVSHL, "_BVSHL"); 01753 getEM()->newKind(BVLSHR, "_BVLSHR"); 01754 getEM()->newKind(BVASHR, "_BVASHR"); 01755 getEM()->newKind(SX,"_SX"); 01756 getEM()->newKind(BVREPEAT,"_BVREPEAT"); 01757 getEM()->newKind(BVZEROEXTEND,"_BVZEROEXTEND"); 01758 getEM()->newKind(BVROTL,"_BVROTL"); 01759 getEM()->newKind(BVROTR,"_BVROTR"); 01760 getEM()->newKind(BVAND, "_BVAND"); 01761 getEM()->newKind(BVOR, "_BVOR"); 01762 getEM()->newKind(BVXOR, "_BVXOR"); 01763 getEM()->newKind(BVXNOR, "_BVXNOR"); 01764 getEM()->newKind(BVNEG, "_BVNEG"); 01765 getEM()->newKind(BVNAND, "_BVNAND"); 01766 getEM()->newKind(BVNOR, "_BVNOR"); 01767 getEM()->newKind(BVCOMP, "_BVCOMP"); 01768 getEM()->newKind(BVUMINUS, "_BVUMINUS"); 01769 getEM()->newKind(BVPLUS, "_BVPLUS"); 01770 getEM()->newKind(BVSUB, "_BVSUB"); 01771 getEM()->newKind(BVMULT, "_BVMULT"); 01772 getEM()->newKind(BVUDIV, "_BVUDIV"); 01773 getEM()->newKind(BVSDIV, "_BVSDIV"); 01774 getEM()->newKind(BVUREM, "_BVUREM"); 01775 getEM()->newKind(BVSREM, "_BVSREM"); 01776 getEM()->newKind(BVSMOD, "_BVSMOD"); 01777 getEM()->newKind(BVLT, "_BVLT"); 01778 getEM()->newKind(BVLE, "_BVLE"); 01779 getEM()->newKind(BVGT, "_BVGT"); 01780 getEM()->newKind(BVGE, "_BVGE"); 01781 getEM()->newKind(BVSLT, "_BVSLT"); 01782 getEM()->newKind(BVSLE, "_BVSLE"); 01783 getEM()->newKind(BVSGT, "_BVSGT"); 01784 getEM()->newKind(BVSGE, "_BVSGE"); 01785 getEM()->newKind(INTTOBV, "_INTTOBV"); 01786 getEM()->newKind(BVTOINT, "_BVTOINT"); 01787 getEM()->newKind(BVTYPEPRED, "_BVTYPEPRED"); 01788 01789 std::vector<int> kinds; 01790 kinds.push_back(BITVECTOR); 01791 kinds.push_back(BVCONST); 01792 kinds.push_back(CONCAT); 01793 kinds.push_back(EXTRACT); 01794 kinds.push_back(BOOLEXTRACT); 01795 kinds.push_back(LEFTSHIFT); 01796 kinds.push_back(CONST_WIDTH_LEFTSHIFT); 01797 kinds.push_back(RIGHTSHIFT); 01798 kinds.push_back(BVSHL); 01799 kinds.push_back(BVLSHR); 01800 kinds.push_back(BVASHR); 01801 kinds.push_back(SX); 01802 kinds.push_back(BVREPEAT); 01803 kinds.push_back(BVZEROEXTEND); 01804 kinds.push_back(BVROTL); 01805 kinds.push_back(BVROTR); 01806 kinds.push_back(BVAND); 01807 kinds.push_back(BVOR); 01808 kinds.push_back(BVXOR); 01809 kinds.push_back(BVXNOR); 01810 kinds.push_back(BVNEG); 01811 kinds.push_back(BVNAND); 01812 kinds.push_back(BVNOR); 01813 kinds.push_back(BVCOMP); 01814 kinds.push_back(BVUMINUS); 01815 kinds.push_back(BVPLUS); 01816 kinds.push_back(BVSUB); 01817 kinds.push_back(BVMULT); 01818 kinds.push_back(BVUDIV); 01819 kinds.push_back(BVSDIV); 01820 kinds.push_back(BVUREM); 01821 kinds.push_back(BVSREM); 01822 kinds.push_back(BVSMOD); 01823 kinds.push_back(BVLT); 01824 kinds.push_back(BVLE); 01825 kinds.push_back(BVGT); 01826 kinds.push_back(BVGE); 01827 kinds.push_back(BVSLT); 01828 kinds.push_back(BVSLE); 01829 kinds.push_back(BVSGT); 01830 kinds.push_back(BVSGE); 01831 kinds.push_back(INTTOBV); 01832 kinds.push_back(BVTOINT); 01833 kinds.push_back(BVTYPEPRED); 01834 01835 registerTheory(this, kinds); 01836 01837 d_bvConstExprIndex = getEM()->registerSubclass(sizeof(BVConstExpr)); 01838 01839 // Cache constants 0bin0 and 0bin1 01840 vector<bool> bits(1); 01841 bits[0]=false; 01842 d_bvZero = newBVConstExpr(bits); 01843 bits[0]=true; 01844 d_bvOne = newBVConstExpr(bits); 01845 01846 // Instantiate the rules after all expression creation is 01847 // registered, since the constructor creates some bit-vector 01848 // expressions. 01849 d_rules = createProofRules(); 01850 } 01851 01852 01853 // Destructor: delete the proof rules class if it's present 01854 TheoryBitvector::~TheoryBitvector() { 01855 if(d_rules != NULL) delete d_rules; 01856 } 01857 01858 01859 // Main theory API 01860 01861 01862 void TheoryBitvector::addSharedTerm(const Expr& e) 01863 { 01864 if(d_sharedSubterms.count(e)>0) return; 01865 TRACE("bvAddSharedTerm", "TheoryBitvector::addSharedTerm(", e.toString(PRESENTATION_LANG), ")"); 01866 IF_DEBUG(debugger.counter("bv shared subterms")++;) 01867 d_sharedSubterms[e]=e; 01868 d_sharedSubtermsList.push_back(e); 01869 e.addToNotify(this, Expr()); 01870 } 01871 01872 01873 /*Modified by Lorenzo PLatania*/ 01874 01875 // solvable fact (e.g. solvable equations) are added to d_eq CDList, 01876 // all the others have to be in a different CDList. If the equation is 01877 // solvable it comes here already solved. Should distinguish between 01878 // solved and not solved eqs 01879 void TheoryBitvector::assertFact(const Theorem& e) 01880 { 01881 const Expr& expr = e.getExpr(); 01882 TRACE("bvAssertFact", "TheoryBitvector::assertFact(", e.getExpr().toString(), ")"); 01883 // cout<<"TheoryBitvector::assertFact, expr: "<<expr.toString()<<endl; 01884 // every time a new fact is added to the list the whole set may be 01885 // not in a solved form 01886 01887 switch (expr.getOpKind()) { 01888 01889 case BVTYPEPRED: 01890 assertTypePred(expr[0], e); 01891 break; 01892 01893 case BOOLEXTRACT: 01894 // facts form the SAT solver are just ignored 01895 return; 01896 01897 case NOT: 01898 // facts form the SAT solver are just ignored 01899 if (expr[0].getOpKind() == BOOLEXTRACT) return; 01900 01901 if (expr[0].getOpKind() == BVTYPEPRED) { 01902 Expr tpExpr = getTypePredExpr(expr[0]); 01903 Theorem tpThm = typePred(tpExpr); 01904 DebugAssert(tpThm.getExpr() == expr[0], "Expected BVTYPEPRED theorem"); 01905 setInconsistent(getCommonRules()->contradictionRule(tpThm, e)); 01906 return; 01907 } 01908 01909 DebugAssert(expr[0].isEq(), "Unexpected negation"); 01910 01911 d_bitblast.push_back(e); 01912 break; 01913 01914 case EQ: 01915 // Updates are also ignored: 01916 // Note: this can only be true if this fact was asserted as a result of 01917 // assertEqualities. For BV theory, this should only be possible if 01918 // the update was made from our own theory, so we can ignore it. 01919 if (theoryCore()->inUpdate()) return; 01920 01921 // If we have already started bitblasting, just store the eq in d_bitblast; 01922 // if we haven't yet bitblasted and expr is a solved linear equation then 01923 // we store it in d_eq CDList, otherwise we store it in d_eqPending 01924 if (d_bb_index != 0) { 01925 d_bitblast.push_back(e); 01926 } 01927 else if (isLeaf(expr[0]) && !isLeafIn(expr[0], expr[1])) { 01928 d_eq.push_back( e ); 01929 } 01930 else { 01931 d_eqPending.push_back( e ); 01932 } 01933 break; 01934 01935 default: 01936 // if the fact is not an equation it will be bit-blasted 01937 d_bitblast.push_back( e ); 01938 break; 01939 } 01940 } 01941 01942 01943 //TODO: can we get rid of this in exchange for a more general politeness-based sharing mechanism? 01944 void TheoryBitvector::assertTypePred(const Expr& e, const Theorem& pred) { 01945 // Ignore bitvector constants (they always satisfy type predicates) 01946 // and bitvector operators. When rewrites and updates are enabled. 01947 // their type predicates will be implicitly derived from the type 01948 // predicates of the arguments. 01949 01950 if (theoryOf(e) == this) return; 01951 TRACE("bvAssertTypePred", "TheoryBitvector::assertTypePred(", e.toString(PRESENTATION_LANG), ")"); 01952 addSharedTerm(e); 01953 } 01954 01955 01956 /*Beginning of Lorenzo PLatania's methods*/ 01957 01958 // evaluates the gcd of two integers using 01959 // Euclid algorithm 01960 // int TheoryBitvector::gcd(int c1, int c2) 01961 // { 01962 // if(c2==0) 01963 // return c1; 01964 // else 01965 // return gcd( c2, c1%c2); 01966 // } 01967 01968 void TheoryBitvector::extract_vars(const Expr& e, vector<Expr>& result) 01969 { 01970 if (e.getOpKind() == BVMULT ) { 01971 extract_vars(e[0], result); 01972 extract_vars(e[1], result); 01973 } 01974 else { 01975 DebugAssert(e.getOpKind() != BVCONST && 01976 e.getOpKind() != BVUMINUS && 01977 e.getOpKind() != BVPLUS, "Unexpected structure"); 01978 result.push_back(e); 01979 } 01980 } 01981 01982 01983 Expr TheoryBitvector::multiply_coeff( Rational mult_inv, const Expr& e) 01984 { 01985 01986 // nothing to be done 01987 if( mult_inv == 1) 01988 return e; 01989 if(e.isEq()) 01990 { 01991 Expr lhs = e[0]; 01992 Expr rhs = e[1]; 01993 Expr new_lhs = multiply_coeff( mult_inv, lhs); 01994 Expr new_rhs = multiply_coeff( mult_inv, rhs); 01995 Expr res(EQ, new_lhs, new_rhs); 01996 return res; 01997 } 01998 else 01999 { 02000 int kind = e.getOpKind(); 02001 int size = BVSize(e); 02002 if( kind == BVMULT ) 02003 { 02004 02005 //lhs is like 'a_0*x_0' 02006 Rational new_coeff = mult_inv * computeBVConst( e[0] ); 02007 Expr new_expr_coeff = newBVConstExpr( new_coeff, size); 02008 Expr BV_one = newBVConstExpr(1,size); 02009 if( new_expr_coeff == BV_one ) 02010 { 02011 return e[1]; 02012 } 02013 else 02014 { 02015 return newBVMultExpr( size, new_expr_coeff, e[1]); 02016 } 02017 } 02018 else 02019 if( kind == BVPLUS) 02020 { 02021 02022 int expr_arity= e.arity(); 02023 std::vector<Expr> tmp_list; 02024 for( int i = 0; i < expr_arity; ++i) 02025 { 02026 tmp_list.push_back(multiply_coeff( mult_inv, e[i])); 02027 } 02028 // Expr::iterator i = e.begin(); 02029 // int index; 02030 // Expr::iterator end = e.end(); 02031 // std::vector<Expr> tmp_list; 02032 // for( i = e.begin(), index=0; i!=end; ++i, ++index) 02033 // { 02034 // tmp_list.push_back(multiply_coeff( mult_inv, *i)); 02035 // } 02036 return newBVPlusExpr(size, tmp_list); 02037 } 02038 else 02039 if( kind == BVCONST ) 02040 { 02041 02042 Rational new_const = mult_inv * computeBVConst(e); 02043 Expr res = newBVConstExpr( new_const, size); 02044 // cout<<res.toString()+"\n"; 02045 return res; 02046 } 02047 else 02048 if( isLeaf( e ) ) 02049 { 02050 //lhs is like 'x_0' 02051 // need to know the lenght of the var 02052 // L:: guess it is not correct, mult_inv * e 02053 Expr BV_mult_inv = newBVConstExpr( mult_inv, size); 02054 Expr new_var = newBVMultExpr( size, BV_mult_inv, e); 02055 02056 return new_var; 02057 } 02058 else 02059 { 02060 return e; 02061 } 02062 } 02063 } 02064 02065 // L::return the index of the minimum element returns -1 if the list 02066 // is empty assuming only non-negative elements to be sostituted with 02067 // some debug assertion. ***I guess n_bits can be just an integer, no 02068 // need to declare it as a Rational 02069 02070 Rational TheoryBitvector::multiplicative_inverse(Rational r, int n_bits) 02071 { 02072 02073 // cout<<"TheoryBitvector::multiplicative_inverse: working on "<<r.toString()<<endl; 02074 Rational i=r; 02075 Rational max_val= pow( n_bits, (Rational) 2); 02076 while(r!=1) 02077 { 02078 r = ( r*r ) % max_val; 02079 i = ( i*r ) % max_val; 02080 } 02081 // cout<<"TheoryBitvector::multiplicative_inverse: result is "<<i.toString()<<endl; 02082 return i; 02083 } 02084 02085 // int TheoryBitvector::min(std::vector<Rational> list) 02086 // { 02087 // int res = 0; 02088 // int i; 02089 // int size = list.size(); 02090 // for(i = 0; i < size; ++i) 02091 // { 02092 // cout<<"list["<<i<<"]: "<<list[i]<<endl; 02093 // } 02094 // for(i = 1; i < size; ++i) 02095 // { 02096 // if(list[res]>list[i]) 02097 // res=i; 02098 // cout<<"res: "<<res<<endl; 02099 // cout<<"min: "<<list[res]<<endl; 02100 // } 02101 02102 // cout<<"min: "<<res<<endl; 02103 // return res; 02104 // } 02105 02106 //*************************** 02107 // ecco come fare il delete! 02108 //*************************** 02109 02110 // int main () 02111 // { 02112 // unsigned int i; 02113 // deque<unsigned int> mydeque; 02114 02115 // // set some values (from 1 to 10) 02116 // for (i=1; i<=10; i++) mydeque.push_back(i); 02117 02118 // // erase the 6th element 02119 // mydeque.erase (mydeque.begin()+5); 02120 02121 // // erase the first 3 elements: 02122 // mydeque.erase (mydeque.begin(),mydeque.begin()+3); 02123 02124 // cout << "mydeque contains:"; 02125 // for (i=0; i<mydeque.size(); i++) 02126 // cout << " " << mydeque[i]; 02127 // cout << endl; 02128 02129 // return 0; 02130 // } 02131 02132 // use the method in rational.h 02133 // it uses std::vector<Rational> instead of std::deque<int> 02134 // int TheoryBitvector::gcd(std::deque<int> coeff_list) 02135 // { 02136 02137 // cout<<"TheoryBitvector::gcd: begin\n"; 02138 // for(unsigned int i=0; i<coeff_list.size(); ++i) 02139 // { 02140 // cout<<"coeff_list["<<i<<"]: "<<coeff_list[i]<<endl; 02141 // } 02142 // int gcd_list; 02143 // int min_index = min(coeff_list); 02144 // int min_coeff_1 = coeff_list[min_index]; 02145 // cout<<"erasing element: "<<coeff_list[min_index]; 02146 // coeff_list.erase( coeff_list.begin() + min_index ); 02147 02148 // while(coeff_list.size()>0) 02149 // { 02150 // min_index = min(coeff_list); 02151 // int min_coeff_2 = coeff_list[min_index]; 02152 // cout<<"erasing element: "<<coeff_list[min_index]; 02153 // coeff_list.erase( coeff_list.begin() + min_index ); 02154 02155 // // save one recursion 02156 // gcd_list = gcd( min_coeff_2, min_coeff_1); 02157 // cout<<"TheoryBitvector::gcd: erased min1\n"; 02158 // min_coeff_1 = gcd_list; 02159 // } 02160 // cout<<"gcd_list: "<<gcd_list<<endl; 02161 // return gcd_list; 02162 // } 02163 02164 // int TheoryBitvector::bv2int(const Expr& e) 02165 // { 02166 // int sum=0; 02167 // if(e.arity()==0 && ! e.isVar()) 02168 // { 02169 // std::string tmp = e.toString(); 02170 // int s_length = tmp.length(); 02171 // int bit; 02172 // int exp; 02173 // // first 4 cells contains the bv prefix 0bin 02174 // // just discard them 02175 // for(int i=3; i < s_length; ++i) 02176 // { 02177 // if(tmp[i]=='1') 02178 // { 02179 // sum += (int)std::pow((float) 2, s_length - 1 - i); 02180 // } 02181 // } 02182 // } 02183 // else 02184 // { 02185 // cerr<<"error: non-constant to be converted\n"; 02186 // } 02187 // return sum; 02188 // } 02189 02190 // returning the position of the first odd coefficient found; 02191 // moreover, it multiplies a variable which does not appear in other 02192 // subterms. It assumes that the input expression has already been 02193 // canonized, so the lhs is a flat BVPLUS expression and the rhs is a 02194 // zero BVCONST 02195 02196 Rational TheoryBitvector::Odd_coeff( const Expr& e ) 02197 { 02198 int bv_size = BVSize(e[0]); 02199 Expr bv_zero( newBVZeroString(bv_size)); 02200 02201 DebugAssert(e.getOpKind()==EQ && e[1] == bv_zero, 02202 "TheoryBitvector::Odd_coeff: the input expression has a non valid form "); 02203 02204 Expr lhs = e[0]; 02205 if( lhs.getOpKind() == BVMULT ) 02206 { 02207 if( lhs[0].getOpKind() == BVCONST && computeBVConst( lhs[0]) % 2 != 0) 02208 return computeBVConst( lhs[0] ); 02209 } 02210 else 02211 if( isLeaf( lhs)) 02212 return 1; 02213 else 02214 if( lhs.getOpKind() == BVPLUS ) 02215 { 02216 int lhs_arity = lhs.arity(); 02217 // scanning lhs in order to find a good odd coefficient 02218 for( int i = 0; i < lhs_arity; ++i) 02219 { 02220 // checking that the subterm is a leaf 02221 if( isLeaf( lhs[i] ) ) 02222 { 02223 // checking that the current subterm does not appear in other 02224 // subterms 02225 for( int j = 0; j < lhs_arity; ++j) 02226 if( j != i && !isLeafIn( lhs[i], lhs[j] )) 02227 return 1; 02228 } 02229 else 02230 if( lhs[i].getOpKind() == BVMULT) 02231 { 02232 // the subterm is a BVMULT with a odd coefficient 02233 if( lhs[i][0].getOpKind() == BVCONST && computeBVConst( lhs[i][0]) % 2 != 0) 02234 { 02235 // checking that the current subterm does not appear in other 02236 // subterms 02237 int flag = 0; 02238 for( int j = 0; j < lhs_arity; ++j) 02239 { 02240 // as we can solve also for non-leaf terms we use 02241 // isTermIn instead of isLeafIn 02242 if( j != i && isTermIn( lhs[i][1], lhs[j] )) 02243 flag = 1; 02244 } 02245 // if the leaf is not a subterm of other terms in the 02246 // current expression then we can solve for it 02247 if( flag == 0) 02248 return computeBVConst( lhs[i][0] ); 02249 } 02250 } 02251 else 02252 // the subterm is a non-linear one 02253 if ( lhs[i].getOpKind() != BVCONST ) 02254 { 02255 // checking that the current subterm does not appear in other 02256 // subterms 02257 for( int j = 0; j < lhs_arity; ++j) 02258 if( j != i && !isLeafIn( lhs[i][1], lhs[j] )) 02259 return 1; 02260 } 02261 else 02262 ; 02263 } 02264 } 02265 // no leaf found to solve for 02266 return 0; 02267 } 02268 02269 int TheoryBitvector::check_linear( const Expr &e ) 02270 { 02271 TRACE("bv_check_linear", "TheoryBitvector::check_linear(", e.toString(PRESENTATION_LANG), ")"); 02272 // recursively check if the expression is linear 02273 if( e.isVar() || e.getOpKind() == BVCONST ) 02274 return 1; 02275 else 02276 if( e.getOpKind() == BVPLUS ) 02277 { 02278 int e_arity= e.arity(); 02279 int flag = 1; 02280 for( int i=0; i < e_arity && flag == 1; ++i) 02281 { 02282 flag = check_linear( e[i]); 02283 } 02284 return flag; 02285 } 02286 else 02287 if( e.getOpKind() == BVMULT) 02288 { 02289 if( e[0].getOpKind() == BVCONST && e[1].isVar() ) 02290 return 1; 02291 else 02292 return 0; 02293 } 02294 else 02295 if( e.getOpKind() == BVUMINUS) 02296 return check_linear( e[0]); 02297 else 02298 if( e.getOpKind() == EQ ) 02299 return ( check_linear( e[0] ) && check_linear( e[1] )); 02300 else 02301 // all other operators are non-linear 02302 return 0; 02303 } 02304 02305 // please check it is right. It is the same as Theory::isLeafIn but it 02306 // does not require e1 to be a leaf. In this way we can check for e1 02307 // to be a subterm of other expressions even if it is not a leaf, 02308 // i.e. a non-linear term 02309 bool TheoryBitvector::isTermIn(const Expr& e1, const Expr& e2) 02310 { 02311 if (e1 == e2) return true; 02312 if (theoryOf(e2) != this) return false; 02313 for(Expr::iterator i=e2.begin(), iend=e2.end(); i != iend; ++i) 02314 if (isTermIn(e1, *i)) return true; 02315 return false; 02316 } 02317 02318 // checks whether e can be solved in term 02319 bool TheoryBitvector::canSolveFor( const Expr& term, const Expr& e ) 02320 { 02321 DebugAssert( e.getOpKind() == EQ, "TheoryBitvector::canSolveFor, input 'e' must be an equation"); 02322 02323 // cout<<"TheoryBitvector::canSolveFor, term: "<<term.toString()<<endl; 02324 // the term has not a unary coefficient, so we did not multiply the 02325 // equation by its multiplicative inverse 02326 if( term.getOpKind() == BVMULT && term[0].getOpKind() == BVCONST) 02327 return 0; 02328 else 02329 if( isLeaf( term ) || !isLinearTerm( term)) 02330 { 02331 int count = countTermIn( term, e); 02332 // cout<<"TheoryBitvector::canSolveFor, count for "<<term.toString()<<" is: "<<count<<endl; 02333 if( count == 1) 02334 return true; 02335 else 02336 return false; 02337 } 02338 else 02339 { 02340 DebugAssert( false, "TheoryBitvector::canSolveFor, input 'term' of not treated kind"); 02341 return false; 02342 } 02343 } 02344 02345 int TheoryBitvector::countTermIn( const Expr& term, const Expr& e) 02346 { 02347 // cout<<"TheoryBitvector::countTermIn, term: "<<term.toString()<<" e: "<<e.toString()<<endl; 02348 int e_arity = e.arity(); 02349 int result = 0; 02350 // base cases recursion happen when e is a constant or a leaf 02351 if( e.getOpKind() == BVCONST ) 02352 return 0; 02353 if( term == e ) 02354 return 1; 02355 02356 for( int i = 0; i < e_arity; ++i) 02357 { 02358 result += countTermIn( term, e[i]); 02359 } 02360 return result; 02361 } 02362 02363 bool TheoryBitvector::isLinearTerm( const Expr& e ) 02364 { 02365 if( isLeaf( e ) ) 02366 return true; 02367 switch( e.getOpKind()) 02368 { 02369 case BVPLUS: 02370 return true; 02371 case BVMULT: 02372 if( e[0].getOpKind() == BVCONST && isLinearTerm( e[1] )) 02373 return true; 02374 else 02375 return false; 02376 break; 02377 default: 02378 return false; 02379 } 02380 } 02381 02382 02383 // returns thm if no change 02384 Theorem TheoryBitvector::simplifyPendingEq(const Theorem& thm, int maxEffort) 02385 { 02386 Expr e = thm.getExpr(); 02387 DebugAssert(e.getKind() == EQ, "Expected EQ"); 02388 Expr lhs = e[0]; 02389 Expr rhs = e[1]; 02390 02391 Theorem thm2 = thm; 02392 if (!isLeaf(lhs)) { 02393 // Carefully simplify lhs: 02394 // We can't take find(lhs) because find(lhs) = find(rhs) and this would result in a trivially true equation. 02395 // So, take the find of the children instead. 02396 int ar = lhs.arity(); 02397 vector<Theorem> newChildrenThm; 02398 vector<unsigned> changed; 02399 Theorem thm0; 02400 for (int k = 0; k < ar; ++k) { 02401 thm0 = find(lhs[k]); 02402 if (thm0.getLHS() != thm0.getRHS()) { 02403 newChildrenThm.push_back(thm0); 02404 changed.push_back(k); 02405 } 02406 } 02407 if(changed.size() > 0) { 02408 // lhs = updated_lhs 02409 thm0 = substitutivityRule(lhs, changed, newChildrenThm); 02410 // lhs = updated_and_rewritten_lhs 02411 thm0 = transitivityRule(thm0, rewrite(thm0.getRHS())); 02412 // updated_and_rewritten_lhs = rhs 02413 thm2 = transitivityRule(symmetryRule(thm0), thm); 02414 } 02415 } 02416 // updated_and_rewritten_lhs = find(rhs) 02417 thm2 = transitivityRule(thm2, find(rhs)); 02418 // canonized EQ 02419 thm2 = iffMP(thm2, d_rules->canonBVEQ(thm2.getExpr(), maxEffort)); 02420 if (thm2.isRewrite() && thm2.getRHS() == lhs && thm2.getLHS() == rhs) { 02421 thm2 = thm; 02422 } 02423 return thm2; 02424 } 02425 02426 02427 Theorem TheoryBitvector::generalBitBlast( const Theorem& thm ) 02428 { 02429 // cout<<"TheoryBitvector::generalBitBlast, thm: "<<thm.toString()<<" to expr(): "<<thm.getExpr().toString()<<endl; 02430 Expr e = thm.getExpr(); 02431 switch (e.getOpKind()) { 02432 case EQ: { 02433 Theorem thm2 = simplifyPendingEq(thm, 6); 02434 const Expr& e2 = thm2.getExpr(); 02435 switch (e2.getKind()) { 02436 case TRUE_EXPR: 02437 case FALSE_EXPR: 02438 return thm2; 02439 case EQ: 02440 return iffMP(thm2, bitBlastEqn(thm2.getExpr())); 02441 case AND: { 02442 DebugAssert(e2.arity() == 2 && e2[0].getKind() == EQ && e2[1].getKind() == EQ, 02443 "Expected two equations"); 02444 Theorem t1 = bitBlastEqn(e2[0]); 02445 Theorem t2 = bitBlastEqn(e2[1]); 02446 Theorem thm3 = substitutivityRule(e2, t1, t2); 02447 return iffMP(thm2, thm3); 02448 } 02449 default: 02450 FatalAssert(false, "Unexpected Expr"); 02451 break; 02452 } 02453 break; 02454 } 02455 case BVLT: 02456 case BVLE: { 02457 // Carefully simplify 02458 int ar = e.arity(); 02459 DebugAssert(ar == 2, "Expected arity 2"); 02460 vector<Theorem> newChildrenThm; 02461 vector<unsigned> changed; 02462 Theorem thm0; 02463 for (int k = 0; k < ar; ++k) { 02464 thm0 = find(e[k]); 02465 if (thm0.getLHS() != thm0.getRHS()) { 02466 newChildrenThm.push_back(thm0); 02467 changed.push_back(k); 02468 } 02469 } 02470 if(changed.size() > 0) { 02471 // updated_e 02472 thm0 = iffMP(thm, substitutivityRule(e, changed, newChildrenThm)); 02473 // updated_and_rewritten_e 02474 thm0 = iffMP(thm0, rewrite(thm0.getExpr())); 02475 if (thm0.getExpr().getOpKind() != e.getOpKind()) return thm0; 02476 return iffMP(thm0, bitBlastIneqn(thm0.getExpr())); 02477 } 02478 return iffMP(thm, bitBlastIneqn(e)); 02479 } 02480 // a NOT should mean a disequality, as negation of inequalities 02481 // can be expressed as other inequalities. 02482 case NOT: { 02483 // Carefully simplify 02484 DebugAssert(e.arity() == 1, "Expected arity 1"); 02485 DebugAssert(e[0].isEq(), "Expected disequality"); 02486 DebugAssert(e[0].arity() == 2, "Expected arity 2"); 02487 vector<Theorem> newChildrenThm; 02488 vector<unsigned> changed; 02489 Theorem thm0; 02490 for (int k = 0; k < 2; ++k) { 02491 thm0 = find(e[0][k]); 02492 if (thm0.getLHS() != thm0.getRHS()) { 02493 newChildrenThm.push_back(thm0); 02494 changed.push_back(k); 02495 } 02496 } 02497 if(changed.size() > 0) { 02498 // a = b <=> a' = b' 02499 thm0 = substitutivityRule(e[0], changed, newChildrenThm); 02500 } 02501 else thm0 = reflexivityRule(e[0]); 02502 // a = b <=> canonized EQ 02503 thm0 = transitivityRule(thm0, d_rules->canonBVEQ(thm0.getRHS(), 6)); 02504 // NOT(canonized EQ) 02505 thm0 = iffMP(thm, substitutivityRule(e, thm0)); 02506 if (thm0.getExpr()[0].isEq()) { 02507 return bitBlastDisEqn(thm0); 02508 } 02509 else return thm0; 02510 } 02511 default: 02512 FatalAssert(false, "TheoryBitvector::generalBitBlast: unknown expression kind"); 02513 break; 02514 } 02515 return reflexivityRule( e ); 02516 } 02517 /*End of Lorenzo PLatania's methods*/ 02518 02519 static Expr findAtom(const Expr& e) 02520 { 02521 if (e.isAbsAtomicFormula()) return e; 02522 for (int i = 0; i < e.arity(); ++i) { 02523 Expr e_i = findAtom(e[i]); 02524 if (!e_i.isNull()) return e_i; 02525 } 02526 return Expr(); 02527 } 02528 02529 02530 bool TheoryBitvector::comparebv(const Expr& e1, const Expr& e2) 02531 { 02532 int size = BVSize(e1); 02533 FatalAssert(size == BVSize(e2), "expected same size"); 02534 Theorem c1, c2; 02535 int idx1 = -1; 02536 vector<Theorem> thms1; 02537 02538 if (d_bb_index == 0) { 02539 Expr splitter = e1.eqExpr(e2); 02540 Theorem thm = simplify(splitter); 02541 if (!thm.getRHS().isBoolConst()) { 02542 addSplitter(e1.eqExpr(e2)); 02543 return true; 02544 } 02545 // Store a dummy theorem to indicate bitblasting has begun 02546 d_bb_index = 1; 02547 d_bitblast.push_back(getCommonRules()->trueTheorem()); 02548 } 02549 02550 for (int i = 0; i < size; ++i) { 02551 c1 = bitBlastTerm(e1, i); 02552 c1 = transitivityRule(c1, simplify(c1.getRHS())); 02553 c2 = bitBlastTerm(e2, i); 02554 c2 = transitivityRule(c2, simplify(c2.getRHS())); 02555 thms1.push_back(c1); 02556 if (!c1.getRHS().isBoolConst()) { 02557 if (idx1 == -1) idx1 = i; 02558 continue; 02559 } 02560 if (!c2.getRHS().isBoolConst()) { 02561 continue; 02562 } 02563 if (c1.getRHS() != c2.getRHS()) return false; 02564 } 02565 if (idx1 == -1) { 02566 // If e1 is known to be a constant, assert that 02567 DebugAssert(e1.getKind() != BVCONST, "Expected non-const"); 02568 assertEqualities(d_rules->bitExtractAllToConstEq(thms1)); 02569 addSplitter(e1.eqExpr(e2)); 02570 // enqueueFact(getCommonRules()->trueTheorem()); 02571 return true; 02572 } 02573 02574 Theorem thm = bitBlastEqn(e1.eqExpr(e2)); 02575 thm = iffMP(thm, simplify(thm.getExpr())); 02576 if (!thm.getExpr().isTrue()) { 02577 enqueueFact(thm); 02578 return true; 02579 } 02580 02581 // Nothing to assert from bitblasted equation. Best way to resolve this 02582 // problem is to split until the term can be equated with a bitvector 02583 // constant. 02584 Expr e = findAtom(thms1[idx1].getRHS()); 02585 DebugAssert(!e.isNull(), "Expected atom"); 02586 addSplitter(e); 02587 return true; 02588 } 02589 02590 static bool bvdump = false; 02591 02592 void TheoryBitvector::checkSat(bool fullEffort) 02593 { 02594 if(fullEffort) { 02595 02596 for (unsigned i = 0; i < additionalRewriteConstraints.size(); i ++) 02597 enqueueFact(additionalRewriteConstraints[i]); 02598 additionalRewriteConstraints.clear(); 02599 02600 if (bvdump) { 02601 CDList<Theorem>::const_iterator it_list=d_eq.begin(); 02602 unsigned int i; 02603 for(i=0; i<d_eq.size(); ++i) 02604 { 02605 cout<<"d_eq [" << i << "]= "<< it_list[i].getExpr().toString() << endl; 02606 } 02607 02608 it_list=d_eqPending.begin(); 02609 02610 for(i=0; i<d_eqPending.size(); ++i) 02611 { 02612 cout<<"d_eqPending [" << i << "]= "<< it_list[i].getExpr().toString() << endl; 02613 } 02614 02615 it_list=d_bitblast.begin(); 02616 02617 for(i=0; i<d_bitblast.size(); ++i) 02618 { 02619 cout<<"d_bitblast [" << i << "]= "<< it_list[i].getExpr().toString() << endl; 02620 } 02621 02622 if (d_eq.size() || d_eqPending.size() || d_bitblast.size()) cout << endl; 02623 } 02624 02625 unsigned eq_list_size = d_eqPending.size(); 02626 bool bitBlastEq = d_eq_index < eq_list_size; 02627 if (d_bb_index == 0 && bitBlastEq) { 02628 bitBlastEq = false; 02629 unsigned eqIdx = d_eq_index; 02630 for(; eqIdx < eq_list_size; ++eqIdx) { 02631 Expr eq = d_eqPending[eqIdx].getExpr(); 02632 DebugAssert(eq[1] == newBVConstExpr(Rational(0), BVSize(eq[0])), "Expected 0 on rhs"); 02633 Theorem thm = simplifyPendingEq(d_eqPending[eqIdx], 5); 02634 if (thm == d_eqPending[eqIdx]) { 02635 bitBlastEq = true; 02636 continue; 02637 } 02638 const Expr& e2 = thm.getExpr(); 02639 switch (e2.getKind()) { 02640 case TRUE_EXPR: 02641 break; 02642 case FALSE_EXPR: 02643 enqueueFact(thm); 02644 return; 02645 case EQ: 02646 case AND: 02647 if (simplify(thm.getExpr()).getRHS() == trueExpr()) { 02648 bitBlastEq = true; 02649 break; 02650 } 02651 for (; d_eq_index < eqIdx; d_eq_index = d_eq_index + 1) { 02652 d_eqPending.push_back(d_eqPending[d_eq_index]); 02653 } 02654 d_eq_index = d_eq_index + 1; 02655 enqueueFact(thm); 02656 return; 02657 default: 02658 FatalAssert(false, "Unexpected expr"); 02659 break; 02660 } 02661 } 02662 } 02663 02664 // Bitblast any new formulas 02665 unsigned bb_list_size = d_bitblast.size(); 02666 bool bbflag = d_bb_index < bb_list_size || bitBlastEq; 02667 if (bbflag) { 02668 for( ; d_bb_index < bb_list_size; d_bb_index = d_bb_index + 1) { 02669 Theorem bb_result = generalBitBlast( d_bitblast[ d_bb_index ]); 02670 enqueueFact( bb_result); 02671 } 02672 if (d_bb_index == 0) { 02673 // push dummy on the stack to indicate bitblasting has started 02674 d_bb_index = 1; 02675 d_bitblast.push_back(getCommonRules()->trueTheorem()); 02676 } 02677 for( ; d_eq_index < eq_list_size; d_eq_index = d_eq_index + 1) { 02678 Theorem bb_result = generalBitBlast( d_eqPending[ d_eq_index ]); 02679 enqueueFact( bb_result); 02680 } 02681 // If newly bitblasted formulas, skip the shared term check 02682 return; 02683 } 02684 02685 // Check that all shared terms are distinct 02686 Theorem thm; 02687 for (; d_index1 < d_sharedSubtermsList.size(); d_index1 = d_index1 + 1, d_index2 = 0) { 02688 const Expr& e1 = d_sharedSubtermsList[d_index1]; 02689 if (find(e1).getRHS() != e1) continue; 02690 for (; d_index2 < d_index1; d_index2 = d_index2 + 1) { 02691 const Expr& e2 = d_sharedSubtermsList[d_index2]; 02692 DebugAssert(e1 != e2, "should be distinct"); 02693 if (e1.getKind() == BVCONST && e2.getKind() == BVCONST) continue; 02694 if (find(e2).getRHS() != e2) continue; 02695 if (BVSize(e1) != BVSize(e2)) continue; 02696 if (e1.getKind() == BVCONST) { 02697 if (!comparebv(e2, e1)) continue; 02698 } 02699 else { 02700 if (!comparebv(e1, e2)) continue; 02701 } 02702 // comparebv enqueued something, so we can return 02703 return; 02704 } 02705 } 02706 } 02707 } 02708 02709 02710 Theorem TheoryBitvector::rewrite(const Expr& e) 02711 { 02712 ExprMap<Theorem> cache; 02713 return rewriteBV(e, cache); 02714 } 02715 02716 02717 Theorem TheoryBitvector::rewriteAtomic(const Expr& e) 02718 { 02719 return reflexivityRule(e); 02720 } 02721 02722 02723 void TheoryBitvector::setup(const Expr& e) 02724 { 02725 int k(0), ar(e.arity()); 02726 if( e.isTerm() ) { 02727 for ( ; k < ar; ++k) { 02728 e[k].addToNotify(this, e); 02729 } 02730 } 02731 } 02732 02733 02734 // Lorenzo's version 02735 void TheoryBitvector::update(const Theorem& e, const Expr& d) { 02736 02737 if (inconsistent()) return; 02738 // cout<<"TheoryBitvector::update, theorem e:"<<e.toString()<<" expression d: "<<d.toString()<<endl; 02739 // Updating shared terms informations, code inherited from the old 02740 // version of the bitvector theory 02741 02742 // Constants should never change their find pointers to non-constant 02743 // expressions 02744 DebugAssert(e.getLHS().getOpKind()!=BVCONST, 02745 "TheoryBitvector::update(e="+e.getExpr().toString() 02746 +", d="+d.toString()); 02747 if (d.isNull()) { 02748 Expr lhs = e.getLHS(); 02749 Expr rhs = e.getRHS(); 02750 DebugAssert(d_sharedSubterms.find(lhs) != d_sharedSubterms.end(), 02751 "Expected lhs to be shared"); 02752 CDMap<Expr,Expr>::iterator it = d_sharedSubterms.find(rhs); 02753 if (it == d_sharedSubterms.end()) { 02754 addSharedTerm(rhs); 02755 } 02756 return; 02757 } 02758 // { 02759 // // found an equality between shared subterms! 02760 // bool changed = false; 02761 // if ((*it).second != lhs) { 02762 // lhs = (*it).second; 02763 // it = d_sharedSubterms.find(lhs); 02764 // DebugAssert(it != d_sharedSubterms.end() && (*it).second == lhs, 02765 // "Invariant violated in TheoryBitvector::update"); 02766 // changed = true; 02767 // } 02768 // if ((*it2).second != rhs) { 02769 // rhs = (*it2).second; 02770 // it2 = d_sharedSubterms.find(rhs); 02771 // DebugAssert(it2 != d_sharedSubterms.end() && (*it2).second == rhs, 02772 // "Invariant violated in TheoryBitvector::update"); 02773 // changed = true; 02774 // } 02775 // DebugAssert(findExpr(lhs) == e.getRHS() && 02776 // findExpr(rhs) == e.getRHS(), "Unexpected value for finds"); 02777 // // It may be needed to check whether the two terms are the 02778 // // same, in that case don't do anything 02779 // if (changed) { 02780 // Theorem thm = transitivityRule(find(lhs),symmetryRule(find(rhs))); 02781 // const Expr& expr = thm.getExpr(); 02782 02783 // if (d_bb_index == 0 && 02784 // isLeaf(expr[0]) && !isLeafIn(expr[0], expr[1])) { 02785 // d_eq.push_back( thm ); 02786 // } 02787 // else { 02788 // d_bitblast.push_back( thm ); 02789 // } 02790 // } 02791 02792 02793 // // canonize and solve befor asserting it 02794 // // cout<<"TheoryBitvector::update, thm.getRHS(): "<<thm.getRHS()<<" thm.getLHS():"<<thm.getLHS()<<" thm.getExpr():"<<thm.getExpr()<<endl; 02795 // Theorem rwt_thm = rewrite( thm.getExpr() ); 02796 // Theorem solved_thm = solve( rwt_thm); 02797 // assertFact( solved_thm ); 02798 // assertFact( thm ); 02799 // enqueueFact(iffMP(thm, bitBlastEqn(thm.getExpr()))); 02800 // } 02801 // else 02802 // { 02803 // d_sharedSubterms[rhs] = (*it).second; 02804 // } 02805 // } 02806 // Propagate the "find" information to all the terms in the notify 02807 // list of d 02808 02809 // if d has no find there is nothing to be updated 02810 if (!d.hasFind()) return; 02811 02812 if (find(d).getRHS() == d) { 02813 // Theorem thm = updateSubterms(d); 02814 // TRACE("bvupdate", "TheoryArithOld::update(): thm = ", thm, ""); 02815 // DebugAssert(leavesAreSimp(thm.getRHS()), "updateHelper error: " 02816 // +thm.getExpr().toString()); 02817 Theorem thm = simplify(d); 02818 DebugAssert(thm.getRHS().isAtomic(), "Expected atomic"); 02819 assertEqualities(thm); 02820 } 02821 } 02822 02823 02824 Theorem TheoryBitvector::updateSubterms( const Expr& e ) 02825 { 02826 // DebugAssert(canonRec(e).getRHS() == e, "canonSimp expects input to be canonized"); 02827 int ar = e.arity(); 02828 if (isLeaf(e)) return find(e); 02829 if (ar > 0) { 02830 vector<Theorem> newChildrenThm; 02831 vector<unsigned> changed; 02832 Theorem thm; 02833 for (int k = 0; k < ar; ++k) { 02834 thm = updateSubterms(e[k]); 02835 if (thm.getLHS() != thm.getRHS()) { 02836 newChildrenThm.push_back(thm); 02837 changed.push_back(k); 02838 } 02839 } 02840 if(changed.size() > 0) { 02841 thm = substitutivityRule(e, changed, newChildrenThm); 02842 thm = transitivityRule(thm, rewrite(thm.getRHS())); 02843 return transitivityRule(thm, find(thm.getRHS())); 02844 } 02845 else return find(e); 02846 } 02847 return find(e); 02848 } 02849 02850 02851 Theorem TheoryBitvector::solve(const Theorem& t) 02852 { 02853 DebugAssert(t.isRewrite() && t.getLHS().isTerm(), ""); 02854 Expr e = t.getExpr(); 02855 02856 if (isLeaf(e[0]) && !isLeafIn(e[0], e[1])) { 02857 // already solved 02858 return t; 02859 } 02860 else if (isLeaf(e[1]) && !isLeafIn(e[1], e[0])) { 02861 return symmetryRule(t); 02862 } 02863 else if (e[0].getOpKind() == EXTRACT && isLeaf(e[0][0])) { 02864 bool solvedForm; 02865 Theorem thm; 02866 if (d_rules->solveExtractOverlapApplies(e)) 02867 { 02868 thm = iffMP(t, d_rules->solveExtractOverlap(e)); 02869 solvedForm = true; 02870 } 02871 else 02872 thm = d_rules->processExtract(t, solvedForm); 02873 02874 thm = getCommonRules()->skolemize(thm); 02875 02876 if (solvedForm) return thm; 02877 else { 02878 enqueueFact(getCommonRules()->andElim(thm, 1)); 02879 return getCommonRules()->andElim(thm, 0); 02880 } 02881 } 02882 else if (e[1].getOpKind() == EXTRACT && isLeaf(e[1][0])) { 02883 bool solvedForm; 02884 Theorem thm = getCommonRules()->skolemize(d_rules->processExtract(symmetryRule(t), solvedForm)); 02885 if (solvedForm) return thm; 02886 else { 02887 enqueueFact(getCommonRules()->andElim(thm, 1)); 02888 return getCommonRules()->andElim(thm, 0); 02889 } 02890 } 02891 02892 IF_DEBUG( 02893 Theorem t2 = iffMP(t, d_rules->canonBVEQ(e)); 02894 if (e[0] < e[1]) { 02895 DebugAssert(e[1].getOpKind() == BVCONST, 02896 "Should be only case when lhs < rhs"); 02897 t2 = symmetryRule(t2); 02898 } 02899 DebugAssert(t2.getExpr() == e, "Expected no change"); 02900 ) 02901 02902 if (e[0].getOpKind() == BVCONST) { 02903 DebugAssert(e[1].getOpKind() != BVCONST, "should not have const = const"); 02904 return symmetryRule(t); 02905 } 02906 return t; 02907 } 02908 02909 // // solving just linear equations; for everything else I just return 02910 // // the same expression 02911 // if( ! e.isEq()) 02912 // { 02913 // return reflexivityRule( e ); 02914 // } 02915 // //the search for the odd coefficient should also check that the 02916 // //multiplied term does not appear in other terms. The coefficient can 02917 // //also multiply a non-linear term 02918 02919 02920 // // L:: look for a odd coefficient, if one, then the eq is solvable 02921 // // and we can find the mult-inverse using Barrett-Dill-Levitt 02922 // Expr lhs = e[0]; 02923 // Expr::iterator it = lhs.begin(), iend = lhs.end(); 02924 // for (; it != iend; ++it) { 02925 // switch ((*it).getOpKind()) { 02926 // case BVCONST: continue; 02927 // case BVMULT: { 02928 // DebugAssert((*it).arity() == 2 && 02929 // (*it)[0].getOpKind() == BVCONST && 02930 // computeBVConst((*it)[0]) != 1, "Unexpected format"); 02931 // continue 02932 // } 02933 02934 // coefficient = Odd_coeff( e ); 02935 // // Rational odd_coeff = anyOdd( coeff ); 02936 // if( coefficient != 0) 02937 // { 02938 // // the equation is solvable 02939 // cout<<"Odd coefficient found => the equation is solvable\n"; 02940 // if (coefficient != 1) { 02941 // Rational mult_inv = multiplicative_inverse( coefficient, BVSize(e[0])); 02942 // // multiply all the coefficients in the expression by the inverse 02943 // // Expr tmp_expr = e; 02944 // e = multiply_coeff( mult_inv, e); 02945 // // Expr isolated_expr = isolate_var( new_expr); 02946 // } 02947 02948 // Theorem solved_th = d_rules->isolate_var( t, e); 02949 // cout<<"solved theorem: "<<solved_th.toString()<<endl; 02950 // cout<<"solved theorem expr: "<<solved_th.getExpr().toString()<<endl; 02951 02952 // return iffMP( t, solved_th); 02953 // } 02954 // else 02955 // { 02956 // cout<<"Odd coefficient not found => the equation is not solvable\n"; 02957 // Theorem thm = d_rules->MarkNonSolvableEq( e ); 02958 // cout<<"TheoryBitvector::solve, input e: "<<e.toString()<<" thm: "<<thm.toString()<<endl; 02959 // return iffMP( t, thm); 02960 // //return reflexivityRule(e); 02961 // } 02962 //} 02963 02964 02965 void TheoryBitvector::checkType(const Expr& e) 02966 { 02967 switch (e.getOpKind()) { 02968 case BITVECTOR: 02969 //TODO: check that this is a well-formed type 02970 break; 02971 default: 02972 FatalAssert(false, "Unexpected kind in TheoryBitvector::checkType" 02973 +getEM()->getKindName(e.getOpKind())); 02974 } 02975 } 02976 02977 02978 Cardinality TheoryBitvector::finiteTypeInfo(Expr& e, Unsigned& n, 02979 bool enumerate, bool computeSize) 02980 { 02981 FatalAssert(e.getKind() == BITVECTOR, 02982 "Unexpected kind in TheoryBitvector::finiteTypeInfo"); 02983 if (enumerate || computeSize) { 02984 int bitwidth = getBitvectorTypeParam(e); 02985 Rational max_val = pow( bitwidth, (Rational) 2); 02986 02987 if (enumerate) { 02988 if (n < max_val.getUnsigned()) { 02989 e = newBVConstExpr(n, bitwidth); 02990 } 02991 else e = Expr(); 02992 } 02993 02994 if (computeSize) { 02995 n = max_val.getUnsigned(); 02996 } 02997 } 02998 return CARD_FINITE; 02999 } 03000 03001 03002 void TheoryBitvector::computeType(const Expr& e) 03003 { 03004 if (e.isApply()) { 03005 switch(e.getOpKind()) { 03006 case BOOLEXTRACT: { 03007 if(!(1 == e.arity() && 03008 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03009 throw TypecheckException("Type Checking error:"\ 03010 "attempted extraction from non-bitvector \n"+ 03011 e.toString()); 03012 int extractLength = getBoolExtractIndex(e); 03013 if(!(0 <= extractLength)) 03014 throw TypecheckException("Type Checking error: \n" 03015 "attempted out of range extraction \n"+ 03016 e.toString()); 03017 e.setType(boolType()); 03018 break; 03019 } 03020 case BVMULT:{ 03021 if(!(2 == e.arity() && 03022 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() && 03023 BITVECTOR == getBaseType(e[1]).getExpr().getOpKind())) 03024 throw TypecheckException 03025 ("Not a bit-vector expression in BVMULT:\n\n " 03026 +e.toString()); 03027 int bvLen = getBVMultParam(e); 03028 Type bvType = newBitvectorType(bvLen); 03029 e.setType(bvType); 03030 break; 03031 } 03032 case EXTRACT:{ 03033 if(!(1 == e.arity() && 03034 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03035 throw TypecheckException 03036 ("Not a bit-vector expression in bit-vector extraction:\n\n " 03037 + e.toString()); 03038 int bvLength = BVSize(e[0]); 03039 int leftExtract = getExtractHi(e); 03040 int rightExtract = getExtractLow(e); 03041 if(!(0 <= rightExtract && 03042 rightExtract <= leftExtract && leftExtract < bvLength)) 03043 throw TypecheckException 03044 ("Wrong bounds in bit-vector extract:\n\n "+e.toString()); 03045 int extractLength = leftExtract - rightExtract + 1; 03046 Type bvType = newBitvectorType(extractLength); 03047 e.setType(bvType); 03048 break; 03049 } 03050 case BVPLUS: { 03051 int bvPlusLength = getBVPlusParam(e); 03052 if(!(0 <= bvPlusLength)) 03053 throw TypecheckException 03054 ("Bad bit-vector length specified in BVPLUS expression:\n\n " 03055 + e.toString()); 03056 for(Expr::iterator i=e.begin(), iend=e.end(); i != iend; ++i) { 03057 if(BITVECTOR != getBaseType(*i).getExpr().getOpKind()) 03058 throw TypecheckException 03059 ("Not a bit-vector expression in BVPLUS:\n\n "+e.toString()); 03060 } 03061 Type bvType = newBitvectorType(bvPlusLength); 03062 e.setType(bvType); 03063 break; 03064 } 03065 case LEFTSHIFT: { 03066 if(!(1 == e.arity() && 03067 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03068 throw TypecheckException 03069 ("Not a bit-vector expression in bit-vector shift:\n\n " 03070 +e.toString()); 03071 int bvLength = BVSize(e[0]); 03072 int shiftLength = getFixedLeftShiftParam(e); 03073 if(!(shiftLength >= 0)) 03074 throw TypecheckException("Bad shift value in bit-vector shift:\n\n " 03075 +e.toString()); 03076 int newLength = bvLength + shiftLength; 03077 Type bvType = newBitvectorType(newLength); 03078 e.setType(bvType); 03079 break; 03080 } 03081 case CONST_WIDTH_LEFTSHIFT: { 03082 if(!(1 == e.arity() && 03083 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03084 throw TypecheckException 03085 ("Not a bit-vector expression in bit-vector shift:\n\n " 03086 +e.toString()); 03087 int bvLength = BVSize(e[0]); 03088 int shiftLength = getFixedLeftShiftParam(e); 03089 if(!(shiftLength >= 0)) 03090 throw TypecheckException("Bad shift value in bit-vector shift:\n\n " 03091 +e.toString()); 03092 Type bvType = newBitvectorType(bvLength); 03093 e.setType(bvType); 03094 break; 03095 } 03096 case RIGHTSHIFT: { 03097 if(!(1 == e.arity() && 03098 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03099 throw TypecheckException 03100 ("Not a bit-vector expression in bit-vector shift:\n\n " 03101 +e.toString()); 03102 int bvLength = BVSize(e[0]); 03103 int shiftLength = getFixedRightShiftParam(e); 03104 if(!(shiftLength >= 0)) 03105 throw TypecheckException("Bad shift value in bit-vector shift:\n\n " 03106 +e.toString()); 03107 //int newLength = bvLength + shiftLength; 03108 Type bvType = newBitvectorType(bvLength); 03109 e.setType(bvType); 03110 break; 03111 } 03112 case BVTYPEPRED: 03113 e.setType(boolType()); 03114 break; 03115 case SX: { 03116 if(!(1 == e.arity() && 03117 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03118 throw TypecheckException("Type Checking error:"\ 03119 "non-bitvector \n"+ e.toString()); 03120 int bvLength = getSXIndex(e); 03121 if(!(1 <= bvLength)) 03122 throw TypecheckException("Type Checking error: \n" 03123 "out of range\n"+ e.toString()); 03124 Type bvType = newBitvectorType(bvLength); 03125 e.setType(bvType); 03126 break; 03127 } 03128 case BVREPEAT: { 03129 if(!(1 == e.arity() && 03130 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03131 throw TypecheckException("Type Checking error:"\ 03132 "non-bitvector \n"+ e.toString()); 03133 int bvLength = getBVIndex(e) * BVSize(e[0]); 03134 if(!(1 <= bvLength)) 03135 throw TypecheckException("Type Checking error: \n" 03136 "out of range\n"+ e.toString()); 03137 Type bvType = newBitvectorType(bvLength); 03138 e.setType(bvType); 03139 break; 03140 } 03141 case BVZEROEXTEND: { 03142 if(!(1 == e.arity() && 03143 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03144 throw TypecheckException("Type Checking error:"\ 03145 "non-bitvector \n"+ e.toString()); 03146 int bvLength = getBVIndex(e) + BVSize(e[0]); 03147 if(!(1 <= bvLength)) 03148 throw TypecheckException("Type Checking error: \n" 03149 "out of range\n"+ e.toString()); 03150 Type bvType = newBitvectorType(bvLength); 03151 e.setType(bvType); 03152 break; 03153 } 03154 case BVROTL: 03155 case BVROTR: { 03156 if(!(1 == e.arity() && 03157 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03158 throw TypecheckException("Type Checking error:"\ 03159 "non-bitvector \n"+ e.toString()); 03160 e.setType(getBaseType(e[0])); 03161 break; 03162 } 03163 default: 03164 FatalAssert(false, 03165 "TheoryBitvector::computeType: unexpected kind in application" + 03166 int2string(e.getOpKind())); 03167 break; 03168 } 03169 } 03170 else { 03171 switch(e.getKind()) { 03172 case BOOLEXTRACT: 03173 case BVMULT: 03174 case EXTRACT: 03175 case BVPLUS: 03176 case LEFTSHIFT: 03177 case CONST_WIDTH_LEFTSHIFT: 03178 case RIGHTSHIFT: 03179 case BVTYPEPRED: 03180 case SX: 03181 case BVREPEAT: 03182 case BVZEROEXTEND: 03183 case BVROTL: 03184 case BVROTR: 03185 // These operators are handled above when applied to arguments, here we 03186 // are dealing with the operators themselves which are polymorphic, so 03187 // don't assign them a specific type. 03188 e.setType(Type::anyType(getEM())); 03189 break; 03190 case BVCONST: { 03191 Type bvType = newBitvectorType(getBVConstSize(e)); 03192 e.setType(bvType); 03193 break; 03194 } 03195 case CONCAT: { 03196 if(e.arity() < 2) 03197 throw TypecheckException 03198 ("Concatenation must have at least 2 bit-vectors:\n\n "+e.toString()); 03199 03200 // Compute the total length of concatenation 03201 int bvLength(0); 03202 for(int i=0, iend=e.arity(); i<iend; ++i) { 03203 if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind()) 03204 throw TypecheckException 03205 ("Not a bit-vector expression (child #"+int2string(i+1) 03206 +") in concatenation:\n\n "+e[i].toString() 03207 +"\n\nIn the expression:\n\n "+e.toString()); 03208 bvLength += BVSize(e[i]); 03209 } 03210 Type bvType = newBitvectorType(bvLength); 03211 e.setType(bvType); 03212 break; 03213 } 03214 case BVAND: 03215 case BVOR: 03216 case BVXOR: 03217 case BVXNOR: 03218 { 03219 string kindStr((e.getOpKind()==BVAND)? "AND" : 03220 ((e.getOpKind()==BVOR)? "OR" : 03221 ((e.getOpKind()==BVXOR)? "BVXOR" : "BVXNOR"))); 03222 03223 if(e.arity() < 2) 03224 throw TypecheckException 03225 ("Bit-wise "+kindStr+" must have at least 2 bit-vectors:\n\n " 03226 +e.toString()); 03227 03228 int bvLength(0); 03229 bool first(true); 03230 for(int i=0, iend=e.arity(); i<iend; ++i) { 03231 if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind()) 03232 throw TypecheckException 03233 ("Not a bit-vector expression (child #"+int2string(i+1) 03234 +") in bit-wise "+kindStr+":\n\n "+e[i].toString() 03235 +"\n\nIn the expression:\n\n "+e.toString()); 03236 if(first) { 03237 bvLength = BVSize(e[i]); 03238 first=false; 03239 } else { // Check that the size is the same for all subsequent BVs 03240 if(BVSize(e[i]) != bvLength) 03241 throw TypecheckException 03242 ("Mismatched bit-vector size in bit-wise "+kindStr+" (child #" 03243 +int2string(i)+").\nExpected type: " 03244 +newBitvectorType(bvLength).toString() 03245 +"\nFound: "+e[i].getType().toString() 03246 +"\nIn the following expression:\n\n "+e.toString()); 03247 } 03248 } 03249 e.setType(newBitvectorType(bvLength)); 03250 break; 03251 } 03252 case BVNEG:{ 03253 if(!(1 == e.arity() && 03254 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind())) 03255 throw TypecheckException 03256 ("Not a bit-vector expression in bit-wise negation:\n\n " 03257 + e.toString()); 03258 e.setType(e[0].getType()); 03259 break; 03260 } 03261 case BVNAND: 03262 case BVNOR: 03263 case BVCOMP: 03264 case BVSUB: 03265 case BVUDIV: 03266 case BVSDIV: 03267 case BVUREM: 03268 case BVSREM: 03269 case BVSMOD: 03270 case BVSHL: 03271 case BVASHR: 03272 case BVLSHR: 03273 if(!(2 == e.arity() && 03274 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() && 03275 BITVECTOR == getBaseType(e[1]).getExpr().getOpKind())) 03276 throw TypecheckException 03277 ("Expressions must have arity=2, and" 03278 "each subterm must be a bitvector term:\n" 03279 "e = " +e.toString()); 03280 if (BVSize(e[0]) != BVSize(e[1])) 03281 throw TypecheckException 03282 ("Expected args of same size:\n" 03283 "e = " +e.toString()); 03284 if (e.getKind() == BVCOMP) { 03285 e.setType(newBitvectorTypeExpr(1)); 03286 } 03287 else { 03288 e.setType(getBaseType(e[0])); 03289 } 03290 break; 03291 case BVUMINUS:{ 03292 Type bvType(getBaseType(e[0])); 03293 if(!(1 == e.arity() && 03294 BITVECTOR == bvType.getExpr().getOpKind())) 03295 throw TypecheckException 03296 ("Not a bit-vector expression in BVUMINUS:\n\n " 03297 +e.toString()); 03298 e.setType(bvType); 03299 break; 03300 } 03301 case BVLT: 03302 case BVLE: 03303 case BVGT: 03304 case BVGE: 03305 case BVSLT: 03306 case BVSLE: 03307 case BVSGT: 03308 case BVSGE: 03309 if(!(2 == e.arity() && 03310 BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() && 03311 BITVECTOR == getBaseType(e[1]).getExpr().getOpKind())) 03312 throw TypecheckException 03313 ("BVLT/BVLE expressions must have arity=2, and" 03314 "each subterm must be a bitvector term:\n" 03315 "e = " +e.toString()); 03316 e.setType(boolType()); 03317 break; 03318 default: 03319 FatalAssert(false, 03320 "TheoryBitvector::computeType: wrong input" + 03321 int2string(e.getOpKind())); 03322 break; 03323 } 03324 } 03325 TRACE("bitvector", "TheoryBitvector::computeType => ", e.getType(), " }"); 03326 } 03327 03328 03329 void TheoryBitvector::computeModelTerm(const Expr& e, std::vector<Expr>& v) { 03330 switch(e.getOpKind()) { 03331 case BVPLUS: 03332 case BVSUB: 03333 case BVUMINUS: 03334 case BVMULT: 03335 case LEFTSHIFT: 03336 case CONST_WIDTH_LEFTSHIFT: 03337 case RIGHTSHIFT: 03338 case BVOR: 03339 case BVAND: 03340 case BVXOR: 03341 case BVXNOR: 03342 case BVNAND: 03343 case BVNOR: 03344 case BVNEG: 03345 case CONCAT: 03346 case EXTRACT: 03347 case BVSLT: 03348 case BVSLE: 03349 case BVSGT: 03350 case BVSGE: 03351 case BVLT: 03352 case BVLE: 03353 case BVGT: 03354 case BVGE: 03355 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) 03356 // getModelTerm(*i, v); 03357 v.push_back(*i); 03358 return; 03359 case BVCONST: // No model variables here 03360 return; 03361 default: break; // It's a variable; continue processing 03362 } 03363 03364 Type tp(e.getType()); 03365 switch(tp.getExpr().getOpKind()) { 03366 case BITVECTOR: { 03367 int n = getBitvectorTypeParam(tp); 03368 for(int i=0; i<n; i = i+1) 03369 v.push_back(newBoolExtractExpr(e, i)); 03370 break; 03371 } 03372 default: 03373 v.push_back(e); 03374 } 03375 } 03376 03377 03378 void TheoryBitvector::computeModel(const Expr& e, std::vector<Expr>& v) { 03379 switch(e.getOpKind()) { 03380 case BVPLUS: 03381 case BVSUB: 03382 case BVUMINUS: 03383 case BVMULT: 03384 case LEFTSHIFT: 03385 case CONST_WIDTH_LEFTSHIFT: 03386 case RIGHTSHIFT: 03387 case BVOR: 03388 case BVAND: 03389 case BVXOR: 03390 case BVXNOR: 03391 case BVNAND: 03392 case BVNOR: 03393 case BVNEG: 03394 case CONCAT: 03395 case EXTRACT: 03396 case SX: 03397 case BVSLT: 03398 case BVSLE: 03399 case BVSGT: 03400 case BVSGE: 03401 case BVLT: 03402 case BVLE: 03403 case BVGT: 03404 case BVGE: { 03405 // More primitive vars are kids, and they should have been 03406 // assigned concrete values 03407 assignValue(simplify(e)); 03408 v.push_back(e); 03409 return; 03410 } 03411 case BVCONST: // No model variables here 03412 return; 03413 default: break; // It's a variable; continue processing 03414 } 03415 03416 Type tp(e.getType()); 03417 switch(tp.getExpr().getOpKind()) { 03418 case BITVECTOR: { 03419 const Rational& n = getBitvectorTypeParam(tp); 03420 vector<bool> bits; 03421 // FIXME: generate concrete assignment from bits using proof 03422 // rules. For now, just create a new assignment. 03423 for(int i=0; i<n; i++) { 03424 Theorem val(getModelValue(newBoolExtractExpr(e, i))); 03425 DebugAssert(val.getRHS().isBoolConst(), 03426 "TheoryBitvector::computeModel: unassigned bit: " 03427 +val.getExpr().toString()); 03428 bits.push_back(val.getRHS().isTrue()); 03429 } 03430 Expr c(newBVConstExpr(bits)); 03431 assignValue(e, c); 03432 v.push_back(e); 03433 break; 03434 } 03435 default: 03436 FatalAssert(false, "TheoryBitvector::computeModel[not BITVECTOR type](" 03437 +e.toString()+")"); 03438 } 03439 } 03440 03441 03442 // TODO: get rid of this - don't need type predicates for bv's, just need to share the right terms 03443 Expr 03444 TheoryBitvector::computeTypePred(const Type& t, const Expr& e) { 03445 DebugAssert(t.getExpr().getOpKind() == BITVECTOR, 03446 "TheoryBitvector::computeTypePred: t = "+t.toString()); 03447 // switch(e.getKind()) { 03448 // case BVCONST: 03449 // return getEM()->trueExpr(); 03450 // default: 03451 return e.getEM()->trueExpr(); 03452 03453 // return newBitvectorTypePred(t, e); 03454 // } 03455 } 03456 03457 /////////////////////////////////////////////////////////////////////////////// 03458 // Pretty-printing // 03459 /////////////////////////////////////////////////////////////////////////////// 03460 03461 ExprStream& 03462 TheoryBitvector::print(ExprStream& os, const Expr& e) { 03463 switch(os.lang()) { 03464 case PRESENTATION_LANG: 03465 switch(e.getOpKind()) { 03466 03467 case BITVECTOR: //printing type expression 03468 os << "BITVECTOR(" << push 03469 << getBitvectorTypeParam(e) << push << ")"; 03470 break; 03471 03472 case BVCONST: { 03473 std::ostringstream ss; 03474 ss << "0bin"; 03475 for(int i=(int)getBVConstSize(e)-1; i>=0; --i) 03476 ss << (getBVConstValue(e, i) ? "1" : "0"); 03477 os << ss.str(); 03478 break; 03479 } 03480 03481 case CONCAT: 03482 if(e.arity() <= 1) e.printAST(os); 03483 else { 03484 os << "(" << push; 03485 bool first(true); 03486 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 03487 if(first) first=false; 03488 else os << space << "@" << space; 03489 os << (*i); 03490 } 03491 os << push << ")"; 03492 } 03493 break; 03494 case EXTRACT: 03495 os << "(" << push << e[0] << push << ")" << pop << pop 03496 << "[" << push << getExtractHi(e) << ":"; 03497 os << getExtractLow(e) << push << "]"; 03498 break; 03499 case BOOLEXTRACT: 03500 os << "BOOLEXTRACT(" << push << e[0] << "," 03501 << getBoolExtractIndex(e) << push << ")"; 03502 break; 03503 03504 case LEFTSHIFT: 03505 os << "(" << push << e[0] << space << "<<" << space 03506 << getFixedLeftShiftParam(e) << push << ")"; 03507 break; 03508 case CONST_WIDTH_LEFTSHIFT: 03509 os << "(" << push << e[0] << space << "<<" << space 03510 << getFixedLeftShiftParam(e) << push << ")"; 03511 os << "[" << push << BVSize(e)-1 << ":0]"; 03512 break; 03513 case RIGHTSHIFT: 03514 os << "(" << push << e[0] << space << ">>" << space 03515 << getFixedRightShiftParam(e) << push << ")"; 03516 break; 03517 case BVSHL: 03518 os << "BVSHL(" << push << e[0] << "," << e[1] << push << ")"; 03519 break; 03520 case BVLSHR: 03521 os << "BVLSHR(" << push << e[0] << "," << e[1] << push << ")"; 03522 break; 03523 case BVASHR: 03524 os << "BVASHR(" << push << e[0] << "," << e[1] << push << ")"; 03525 break; 03526 case BVZEROEXTEND: 03527 os << "BVZEROEXTEND(" << push << e[0] << "," << getBVIndex(e) << push << ")"; 03528 break; 03529 case BVREPEAT: 03530 os << "BVREPEAT(" << push << e[0] << "," << getBVIndex(e) << push << ")"; 03531 break; 03532 case BVROTL: 03533 os << "BVROTL(" << push << e[0] << "," << getBVIndex(e) << push << ")"; 03534 break; 03535 case BVROTR: 03536 os << "BVROTR(" << push << e[0] << "," << getBVIndex(e) << push << ")"; 03537 break; 03538 case SX: 03539 os << "SX(" << push << e[0] << "," 03540 << push << getSXIndex(e) << ")"; 03541 break; 03542 03543 case BVAND: 03544 if(e.arity() <= 1) e.printAST(os); 03545 else { 03546 os << "(" << push; 03547 bool first(true); 03548 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 03549 if(first) first=false; 03550 else os << space << "&" << space; 03551 os << (*i); 03552 } 03553 os << push << ")"; 03554 } 03555 break; 03556 case BVOR: 03557 if(e.arity() <= 1) e.printAST(os); 03558 else { 03559 os << "(" << push; 03560 bool first(true); 03561 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 03562 if(first) first=false; 03563 else os << space << "|" << space; 03564 os << (*i); 03565 } 03566 os << push << ")"; 03567 } 03568 break; 03569 case BVXOR: 03570 DebugAssert(e.arity() > 0, "TheoryBitvector::print: BVXOR arity <= 0"); 03571 if (e.arity() == 1) os << e[0]; 03572 else { 03573 int i; 03574 for(i = 0; i < e.arity(); ++i) { 03575 if ((i+1) == e.arity()) { 03576 os << e[i]; 03577 } 03578 else { 03579 os << "BVXOR(" << push << e[i] << "," << push; 03580 } 03581 } 03582 for (--i; i != 0; --i) os << push << ")"; 03583 } 03584 break; 03585 case BVXNOR: 03586 DebugAssert(e.arity() > 0, "TheoryBitvector::print: BVXNOR arity <= 0"); 03587 if (e.arity() == 1) os << e[0]; 03588 else { 03589 int i; 03590 for(i = 0; i < e.arity(); ++i) { 03591 if ((i+1) == e.arity()) { 03592 os << e[i]; 03593 } 03594 else { 03595 os << "BVXNOR(" << push << e[i] << "," << push; 03596 } 03597 } 03598 for (--i; i != 0; --i) os << push << ")"; 03599 } 03600 break; 03601 case BVNEG: 03602 os << "(~(" << push << e[0] << push << "))"; 03603 break; 03604 case BVNAND: 03605 os << "BVNAND(" << push << e[0] << "," << e[1] << push << ")"; 03606 break; 03607 case BVNOR: 03608 os << "BVNAND(" << push << e[0] << "," << e[1] << push << ")"; 03609 break; 03610 case BVCOMP: 03611 os << "BVCOMP(" << push << e[0] << "," << e[1] << push << ")"; 03612 break; 03613 03614 case BVUMINUS: 03615 os << "BVUMINUS(" << push << e[0] << push << ")"; 03616 break; 03617 case BVPLUS: 03618 os << "BVPLUS(" << push << getBVPlusParam(e); 03619 for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) { 03620 os << push << "," << pop << space << (*i); 03621 } 03622 os << push << ")"; 03623 break; 03624 case BVSUB: 03625 os << "BVSUB(" << push << BVSize(e) << "," << e[0] << "," << e[1] << push << ")"; 03626 break; 03627 case BVMULT: 03628 os << "BVMULT(" << push << getBVMultParam(e) << "," << e[0] << "," << e[1]<<push<<")"; 03629 break; 03630 case BVUDIV: 03631 os << "BVUDIV(" << push << e[0] << "," << e[1]<<push<<")"; 03632 break; 03633 case BVSDIV: 03634 os << "BVSDIV(" << push << e[0] << "," << e[1]<<push<<")"; 03635 break; 03636 case BVUREM: 03637 os << "BVUREM(" << push << e[0] << "," << e[1]<<push<<")"; 03638 break; 03639 case BVSREM: 03640 os << "BVSREM(" << push << e[0] << "," << e[1]<<push<<")"; 03641 break; 03642 case BVSMOD: 03643 os << "BVSMOD(" << push << e[0] << "," << e[1]<<push<<")"; 03644 break; 03645 case BVLT: 03646 os << "BVLT(" << push << e[0] << "," << e[1] << push << ")"; 03647 break; 03648 case BVLE: 03649 os << "BVLE(" << push << e[0] << "," << e[1] << push << ")"; 03650 break; 03651 case BVGT: 03652 os << "BVGT(" << push << e[0] << "," << e[1] << push << ")"; 03653 break; 03654 case BVGE: 03655 os << "BVGE(" << push << e[0] << "," << e[1] << push << ")"; 03656 break; 03657 case BVSLT: 03658 os << "BVSLT(" << push << e[0] << "," << e[1] << push << ")"; 03659 break; 03660 case BVSLE: 03661 os << "BVSLE(" << push << e[0] << "," << e[1] << push << ")"; 03662 break; 03663 case BVSGT: 03664 os << "BVSGT(" << push << e[0] << "," << e[1] << push << ")"; 03665 break; 03666 case BVSGE: 03667 os << "BVSGE(" << push << e[0] << "," << e[1] << push << ")"; 03668 break; 03669 03670 case INTTOBV: 03671 FatalAssert(false, "INTTOBV not implemented yet"); 03672 break; 03673 case BVTOINT: 03674 FatalAssert(false, "BVTOINT not implemented yet"); 03675 break; 03676 03677 case BVTYPEPRED: 03678 if(e.isApply()) { 03679 os << "BVTYPEPRED[" << push << e.getOp().getExpr() 03680 << push << "," << pop << space << e[0] 03681 << push << "]"; 03682 } else 03683 e.printAST(os); 03684 break; 03685 03686 default: 03687 FatalAssert(false, "Unknown BV kind"); 03688 e.printAST(os); 03689 break; 03690 } 03691 break; 03692 03693 case SMTLIB_LANG: 03694 d_theoryUsed = true; 03695 switch(e.getOpKind()) { 03696 03697 case BITVECTOR: //printing type expression 03698 os << push << "BitVec[" << getBitvectorTypeParam(e) << "]"; 03699 break; 03700 03701 case BVCONST: { 03702 Rational r = computeBVConst(e); 03703 DebugAssert(r.isInteger() && r >= 0, "Expected non-negative integer"); 03704 os << push << "bv" << r << "[" << BVSize(e) << "]"; 03705 break; 03706 } 03707 03708 case CONCAT: 03709 if (e.arity() == 0) throw SmtlibException("TheoryBitvector::print: CONCAT arity = 0"); 03710 else if (e.arity() == 1) os << e[0]; 03711 else { 03712 int i; 03713 for(i = 0; i < e.arity(); ++i) { 03714 if ((i+1) == e.arity()) { 03715 os << e[i]; 03716 } 03717 else { 03718 os << "(concat" << space << push << e[i] << space << push; 03719 } 03720 } 03721 for (--i; i != 0; --i) os << push << ")"; 03722 } 03723 break; 03724 case EXTRACT: 03725 os << push << "(extract[" << getExtractHi(e) << ":" << getExtractLow(e) << "]"; 03726 os << space << push << e[0] << push << ")"; 03727 break; 03728 case BOOLEXTRACT: 03729 os << "(=" << space << push 03730 << "(extract[" << getBoolExtractIndex(e) << ":" << getBoolExtractIndex(e) << "]"; 03731 os << space << push << e[0] << push << ")" << space << "bit1" << push << ")"; 03732 break; 03733 03734 case LEFTSHIFT: { 03735 int bvLength = getFixedLeftShiftParam(e); 03736 if (bvLength != 0) { 03737 os << "(concat" << space << push << e[0] << space; 03738 os << push << "bv0[" << bvLength << "]" << push << ")"; 03739 break; 03740 } 03741 // else fall-through 03742 } 03743 case CONST_WIDTH_LEFTSHIFT: 03744 os << "(bvshl" << space << push << e[0] << space << push 03745 << "bv" << getFixedLeftShiftParam(e) << "[" << BVSize(e[0]) << "]" << push << ")"; 03746 break; 03747 case RIGHTSHIFT: 03748 os << "(bvlshr" << space << push << e[0] << space << push 03749 << "bv" << getFixedRightShiftParam(e) << "[" << BVSize(e[0]) << "]" << push << ")"; 03750 break; 03751 case BVSHL: 03752 os << "(bvshl" << space << push << e[0] << space << push << e[1] << push << ")"; 03753 break; 03754 case BVLSHR: 03755 os << "(bvlshr" << space << push << e[0] << space << push << e[1] << push << ")"; 03756 break; 03757 case BVASHR: 03758 os << "(bvashr" << space << push << e[0] << space << push << e[1] << push << ")"; 03759 break; 03760 case SX: { 03761 int extend = getSXIndex(e) - BVSize(e[0]); 03762 if (extend == 0) os << e[0]; 03763 else if (extend < 0) 03764 throw SmtlibException("TheoryBitvector::print: SX: extension is shorter than argument"); 03765 else os << "(sign_extend[" << extend << "]" << space << push << e[0] << push << ")"; 03766 break; 03767 } 03768 case BVREPEAT: 03769 os << "(repeat[" << getBVIndex(e) << "]" << space << push << e[0] << push << ")"; 03770 break; 03771 case BVZEROEXTEND: { 03772 int extend = getBVIndex(e); 03773 if (extend == 0) os << e[0]; 03774 else if (extend < 0) 03775 throw SmtlibException("TheoryBitvector::print: ZEROEXTEND: extension is less than zero"); 03776 else os << "(zero_extend[" << extend << "]" << space << push << e[0] << push << ")"; 03777 break; 03778 } 03779 case BVROTL: 03780 os << "(rotate_left[" << getBVIndex(e) << "]" << space << push << e[0] << push << ")"; 03781 break; 03782 case BVROTR: 03783 os << "(rotate_right[" << getBVIndex(e) << "]" << space << push << e[0] << push << ")"; 03784 break; 03785 03786 case BVAND: 03787 if (e.arity() == 0) throw SmtlibException("TheoryBitvector::print: BVAND arity = 0"); 03788 else if (e.arity() == 1) os << e[0]; 03789 else { 03790 int i; 03791 for(i = 0; i < e.arity(); ++i) { 03792 if ((i+1) == e.arity()) { 03793 os << e[i]; 03794 } 03795 else { 03796 os << "(bvand" << space << push << e[i] << space << push; 03797 } 03798 } 03799 for (--i; i != 0; --i) os << push << ")"; 03800 } 03801 break; 03802 case BVOR: 03803 if (e.arity() == 0) throw SmtlibException("TheoryBitvector::print: BVAND arity = 0"); 03804 else if (e.arity() == 1) os << e[0]; 03805 else { 03806 int i; 03807 for(i = 0; i < e.arity(); ++i) { 03808 if ((i+1) == e.arity()) { 03809 os << e[i]; 03810 } 03811 else { 03812 os << "(bvor" << space << push << e[i] << space << push; 03813 } 03814 } 03815 for (--i; i != 0; --i) os << push << ")"; 03816 } 03817 break; 03818 case BVXOR: 03819 if (e.arity() == 0) throw SmtlibException("TheoryBitvector::print: BVXOR arity = 0"); 03820 else if (e.arity() == 1) os << e[0]; 03821 else { 03822 int i; 03823 for(i = 0; i < e.arity(); ++i) { 03824 if ((i+1) == e.arity()) { 03825 os << e[i]; 03826 } 03827 else { 03828 os << "(bvxor" << space << push << e[i] << space << push; 03829 } 03830 } 03831 for (--i; i != 0; --i) os << push << ")"; 03832 } 03833 break; 03834 case BVXNOR: 03835 if (e.arity() == 0) throw SmtlibException("TheoryBitvector::print: BVXNOR arity = 0"); 03836 else if (e.arity() == 1) os << e[0]; 03837 else { 03838 int i; 03839 for(i = 0; i < e.arity(); ++i) { 03840 if ((i+1) == e.arity()) { 03841 os << e[i]; 03842 } 03843 else { 03844 os << "(bvxnor" << space << push << e[i] << space << push; 03845 } 03846 } 03847 for (--i; i != 0; --i) os << push << ")"; 03848 } 03849 break; 03850 case BVNEG: 03851 os << "(bvnot" << space << push << e[0] << push << ")"; 03852 break; 03853 case BVNAND: 03854 os << "(bvnand" << space << push << e[0] << space << push << e[1] << push << ")"; 03855 break; 03856 case BVNOR: 03857 os << "(bvnor" << space << push << e[0] << space << push << e[1] << push << ")"; 03858 break; 03859 case BVCOMP: 03860 os << "(bvcomp" << space << push << e[0] << space << push << e[1] << push << ")"; 03861 break; 03862 03863 case BVUMINUS: 03864 os << "(bvneg" << space << push << e[0] << push << ")"; 03865 break; 03866 case BVPLUS: 03867 { 03868 DebugAssert(e.arity() > 0, "expected arity > 0 in BVPLUS"); 03869 int length = getBVPlusParam(e); 03870 int i; 03871 for(i = 0; i < e.arity(); ++i) { 03872 if ((i+1) == e.arity()) { 03873 os << pad(length, e[i]); 03874 } 03875 else { 03876 os << "(bvadd" << space << push << pad(length, e[i]) << space << push; 03877 } 03878 } 03879 for (--i; i != 0; --i) os << push << ")"; 03880 } 03881 break; 03882 case BVSUB: 03883 os << "(bvsub" << space << push << e[0] << space << push << e[1] << push << ")"; 03884 break; 03885 case BVMULT: { 03886 int length = getBVMultParam(e); 03887 os << "(bvmul" 03888 << space << push << pad(length, e[0]) 03889 << space << push << pad(length, e[1]) 03890 << push << ")"; 03891 break; 03892 } 03893 case BVUDIV: 03894 os << "(bvudiv" << space << push << e[0] << space << push << e[1] << push << ")"; 03895 break; 03896 case BVSDIV: 03897 os << "(bvsdiv" << space << push << e[0] << space << push << e[1] << push << ")"; 03898 break; 03899 case BVUREM: 03900 os << "(bvurem" << space << push << e[0] << space << push << e[1] << push << ")"; 03901 break; 03902 case BVSREM: 03903 os << "(bvsrem" << space << push << e[0] << space << push << e[1] << push << ")"; 03904 break; 03905 case BVSMOD: 03906 os << "(bvsmod" << space << push << e[0] << space << push << e[1] << push << ")"; 03907 break; 03908 03909 case BVLT: 03910 os << "(bvult" << space << push << e[0] << space << push << e[1] << push << ")"; 03911 break; 03912 case BVLE: 03913 os << "(bvule" << space << push << e[0] << space << push << e[1] << push << ")"; 03914 break; 03915 case BVGT: 03916 os << "(bvugt" << space << push << e[0] << space << push << e[1] << push << ")"; 03917 break; 03918 case BVGE: 03919 os << "(bvuge" << space << push << e[0] << space << push << e[1] << push << ")"; 03920 break; 03921 case BVSLT: 03922 os << "(bvslt" << space << push << e[0] << space << push << e[1] << push << ")"; 03923 break; 03924 case BVSLE: 03925 os << "(bvsle" << space << push << e[0] << space << push << e[1] << push << ")"; 03926 break; 03927 case BVSGT: 03928 os << "(bvsgt" << space << push << e[0] << space << push << e[1] << push << ")"; 03929 break; 03930 case BVSGE: 03931 os << "(bvsge" << space << push << e[0] << space << push << e[1] << push << ")"; 03932 break; 03933 03934 case INTTOBV: 03935 throw SmtlibException("TheoryBitvector::print: INTTOBV, SMTLIB not supported"); 03936 break; 03937 case BVTOINT: 03938 throw SmtlibException("TheoryBitvector::print: BVTOINT, SMTLIB not supported"); 03939 break; 03940 03941 case BVTYPEPRED: 03942 throw SmtlibException("TheoryBitvector::print: BVTYPEPRED, SMTLIB not supported"); 03943 if(e.isApply()) { 03944 os << "BVTYPEPRED[" << push << e.getOp().getExpr() 03945 << push << "," << pop << space << e[0] 03946 << push << "]"; 03947 } else 03948 e.printAST(os); 03949 break; 03950 03951 default: 03952 FatalAssert(false, "Unknown BV kind"); 03953 e.printAST(os); 03954 break; 03955 } 03956 break; 03957 03958 default: 03959 switch(e.getOpKind()) { 03960 case BVCONST: { 03961 os << "0bin"; 03962 for(int i=(int)getBVConstSize(e)-1; i>=0; --i) 03963 os << (getBVConstValue(e, i) ? "1" : "0"); 03964 break; 03965 } 03966 default: 03967 e.printAST(os); 03968 break; 03969 } 03970 } 03971 return os; 03972 } 03973 03974 03975 /////////////////////////////////////////////////////////////////////////////// 03976 //parseExprOp: 03977 //translating special Exprs to regular EXPR?? 03978 /////////////////////////////////////////////////////////////////////////////// 03979 Expr TheoryBitvector::parseExprOp(const Expr& e) 03980 { 03981 d_theoryUsed = true; 03982 TRACE("parser", "TheoryBitvector::parseExprOp(", e, ")"); 03983 03984 // If the expression is not a list, it must have been already 03985 // parsed, so just return it as is. 03986 if(RAW_LIST != e.getKind()) return e; 03987 03988 if(!(e.arity() > 0)) 03989 throw ParserException("TheoryBitvector::parseExprOp: wrong input:\n\n" 03990 +e.toString()); 03991 03992 const Expr& c1 = e[0][0]; 03993 int kind = getEM()->getKind(c1.getString()); 03994 switch(kind) { 03995 03996 case BITVECTOR: 03997 if(!(e.arity() == 2)) 03998 throw ParserException("TheoryBitvector::parseExprOp: BITVECTOR" 03999 "kind should have exactly 1 arg:\n\n" 04000 + e.toString()); 04001 if(!(e[1].isRational() && e[1].getRational().isInteger())) 04002 throw ParserException("BITVECTOR TYPE must have an integer constant" 04003 "as its first argument:\n\n" 04004 +e.toString()); 04005 if(!(e[1].getRational().getInt() >=0 )) 04006 throw ParserException("parameter must be an integer constant >= 0.\n" 04007 +e.toString()); 04008 return newBitvectorTypeExpr(e[1].getRational().getInt()); 04009 break; 04010 04011 case BVCONST: 04012 if(!(e.arity() == 2 || e.arity() == 3)) 04013 throw ParserException("TheoryBitvector::parseExprOp: BVCONST " 04014 "kind should have 1 or 2 args:\n\n" 04015 + e.toString()); 04016 if(!(e[1].isRational() || e[1].isString())) 04017 throw ParserException("TheoryBitvector::parseExprOp: BVCONST " 04018 "kind should have arg of type Rational " 04019 "or String:\n\n" + e.toString()); 04020 if(e[1].isRational()) { // ("BVCONST" value [bitwidth]) 04021 if(e.arity()==3) { 04022 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04023 throw ParserException("TheoryBitvector::parseExprOp: BVCONST " 04024 "2nd argument must be an integer:\n\n" 04025 +e.toString()); 04026 return newBVConstExpr(e[1].getRational(), e[2].getRational().getInt()); 04027 } else 04028 return newBVConstExpr(e[1].getRational()); 04029 } else if(e[1].isString()) { // ("BVCONST" string [base]) 04030 if(e.arity() == 3) { 04031 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04032 throw ParserException("TheoryBitvector::parseExprOp: BVCONST " 04033 "2nd argument must be an integer:\n\n" 04034 +e.toString()); 04035 return newBVConstExpr(e[1].getString(), e[2].getRational().getInt()); 04036 } else 04037 return newBVConstExpr(e[1].getString()); 04038 } 04039 break; 04040 04041 case CONCAT: { 04042 if(!(e.arity() >= 3)) 04043 throw ParserException("TheoryBitvector::parseExprOp: CONCAT" 04044 "kind should have at least 2 args:\n\n" 04045 + e.toString()); 04046 vector<Expr> kids; 04047 Expr::iterator i=e.begin(), iend=e.end(); 04048 DebugAssert(i!=iend, "TheoryBitvector::parseExprOp("+e.toString()+")"); 04049 ++i; // Skip the first element - the operator name 04050 for(; i!=iend; ++i) 04051 kids.push_back(parseExpr(*i)); 04052 return newConcatExpr(kids); 04053 break; 04054 } 04055 case EXTRACT: { 04056 if(!(e.arity() == 4)) 04057 throw ParserException("TheoryBitvector::parseExprOp: EXTRACT" 04058 "kind should have exactly 3 arg:\n\n" 04059 + e.toString()); 04060 if(!e[1].isRational() || !e[1].getRational().isInteger()) 04061 throw ParserException("EXTRACT must have an integer constant as its " 04062 "1st argument:\n\n" 04063 +e.toString()); 04064 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04065 throw ParserException("EXTRACT must have an integer constant as its " 04066 "2nd argument:\n\n" 04067 +e.toString()); 04068 int hi = e[1].getRational().getInt(); 04069 int lo = e[2].getRational().getInt(); 04070 if(!(hi >= lo && lo >=0)) 04071 throw ParserException("parameter must be an integer constant >= 0.\n" 04072 +e.toString()); 04073 04074 // Check for extract of left shift 04075 Expr arg = e[3]; 04076 if (lo == 0 && arg.getKind() == RAW_LIST && arg[0].getKind() == ID && 04077 getEM()->getKind(arg[0][0].getString()) == LEFTSHIFT) { 04078 if(!(arg.arity() == 3)) 04079 throw ParserException("TheoryBitvector::parseExprOp: LEFTSHIFT" 04080 "kind should have exactly 2 arg:\n\n" 04081 + arg.toString()); 04082 if(!arg[2].isRational() || !arg[2].getRational().isInteger()) 04083 throw ParserException("LEFTSHIFT must have an integer constant as its " 04084 "2nd argument:\n\n" 04085 +arg.toString()); 04086 if(!(arg[2].getRational().getInt() >=0 )) 04087 throw ParserException("parameter must be an integer constant >= 0.\n" 04088 +arg.toString()); 04089 Expr ls_arg = parseExpr(arg[1]); 04090 if (BVSize(ls_arg) == hi + 1) { 04091 return newFixedConstWidthLeftShiftExpr(ls_arg, arg[2].getRational().getInt()); 04092 } 04093 } 04094 return newBVExtractExpr(parseExpr(arg), hi, lo); 04095 break; 04096 } 04097 case BOOLEXTRACT: 04098 if(!(e.arity() == 3)) 04099 throw ParserException("TheoryBitvector::parseExprOp: BOOLEXTRACT" 04100 "kind should have exactly 2 arg:\n\n" 04101 + e.toString()); 04102 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04103 throw ParserException("BOOLEXTRACT must have an integer constant as its" 04104 " 2nd argument:\n\n" 04105 +e.toString()); 04106 if(!(e[2].getRational().getInt() >=0 )) 04107 throw ParserException("parameter must be an integer constant >= 0.\n" 04108 +e.toString()); 04109 return newBoolExtractExpr(parseExpr(e[1]), e[2].getRational().getInt()); 04110 break; 04111 04112 case LEFTSHIFT: 04113 if(!(e.arity() == 3)) 04114 throw ParserException("TheoryBitvector::parseExprOp: LEFTSHIFT" 04115 "kind should have exactly 2 arg:\n\n" 04116 + e.toString()); 04117 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04118 throw ParserException("LEFTSHIFT must have an integer constant as its " 04119 "2nd argument:\n\n" 04120 +e.toString()); 04121 if(!(e[2].getRational().getInt() >=0 )) 04122 throw ParserException("parameter must be an integer constant >= 0.\n" 04123 +e.toString()); 04124 return newFixedLeftShiftExpr(parseExpr(e[1]), e[2].getRational().getInt()); 04125 break; 04126 case CONST_WIDTH_LEFTSHIFT: 04127 if(!(e.arity() == 3)) 04128 throw ParserException("TheoryBitvector::parseExprOp: CONST_WIDTH_LEFTSHIFT" 04129 "kind should have exactly 2 arg:\n\n" 04130 + e.toString()); 04131 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04132 throw ParserException("CONST_WIDTH_LEFTSHIFT must have an integer constant as its " 04133 "2nd argument:\n\n" 04134 +e.toString()); 04135 if(!(e[2].getRational().getInt() >=0 )) 04136 throw ParserException("parameter must be an integer constant >= 0.\n" 04137 +e.toString()); 04138 return newFixedConstWidthLeftShiftExpr(parseExpr(e[1]), e[2].getRational().getInt()); 04139 break; 04140 case RIGHTSHIFT: 04141 if(!(e.arity() == 3)) 04142 throw ParserException("TheoryBitvector::parseExprOp: RIGHTSHIFT" 04143 "kind should have exactly 2 arg:\n\n" 04144 + e.toString()); 04145 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04146 throw ParserException("RIGHTSHIFT must have an integer constant as its " 04147 "2nd argument:\n\n" 04148 +e.toString()); 04149 if(!(e[2].getRational().getInt() >=0 )) 04150 throw ParserException("parameter must be an integer constant >= 0.\n" 04151 +e.toString()); 04152 return newFixedRightShiftExpr(parseExpr(e[1]), e[2].getRational().getInt()); 04153 break; 04154 // BVSHL, BVLSHR, BVASHR handled with arith operators below 04155 case SX: 04156 // smtlib format interprets the integer argument as the number of bits to 04157 // extend, while CVC format interprets it as the new total size. 04158 // The smtlib parser inserts an extra argument "_smtlib" for this operator 04159 // so that we can distinguish the two cases here. 04160 if (e.arity() == 4 && 04161 e[1].getKind() == ID && 04162 e[1][0].getString() == "_smtlib") { 04163 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04164 throw ParserException("sign_extend must have an integer constant as its" 04165 " 1st argument:\n\n" 04166 +e.toString()); 04167 if(!(e[2].getRational().getInt() >=0 )) 04168 throw ParserException("sign_extend must have an integer constant as its" 04169 " 1st argument >= 0:\n\n" 04170 +e.toString()); 04171 Expr e3 = parseExpr(e[3]); 04172 return newSXExpr(e3, BVSize(e3) + e[2].getRational().getInt()); 04173 } 04174 if(!(e.arity() == 3)) 04175 throw ParserException("TheoryBitvector::parseExprOp: SX" 04176 "kind should have exactly 2 arg:\n\n" 04177 + e.toString()); 04178 if(!e[2].isRational() || !e[2].getRational().isInteger()) 04179 throw ParserException("SX must have an integer constant as its" 04180 " 2nd argument:\n\n" 04181 +e.toString()); 04182 if(!(e[2].getRational().getInt() >=0 )) 04183 throw ParserException("SX must have an integer constant as its" 04184 " 2nd argument >= 0:\n\n" 04185 +e.toString()); 04186 return newSXExpr(parseExpr(e[1]), e[2].getRational().getInt()); 04187 break; 04188 case BVROTL: 04189 case BVROTR: 04190 case BVREPEAT: 04191 case BVZEROEXTEND: 04192 if(!(e.arity() == 3)) 04193 throw ParserException("TheoryBitvector::parseExprOp:" 04194 "kind should have exactly 2 arg:\n\n" 04195 + e.toString()); 04196 if(!e[1].isRational() || !e[1].getRational().isInteger()) 04197 throw ParserException("BVIndexExpr must have an integer constant as its" 04198 " 1st argument:\n\n" 04199 +e.toString()); 04200 if (kind == BVREPEAT && !(e[1].getRational().getInt() >0 )) 04201 throw ParserException("BVREPEAT must have an integer constant as its" 04202 " 1st argument > 0:\n\n" 04203 +e.toString()); 04204 if(!(e[1].getRational().getInt() >=0 )) 04205 throw ParserException("BVIndexExpr must have an integer constant as its" 04206 " 1st argument >= 0:\n\n" 04207 +e.toString()); 04208 return newBVIndexExpr(kind, parseExpr(e[2]), e[1].getRational().getInt()); 04209 break; 04210 04211 case BVAND: { 04212 if(!(e.arity() >= 3)) 04213 throw ParserException("TheoryBitvector::parseExprOp: BVAND " 04214 "kind should have at least 2 arg:\n\n" 04215 + e.toString()); 04216 vector<Expr> kids; 04217 for(int i=1, iend=e.arity(); i<iend; ++i) 04218 kids.push_back(parseExpr(e[i])); 04219 return newBVAndExpr(kids); 04220 break; 04221 } 04222 case BVOR: { 04223 if(!(e.arity() >= 3)) 04224 throw ParserException("TheoryBitvector::parseExprOp: BVOR " 04225 "kind should have at least 2 arg:\n\n" 04226 + e.toString()); 04227 vector<Expr> kids; 04228 for(int i=1, iend=e.arity(); i<iend; ++i) 04229 kids.push_back(parseExpr(e[i])); 04230 return newBVOrExpr(kids); 04231 break; 04232 } 04233 case BVXOR: { 04234 if(!(e.arity() == 3)) 04235 throw ParserException("TheoryBitvector::parseExprOp: BVXOR " 04236 "kind should have exactly 2 arg:\n\n" 04237 + e.toString()); 04238 return newBVXorExpr(parseExpr(e[1]), parseExpr(e[2])); 04239 break; 04240 } 04241 case BVXNOR: { 04242 if(!(e.arity() == 3)) 04243 throw ParserException("TheoryBitvector::parseExprOp: BVXNOR" 04244 "kind should have exactly 2 arg:\n\n" 04245 + e.toString()); 04246 return newBVXnorExpr(parseExpr(e[1]), parseExpr(e[2])); 04247 break; 04248 } 04249 case BVNEG: 04250 if(!(e.arity() == 2)) 04251 throw ParserException("TheoryBitvector::parseExprOp: BVNEG" 04252 "kind should have exactly 1 arg:\n\n" 04253 + e.toString()); 04254 return newBVNegExpr(parseExpr(e[1])); 04255 break; 04256 case BVNAND: 04257 if(!(e.arity() == 3)) 04258 throw ParserException("TheoryBitvector::parseExprOp: BVNAND" 04259 "kind should have exactly 2 arg:\n\n" 04260 + e.toString()); 04261 return newBVNandExpr(parseExpr(e[1]), parseExpr(e[2])); 04262 break; 04263 case BVNOR: 04264 if(!(e.arity() == 3)) 04265 throw ParserException("TheoryBitvector::parseExprOp: BVNOR" 04266 "kind should have exactly 2 arg:\n\n" 04267 + e.toString()); 04268 return newBVNorExpr(parseExpr(e[1]), parseExpr(e[2])); 04269 break; 04270 case BVCOMP: { 04271 if(!(e.arity() == 3)) 04272 throw ParserException("TheoryBitvector::parseExprOp: BVXNOR" 04273 "kind should have exactly 2 arg:\n\n" 04274 + e.toString()); 04275 return newBVCompExpr(parseExpr(e[1]), parseExpr(e[2])); 04276 break; 04277 } 04278 04279 case BVUMINUS: 04280 if(!(e.arity() == 2)) 04281 throw ParserException("TheoryBitvector::parseExprOp: BVUMINUS" 04282 "kind should have exactly 1 arg:\n\n" 04283 + e.toString()); 04284 return newBVUminusExpr(parseExpr(e[1])); 04285 break; 04286 case BVPLUS: { 04287 vector<Expr> k; 04288 Expr::iterator i = e.begin(), iend=e.end(); 04289 if (!e[1].isRational()) { 04290 int maxsize = 0; 04291 Expr child; 04292 // Parse the kids of e and push them into the vector 'k' 04293 for(++i; i!=iend; ++i) { 04294 child = parseExpr(*i); 04295 if (getBaseType(child).getExpr().getOpKind() != BITVECTOR) { 04296 throw ParserException("BVPLUS argument is not bitvector"); 04297 } 04298 if (BVSize(child) > maxsize) maxsize = BVSize(child); 04299 k.push_back(child); 04300 } 04301 if (e.arity() == 1) return k[0]; 04302 return newBVPlusPadExpr(maxsize, k); 04303 } 04304 else { 04305 if(!(e.arity() >= 4)) 04306 throw ParserException("Expected at least 3 args in BVPLUS:\n\n" 04307 +e.toString()); 04308 if(!e[1].isRational() || !e[1].getRational().isInteger()) 04309 throw ParserException 04310 ("Expected integer constant in BVPLUS:\n\n" 04311 +e.toString()); 04312 if(!(e[1].getRational().getInt() > 0)) 04313 throw ParserException("parameter must be an integer constant > 0.\n" 04314 +e.toString()); 04315 // Skip first two elements of the vector of kids in 'e'. 04316 // The first element is the kind, and the second is the 04317 // numOfBits of the bvplus operator. 04318 ++i;++i; 04319 // Parse the kids of e and push them into the vector 'k' 04320 for(; i!=iend; ++i) k.push_back(parseExpr(*i)); 04321 return newBVPlusPadExpr(e[1].getRational().getInt(), k); 04322 } 04323 break; 04324 } 04325 case BVSUB: { 04326 if (e.arity() == 3) { 04327 Expr summand1 = parseExpr(e[1]); 04328 Expr summand2 = parseExpr(e[2]); 04329 if (BVSize(summand1) != BVSize(summand2)) { 04330 throw ParserException("BVSUB: expected same sized arguments" 04331 +e.toString()); 04332 } 04333 return newBVSubExpr(summand1, summand2); 04334 } 04335 else if (e.arity() != 4) 04336 throw ParserException("BVSUB: wrong number of arguments:\n\n" 04337 +e.toString()); 04338 if (!e[1].isRational() || !e[1].getRational().isInteger()) 04339 throw ParserException("BVSUB: expected an integer constant as " 04340 "first argument:\n\n" 04341 +e.toString()); 04342 if (!(e[1].getRational().getInt() > 0)) 04343 throw ParserException("parameter must be an integer constant > 0.\n" 04344 +e.toString()); 04345 int bvsublength = e[1].getRational().getInt(); 04346 Expr summand1 = parseExpr(e[2]); 04347 summand1 = pad(bvsublength, summand1); 04348 Expr summand2 = parseExpr(e[3]); 04349 summand2 = pad(bvsublength, summand2); 04350 return newBVSubExpr(summand1, summand2); 04351 break; 04352 } 04353 case BVMULT: { 04354 vector<Expr> k; 04355 Expr::iterator i = e.begin(), iend=e.end(); 04356 if (!e[1].isRational()) { 04357 if (e.arity() != 3) { 04358 throw ParserException("TheoryBitvector::parseExprOp: BVMULT: " 04359 "expected exactly 2 args:\n\n" 04360 + e.toString()); 04361 } 04362 int maxsize = 0; 04363 Expr child; 04364 // Parse the kids of e and push them into the vector 'k' 04365 for(++i; i!=iend; ++i) { 04366 child = parseExpr(*i); 04367 if (getBaseType(child).getExpr().getOpKind() != BITVECTOR) { 04368 throw ParserException("BVMULT argument is not bitvector"); 04369 } 04370 if (BVSize(child) > maxsize) maxsize = BVSize(child); 04371 k.push_back(child); 04372 } 04373 if (e.arity() == 1) return k[0]; 04374 return newBVMultPadExpr(maxsize, k[0], k[1]); 04375 } 04376 if(!(e.arity() == 4)) 04377 throw ParserException("TheoryBitvector::parseExprOp: BVMULT: " 04378 "expected exactly 3 args:\n\n" 04379 + e.toString()); 04380 if(!e[1].isRational() || !e[1].getRational().isInteger()) 04381 throw ParserException("BVMULT: expected integer constant" 04382 "as first argument:\n\n" 04383 +e.toString()); 04384 if(!(e[1].getRational().getInt() > 0)) 04385 throw ParserException("parameter must be an integer constant > 0.\n" 04386 +e.toString()); 04387 return newBVMultPadExpr(e[1].getRational().getInt(), 04388 parseExpr(e[2]), parseExpr(e[3])); 04389 break; 04390 } 04391 case BVUDIV: 04392 case BVSDIV: 04393 case BVUREM: 04394 case BVSREM: 04395 case BVSMOD: 04396 case BVSHL: 04397 case BVASHR: 04398 case BVLSHR: { 04399 if(!(e.arity() == 3)) 04400 throw ParserException("TheoryBitvector::parseExprOp:" 04401 "kind should have exactly 2 args:\n\n" 04402 + e.toString()); 04403 Expr e1 = parseExpr(e[1]); 04404 Expr e2 = parseExpr(e[2]); 04405 if (e1.getType().getExpr().getOpKind() != BITVECTOR || 04406 e2.getType().getExpr().getOpKind() != BITVECTOR) 04407 throw ParserException("TheoryBitvector::parseExprOp:" 04408 "Expected bitvector arguments:\n\n" 04409 + e.toString()); 04410 if (BVSize(e1) != BVSize(e2)) 04411 throw ParserException("TheoryBitvector::parseExprOp:" 04412 "Expected bitvectors of same size:\n\n" 04413 + e.toString()); 04414 if (kind == BVSHL) { 04415 if (e2.getKind() == BVCONST) 04416 return newFixedConstWidthLeftShiftExpr(e1, 04417 computeBVConst(e2).getInt()); 04418 } 04419 else if (kind == BVLSHR) { 04420 if (e2.getKind() == BVCONST) 04421 return newFixedRightShiftExpr(e1, computeBVConst(e2).getInt()); 04422 } 04423 return Expr(kind, e1, e2); 04424 break; 04425 } 04426 04427 case BVLT: 04428 if(!(e.arity() == 3)) 04429 throw ParserException("TheoryBitvector::parseExprOp: BVLT" 04430 "kind should have exactly 2 arg:\n\n" 04431 + e.toString()); 04432 return newBVLTExpr(parseExpr(e[1]),parseExpr(e[2])); 04433 break; 04434 case BVLE: 04435 if(!(e.arity() == 3)) 04436 throw ParserException("TheoryBitvector::parseExprOp: BVLE" 04437 "kind should have exactly 2 arg:\n\n" 04438 + e.toString()); 04439 return newBVLEExpr(parseExpr(e[1]),parseExpr(e[2])); 04440 break; 04441 case BVGT: 04442 if(!(e.arity() == 3)) 04443 throw ParserException("TheoryBitvector::parseExprOp: BVGT" 04444 "kind should have exactly 2 arg:\n\n" 04445 + e.toString()); 04446 return newBVLTExpr(parseExpr(e[2]),parseExpr(e[1])); 04447 break; 04448 case BVGE: 04449 if(!(e.arity() == 3)) 04450 throw ParserException("TheoryBitvector::parseExprOp: BVGE" 04451 "kind should have exactly 2 arg:\n\n" 04452 + e.toString()); 04453 return newBVLEExpr(parseExpr(e[2]),parseExpr(e[1])); 04454 break; 04455 case BVSLT: 04456 if(!(e.arity() == 3)) 04457 throw ParserException("TheoryBitvector::parseExprOp: BVLT" 04458 "kind should have exactly 2 arg:\n\n" 04459 + e.toString()); 04460 return newBVSLTExpr(parseExpr(e[1]),parseExpr(e[2])); 04461 break; 04462 case BVSLE: 04463 if(!(e.arity() == 3)) 04464 throw ParserException("TheoryBitvector::parseExprOp: BVLE" 04465 "kind should have exactly 2 arg:\n\n" 04466 + e.toString()); 04467 return newBVSLEExpr(parseExpr(e[1]),parseExpr(e[2])); 04468 break; 04469 case BVSGT: 04470 if(!(e.arity() == 3)) 04471 throw ParserException("TheoryBitvector::parseExprOp: BVGT" 04472 "kind should have exactly 2 arg:\n\n" 04473 + e.toString()); 04474 return newBVSLTExpr(parseExpr(e[2]),parseExpr(e[1])); 04475 break; 04476 case BVSGE: 04477 if(!(e.arity() == 3)) 04478 throw ParserException("TheoryBitvector::parseExprOp: BVGE" 04479 "kind should have exactly 2 arg:\n\n" 04480 + e.toString()); 04481 return newBVSLEExpr(parseExpr(e[2]),parseExpr(e[1])); 04482 break; 04483 04484 case INTTOBV: 04485 throw ParserException("INTTOBV not implemented"); 04486 break; 04487 case BVTOINT: 04488 throw ParserException("BVTOINT not implemented"); 04489 break; 04490 04491 case BVTYPEPRED: 04492 throw ParserException("BVTYPEPRED is used internally"); 04493 break; 04494 04495 default: 04496 FatalAssert(false, 04497 "TheoryBitvector::parseExprOp: unrecognized input operator" 04498 +e.toString()); 04499 break; 04500 } 04501 return e; 04502 } 04503 04504 04505 /////////////////////////////////////////////////////////////////////////////// 04506 //helper functions 04507 /////////////////////////////////////////////////////////////////////////////// 04508 04509 04510 Expr TheoryBitvector::newBitvectorTypeExpr(int bvLength) 04511 { 04512 DebugAssert(bvLength > 0, 04513 "TheoryBitvector::newBitvectorTypeExpr:\n" 04514 "len of a BV must be a positive integer:\n bvlength = "+ 04515 int2string(bvLength)); 04516 if (bvLength > d_maxLength) 04517 d_maxLength = bvLength; 04518 return Expr(BITVECTOR, getEM()->newRatExpr(bvLength)); 04519 } 04520 04521 04522 Expr TheoryBitvector::newBitvectorTypePred(const Type& t, const Expr& e) 04523 { 04524 return Expr(Expr(BVTYPEPRED, t.getExpr()).mkOp(), e); 04525 } 04526 04527 04528 Expr TheoryBitvector::newBVAndExpr(const Expr& t1, const Expr& t2) 04529 { 04530 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04531 BITVECTOR == t2.getType().getExpr().getOpKind(), 04532 "TheoryBitvector::newBVAndExpr:" 04533 "inputs must have type BITVECTOR:\n t1 = " + 04534 t1.toString() + "\n t2 = " +t2.toString()); 04535 DebugAssert(BVSize(t1) == BVSize(t2), 04536 "TheoryBitvector::bitwise operator" 04537 "inputs must have same length:\n t1 = " + t1.toString() 04538 + "\n t2 = " + t2.toString()); 04539 return Expr(CVC3::BVAND, t1, t2); 04540 } 04541 04542 04543 Expr TheoryBitvector::newBVAndExpr(const vector<Expr>& kids) 04544 { 04545 DebugAssert(kids.size() >= 2, 04546 "TheoryBitvector::newBVAndExpr:" 04547 "# of subterms must be at least 2"); 04548 for(unsigned int i=0; i<kids.size(); ++i) { 04549 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04550 "TheoryBitvector::newBVAndExpr:" 04551 "inputs must have type BITVECTOR:\n t1 = " + 04552 kids[i].toString()); 04553 if(i < kids.size()-1) { 04554 DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]), 04555 "TheoryBitvector::bitwise operator" 04556 "inputs must have same length:\n t1 = " + kids[i].toString() 04557 + "\n t2 = " + kids[i+1].toString()); 04558 } 04559 } 04560 return Expr(CVC3::BVAND, kids, getEM()); 04561 } 04562 04563 04564 Expr TheoryBitvector::newBVOrExpr(const Expr& t1, const Expr& t2) 04565 { 04566 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04567 BITVECTOR == t2.getType().getExpr().getOpKind(), 04568 "TheoryBitvector::newBVOrExpr: " 04569 "inputs must have type BITVECTOR:\n t1 = " + 04570 t1.toString() + "\n t2 = " +t2.toString()); 04571 DebugAssert(BVSize(t1) == BVSize(t2), 04572 "TheoryBitvector::bitwise OR operator: " 04573 "inputs must have same length:\n t1 = " + t1.toString() 04574 + "\n t2 = " + t2.toString()); 04575 return Expr(CVC3::BVOR, t1, t2); 04576 } 04577 04578 04579 Expr TheoryBitvector::newBVOrExpr(const vector<Expr>& kids) 04580 { 04581 DebugAssert(kids.size() >= 2, 04582 "TheoryBitvector::newBVOrExpr: " 04583 "# of subterms must be at least 2"); 04584 for(unsigned int i=0; i<kids.size(); ++i) { 04585 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04586 "TheoryBitvector::newBVOrExpr: " 04587 "inputs must have type BITVECTOR:\n t1 = " + 04588 kids[i].toString()); 04589 if(i < kids.size()-1) { 04590 DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]), 04591 "TheoryBitvector::bitwise operator" 04592 "inputs must have same length:\n t1 = " + kids[i].toString() 04593 + "\n t2 = " + kids[i+1].toString()); 04594 } 04595 } 04596 return Expr(CVC3::BVOR, kids, getEM()); 04597 } 04598 04599 04600 Expr TheoryBitvector::newBVNandExpr(const Expr& t1, const Expr& t2) 04601 { 04602 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04603 BITVECTOR == t2.getType().getExpr().getOpKind(), 04604 "TheoryBitvector::newBVNandExpr:" 04605 "inputs must have type BITVECTOR:\n t1 = " + 04606 t1.toString() + "\n t2 = " +t2.toString()); 04607 DebugAssert(BVSize(t1) == BVSize(t2), 04608 "TheoryBitvector::bitwise operator" 04609 "inputs must have same length:\n t1 = " + t1.toString() 04610 + "\n t2 = " + t2.toString()); 04611 return Expr(CVC3::BVNAND, t1, t2); 04612 } 04613 04614 04615 Expr TheoryBitvector::newBVNorExpr(const Expr& t1, const Expr& t2) 04616 { 04617 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04618 BITVECTOR == t2.getType().getExpr().getOpKind(), 04619 "TheoryBitvector::newBVNorExpr:" 04620 "inputs must have type BITVECTOR:\n t1 = " + 04621 t1.toString() + "\n t2 = " +t2.toString()); 04622 DebugAssert(BVSize(t1) == BVSize(t2), 04623 "TheoryBitvector::bitwise operator" 04624 "inputs must have same length:\n t1 = " + t1.toString() 04625 + "\n t2 = " + t2.toString()); 04626 return Expr(CVC3::BVNOR, t1, t2); 04627 } 04628 04629 04630 Expr TheoryBitvector::newBVXorExpr(const Expr& t1, const Expr& t2) 04631 { 04632 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04633 BITVECTOR == t2.getType().getExpr().getOpKind(), 04634 "TheoryBitvector::newBVXorExpr:" 04635 "inputs must have type BITVECTOR:\n t1 = " + 04636 t1.toString() + "\n t2 = " +t2.toString()); 04637 DebugAssert(BVSize(t1) == BVSize(t2), 04638 "TheoryBitvector::bitwise operator" 04639 "inputs must have same length:\n t1 = " + t1.toString() 04640 + "\n t2 = " + t2.toString()); 04641 return Expr(CVC3::BVXOR, t1, t2); 04642 } 04643 04644 04645 Expr TheoryBitvector::newBVXorExpr(const vector<Expr>& kids) 04646 { 04647 DebugAssert(kids.size() >= 2, 04648 "TheoryBitvector::newBVXorExpr:" 04649 "# of subterms must be at least 2"); 04650 for(unsigned int i=0; i<kids.size(); ++i) { 04651 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04652 "TheoryBitvector::newBVXorExpr:" 04653 "inputs must have type BITVECTOR:\n t1 = " + 04654 kids[i].toString()); 04655 if(i < kids.size()-1) { 04656 DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]), 04657 "TheoryBitvector::bitwise operator" 04658 "inputs must have same length:\n t1 = " + kids[i].toString() 04659 + "\n t2 = " + kids[i+1].toString()); 04660 } 04661 } 04662 return Expr(CVC3::BVXOR, kids, getEM()); 04663 } 04664 04665 04666 Expr TheoryBitvector::newBVXnorExpr(const Expr& t1, const Expr& t2) 04667 { 04668 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04669 BITVECTOR == t2.getType().getExpr().getOpKind(), 04670 "TheoryBitvector::newBVXnorExpr:" 04671 "inputs must have type BITVECTOR:\n t1 = " + 04672 t1.toString() + "\n t2 = " +t2.toString()); 04673 DebugAssert(BVSize(t1) == BVSize(t2), 04674 "TheoryBitvector::bitwise operator" 04675 "inputs must have same length:\n t1 = " + t1.toString() 04676 + "\n t2 = " + t2.toString()); 04677 return Expr(CVC3::BVXNOR, t1, t2); 04678 } 04679 04680 04681 Expr TheoryBitvector::newBVCompExpr(const Expr& t1, const Expr& t2) 04682 { 04683 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04684 BITVECTOR == t2.getType().getExpr().getOpKind(), 04685 "TheoryBitvector::newBVCompExpr:" 04686 "inputs must have type BITVECTOR:\n t1 = " + 04687 t1.toString() + "\n t2 = " +t2.toString()); 04688 DebugAssert(BVSize(t1) == BVSize(t2), 04689 "TheoryBitvector::bitwise operator" 04690 "inputs must have same length:\n t1 = " + t1.toString() 04691 + "\n t2 = " + t2.toString()); 04692 return Expr(CVC3::BVCOMP, t1, t2); 04693 } 04694 04695 04696 Expr TheoryBitvector::newBVXnorExpr(const vector<Expr>& kids) 04697 { 04698 DebugAssert(kids.size() >= 2, 04699 "TheoryBitvector::newBVXnorExpr:" 04700 "# of subterms must be at least 2"); 04701 for(unsigned int i=0; i<kids.size(); ++i) { 04702 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04703 "TheoryBitvector::newBVXnorExpr:" 04704 "inputs must have type BITVECTOR:\n t1 = " + 04705 kids[i].toString()); 04706 if(i < kids.size()-1) { 04707 DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]), 04708 "TheoryBitvector::bitwise operator" 04709 "inputs must have same length:\n t1 = " + kids[i].toString() 04710 + "\n t2 = " + kids[i+1].toString()); 04711 } 04712 } 04713 return Expr(CVC3::BVXNOR, kids, getEM()); 04714 } 04715 04716 04717 Expr TheoryBitvector::newBVLTExpr(const Expr& t1, const Expr& t2) 04718 { 04719 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04720 BITVECTOR == t2.getType().getExpr().getOpKind(), 04721 "TheoryBitvector::newBVLTExpr:" 04722 "inputs must have type BITVECTOR:\n t1 = " + 04723 t1.toString() + "\n t2 = " +t2.toString()); 04724 return Expr(CVC3::BVLT, t1, t2); 04725 } 04726 04727 04728 Expr TheoryBitvector::newBVLEExpr(const Expr& t1, const Expr& t2) 04729 { 04730 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04731 BITVECTOR == t2.getType().getExpr().getOpKind(), 04732 "TheoryBitvector::newBVLEExpr:" 04733 "inputs must have type BITVECTOR:\n t1 = " + 04734 t1.toString() + "\n t2 = " +t2.toString()); 04735 return Expr(CVC3::BVLE, t1, t2); 04736 } 04737 04738 04739 Expr TheoryBitvector::newSXExpr(const Expr& t1, int len) 04740 { 04741 DebugAssert(len >=0, 04742 " TheoryBitvector::newSXExpr:" 04743 "SX index must be a non-negative integer"+ 04744 int2string(len)); 04745 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04746 "TheoryBitvector::newSXExpr:" 04747 "inputs must have type BITVECTOR:\n t1 = " + 04748 t1.toString()); 04749 if(len==0) return t1; 04750 return Expr(Expr(SX, getEM()->newRatExpr(len)).mkOp(), t1); 04751 } 04752 04753 04754 Expr TheoryBitvector::newBVIndexExpr(int kind, const Expr& t1, int len) 04755 { 04756 DebugAssert(kind != BVREPEAT || len > 0, 04757 "repeat requires index > 0"); 04758 DebugAssert(len >=0, 04759 "TheoryBitvector::newBVIndexExpr:" 04760 "index must be a non-negative integer"+ 04761 int2string(len)); 04762 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04763 "TheoryBitvector::newBVIndexExpr:" 04764 "inputs must have type BITVECTOR:\n t1 = " + 04765 t1.toString()); 04766 return Expr(Expr(kind, getEM()->newRatExpr(len)).mkOp(), t1); 04767 } 04768 04769 04770 Expr TheoryBitvector::newBVSLTExpr(const Expr& t1, const Expr& t2) 04771 { 04772 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04773 BITVECTOR == t2.getType().getExpr().getOpKind(), 04774 "TheoryBitvector::newBVSLTExpr:" 04775 "inputs must have type BITVECTOR:\n t1 = " + 04776 t1.toString() + "\n t2 = " +t2.toString()); 04777 return Expr(CVC3::BVSLT, t1, t2); 04778 } 04779 04780 04781 Expr TheoryBitvector::newBVSLEExpr(const Expr& t1, const Expr& t2) 04782 { 04783 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04784 BITVECTOR == t2.getType().getExpr().getOpKind(), 04785 "TheoryBitvector::newBVSLEExpr:" 04786 "inputs must have type BITVECTOR:\n t1 = " + 04787 t1.toString() + "\n t2 = " +t2.toString()); 04788 return Expr(CVC3::BVSLE, t1, t2); 04789 } 04790 04791 04792 Expr TheoryBitvector::newBVNegExpr(const Expr& t1) 04793 { 04794 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04795 "TheoryBitvector::newBVNegExpr:" 04796 "inputs must have type BITVECTOR:\n t1 = " + 04797 t1.toString()); 04798 return Expr(CVC3::BVNEG, t1); 04799 } 04800 04801 04802 Expr TheoryBitvector::newBVUminusExpr(const Expr& t1) 04803 { 04804 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04805 "TheoryBitvector::newBVNegExpr:" 04806 "inputs must have type BITVECTOR:\n t1 = " + 04807 t1.toString()); 04808 return Expr(CVC3::BVUMINUS, t1); 04809 } 04810 04811 04812 Expr TheoryBitvector::newBoolExtractExpr(const Expr& t1, int index) 04813 { 04814 DebugAssert(index >=0, 04815 " TheoryBitvector::newBoolExtractExpr:" 04816 "bool_extract index must be a non-negative integer"+ 04817 int2string(index)); 04818 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04819 "TheoryBitvector::newBVBoolExtractExpr:" 04820 "inputs must have type BITVECTOR:\n t1 = " + 04821 t1.toString()); 04822 return Expr(Expr(BOOLEXTRACT, getEM()->newRatExpr(index)).mkOp(), t1); 04823 } 04824 04825 04826 Expr TheoryBitvector::newFixedLeftShiftExpr(const Expr& t1, int shiftLength) 04827 { 04828 DebugAssert(shiftLength >=0, 04829 " TheoryBitvector::newFixedleftshift:" 04830 "fixed_shift index must be a non-negative integer"+ 04831 int2string(shiftLength)); 04832 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04833 "TheoryBitvector::newBVFixedleftshiftExpr:" 04834 "inputs must have type BITVECTOR:\n t1 = " + 04835 t1.toString()); 04836 return Expr(Expr(LEFTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1); 04837 } 04838 04839 04840 Expr TheoryBitvector::newFixedConstWidthLeftShiftExpr(const Expr& t1, int shiftLength) 04841 { 04842 DebugAssert(shiftLength >=0, 04843 " TheoryBitvector::newFixedConstWidthLeftShift:" 04844 "fixed_shift index must be a non-negative integer"+ 04845 int2string(shiftLength)); 04846 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04847 "TheoryBitvector::newBVFixedleftshiftExpr:" 04848 "inputs must have type BITVECTOR:\n t1 = " + 04849 t1.toString()); 04850 return Expr(Expr(CONST_WIDTH_LEFTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1); 04851 } 04852 04853 04854 Expr TheoryBitvector::newFixedRightShiftExpr(const Expr& t1, int shiftLength) 04855 { 04856 DebugAssert(shiftLength >=0, 04857 " TheoryBitvector::newFixedRightShift:" 04858 "fixed_shift index must be a non-negative integer"+ 04859 int2string(shiftLength)); 04860 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(), 04861 "TheoryBitvector::newBVFixedRightShiftExpr:" 04862 "inputs must have type BITVECTOR:\n t1 = " + 04863 t1.toString()); 04864 if(shiftLength==0) return t1; 04865 return Expr(Expr(RIGHTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1); 04866 } 04867 04868 04869 Expr TheoryBitvector::newConcatExpr(const Expr& t1, const Expr& t2) 04870 { 04871 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04872 BITVECTOR == t2.getType().getExpr().getOpKind(), 04873 "TheoryBitvector::newBVConcatExpr:" 04874 "inputs must have type BITVECTOR:\n t1 = " + 04875 t1.toString() + "\n t2 = " +t2.toString()); 04876 return Expr(CONCAT, t1, t2); 04877 } 04878 04879 04880 Expr TheoryBitvector::newConcatExpr(const Expr& t1, const Expr& t2, 04881 const Expr& t3) 04882 { 04883 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04884 BITVECTOR == t2.getType().getExpr().getOpKind() && 04885 BITVECTOR == t3.getType().getExpr().getOpKind(), 04886 "TheoryBitvector::newBVConcatExpr:" 04887 "inputs must have type BITVECTOR:\n t1 = " + 04888 t1.toString() + 04889 "\n t2 = " +t2.toString() + 04890 "\n t3 =" + t3.toString()); 04891 return Expr(CONCAT, t1, t2, t3); 04892 } 04893 04894 04895 Expr TheoryBitvector::newConcatExpr(const vector<Expr>& kids) 04896 { 04897 DebugAssert(kids.size() >= 2, 04898 "TheoryBitvector::newBVConcatExpr:" 04899 "# of subterms must be at least 2"); 04900 for(unsigned int i=0; i<kids.size(); ++i) { 04901 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04902 "TheoryBitvector::newBVConcatExpr:" 04903 "inputs must have type BITVECTOR:\n t1 = " + 04904 kids[i].toString()); 04905 } 04906 return Expr(CONCAT, kids, getEM()); 04907 } 04908 04909 04910 Expr TheoryBitvector::newBVMultExpr(int bvLength, 04911 const Expr& t1, const Expr& t2) 04912 { 04913 DebugAssert(bvLength > 0, 04914 "TheoryBitvector::newBVmultExpr:" 04915 "bvLength must be an integer > 0: bvLength = " + 04916 int2string(bvLength)); 04917 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04918 BITVECTOR == t2.getType().getExpr().getOpKind(), 04919 "TheoryBitvector::newBVmultExpr:" 04920 "inputs must have type BITVECTOR:\n t1 = " + 04921 t1.toString() + "\n t2 = " +t2.toString()); 04922 DebugAssert(bvLength == BVSize(t1) && 04923 bvLength == BVSize(t2), "Expected same length"); 04924 return Expr(Expr(BVMULT, getEM()->newRatExpr(bvLength)).mkOp(), t1, t2); 04925 } 04926 04927 04928 Expr TheoryBitvector::newBVMultExpr(int bvLength, const vector<Expr>& kids) 04929 { 04930 DebugAssert(bvLength > 0, 04931 "TheoryBitvector::newBVmultExpr:" 04932 "bvLength must be an integer > 0: bvLength = " + 04933 int2string(bvLength)); 04934 for(unsigned int i=0; i<kids.size(); ++i) { 04935 DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(), 04936 "TheoryBitvector::newBVPlusExpr:" 04937 "inputs must have type BITVECTOR:\n t1 = " + 04938 kids[i].toString()); 04939 DebugAssert(BVSize(kids[i]) == bvLength, "Expected matching sizes"); 04940 } 04941 return Expr(Expr(BVMULT, getEM()->newRatExpr(bvLength)).mkOp(), kids); 04942 } 04943 04944 04945 Expr TheoryBitvector::newBVMultPadExpr(int bvLength, const vector<Expr>& kids) 04946 { 04947 vector<Expr> newKids; 04948 for (unsigned i = 0; i < kids.size(); ++i) { 04949 newKids.push_back(pad(bvLength, kids[i])); 04950 } 04951 return newBVMultExpr(bvLength, newKids); 04952 } 04953 04954 04955 Expr TheoryBitvector::newBVMultPadExpr(int bvLength, 04956 const Expr& t1, const Expr& t2) 04957 { 04958 return newBVMultExpr(bvLength, pad(bvLength, t1), pad(bvLength, t2)); 04959 } 04960 04961 Expr TheoryBitvector::newBVUDivExpr(const Expr& t1, const Expr& t2) 04962 { 04963 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04964 BITVECTOR == t2.getType().getExpr().getOpKind(), 04965 "TheoryBitvector::newBVUDivExpr:" 04966 "inputs must have type BITVECTOR:\n t1 = " + 04967 t1.toString() + "\n t2 = " +t2.toString()); 04968 DebugAssert(BVSize(t2) == BVSize(t1), "Expected same length"); 04969 return Expr(BVUDIV, t1, t2); 04970 } 04971 04972 Expr TheoryBitvector::newBVURemExpr(const Expr& t1, const Expr& t2) 04973 { 04974 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04975 BITVECTOR == t2.getType().getExpr().getOpKind(), 04976 "TheoryBitvector::newBVURemExpr:" 04977 "inputs must have type BITVECTOR:\n t1 = " + 04978 t1.toString() + "\n t2 = " +t2.toString()); 04979 DebugAssert(BVSize(t2) == BVSize(t1), "Expected same length"); 04980 return Expr(BVUREM, t1, t2); 04981 } 04982 04983 Expr TheoryBitvector::newBVSDivExpr(const Expr& t1, const Expr& t2) 04984 { 04985 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04986 BITVECTOR == t2.getType().getExpr().getOpKind(), 04987 "TheoryBitvector::newBVSDivExpr:" 04988 "inputs must have type BITVECTOR:\n t1 = " + 04989 t1.toString() + "\n t2 = " +t2.toString()); 04990 DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length"); 04991 return Expr(BVSDIV, t1, t2); 04992 } 04993 04994 Expr TheoryBitvector::newBVSRemExpr(const Expr& t1, const Expr& t2) 04995 { 04996 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 04997 BITVECTOR == t2.getType().getExpr().getOpKind(), 04998 "TheoryBitvector::newBVSRemExpr:" 04999 "inputs must have type BITVECTOR:\n t1 = " + 05000 t1.toString() + "\n t2 = " +t2.toString()); 05001 DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length"); 05002 return Expr(BVSREM, t1, t2); 05003 } 05004 05005 Expr TheoryBitvector::newBVSModExpr(const Expr& t1, const Expr& t2) 05006 { 05007 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 05008 BITVECTOR == t2.getType().getExpr().getOpKind(), 05009 "TheoryBitvector::newBVSModExpr:" 05010 "inputs must have type BITVECTOR:\n t1 = " + 05011 t1.toString() + "\n t2 = " +t2.toString()); 05012 DebugAssert(BVSize(t1) == BVSize(t2), "Expected same length"); 05013 return Expr(BVSMOD, t1, t2); 05014 } 05015 05016 //! produces a string of 0's of length bvLength 05017 Expr TheoryBitvector::newBVZeroString(int bvLength) 05018 { 05019 DebugAssert(bvLength > 0, 05020 "TheoryBitvector::newBVZeroString:must be >= 0: " 05021 + int2string(bvLength)); 05022 std::vector<bool> bits; 05023 for(int count=0; count < bvLength; count++) { 05024 bits.push_back(false); 05025 } 05026 return newBVConstExpr(bits); 05027 } 05028 05029 05030 //! produces a string of 1's of length bvLength 05031 Expr TheoryBitvector::newBVOneString(int bvLength) 05032 { 05033 DebugAssert(bvLength > 0, 05034 "TheoryBitvector::newBVOneString:must be >= 0: " 05035 + int2string(bvLength)); 05036 std::vector<bool> bits; 05037 for(int count=0; count < bvLength; count++) { 05038 bits.push_back(true); 05039 } 05040 return newBVConstExpr(bits); 05041 } 05042 05043 05044 Expr TheoryBitvector::newBVConstExpr(const vector<bool>& bits) 05045 { 05046 DebugAssert(bits.size() > 0, 05047 "TheoryBitvector::newBVConstExpr:" 05048 "size of bits should be > 0"); 05049 BVConstExpr bv(getEM(), bits, d_bvConstExprIndex); 05050 return getEM()->newExpr(&bv); 05051 } 05052 05053 05054 Expr TheoryBitvector::newBVConstExpr(const Rational& r, int bvLength) 05055 { 05056 DebugAssert(r.isInteger(), 05057 "TheoryBitvector::newBVConstExpr: not an integer: " 05058 + r.toString()); 05059 DebugAssert(bvLength > 0, 05060 "TheoryBitvector::newBVConstExpr: bvLength = " 05061 + int2string(bvLength)); 05062 string s(r.toString(2)); 05063 size_t strsize = s.size(); 05064 size_t length = bvLength; 05065 Expr res; 05066 if(length > 0 && length != strsize) { 05067 //either (length > strsize) or (length < strsize) 05068 if(length < strsize) { 05069 s = s.substr((strsize-length), length); 05070 } else { 05071 string zeros(""); 05072 for(size_t i=0, pad=length-strsize; i < pad; ++i) 05073 zeros += "0"; 05074 s = zeros+s; 05075 } 05076 05077 res = newBVConstExpr(s, 2); 05078 } 05079 else 05080 res = newBVConstExpr(s, 2); 05081 05082 return res; 05083 } 05084 05085 05086 Expr TheoryBitvector::newBVConstExpr(const std::string& s, int base) 05087 { 05088 DebugAssert(s.size() > 0, 05089 "TheoryBitvector::newBVConstExpr:" 05090 "# of subterms must be at least 2"); 05091 DebugAssert(base == 2 || base == 16, 05092 "TheoryBitvector::newBVConstExpr: base = " 05093 +int2string(base)); 05094 //hexadecimal 05095 std::string str = s; 05096 if(16 == base) { 05097 Rational r(str, 16); 05098 return newBVConstExpr(r, str.size()*4); 05099 } 05100 else { 05101 BVConstExpr bv(getEM(), str, d_bvConstExprIndex); 05102 return getEM()->newExpr(&bv); 05103 } 05104 } 05105 05106 05107 Expr 05108 TheoryBitvector:: 05109 newBVExtractExpr(const Expr& e, int hi, int low) 05110 { 05111 DebugAssert(low>=0 && hi>=low, 05112 " TheoryBitvector::newBVExtractExpr: " 05113 "bad bv_extract indices: hi = " 05114 + int2string(hi) 05115 + ", low = " 05116 + int2string(low)); 05117 if (e.getOpKind() == LEFTSHIFT && 05118 hi == BVSize(e[0])-1 && 05119 low == 0) { 05120 return newFixedConstWidthLeftShiftExpr(e[0], getFixedLeftShiftParam(e)); 05121 } 05122 DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(), 05123 "TheoryBitvector::newBVExtractExpr:" 05124 "inputs must have type BITVECTOR:\n e = " + 05125 e.toString()); 05126 return Expr(Expr(EXTRACT, 05127 getEM()->newRatExpr(hi), 05128 getEM()->newRatExpr(low)).mkOp(), e); 05129 } 05130 05131 05132 Expr TheoryBitvector::newBVSubExpr(const Expr& t1, const Expr& t2) 05133 { 05134 DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() && 05135 BITVECTOR == t2.getType().getExpr().getOpKind(), 05136 "TheoryBitvector::newBVSubExpr:" 05137 "inputs must have type BITVECTOR:\n t1 = " + 05138 t1.toString() + "\n t2 = " +t2.toString()); 05139 DebugAssert(BVSize(t1) == BVSize(t2), 05140 "TheoryBitvector::newBVSubExpr" 05141 "inputs must have same length:\n t1 = " + t1.toString() 05142 + "\n t2 = " + t2.toString()); 05143 return Expr(BVSUB, t1, t2); 05144 } 05145 05146 05147 Expr TheoryBitvector::newBVPlusExpr(int bvLength, const Expr& k1, const Expr& k2) 05148 { 05149 DebugAssert(bvLength > 0, 05150 " TheoryBitvector::newBVPlusExpr:" 05151 "bvplus length must be a positive integer: "+ 05152 int2string(bvLength)); 05153 DebugAssert(BITVECTOR == k1.getType().getExpr().getOpKind(), 05154 "TheoryBitvector::newBVPlusExpr:" 05155 "inputs must have type BITVECTOR:\n t1 = " + 05156 k1.toString()); 05157 DebugAssert(BVSize(k1) == bvLength, "Expected matching sizes"); 05158 DebugAssert(BITVECTOR == k2.getType().getExpr().getOpKind(), 05159 "TheoryBitvector::newBVPlusExpr:" 05160 "inputs must have type BITVECTOR:\n t1 = " + 05161 k2.toString()); 05162 DebugAssert(BVSize(k2) == bvLength, "Expected matching sizes"); 05163 05164 return Expr(Expr(BVPLUS, getEM()->newRatExpr(bvLength)).mkOp(), k1, k2); 05165 } 05166 05167 05168 Expr TheoryBitvector::newBVPlusExpr(int bvLength, 05169 const vector<Expr>& k) 05170 { 05171 DebugAssert(bvLength > 0, 05172 " TheoryBitvector::newBVPlusExpr:" 05173 "bvplus length must be a positive integer: "+ 05174 int2string(bvLength)); 05175 DebugAssert(k.size() > 1, 05176 " TheoryBitvector::newBVPlusExpr:" 05177 " size of input vector must be greater than 0: "); 05178 for(unsigned int i=0; i<k.size(); ++i) { 05179 DebugAssert(BITVECTOR == k[i].getType().getExpr().getOpKind(), 05180 "TheoryBitvector::newBVPlusExpr:" 05181 "inputs must have type BITVECTOR:\n t1 = " + 05182 k[i].toString()); 05183 DebugAssert(BVSize(k[i]) == bvLength, "Expected matching sizes"); 05184 } 05185 return Expr(Expr(BVPLUS, getEM()->newRatExpr(bvLength)).mkOp(), k); 05186 } 05187 05188 05189 Expr TheoryBitvector::newBVPlusPadExpr(int bvLength, 05190 const vector<Expr>& k) 05191 { 05192 vector<Expr> newKids; 05193 for (unsigned i = 0; i < k.size(); ++i) { 05194 newKids.push_back(pad(bvLength, k[i])); 05195 } 05196 return newBVPlusExpr(bvLength, newKids); 05197 } 05198 05199 05200 // Accessors for expression parameters 05201 05202 05203 int TheoryBitvector::getBitvectorTypeParam(const Expr& e) 05204 { 05205 DebugAssert(BITVECTOR == e.getKind(), 05206 "TheoryBitvector::getBitvectorTypeParam: wrong kind: " + 05207 e.toString()); 05208 return e[0].getRational().getInt(); 05209 } 05210 05211 05212 Type TheoryBitvector::getTypePredType(const Expr& tp) 05213 { 05214 DebugAssert(tp.getOpKind()==BVTYPEPRED && tp.isApply(), 05215 "TheoryBitvector::getTypePredType:\n tp = "+tp.toString()); 05216 return Type(tp.getOpExpr()[0]); 05217 } 05218 05219 05220 const Expr& TheoryBitvector::getTypePredExpr(const Expr& tp) 05221 { 05222 DebugAssert(tp.getOpKind()==BVTYPEPRED, 05223 "TheoryBitvector::getTypePredType:\n tp = "+tp.toString()); 05224 return tp[0]; 05225 } 05226 05227 05228 int TheoryBitvector::getBoolExtractIndex(const Expr& e) 05229 { 05230 DebugAssert(BOOLEXTRACT == e.getOpKind() && e.isApply(), 05231 "TheoryBitvector::getBoolExtractIndex: wrong kind" + 05232 e.toString()); 05233 return e.getOpExpr()[0].getRational().getInt(); 05234 } 05235 05236 05237 int TheoryBitvector::getSXIndex(const Expr& e) 05238 { 05239 DebugAssert(SX == e.getOpKind() && e.isApply(), 05240 "TheoryBitvector::getSXIndex: wrong kind\n"+e.toString()); 05241 return e.getOpExpr()[0].getRational().getInt(); 05242 } 05243 05244 05245 int TheoryBitvector::getBVIndex(const Expr& e) 05246 { 05247 DebugAssert(e.isApply() && 05248 (e.getOpKind() == BVREPEAT || 05249 e.getOpKind() == BVROTL || 05250 e.getOpKind() == BVROTR || 05251 e.getOpKind() == BVZEROEXTEND), 05252 "TheoryBitvector::getBVIndex: wrong kind\n"+e.toString()); 05253 return e.getOpExpr()[0].getRational().getInt(); 05254 } 05255 05256 05257 int TheoryBitvector::getFixedLeftShiftParam(const Expr& e) 05258 { 05259 DebugAssert(e.isApply() && 05260 (LEFTSHIFT == e.getOpKind() || 05261 CONST_WIDTH_LEFTSHIFT == e.getOpKind()), 05262 "TheoryBitvector::getFixedLeftShiftParam: wrong kind" + 05263 e.toString()); 05264 return e.getOpExpr()[0].getRational().getInt(); 05265 } 05266 05267 05268 int TheoryBitvector::getFixedRightShiftParam(const Expr& e) 05269 { 05270 DebugAssert(RIGHTSHIFT == e.getOpKind() && e.isApply(), 05271 "TheoryBitvector::getFixedRightShiftParam: wrong kind" + 05272 e.toString()); 05273 return e.getOpExpr()[0].getRational().getInt(); 05274 } 05275 05276 05277 int TheoryBitvector::getExtractLow(const Expr& e) 05278 { 05279 DebugAssert(EXTRACT == e.getOpKind() && e.isApply(), 05280 "TheoryBitvector::getExtractLow: wrong kind" + 05281 e.toString()); 05282 return e.getOpExpr()[1].getRational().getInt(); 05283 } 05284 05285 05286 int TheoryBitvector::getExtractHi(const Expr& e) 05287 { 05288 DebugAssert(EXTRACT == e.getOpKind() && e.isApply(), 05289 "TheoryBitvector::getExtractHi: wrong kind" + 05290 e.toString()); 05291 return e.getOpExpr()[0].getRational().getInt(); 05292 } 05293 05294 05295 int TheoryBitvector::getBVPlusParam(const Expr& e) 05296 { 05297 DebugAssert(BVPLUS == e.getOpKind() && e.isApply(), 05298 "TheoryBitvector::getBVPlusParam: wrong kind" + 05299 e.toString(AST_LANG)); 05300 return e.getOpExpr()[0].getRational().getInt(); 05301 } 05302 05303 int TheoryBitvector::getBVMultParam(const Expr& e) 05304 { 05305 DebugAssert(BVMULT == e.getOpKind() && e.isApply(), 05306 "TheoryBitvector::getBVMultParam: wrong kind " + 05307 e.toString(AST_LANG)); 05308 return e.getOpExpr()[0].getRational().getInt(); 05309 } 05310 05311 unsigned TheoryBitvector::getBVConstSize(const Expr& e) 05312 { 05313 DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst"); 05314 const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue()); 05315 DebugAssert(bvc, "getBVConstSize: cast failed"); 05316 return bvc->size(); 05317 } 05318 05319 05320 bool TheoryBitvector::getBVConstValue(const Expr& e, int i) 05321 { 05322 DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst"); 05323 const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue()); 05324 DebugAssert(bvc, "getBVConstSize: cast failed"); 05325 return bvc->getValue(i); 05326 } 05327 05328 05329 // as newBVConstExpr can not give the BV expr of a negative rational, 05330 // I use this wrapper to do that 05331 Expr TheoryBitvector::signed_newBVConstExpr( Rational c, int bv_size) 05332 { 05333 if( c > 0) 05334 return newBVConstExpr( c, bv_size); 05335 else 05336 { 05337 c = -c; 05338 Expr tmp = newBVConstExpr( c, bv_size); 05339 Rational neg_tmp = computeNegBVConst( tmp ); 05340 return newBVConstExpr( neg_tmp, bv_size ); 05341 } 05342 } 05343 05344 05345 // Computes the integer value of a bitvector constant 05346 Rational TheoryBitvector::computeBVConst(const Expr& e) 05347 { 05348 DebugAssert(BVCONST == e.getKind(), 05349 "TheoryBitvector::computeBVConst:" 05350 "input must be a BITVECTOR CONST: " + e.toString()); 05351 if(*d_bv32Flag) { 05352 int c(0); 05353 for(int j=(int)getBVConstSize(e)-1; j>=0; j--) 05354 c = 2*c + getBVConstValue(e, j) ? 1 : 0; 05355 Rational d(c); 05356 return d; 05357 } else { 05358 Rational c(0); 05359 for(int j=(int)getBVConstSize(e)-1; j>=0; j--) 05360 c = 2*c + (getBVConstValue(e, j) ? Rational(1) : Rational(0)); 05361 return c; 05362 } 05363 } 05364 05365 05366 // Computes the integer value of ~c+1 05367 Rational TheoryBitvector::computeNegBVConst(const Expr& e) 05368 { 05369 DebugAssert(BVCONST == e.getKind(), 05370 "TheoryBitvector::computeBVConst:" 05371 "input must be a BITVECTOR CONST: " + e.toString()); 05372 if(*d_bv32Flag) { 05373 int c(0); 05374 for(int j=(int)getBVConstSize(e)-1; j>=0; j--) 05375 c = 2*c + getBVConstValue(e, j) ? 0 : 1; 05376 Rational d(c+1); 05377 return d; 05378 } else { 05379 Rational c(0); 05380 for(int j=(int)getBVConstSize(e)-1; j>=0; j--) 05381 c = 2*c + (getBVConstValue(e, j) ? Rational(0) : Rational(1)); 05382 return c+1; 05383 } 05384 } 05385 05386 05387 ////////////////////////////////////////////////////////////////////// 05388 // class BVConstExpr methods 05389 ///////////////////////////////////////////////////////////////////// 05390 05391 05392 //! Constructor 05393 BVConstExpr::BVConstExpr(ExprManager* em, std::string bvconst, 05394 size_t mmIndex, ExprIndex idx) 05395 : ExprValue(em, BVCONST, idx), d_MMIndex(mmIndex) 05396 { 05397 std::string::reverse_iterator i = bvconst.rbegin(); 05398 std::string::reverse_iterator iend = bvconst.rend(); 05399 DebugAssert(bvconst.size() > 0, 05400 "TheoryBitvector::newBVConstExpr:" 05401 "# of subterms must be at least 2"); 05402 05403 for(;i != iend; ++i) { 05404 TRACE("bitvector", "BVConstExpr: bit ", *i, ""); 05405 if('0' == *i) 05406 d_bvconst.push_back(false); 05407 else { 05408 if('1' == *i) 05409 d_bvconst.push_back(true); 05410 else 05411 DebugAssert(false, "BVConstExpr: bad binary bit-vector: " 05412 + bvconst); 05413 } 05414 } 05415 TRACE("bitvector", "BVConstExpr: #bits ", d_bvconst.size(), ""); 05416 } 05417 05418 05419 BVConstExpr::BVConstExpr(ExprManager* em, std::vector<bool> bvconst, 05420 size_t mmIndex, ExprIndex idx) 05421 : ExprValue(em, BVCONST, idx), d_bvconst(bvconst), d_MMIndex(mmIndex) 05422 { 05423 TRACE("bitvector", "BVConstExpr(vector<bool>): arg. size = ", bvconst.size(), 05424 ", d_bvconst.size = "+int2string(d_bvconst.size())); 05425 } 05426 05427 05428 size_t BVConstExpr::computeHash() const 05429 { 05430 std::vector<bool>::const_iterator i = d_bvconst.begin(); 05431 std::vector<bool>::const_iterator iend = d_bvconst.end(); 05432 size_t hash_value = 0; 05433 hash_value = ExprValue::hash(BVCONST); 05434 for (;i != iend; i++) 05435 if(*i) 05436 hash_value = PRIME*hash_value + HASH_VALUE_ONE; 05437 else 05438 hash_value = PRIME*hash_value + HASH_VALUE_ZERO; 05439 return hash_value; 05440 } 05441 05442 Expr TheoryBitvector::computeTCC(const Expr& e) 05443 { 05444 // inline recursive computation for deeply nested bitvector Exprs 05445 05446 vector<Expr> operatorStack; 05447 vector<Expr> operandStack; 05448 vector<int> childStack; 05449 Expr e2, tcc; 05450 05451 operatorStack.push_back(e); 05452 childStack.push_back(0); 05453 05454 while (!operatorStack.empty()) { 05455 DebugAssert(operatorStack.size() == childStack.size(), "Invariant violated"); 05456 05457 if (childStack.back() < operatorStack.back().arity()) { 05458 05459 e2 = operatorStack.back()[childStack.back()++]; 05460 05461 if (e2.isVar()) { 05462 operandStack.push_back(trueExpr()); 05463 } 05464 else { 05465 ExprMap<Expr>::iterator itccCache = theoryCore()->tccCache().find(e2); 05466 if (itccCache != theoryCore()->tccCache().end()) { 05467 operandStack.push_back((*itccCache).second); 05468 } 05469 else if (theoryOf(e2) == this) { 05470 if (e2.arity() == 0) { 05471 operandStack.push_back(trueExpr()); 05472 } 05473 else { 05474 operatorStack.push_back(e2); 05475 childStack.push_back(0); 05476 } 05477 } 05478 else { 05479 operandStack.push_back(getTCC(e2)); 05480 } 05481 } 05482 } 05483 else { 05484 e2 = operatorStack.back(); 05485 operatorStack.pop_back(); 05486 childStack.pop_back(); 05487 vector<Expr> children; 05488 vector<Expr>::iterator childStart = operandStack.end() - (e2.arity()); 05489 children.insert(children.begin(), childStart, operandStack.end()); 05490 operandStack.erase(childStart, operandStack.end()); 05491 tcc = (children.size() == 0) ? trueExpr() : 05492 (children.size() == 1) ? children[0] : 05493 getCommonRules()->rewriteAnd(andExpr(children)).getRHS(); 05494 switch(e2.getKind()) { 05495 case BVUDIV: 05496 case BVSDIV: 05497 case BVUREM: 05498 case BVSREM: 05499 case BVSMOD: { 05500 DebugAssert(e2.arity() == 2, ""); 05501 int size = BVSize(e2); 05502 tcc = getCommonRules()->rewriteAnd(tcc.andExpr(!(e2[1].eqExpr(newBVZeroString(size))))).getRHS(); 05503 break; 05504 } 05505 default: 05506 break; 05507 } 05508 operandStack.push_back(tcc); 05509 theoryCore()->tccCache()[e2] = tcc; 05510 } 05511 } 05512 DebugAssert(childStack.empty(), "Invariant violated"); 05513 DebugAssert(operandStack.size() == 1, "Expected single operand left"); 05514 return operandStack.back(); 05515 }