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   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

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1