00001 /*****************************************************************************/ 00002 /*! 00003 * \file bitvector_theorem_producer.h 00004 * \brief TRUSTED implementation of bitvector proof rules 00005 * 00006 * Author: Vijay Ganesh 00007 * 00008 * Created: Wed May 5 16:10:28 PST 2004 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 */ 00020 /*****************************************************************************/ 00021 00022 #ifndef _cvc3__bitvector_theorem_producer_h_ 00023 #define _cvc3__bitvector_theorem_producer_h_ 00024 00025 #include "bitvector_proof_rules.h" 00026 #include "theorem_producer.h" 00027 00028 namespace CVC3 { 00029 00030 class TheoryBitvector; 00031 00032 /*! @brief This class implements proof rules for bitvector 00033 * normalizers (concatenation normal form, bvplus normal form), 00034 * bitblaster rules, other relevant rewrite rules for bv arithmetic 00035 * and word-level operators 00036 */ 00037 /*! 00038 Author: Vijay Ganesh, May-August, 2004 00039 00040 */ 00041 class BitvectorTheoremProducer: 00042 public BitvectorProofRules, public TheoremProducer { 00043 private: 00044 TheoryBitvector* d_theoryBitvector; //! instance of bitvector DP 00045 //! Constant 1-bit bit-vector 0bin0 00046 Expr d_bvZero; 00047 //! Constant 1-bit bit-vector 0bin1 00048 Expr d_bvOne; 00049 //! Return cached constant 0bin0 00050 const Expr& bvZero() const { return d_bvZero; } 00051 //! Return cached constant 0bin1 00052 const Expr& bvOne() const { return d_bvOne; } 00053 00054 //! Collect all of: a*x1+b*x1 + c*x2-x2 + d*x3 + ~x3 + ~x4 +e into 00055 //! (a+b, x1) , (c-1 , x2), (d-1, x3), (-1, x4) and the constant e-2. 00056 //! The constant is calculated from the formula -x = ~x+1 (or -x-1=~x). 00057 void collectLikeTermsOfPlus(const Expr& e, 00058 ExprMap<Rational> & likeTerms, 00059 Rational & plusConstant); 00060 00061 //! Collect a single coefficient*var pair into likeTerms. 00062 //! Update the counter of likeTerms[var] += coefficient. 00063 //! Potentially update the constant additive plusConstant. 00064 void collectOneTermOfPlus(const Rational & coefficient, 00065 const Expr& var, 00066 ExprMap<Rational> & likeTerms, 00067 Rational & plusConstant); 00068 00069 //! Create a vector which will form the next PVPLUS. 00070 //! Use the colleciton of likeTerms, and the constant additive plusConstant 00071 void createNewPlusCollection(const Expr & e, 00072 const ExprMap<Rational> & likeTerms, 00073 Rational & plusConstant, 00074 std::vector<Expr> & result); 00075 00076 //! Create expression by applying plus to all elements. 00077 //! All elements should be normalized and ready. 00078 //! If there are too few elements, a non BVPLUS expression will be created. 00079 Expr sumNormalizedElements(int bvplusLength, 00080 const std::vector<Expr>& elements); 00081 public: 00082 //! Constructor: constructs an instance of bitvector DP 00083 BitvectorTheoremProducer(TheoryBitvector* theoryBitvector); 00084 ~BitvectorTheoremProducer() {} 00085 00086 //ExprMap<Expr> d_bvPlusCarryCacheLeftBV; 00087 //ExprMap<Expr> d_bvPlusCarryCacheRightBV; 00088 00089 //////////////////////////////////////////////////////////////////// 00090 // Partial Canonization rules 00091 //////////////////////////////////////////////////////////////////// 00092 00093 //////////////////////////////////////////////////////////////////// 00094 // Bitblasting rules for equations 00095 //////////////////////////////////////////////////////////////////// 00096 00097 /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false 00098 * 00099 * \result (e1=e2)<=>false 00100 */ 00101 Theorem bitvectorFalseRule(const Theorem& thm); 00102 00103 /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true 00104 * 00105 * \result (e1!=e2)<=>true 00106 */ 00107 Theorem bitvectorTrueRule(const Theorem& thm); 00108 00109 /*! \param e input equation: e1=e2 over bitvector terms 00110 * \param f formula over the bits of bitvector variables in e: 00111 * 00112 * \result \f[\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i] 00113 * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a 00114 * formula over variables in \f[ e_{1}, e_{2} \f] respectively 00115 */ 00116 Theorem bitBlastEqnRule(const Expr& e, const Expr& f); 00117 00118 /*! \param e : input disequality: e1 != e2 over bitvector terms 00119 * \param f : formula over the bits of bitvector variables in e: 00120 * 00121 * \result \f[\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i]) 00122 * \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a 00123 * formula over variables in \f[ e_{1}, e_{2} \f] respectively 00124 */ 00125 Theorem bitBlastDisEqnRule(const Theorem& e, const Expr& f); 00126 00127 00128 //////////////////////////////////////////////////////////////////// 00129 // Bitblasting and rewrite rules for Inequations 00130 //////////////////////////////////////////////////////////////////// 00131 00132 //! sign extend the input SX(e) appropriately 00133 Theorem signExtendRule(const Expr& e); 00134 00135 //! Pad the kids of BVLT/BVLE to make their length equal 00136 Theorem padBVLTRule(const Expr& e, int len); 00137 00138 //! Sign Extend the kids of BVSLT/BVSLE to make their length equal 00139 Theorem padBVSLTRule(const Expr& e, int len); 00140 00141 /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of 00142 * e0 and e1 are constants. If they are constants then optimizations 00143 * are done, otherwise the following rule is implemented. 00144 * 00145 * e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR 00146 * (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR 00147 * (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0]) 00148 */ 00149 Theorem signBVLTRule(const Expr& e, 00150 const Theorem& topBit0, 00151 const Theorem& topBit1); 00152 00153 /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]), 00154 * NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0]) 00155 */ 00156 Theorem notBVLTRule(const Expr& e, int Kind); 00157 00158 //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true) 00159 Theorem lhsEqRhsIneqn(const Expr& e, int kind); 00160 00161 Theorem zeroLeq(const Expr& e); 00162 Theorem bvConstIneqn(const Expr& e, int kind); 00163 00164 Theorem generalIneqn(const Expr& e, 00165 const Theorem& lhs_i, 00166 const Theorem& rhs_i, int kind); 00167 00168 //////////////////////////////////////////////////////////////////// 00169 // Bitblasting rules for terms 00170 //////////////////////////////////////////////////////////////////// 00171 00172 //! t[i] ==> t[i:i] = 0bin1 or NOT t[i] ==> t[i:i] = 0bin0 00173 Theorem bitExtractToExtract(const Theorem& thm); 00174 //! t[i] <=> t[i:i][0] (to use rewriter for simplifying t[i:i]) 00175 Theorem bitExtractRewrite(const Expr& x); 00176 00177 /*! \param x : input1 is bitvector constant 00178 * \param i : input2 is extracted bitposition 00179 * 00180 * \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff 00181 * \mathrm{TRUE}} \f], if bitposition has a 1; \f[ 00182 * \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if 00183 * the bitposition has a 0 00184 */ 00185 Theorem bitExtractConstant(const Expr & x, int i); 00186 00187 /*! \param x : input1 is bitvector binary concatenation 00188 * \param i : input2 is extracted bitposition 00189 * 00190 * \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]} 00191 * \f], where \f[ 0 \geq i \geq n-1 \f], another case of 00192 * boolextract over concatenation is: 00193 * \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f], 00194 * where \f[ n \geq i \geq m+n-1 \f] 00195 */ 00196 Theorem bitExtractConcatenation(const Expr & x, int i); 00197 00198 /*! \param t : input1 is bitvector binary BVMULT. x[0] must be BVCONST 00199 * \param i : input2 is extracted bitposition 00200 * 00201 * \result bitblast of BVMULT 00202 */ 00203 Theorem bitExtractConstBVMult(const Expr& t, int i); 00204 00205 /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST 00206 * \param i : input2 is extracted bitposition 00207 * 00208 * \result bitblast of BVMULT 00209 */ 00210 Theorem bitExtractBVMult(const Expr& t, int i); 00211 00212 /*! \param x : input1 is bitvector extraction [k:j] 00213 * \param i : input2 is extracted bitposition 00214 * 00215 * \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]} 00216 * \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f] 00217 */ 00218 Theorem bitExtractExtraction(const Expr & x, int i); 00219 00220 /*! \param t1 : input1 is vector of bitblasts of t, from bit i-1 to 0 00221 * \param t2 : input2 is vector of bitblasts of q, from bit i-1 to 0 00222 * \param bvPlusTerm : input3 is BVPLUS term: BVPLUS(n,t,q) 00223 * \param i : input4 is extracted bitposition 00224 * 00225 * \result The base case is: \f[ 00226 * \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]} 00227 * \f], when \f[ 0 < i \leq n-1 \f], we have \f[ 00228 * \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i] 00229 * \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated 00230 * by the addition of bits from 0 to i-1 00231 */ 00232 Theorem bitExtractBVPlus(const std::vector<Theorem>& t1, 00233 const std::vector<Theorem>& t2, 00234 const Expr& bvPlusTerm, int i); 00235 00236 Theorem bitExtractBVPlusPreComputed(const Theorem& t1_i, 00237 const Theorem& t2_i, 00238 const Expr& bvPlusTerm, 00239 int bitPos, 00240 int precomputed); 00241 00242 /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with 00243 * arity > 2 00244 * 00245 * \result : output is iff-Theorem: bvPlusTerm <==> outputTerm, 00246 * where outputTerm is an equivalent BINARY bvplus. 00247 */ 00248 Theorem bvPlusAssociativityRule(const Expr& bvPlusTerm); 00249 00250 /*! \param x : input1 is bitwise NEGATION 00251 * \param i : input2 is extracted bitposition 00252 * 00253 * \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])} 00254 * \f] 00255 */ 00256 Theorem bitExtractNot(const Expr & x, int i); 00257 00258 //! Auxiliary function for bitExtractAnd() and bitExtractOr() 00259 Theorem bitExtractBitwise(const Expr& x, int i, int kind); 00260 00261 /*! \param x : input1 is bitwise AND 00262 * \param i : input2 is extracted bitposition 00263 * 00264 * \result \f[ \frac{}{(t_{[n]} \& q_{[n]})[i] \iff (t_{[n]}[i] 00265 * \wedge q_{[n]}[i])} \f] 00266 */ 00267 Theorem bitExtractAnd(const Expr & x, int i); 00268 00269 /*! \param x : input1 is bitwise OR 00270 * \param i : input2 is extracted bitposition 00271 * 00272 * \result \f[ \frac{}{(t_{[n]} \mid q_{[n]})[i] \iff (t_{[n]}[i] 00273 * \vee q_{[n]}[i])} \f] 00274 */ 00275 Theorem bitExtractOr(const Expr & x, int i); 00276 00277 /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f] 00278 * \param i : input2 is extracted bitposition 00279 * 00280 * \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}} 00281 * \f], if 0 <= i < k. however, if k <= i < n then, result is 00282 * \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f] 00283 */ 00284 Theorem bitExtractFixedLeftShift(const Expr & x, int i); 00285 00286 Theorem bitExtractFixedRightShift(const Expr & x, int i); 00287 /*! \param e : input1 is bitvector term 00288 * \param r : input2 is extracted bitposition 00289 * 00290 * \result we check if r > bvlength(e). if yes, then return 00291 * BOOLEXTRACT(e,r) <==> FALSE; else raise soundness 00292 * exception. (Note: this rule is used in BVPLUS bitblast 00293 * function) 00294 */ 00295 Theorem zeroPaddingRule(const Expr& e, int r); 00296 00297 Theorem bitExtractSXRule(const Expr& e, int i); 00298 00299 //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors) 00300 Theorem eqConst(const Expr& e); 00301 //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits 00302 Theorem eqToBits(const Theorem& eq); 00303 //! t<<n = c @ 0bin00...00, takes e == (t<<n) 00304 Theorem leftShiftToConcat(const Expr& e); 00305 //! t<<n = c @ 0bin00...00, takes e == (t<<n) 00306 Theorem constWidthLeftShiftToConcat(const Expr& e); 00307 //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n) 00308 Theorem rightShiftToConcat(const Expr& e); 00309 //! a XOR b <=> (a & ~b) | (~a & b) 00310 Theorem rewriteXOR(const Expr& e); 00311 //! a XNOR b <=> (~a & ~b) | (a & b) 00312 Theorem rewriteXNOR(const Expr& e); 00313 //! a NAND b <=> ~(a & b) 00314 Theorem rewriteNAND(const Expr& e); 00315 //! a NOR b <=> ~(a | b) 00316 Theorem rewriteNOR(const Expr& e); 00317 //! a - b <=> a + (-b) 00318 Theorem rewriteBVSub(const Expr& e); 00319 //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS 00320 /*! If k = 2^m, return k*t = t\@0...0 */ 00321 Theorem constMultToPlus(const Expr& e); 00322 //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args) 00323 /*! where k is the size of the 0bin0...0 */ 00324 Theorem bvplusZeroConcatRule(const Expr& e); 00325 00326 00327 /////////////////////////////////////////////////////////////////// 00328 ///// Bvplus Normal Form rules 00329 /////////////////////////////////////////////////////////////////// 00330 Theorem zeroCoeffBVMult(const Expr& e); 00331 Theorem oneCoeffBVMult(const Expr& e); 00332 Theorem flipBVMult(const Expr& e); 00333 //! converts e to a bitvector of length rat 00334 Expr pad(int rat, const Expr& e); 00335 Theorem padBVPlus(const Expr& e); 00336 Theorem padBVMult(const Expr& e); 00337 Theorem bvConstMultAssocRule(const Expr& e); 00338 Theorem bvMultAssocRule(const Expr& e); 00339 Theorem bvMultDistRule(const Expr& e); 00340 Theorem flattenBVPlus(const Expr& e); 00341 Theorem combineLikeTermsRule(const Expr& e); 00342 Theorem lhsMinusRhsRule(const Expr& e); 00343 Theorem extractBVMult(const Expr& e); 00344 Theorem extractBVPlus(const Expr& e); 00345 //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j]) 00346 Theorem iteExtractRule(const Expr& e); 00347 //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2) 00348 Theorem iteBVnegRule(const Expr& e); 00349 00350 Theorem bvuminusBVConst(const Expr& e); 00351 Theorem bvuminusBVMult(const Expr& e); 00352 Theorem bvuminusBVUminus(const Expr& e); 00353 Theorem bvuminusVar(const Expr& e); 00354 Theorem bvmultBVUminus(const Expr& e); 00355 //! -t <==> ~t+1 00356 Theorem bvuminusToBVPlus(const Expr& e); 00357 //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn)) 00358 Theorem bvuminusBVPlus(const Expr& e); 00359 00360 00361 /////////////////////////////////////////////////////////////////// 00362 ///// Concatenation Normal Form rules 00363 /////////////////////////////////////////////////////////////////// 00364 00365 // Extraction rules 00366 00367 //! c1[i:j] = c (extraction from a constant bitvector) 00368 Theorem extractConst(const Expr& e); 00369 //! t[n-1:0] = t for n-bit t 00370 Theorem extractWhole(const Expr& e); 00371 //! t[i:j][k:l] = t[k+j:l+j] (eliminate double extraction) 00372 Theorem extractExtract(const Expr& e); 00373 //! (t1 @ t2)[i:j] = t1[...] @ t2[...] (push extraction through concat) 00374 Theorem extractConcat(const Expr& e); 00375 00376 //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j] 00377 Theorem extractBitwise(const Expr& e, int kind, const std::string& name); 00378 //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j] (push extraction through OR) 00379 Theorem extractAnd(const Expr& e); 00380 //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j] (push extraction through AND) 00381 Theorem extractOr(const Expr& e); 00382 //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG) 00383 Theorem extractNeg(const Expr& e); 00384 00385 // Negation rules 00386 00387 //! ~c1 = c (bit-wise negation of a constant bitvector) 00388 Theorem negConst(const Expr& e); 00389 //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat 00390 Theorem negConcat(const Expr& e); 00391 //! ~(~t) = t -- eliminate double negation 00392 Theorem negNeg(const Expr& e); 00393 //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws 00394 Theorem negBVand(const Expr& e); 00395 //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws 00396 Theorem negBVor(const Expr& e); 00397 //! ~(t1 xor t2) = ~t1 xor t2 00398 Theorem negBVxor(const Expr& e); 00399 //! ~(t1 xnor t2) = t1 xor t2 00400 Theorem negBVxnor(const Expr& e); 00401 00402 // Bit-wise AND rules 00403 //! Auxiliary method for andConst() and orConst() 00404 Theorem bitwiseConst(const Expr& e, const std::vector<int>& idxs, 00405 bool isAnd); 00406 //! Auxiliary method for andConcat() and orConcat() 00407 Theorem bitwiseConcat(const Expr& e, int idx, bool isAnd); 00408 //! Auxiliary method for andFlatten() and orFlatten() 00409 Theorem bitwiseFlatten(const Expr& e, bool isAnd); 00410 00411 //! c1&c2&t = c&t -- compute bit-wise AND of constant bitvector arguments 00412 /*!\param e is the bit-wise AND expression; 00413 * 00414 * \param idxs are the indices of the constant bitvectors. There 00415 * must be at least constant expressions in this rule. 00416 * 00417 * \return Theorem(e==e'), where e' is either a constant 00418 * bitvector, or is a bit-wise AND with a single constant 00419 * bitvector in e'[0]. 00420 */ 00421 Theorem andConst(const Expr& e, const std::vector<int>& idxs); 00422 //! 0bin0...0 & t = 0bin0...0 -- bit-wise AND with zero bitvector 00423 /*! \param e is the bit-wise AND expr 00424 * \param idx is the index of the zero bitvector 00425 */ 00426 Theorem andZero(const Expr& e, int idx); 00427 Theorem andOne(const Expr& e, const std::vector<int> idxs); 00428 //! ... & (t1\@...\@tk) & ... = (...& t1 &...)\@...\@(...& tk &...) 00429 /*! 00430 * Lifts concatenation to the top of bit-wise AND. Takes the 00431 * bit-wise AND expression 'e' and the index 'i' of the 00432 * concatenation. 00433 */ 00434 Theorem andConcat(const Expr& e, int idx); 00435 //! (t1 & (t2 & t3) & t4) = t1 & t2 & t3 & t4 -- flatten bit-wise AND 00436 /*! Also reorders the terms according to a fixed total ordering */ 00437 Theorem andFlatten(const Expr& e); 00438 00439 // Bit-wise OR rules 00440 00441 //! c1|c2|t = c|t -- compute bit-wise OR of constant bitvector arguments 00442 /*!\param e is the bit-wise OR expression; 00443 * 00444 * \param idxs are the indices of the constant bitvectors. There 00445 * must be at least constant expressions in this rule. 00446 * 00447 * \return Theorem(e==e'), where e' is either a constant 00448 * bitvector, or is a bit-wise OR with a single constant 00449 * bitvector in e'[0]. 00450 */ 00451 Theorem orConst(const Expr& e, const std::vector<int>& idxs); 00452 //! 0bin1...1 | t = 0bin1...1 -- bit-wise OR with bitvector of 1's 00453 /*! \param e is the bit-wise OR expr 00454 * \param idx is the index of the bitvector of 1's 00455 */ 00456 Theorem orOne(const Expr& e, int idx); 00457 Theorem orZero(const Expr& e, const std::vector<int> idxs); 00458 //! ... | (t1\@...\@tk) | ... = (...| t1 |...)\@...\@(...| tk |...) 00459 /*! 00460 * Lifts concatenation to the top of bit-wise OR. Takes the 00461 * bit-wise OR expression 'e' and the index 'i' of the 00462 * concatenation. 00463 */ 00464 Theorem orConcat(const Expr& e, int idx); 00465 //! (t1 | (t2 | t3) | t4) = t1 | t2 | t3 | t4 -- flatten bit-wise OR 00466 /*! Also reorders the terms according to a fixed total ordering */ 00467 Theorem orFlatten(const Expr& e); 00468 00469 00470 /*! checks if e is already present in likeTerms without conflicts. 00471 * if yes return 1, else{ if conflict return -1 else return 0 } 00472 * we have conflict if 00473 * 1. the kind of e is BVNEG, 00474 * and e[0] is already present in likeTerms 00475 * 2. ~e is present in likeTerms already 00476 */ 00477 int sameKidCheck(const Expr& e, ExprMap<int>& likeTerms); 00478 00479 // Concatenation rules 00480 00481 //! c1\@c2\@...\@cn = c (concatenation of constant bitvectors) 00482 Theorem concatConst(const Expr& e); 00483 //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w 00484 Theorem concatFlatten(const Expr& e); 00485 //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0] 00486 Theorem concatMergeExtract(const Expr& e); 00487 00488 /////////////////////////////////////////////////////////////////// 00489 ///// Modulo arithmetic rules 00490 /////////////////////////////////////////////////////////////////// 00491 00492 //! BVPLUS(n, c1,c2,...,cn) = c (bit-vector plus of constant bitvectors) 00493 Theorem bvplusConst(const Expr& e); 00494 /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant 00495 * bitvector by a non-negative constant) */ 00496 Theorem bvmultConst(const Expr& e); 00497 00498 /////////////////////////////////////////////////////////////////// 00499 ///// Type predicate rules 00500 /////////////////////////////////////////////////////////////////// 00501 00502 //! |- t=0 OR t=1 for any 1-bit bitvector t 00503 Theorem typePredBit(const Expr& e); 00504 00505 //! Expand the type predicate wrapper (compute the actual type predicate) 00506 Theorem expandTypePred(const Theorem& tp); 00507 00508 //////////////////////////////////////////////////////////////////// 00509 // Helper functions 00510 //////////////////////////////////////////////////////////////////// 00511 //! Create Expr from Rational (for convenience) 00512 Expr rat(const Rational& r) { return d_em->newRatExpr(r); } 00513 /*! \param t1BitExtractThms : input1 is vector of bitblasts of t1, 00514 * from bit i-1 to 0 00515 * 00516 * \param t2BitExtractThms : input2 is vector of bitblasts of t2, 00517 * from bit i-1 to 0 00518 * 00519 * \param bitPos : input3 is extracted * bitposition 00520 * 00521 * \result is the expression \f$t1[0] \wedge t2[0]\f$ if 00522 * bitPos=0. this function is recursive; if bitPos > 0 then the 00523 * output expression is 00524 * \f[ (t1[i-1] \wedge t2[i-1]) 00525 * \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1)) 00526 * \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1)) 00527 * \f] 00528 */ 00529 Expr computeCarry(const std::vector<Theorem>& t1BitExtractThms, 00530 const std::vector<Theorem>& t2BitExtractThms, 00531 int bitPos); 00532 00533 Expr computeCarryPreComputed(const Theorem& t1_i, 00534 const Theorem& t2_i, 00535 int bitPos, 00536 int precomputedFlag); 00537 00538 //ExprMap<Expr> carryCache(void); 00539 }; // end of class BitvectorTheoremProducer 00540 } // end of namespace CVC3 00541 00542 #endif