CVC3

bitvector_theorem_producer.h

Go to the documentation of this file.
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 
00082     void getPlusTerms(const Expr& e, Rational& known_term, ExprMap<Rational>& sumHashMap);
00083     Expr buildPlusTerm(int bv_size, Rational& known_term, ExprMap<Rational>& sumHashMap);
00084     Expr chopConcat(int bv_size, Rational c, std::vector<Expr>& concatKids);
00085     bool okToSplit(const Expr& e);
00086 
00087   public:
00088     //! Constructor: constructs an instance of bitvector DP
00089     BitvectorTheoremProducer(TheoryBitvector* theoryBitvector);
00090     ~BitvectorTheoremProducer() {}
00091 
00092     //ExprMap<Expr> d_bvPlusCarryCacheLeftBV;
00093     //ExprMap<Expr> d_bvPlusCarryCacheRightBV;
00094 
00095     ////////////////////////////////////////////////////////////////////
00096     // Partial Canonization rules
00097     ////////////////////////////////////////////////////////////////////
00098 
00099     ////////////////////////////////////////////////////////////////////
00100     // Bitblasting rules for equations
00101     ////////////////////////////////////////////////////////////////////
00102 
00103     /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false
00104      *
00105      *  \result (e1=e2)<=>false
00106      */
00107     Theorem bitvectorFalseRule(const Theorem& thm);
00108 
00109     /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true
00110      *
00111      *  \result (e1!=e2)<=>true
00112      */
00113     Theorem bitvectorTrueRule(const Theorem& thm);
00114 
00115     /*! \param e input equation: e1=e2 over bitvector terms
00116      *  \param f formula over the bits of bitvector variables in e:
00117      *
00118      *  \result \f[\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i]
00119      *  \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a
00120      *  formula over variables in \f[ e_{1}, e_{2} \f] respectively
00121      */
00122     Theorem bitBlastEqnRule(const Expr& e, const Expr& f);
00123 
00124     /*! \param e : input disequality: e1 != e2 over bitvector terms
00125      *  \param f : formula over the bits of bitvector variables in e:
00126      *
00127      *  \result \f[\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i])
00128      *  \iff e_{2}[i]) } \f] where each of \f[ e_{1}[i], e{2}[i] \f] denotes a
00129      *  formula over variables in \f[ e_{1}, e_{2} \f] respectively
00130      */
00131     Theorem bitBlastDisEqnRule(const Theorem& e, const Expr& f);
00132 
00133 
00134     ////////////////////////////////////////////////////////////////////
00135     // Bitblasting and rewrite rules for Inequations
00136     ////////////////////////////////////////////////////////////////////
00137 
00138     //! sign extend the input SX(e) appropriately
00139     Theorem signExtendRule(const Expr& e);
00140 
00141     //! Pad the kids of BVLT/BVLE to make their length equal
00142     Theorem padBVLTRule(const Expr& e, int len);
00143 
00144     //! Sign Extend the kids of BVSLT/BVSLE to make their length equal
00145     Theorem padBVSLTRule(const Expr& e, int len);
00146 
00147     /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
00148      *  e0 and e1 are constants. If they are constants then optimizations
00149      *  are done, otherwise the following rule is implemented.
00150      *
00151      *  e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR
00152      *                   (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR
00153      *                   (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
00154      */
00155     Theorem signBVLTRule(const Expr& e,
00156        const Theorem& topBit0,
00157        const Theorem& topBit1);
00158 
00159     /*! NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
00160      */
00161     Theorem notBVEQ1Rule(const Expr& e);
00162 
00163     /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]),
00164      *  NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
00165      */
00166     Theorem notBVLTRule(const Expr& e);
00167 
00168     //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
00169     Theorem lhsEqRhsIneqn(const Expr& e, int kind);
00170 
00171     Theorem zeroLeq(const Expr& e);
00172     Theorem bvConstIneqn(const Expr& e, int kind);
00173 
00174     Theorem generalIneqn(const Expr& e,
00175        const Theorem& lhs_i,
00176        const Theorem& rhs_i, int kind);
00177 
00178     ////////////////////////////////////////////////////////////////////
00179     // Bitblasting rules for terms
00180     ////////////////////////////////////////////////////////////////////
00181 
00182     // Input: |- BOOLEXTRACT(a,0) <=> bc_0, ... BOOLEXTRACT(a,n-1) <=> bc_(n-1)
00183     // where each bc_0 is TRUE or FALSE
00184     // Output: |- a = c
00185     // where c is an n-bit constant made from the values bc_0..bc_(n-1)
00186     Theorem bitExtractAllToConstEq(std::vector<Theorem>& thms);
00187     //! t[i] ==> t[i:i] = 0bin1   or    NOT t[i] ==> t[i:i] = 0bin0
00188     Theorem bitExtractToExtract(const Theorem& thm);
00189     //! t[i] <=> t[i:i][0]   (to use rewriter for simplifying t[i:i])
00190     Theorem bitExtractRewrite(const Expr& x);
00191 
00192     /*! \param x : input1 is bitvector constant
00193      *  \param i : input2 is extracted bitposition
00194      *
00195      *  \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff
00196      *  \mathrm{TRUE}} \f], if bitposition has a 1; \f[
00197      *  \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if
00198      *  the bitposition has a 0
00199      */
00200     Theorem bitExtractConstant(const Expr & x, int i);
00201 
00202     /*! \param x : input1 is bitvector binary concatenation
00203      *  \param i : input2 is extracted bitposition
00204      *
00205      *  \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}
00206      *  \f], where \f[ 0 \geq i \geq n-1 \f], another case of
00207      *  boolextract over concatenation is:
00208      *  \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f],
00209      *  where \f[ n \geq i \geq m+n-1 \f]
00210      */
00211     Theorem bitExtractConcatenation(const Expr & x, int i);
00212 
00213     /*! \param t : input1 is bitvector binary BVMULT. x[0] must be BVCONST
00214      *  \param i : input2 is extracted bitposition
00215      *
00216      *  \result bitblast of BVMULT
00217      */
00218     Theorem bitExtractConstBVMult(const Expr& t, int i);
00219 
00220     /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST
00221      *  \param i : input2 is extracted bitposition
00222      *
00223      *  \result bitblast of BVMULT
00224      */
00225     Theorem bitExtractBVMult(const Expr& t, int i);
00226 
00227     /*! \param x : input1 is bitvector extraction [k:j]
00228      *  \param i : input2 is extracted bitposition
00229      *
00230      *  \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}
00231      *  \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f]
00232      */
00233     Theorem bitExtractExtraction(const Expr & x, int i);
00234 
00235     /*! \param t1 : input1 is vector of bitblasts of t, from bit i-1 to 0
00236      *  \param t2 : input2 is vector of bitblasts of q, from bit i-1 to 0
00237      *  \param bvPlusTerm : input3 is BVPLUS term: BVPLUS(n,t,q)
00238      *  \param i  : input4 is extracted bitposition
00239      *
00240      *  \result The base case is: \f[
00241      *  \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}
00242      *  \f], when \f[ 0 < i \leq n-1 \f], we have \f[
00243      *  \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i]
00244      *  \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated
00245      *  by the addition of bits from 0 to i-1
00246      */
00247     Theorem bitExtractBVPlus(const std::vector<Theorem>& t1,
00248            const std::vector<Theorem>& t2,
00249            const Expr& bvPlusTerm, int i);
00250 
00251     Theorem bitExtractBVPlusPreComputed(const Theorem& t1_i,
00252           const Theorem& t2_i,
00253           const Expr& bvPlusTerm,
00254           int bitPos,
00255           int precomputed);
00256 
00257     /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with
00258      *  arity > 2
00259      *
00260      *  \result : output is iff-Theorem: bvPlusTerm <==> outputTerm,
00261      *  where outputTerm is an equivalent BINARY bvplus.
00262      */
00263     Theorem bvPlusAssociativityRule(const Expr& bvPlusTerm);
00264 
00265     /*! \param x : input1 is bitwise NEGATION
00266      *  \param i : input2 is extracted bitposition
00267      *
00268      *  \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}
00269      *  \f]
00270      */
00271     Theorem bitExtractNot(const Expr & x, int i);
00272 
00273     //! Extract from bitwise AND, OR, or XOR
00274     Theorem bitExtractBitwise(const Expr& x, int i, int kind);
00275 
00276     /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f]
00277      *  \param i : input2 is extracted bitposition
00278      *
00279      *  \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}
00280      *  \f], if 0 <= i < k. however, if k <= i < n then, result is
00281      *  \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f]
00282      */
00283     Theorem bitExtractFixedLeftShift(const Expr & x, int i);
00284 
00285     Theorem bitExtractFixedRightShift(const Expr & x, int i);
00286 
00287     // BOOLEXTRACT(bvshl(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00288     //                               ((s = 1) AND BOOLEXTRACT(t,i-1)) OR ...
00289     //                               ((s = i) AND BOOLEXTRACT(t,0))
00290     Theorem bitExtractBVSHL(const Expr & x, int i);
00291 
00292     // BOOLEXTRACT(bvlshr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00293     //                                ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
00294     //                                ((s = n-1-i) AND BOOLEXTRACT(t,n-1))
00295     Theorem bitExtractBVLSHR(const Expr & x, int i);
00296 
00297     // BOOLEXTRACT(bvashr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00298     //                                ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
00299     //                                ((s >= n-1-i) AND BOOLEXTRACT(t,n-1))
00300     Theorem bitExtractBVASHR(const Expr & x, int i);
00301 
00302     /*! \param e : input1 is bitvector term
00303      *  \param r : input2 is extracted bitposition
00304      *
00305      *  \result we check if r > bvlength(e). if yes, then return
00306      *  BOOLEXTRACT(e,r) <==> FALSE; else raise soundness
00307      *  exception. (Note: this rule is used in BVPLUS bitblast
00308      *  function)
00309      */
00310     Theorem zeroPaddingRule(const Expr& e, int r);
00311 
00312     Theorem bitExtractSXRule(const Expr& e, int i);
00313 
00314     //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
00315     Theorem eqConst(const Expr& e);
00316     //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
00317     Theorem eqToBits(const Theorem& eq);
00318     //! t<<n = c @ 0bin00...00, takes e == (t<<n)
00319     Theorem leftShiftToConcat(const Expr& e);
00320     //! t<<n = c @ 0bin00...00, takes e == (t<<n)
00321     Theorem constWidthLeftShiftToConcat(const Expr& e);
00322     //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
00323     Theorem rightShiftToConcat(const Expr& e);
00324     //! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
00325     Theorem bvshlToConcat(const Expr& e);
00326     //! BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
00327     Theorem bvshlSplit(const Expr& e);
00328     //! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
00329     Theorem bvlshrToConcat(const Expr& e);
00330     //! All shifts over a 0 constant = 0
00331     Theorem bvShiftZero(const Expr& e);
00332     //! BVASHR(t,c) = SX(t[n-1,c], n-1)
00333     Theorem bvashrToConcat(const Expr& e);
00334     //! a XNOR b <=> (~a & ~b) | (a & b)
00335     Theorem rewriteXNOR(const Expr& e);
00336     //! a NAND b <=> ~(a & b)
00337     Theorem rewriteNAND(const Expr& e);
00338     //! a NOR b <=> ~(a | b)
00339     Theorem rewriteNOR(const Expr& e);
00340     //! BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
00341     Theorem rewriteBVCOMP(const Expr& e);
00342     //! a - b <=> a + (-b)
00343     Theorem rewriteBVSub(const Expr& e);
00344     //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
00345     /*! If k = 2^m, return k*t = t\@0...0 */
00346     Theorem constMultToPlus(const Expr& e);
00347     //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
00348     /*! where k is the size of the 0bin0...0 */
00349     Theorem bvplusZeroConcatRule(const Expr& e);
00350 
00351 
00352     ///////////////////////////////////////////////////////////////////
00353     /////  Bvplus Normal Form rules
00354     ///////////////////////////////////////////////////////////////////
00355     Theorem zeroCoeffBVMult(const Expr& e);
00356     Theorem oneCoeffBVMult(const Expr& e);
00357     Theorem flipBVMult(const Expr& e);
00358     //! converts e to a bitvector of length rat
00359     Expr pad(int rat, const Expr& e);
00360     Theorem padBVPlus(const Expr& e);
00361     Theorem padBVMult(const Expr& e);
00362     Theorem bvConstMultAssocRule(const Expr& e);
00363     Theorem bvMultAssocRule(const Expr& e);
00364     Theorem bvMultDistRule(const Expr& e);
00365     Theorem flattenBVPlus(const Expr& e);
00366     Theorem combineLikeTermsRule(const Expr& e);
00367     Theorem lhsMinusRhsRule(const Expr& e);
00368     Theorem extractBVMult(const Expr& e);
00369     Theorem extractBVPlus(const Expr& e);
00370     //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
00371     Theorem iteExtractRule(const Expr& e);
00372     //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2)
00373     Theorem iteBVnegRule(const Expr& e);
00374 
00375     Theorem bvuminusBVConst(const Expr& e);
00376     Theorem bvuminusBVMult(const Expr& e);
00377     Theorem bvuminusBVUminus(const Expr& e);
00378     Theorem bvuminusVar(const Expr& e);
00379     Theorem bvmultBVUminus(const Expr& e);
00380     //! -t <==> ~t+1
00381     Theorem bvuminusToBVPlus(const Expr& e);
00382     //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
00383     Theorem bvuminusBVPlus(const Expr& e);
00384 
00385 
00386     ///////////////////////////////////////////////////////////////////
00387     /////  Concatenation Normal Form rules
00388     ///////////////////////////////////////////////////////////////////
00389 
00390     // Extraction rules
00391 
00392     //! c1[i:j] = c  (extraction from a constant bitvector)
00393     Theorem extractConst(const Expr& e);
00394     //! t[n-1:0] = t  for n-bit t
00395     Theorem extractWhole(const Expr& e);
00396     //! t[i:j][k:l] = t[k+j:l+j]  (eliminate double extraction)
00397     Theorem extractExtract(const Expr& e);
00398     //! (t1 @ t2)[i:j] = t1[...] @ t2[...]  (push extraction through concat)
00399     Theorem extractConcat(const Expr& e);
00400 
00401     //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]
00402     Theorem extractBitwise(const Expr& e, int kind, const std::string& name);
00403     //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j]  (push extraction through OR)
00404     Theorem extractAnd(const Expr& e);
00405     //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j]  (push extraction through AND)
00406     Theorem extractOr(const Expr& e);
00407     //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
00408     Theorem extractNeg(const Expr& e);
00409 
00410     // Negation rules
00411 
00412     //! ~c1 = c  (bit-wise negation of a constant bitvector)
00413     Theorem negConst(const Expr& e);
00414     //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
00415     Theorem negConcat(const Expr& e);
00416     //! ~(~t) = t  -- eliminate double negation
00417     Theorem negNeg(const Expr& e);
00418     //! ~t = -1*t + 1 -- eliminate negation
00419     Theorem negElim(const Expr& e);
00420     //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
00421     Theorem negBVand(const Expr& e);
00422     //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
00423     Theorem negBVor(const Expr& e);
00424     //! ~(t1 xor t2) = ~t1 xor t2
00425     Theorem negBVxor(const Expr& e);
00426     //! ~(t1 xnor t2) = t1 xor t2
00427     Theorem negBVxnor(const Expr& e);
00428 
00429     // Bit-wise rules
00430     //! Combine constants in bitwise AND, OR, XOR
00431     Theorem bitwiseConst(const Expr& e, const std::vector<int>& idxs,
00432        int kind);
00433     //! Lifts concatenation above bitwise operators.
00434     Theorem bitwiseConcat(const Expr& e, int kind);
00435     //! Flatten bitwise operation
00436     Theorem bitwiseFlatten(const Expr& e, int kind);
00437     //! Simplify bitwise operator containing a constant child
00438     /*! \param e is the bit-wise expr
00439      *  \param idx is the index of the constant bitvector
00440      *  \param kind is the kind of e
00441      */
00442     Theorem bitwiseConstElim(const Expr& e, int idx, int kind);
00443 
00444     /*! checks if e is already present in likeTerms without conflicts.
00445      *  if yes return 1, else{ if conflict return -1 else return 0 }
00446      *  we have conflict if
00447      *          1. the kind of e is BVNEG,
00448      *                 and e[0] is already present in likeTerms
00449      *          2. ~e is present in likeTerms already
00450      */
00451     int sameKidCheck(const Expr& e, ExprMap<int>& likeTerms);
00452 
00453     // Concatenation rules
00454 
00455     //! c1\@c2\@...\@cn = c  (concatenation of constant bitvectors)
00456     Theorem concatConst(const Expr& e);
00457     //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
00458     Theorem concatFlatten(const Expr& e);
00459     //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
00460     Theorem concatMergeExtract(const Expr& e);
00461 
00462     ///////////////////////////////////////////////////////////////////
00463     /////  Modulo arithmetic rules
00464     ///////////////////////////////////////////////////////////////////
00465 
00466     //! BVPLUS(n, c1,c2,...,cn) = c  (bit-vector plus of constant bitvectors)
00467     Theorem bvplusConst(const Expr& e);
00468     /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant
00469      *  bitvector by a non-negative constant) */
00470     Theorem bvmultConst(const Expr& e);
00471 
00472     ///////////////////////////////////////////////////////////////////
00473     /////  Type predicate rules
00474     ///////////////////////////////////////////////////////////////////
00475 
00476     //! |- t=0 OR t=1  for any 1-bit bitvector t
00477     Theorem typePredBit(const Expr& e);
00478 
00479     //! Expand the type predicate wrapper (compute the actual type predicate)
00480     Theorem expandTypePred(const Theorem& tp);
00481 
00482     ////////////////////////////////////////////////////////////////////
00483     // Helper functions
00484     ////////////////////////////////////////////////////////////////////
00485     //! Create Expr from Rational (for convenience)
00486     Expr rat(const Rational& r) { return d_em->newRatExpr(r); }
00487     /*! \param t1BitExtractThms : input1 is vector of bitblasts of t1,
00488      *  from bit i-1 to 0
00489      *
00490      *  \param t2BitExtractThms : input2 is vector of bitblasts of t2,
00491      *  from bit i-1 to 0
00492      *
00493      *  \param bitPos : input3 is extracted * bitposition
00494      *
00495      *  \result is the expression \f$t1[0] \wedge t2[0]\f$ if
00496      *  bitPos=0. this function is recursive; if bitPos > 0 then the
00497      *  output expression is
00498      *  \f[ (t1[i-1] \wedge t2[i-1])
00499      *     \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1))
00500      *     \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1))
00501      *  \f]
00502      */
00503     Expr computeCarry(const std::vector<Theorem>& t1BitExtractThms,
00504           const std::vector<Theorem>& t2BitExtractThms,
00505           int bitPos);
00506 
00507     Expr computeCarryPreComputed(const Theorem& t1_i,
00508          const Theorem& t2_i,
00509          int bitPos,
00510          int precomputedFlag);
00511 
00512     /*Beginning of Lorenzo PLatania's methods*/
00513 
00514     //    virtual Theorem multiply_coeff( Rational mult_inv, const Expr& e);
00515     //! isolate a variable with coefficient = 1 on the Lhs of an
00516     //equality expression
00517     virtual Theorem isolate_var(const Expr& e);
00518 
00519     // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
00520     // where n = BVSize(b), a != 0
00521     virtual Theorem liftConcatBVMult(const Expr& e);
00522 
00523     //! canonize BVMult expressions in order to get one coefficient
00524     //multiplying the variable(s) in the expression
00525     virtual Theorem canonBVMult( const Expr& e );
00526 
00527     // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
00528     // where n = BVSize(b)
00529     virtual Theorem liftConcatBVPlus(const Expr& e);
00530 
00531     //! canonize BVPlus expressions in order to get just one
00532     //coefficient multiplying each variable in the expression
00533     virtual Theorem canonBVPlus( const Expr& e );
00534 
00535     //! canonize BVMinus expressions: push the minus to the leafs in
00536     //BVPLUS expr; simplify minus in BVMULT and BVMINUS expr
00537     virtual Theorem canonBVUMinus( const Expr& e );
00538 
00539     // Input: t[hi:lo] = rhs
00540     // if t appears as leaf in rhs, then:
00541     //    t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
00542     // else
00543     //    t[hi:lo] = rhs |- Exists x,y,z. (t = x @ rhs @ z AND y = rhs), solvedForm = true
00544     virtual Theorem processExtract(const Theorem& e, bool& solvedForm);
00545 
00546     // normalizes equation
00547     virtual Theorem canonBVEQ( const Expr& e, int maxEffort = 3 );
00548 
00549     //! apply the distributive rule on the BVMULT expression e
00550     virtual Theorem distributive_rule( const Expr& e );
00551     //    virtual Theorem BVMultConstTerm( const Expr& e1, const Expr& e2);
00552     // recursively reorder subterms in a BVMULT term
00553     virtual Theorem BVMult_order_subterms( const Expr& e);
00554 
00555     // rewrites the equation in the form 0 = Expr
00556     // this is needed for TheoryBitvector::solve
00557     virtual Theorem MarkNonSolvableEq( const Expr& e);
00558     /*End of Lorenzo PLatania's methods*/
00559 
00560     // rewrite BVZEROEXTEND into CONCAT
00561     virtual Theorem zeroExtendRule(const Expr& e);
00562 
00563     // rewrite BVREPEAT into CONCAT
00564     virtual Theorem repeatRule(const Expr& e);
00565 
00566     // rewrite BVROTL into CONCAT
00567     virtual Theorem rotlRule(const Expr& e);
00568     // rewrite BVROTR into CONCAT
00569     virtual Theorem rotrRule(const Expr& e);
00570 
00571     // Dejan: Division rewrites
00572 
00573     /**
00574      * Divide a with b unsigned and return the bit-vector constant result
00575      */
00576     virtual Theorem bvUDivConst(const Expr& divExpr);
00577 
00578     /**
00579      * Rewrite x/y to
00580      * \exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m & 0 <= m < y)
00581      */
00582     virtual Theorem bvUDivTheorem(const Expr& divExpr);
00583 
00584     /**
00585      * Compute the remainder
00586      */
00587     virtual Theorem bvURemConst(const Expr& remExpr);
00588 
00589     /**
00590      * Rewrite a%b in terms of a/b, i.e. a - a/b
00591      */
00592     virtual Theorem bvURemRewrite(const Expr& remExpr);
00593 
00594     /**
00595      * Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits.
00596      * The resulting output bits will be in the vector output_bits. The return value
00597      * is a theorem saying there is no overflow for this multiplication. (TODO, it's
00598      * just an empty theorem for now).
00599      */
00600     virtual Theorem bitblastBVMult(const std::vector<Theorem>& a_bits,
00601                                const std::vector<Theorem>& b_bits,
00602                                const Expr& a_times_b,
00603                                std::vector<Theorem>& output_bits);
00604 
00605     /**
00606      * Bit-blast the sum a_plus_b given the bits in a_bits and b_bits.
00607      * The resulting output bits will be in the vector output_bits. The return value
00608      * is a theorem saying there is no overflow for this sum. (TODO, it's
00609      * just an empty theorem for now).
00610      */
00611     virtual Theorem bitblastBVPlus(const std::vector<Theorem>& a_bits,
00612                                const std::vector<Theorem>& b_bits,
00613                                const Expr& a_plus_b,
00614                                std::vector<Theorem>& output_bits);
00615 
00616     /**
00617      * Rewrite the signed divide in terms of the unsigned one.
00618      */
00619     virtual Theorem bvSDivRewrite(const Expr& sDivExpr);
00620 
00621     /**
00622      * Rewrite the signed remainder in terms of the unsigned one.
00623      */
00624     virtual Theorem bvSRemRewrite(const Expr& sRemExpr);
00625 
00626     /**
00627      * Rewrite the signed mod in terms of the unsigned one.
00628      */
00629     virtual Theorem bvSModRewrite(const Expr& sModExpr);
00630 
00631     /**
00632      * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
00633      * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
00634      */
00635     virtual Theorem zeroBVOR(const Expr& orEqZero);
00636 
00637     /**
00638      * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
00639      * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
00640      */
00641     virtual Theorem oneBVAND(const Expr& andEqOne);
00642 
00643     /**
00644      * Equalities over constants go to true/false.
00645      */
00646     virtual Theorem constEq(const Expr& eq);
00647 
00648     /**
00649      * Returns true if equation is of the form x[i:j] = x[k:l], where the
00650      * extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
00651      */
00652     bool solveExtractOverlapApplies(const Expr& eq);
00653 
00654     /**
00655      * Returns the theorem that simplifies the equality of two overlapping
00656      * extracts over the same term.
00657      */
00658     Theorem solveExtractOverlap(const Expr& eq);
00659 
00660 
00661 }; // end of class BitvectorTheoremProducer
00662 } // end of name-space CVC3
00663 
00664 
00665 #endif
00666