CVC3

# bitvector_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file bitvector_proof_rules.h
00004  * \brief Arithmetic proof rules
00005  *
00006  * Author: Vijay Ganesh.
00007  *
00008  * Created:Wed May  5 15:47: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_proof_rules_h_
00023 #define _cvc3__bitvector_proof_rules_h_
00024
00025 #include <string>
00026 #include <vector>
00027
00028 namespace CVC3 {
00029
00030   class Expr;
00031   class Theorem;
00032
00033   class BitvectorProofRules {
00034   public:
00035     // Destructor
00036     virtual ~BitvectorProofRules() { }
00037
00038     ////////////////////////////////////////////////////////////////////
00039     // Bitblasting rules for equations
00040     ////////////////////////////////////////////////////////////////////
00041
00042     /*! \param thm input theorem: (e1[i]<=>e2[i])<=>false
00043      *
00044      *  \result (e1=e2)<=>false
00045      */
00046     virtual Theorem bitvectorFalseRule(const Theorem& thm) = 0;
00047
00048     /*! \param thm input theorem: (~e1[i]<=>e2[i])<=>true
00049      *
00050      *  \result (e1!=e2)<=>true
00051      */
00052     virtual Theorem bitvectorTrueRule(const Theorem& thm) = 0;
00053
00054
00055     //! t1=t2 ==> AND_i(t1[i:i] = t2[i:i])
00056     /*!
00057      * \param e is a Expr(t1=t2)
00058      *
00059      * \param f is the resulting expression AND_i(t1[i:i] = t2[i:i])
00060      * is passed to the rule for efficiency.
00061      */
00062     virtual Theorem bitBlastEqnRule(const Expr& e, const Expr& f) = 0;
00063     //! t1/=t2 ==> OR_i(NOT t1[i]<=>t2[i])
00064     /*!
00065      * \param e is a Theorem(t1/=t2)
00066      *
00067      * \param f is the resulting expression OR_i(NOT t1[i]<=>t2[i]),
00068      * passed to the rule for efficiency.
00069      */
00070     virtual Theorem bitBlastDisEqnRule(const Theorem& e, const Expr& f) = 0;
00071
00072
00073     ////////////////////////////////////////////////////////////////////
00074     // Bitblasting and rewrite rules for Inequations
00075     ////////////////////////////////////////////////////////////////////
00076
00077     //! sign extend the input SX(e) appropriately
00078     virtual Theorem signExtendRule(const Expr& e) = 0;
00079
00080     //! Pad the kids of BVLT/BVLE to make their length equal
00081     virtual Theorem padBVLTRule(const Expr& e, int len) = 0;
00082
00083     //! Sign Extend the kids of BVSLT/BVSLE to make their length equal
00084     virtual Theorem padBVSLTRule(const Expr& e, int len) = 0;
00085
00086     /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
00087      *  e0 and e1 are constants. If they are constants then optimizations
00088      *  are done, otherwise the following rule is implemented.
00089      *
00090      *  e0 <=(s) e1 <==> (e0[n-1] AND NOT e1[n-1]) OR
00091      *                   (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR
00092      *                   (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
00093      */
00094     virtual Theorem signBVLTRule(const Expr& e,
00095          const Theorem& topBit0,
00096          const Theorem& topBit1) = 0;
00097
00098     /*! NOT(e[0][0] = e[0][1]) <==> e[0][0] = ~e[0][1]
00099      */
00100     virtual Theorem notBVEQ1Rule(const Expr& e) = 0;
00101
00102     /*! NOT(e[0][0] < e[0][1]) <==> (e[0][1] <= e[0][0]),
00103      *  NOT(e[0][0] <= e[0][1]) <==> (e[0][1] < e[0][0])
00104      */
00105     virtual Theorem notBVLTRule(const Expr& e) = 0;
00106
00107     //! if(lhs==rhs) then we have (lhs < rhs <==> false),(lhs <= rhs <==> true)
00108     virtual Theorem lhsEqRhsIneqn(const Expr& e, int kind) = 0;
00109
00110
00111     virtual Theorem zeroLeq(const Expr& e) = 0;
00112     virtual Theorem bvConstIneqn(const Expr& e, int kind) = 0;
00113
00114     virtual Theorem generalIneqn(const Expr& e,
00115          const Theorem& e0,
00116          const Theorem& e1, int kind) = 0;
00117
00118
00119     ////////////////////////////////////////////////////////////////////
00120     // Bitblast rules for terms
00121     ////////////////////////////////////////////////////////////////////
00122
00123     // Input: |- BOOLEXTRACT(a,0) <=> bc_0, ... BOOLEXTRACT(a,n-1) <=> bc_(n-1)
00124     // where each bc_0 is TRUE or FALSE
00125     // Output: |- a = c
00126     // where c is an n-bit constant made from the values bc_0..bc_(n-1)
00127     virtual Theorem bitExtractAllToConstEq(std::vector<Theorem>& thms) = 0;
00128
00129     //! t[i] ==> t[i:i] = 0bin1   or    NOT t[i] ==> t[i:i] = 0bin0
00130     /*! \param thm is a Theorem(t[i]) or Theorem(NOT t[i]), where t[i]
00131      * is BOOLEXTRACT(t, i).
00132      */
00133     virtual Theorem bitExtractToExtract(const Theorem& thm) = 0;
00134
00135     //! t[i] <=> t[i:i][0]   (to use rewriter for simplifying t[i:i])
00136     virtual Theorem bitExtractRewrite(const Expr& x) = 0;
00137
00138     /*! \param x is bitvector constant
00139      *  \param i is extracted bitposition
00140      *
00141      *  \result \f[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff
00142      *  \mathrm{TRUE}} \f], if bitposition has a 1; \f[
00143      *  \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \f], if
00144      *  the bitposition has a 0
00145      */
00146     virtual Theorem bitExtractConstant(const Expr & x, int i)= 0;
00147
00148     /*! \param x is bitvector binary concatenation
00149      *  \param i is extracted bitposition
00150      *
00151      *  \result \f[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]}
00152      *  \f], where \f[ 0 \geq i \geq n-1 \f], another case of
00153      *  boolextract over concatenation is:
00154      *  \f[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \f],
00155      *  where \f[ n \geq i \geq m+n-1 \f]
00156      */
00157     virtual Theorem bitExtractConcatenation(const Expr & x,
00158               int i)= 0;
00159
00160     /*! \param t is bitvector binary BVMULT. x[0] must be BVCONST
00161      *  \param i is extracted bitposition
00162      *
00163      *  \result bitblast of BVMULT
00164      */
00165     virtual Theorem bitExtractConstBVMult(const Expr& t, int i)= 0;
00166
00167     /*! \param t : input1 is bitvector binary BVMULT. t[0] must not be BVCONST
00168      *  \param i : input2 is extracted bitposition
00169      *
00170      *  \result bitblast of BVMULT
00171      */
00172     virtual Theorem bitExtractBVMult(const Expr& t, int i) = 0;
00173
00174     /*! \param x is bitvector extraction e[k:j]
00175      *  \param i is extracted bitposition
00176      *
00177      *  \result \f[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]}
00178      *  \f], where \f[ 0 \geq j \geq k < n, 0 \geq i < k-j \f]
00179      */
00180     virtual Theorem bitExtractExtraction(const Expr & x, int i)= 0;
00181
00182     /*! \param t1 is vector of bitblasts of t, from bit i-1 to 0
00183      *  \param t2 is vector of bitblasts of q, from bit i-1 to 0
00184      *  \param bvPlusTerm is BVPLUS term: BVPLUS(n,t,q)
00185      *  \param i is extracted bitposition
00186      *
00187      *  \result The base case is: \f[
00188      *  \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]}
00189      *  \f], when \f[ 0 < i \leq n-1 \f], we have \f[
00190      *  \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i]
00191      *  \oplus c(t,q,i)} \f], where c(t,q,i) is the carry generated
00192      *  by the addition of bits from 0 to i-1
00193      */
00194     virtual Theorem bitExtractBVPlus(const std::vector<Theorem>& t1,
00195            const std::vector<Theorem>& t2,
00196            const Expr& bvPlusTerm, int i) = 0;
00197
00198
00199     virtual Theorem bitExtractBVPlusPreComputed(const Theorem& t1_i,
00200             const Theorem& t2_i,
00201             const Expr& bvPlusTerm,
00202             int bitPos,
00203             int precomputed) = 0;
00204
00205
00206     /*! \param bvPlusTerm : input1 is bvPlusTerm, a BVPLUS term with
00207      *  arity > 2
00208      *
00209      *  \result : output is iff-Theorem: bvPlusTerm <==> outputTerm,
00210      *  where outputTerm is an equivalent BINARY bvplus.
00211      */
00212     virtual Theorem bvPlusAssociativityRule(const Expr& bvPlusTerm)= 0;
00213
00214     /*! \param x : input1 is bitwise NEGATION
00215      *  \param i : input2 is extracted bitposition
00216      *
00217      *  \result \f[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])}
00218      *  \f]
00219      */
00220     virtual Theorem bitExtractNot(const Expr & x, int i)= 0;
00221
00222     //! Extract from bitwise AND, OR, or XOR
00223     virtual Theorem bitExtractBitwise(const Expr & x, int i, int kind)= 0;
00224
00225     /*! \param x : input1 is bitvector FIXED SHIFT \f[ e_{[n]} \ll k \f]
00226      *  \param i : input2 is extracted bitposition
00227      *
00228      *  \result \f[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}}
00229      *  \f], if 0 <= i < k. however, if k <= i < n then, result is
00230      *  \f[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \f]
00231      */
00232     virtual Theorem bitExtractFixedLeftShift(const Expr & x,
00233                int i)= 0;
00234
00235     virtual Theorem bitExtractFixedRightShift(const Expr & x,
00236                 int i)= 0;
00237     // BOOLEXTRACT(bvshl(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00238     //                               ((s = 1) AND BOOLEXTRACT(t,i-1)) OR ...
00239     //                               ((s = i) AND BOOLEXTRACT(t,0))
00240     virtual Theorem bitExtractBVSHL(const Expr & x, int i) = 0;
00241
00242     // BOOLEXTRACT(bvlshr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00243     //                                ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
00244     //                                ((s = n-1-i) AND BOOLEXTRACT(t,n-1))
00245     virtual Theorem bitExtractBVLSHR(const Expr & x, int i) = 0;
00246
00247     // BOOLEXTRACT(bvashr(t,s),i) <=> ((s = 0) AND BOOLEXTRACT(t,i)) OR
00248     //                                ((s = 1) AND BOOLEXTRACT(t,i+1)) OR ...
00249     //                                ((s >= n-1-i) AND BOOLEXTRACT(t,n-1))
00250     virtual Theorem bitExtractBVASHR(const Expr & x, int i) = 0;
00251
00252     /*! \param e : input1 is bitvector term
00253      *  \param r : input2 is extracted bitposition
00254      *
00255      *  \result we check if r > bvlength(e). if yes, then return
00256      *  BOOLEXTRACT(e,r) <==> FALSE; else raise soundness
00257      *  exception. (Note: this rule is used in BVPLUS bitblast
00258      *  function)
00259      */
00260     virtual Theorem zeroPaddingRule(const Expr& e, int r)= 0;
00261
00262
00263     virtual Theorem bitExtractSXRule(const Expr& e, int i) = 0;
00264
00265     ///////////////////////////////////////////////////////////////////
00266     /////  Special case rewrite rules
00267     ///////////////////////////////////////////////////////////////////
00268
00269     //! c1=c2 <=> TRUE/FALSE (equality of constant bitvectors)
00270     virtual Theorem eqConst(const Expr& e) = 0;
00271     //! |- c1=c2 ==> |- AND(c1[i:i] = c2[i:i]) - expanding equalities into bits
00272     virtual Theorem eqToBits(const Theorem& eq) = 0;
00273     //! t<<n = c @ 0bin00...00, takes e == (t<<n)
00274     virtual Theorem leftShiftToConcat(const Expr& e) = 0;
00275     //! t<<n = c @ 0bin00...00, takes e == (t<<n)
00276     virtual Theorem constWidthLeftShiftToConcat(const Expr& e) = 0;
00277     //! t>>m = 0bin00...00 @ t[bvlength-1:m], takes e == (t>>n)
00278     virtual Theorem rightShiftToConcat(const Expr& e) = 0;
00279     //! BVSHL(t,c) = t[n-c,0] @ 0bin00...00
00280     virtual Theorem bvshlToConcat(const Expr& e) = 0;
00281     //! BVSHL(t,c) = IF (c = 0) THEN t ELSE IF (c = 1) ...
00282     virtual Theorem bvshlSplit(const Expr& e) = 0;
00283     //! BVLSHR(t,c) = 0bin00...00 @ t[n-1,c]
00284     virtual Theorem bvlshrToConcat(const Expr& e) = 0;
00285     //! Any shift over a zero  = 0
00286     virtual Theorem bvShiftZero(const Expr& e) = 0;
00287     //! BVASHR(t,c) = SX(t[n-1,c], n-1)
00288     virtual Theorem bvashrToConcat(const Expr& e) = 0;
00289     //! a XNOR b <=> (~a & ~b) | (a & b)
00290     virtual Theorem rewriteXNOR(const Expr& e) = 0;
00291     //! a NAND b <=> ~(a & b)
00292     virtual Theorem rewriteNAND(const Expr& e) = 0;
00293     //! a NOR b <=> ~(a | b)
00294     virtual Theorem rewriteNOR(const Expr& e) = 0;
00295     //! BVCOMP(a,b) <=> ITE(a=b,0bin1,0bin0)
00296     virtual Theorem rewriteBVCOMP(const Expr& e) = 0;
00297     //! a - b <=> a + (-b)
00298     virtual Theorem rewriteBVSub(const Expr& e) = 0;
00299     //! k*t = BVPLUS(n, <sum of shifts of t>) -- translation of k*t to BVPLUS
00300     /*! If k = 2^m, return k*t = t\@0...0 */
00301     virtual Theorem constMultToPlus(const Expr& e) = 0;
00302     //! 0bin0...0 @ BVPLUS(n, args) = BVPLUS(n+k, args)
00303     /*! provided that m+ceil(log2(l)) <= n, where k is the size of the
00304      * 0bin0...0, m is the max. length of each argument, and l is the
00305      * number of arguments.
00306      */
00307     virtual Theorem bvplusZeroConcatRule(const Expr& e) = 0;
00308
00309
00310     ///////////////////////////////////////////////////////////////////
00311     /////  Bvplus Normal Form rules
00312     ///////////////////////////////////////////////////////////////////
00313     virtual Theorem zeroCoeffBVMult(const Expr& e)=0;
00314     virtual Theorem oneCoeffBVMult(const Expr& e)=0;
00315     virtual Theorem flipBVMult(const Expr& e) = 0;
00316     //! Make args the same length as the result (zero-extend)
00317     virtual Theorem padBVPlus(const Expr& e) = 0;
00318     //! Make args the same length as the result (zero-extend)
00319     virtual Theorem padBVMult(const Expr& e) = 0;
00320     virtual Theorem bvConstMultAssocRule(const Expr& e) = 0;
00321     virtual Theorem bvMultAssocRule(const Expr& e) = 0;
00322     virtual Theorem bvMultDistRule(const Expr& e) = 0;
00323     virtual Theorem flattenBVPlus(const Expr& e) = 0;
00324     virtual Theorem combineLikeTermsRule(const Expr& e) = 0;
00325     virtual Theorem lhsMinusRhsRule(const Expr& e) = 0;
00326     //! (x *[n] y)[m:k] = (x *[m+1] y)[m:k], where m < n
00327     virtual Theorem extractBVMult(const Expr& e) = 0;
00328     //! (x +[n] y)[m:k] = (x +[m+1] y)[m:k], where m < n
00329     virtual Theorem extractBVPlus(const Expr& e) = 0;
00330     //! ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
00331     virtual Theorem iteExtractRule(const Expr& e) = 0;
00332     //! ~ite(c,t1,t2) <=> ite(c,~t1,~t2)
00333     virtual Theorem iteBVnegRule(const Expr& e) = 0;
00334
00335     virtual Theorem bvuminusBVConst(const Expr& e) = 0;
00336     virtual Theorem bvuminusBVMult(const Expr& e) = 0;
00337     virtual Theorem bvuminusBVUminus(const Expr& e) = 0;
00338     virtual Theorem bvuminusVar(const Expr& e) = 0;
00339     virtual Theorem bvmultBVUminus(const Expr& e) = 0;
00340     //! -t <==> ~t+1
00341     virtual Theorem bvuminusToBVPlus(const Expr& e) = 0;
00342     //! -(c1*t1+...+cn*tn) <==> (-(c1*t1)+...+-(cn*tn))
00343     virtual Theorem bvuminusBVPlus(const Expr& e) = 0;
00344
00345
00346
00347     ///////////////////////////////////////////////////////////////////
00348     /////  Concatenation Normal Form rules
00349     ///////////////////////////////////////////////////////////////////
00350
00351     // Extraction rules
00352
00353     //! c1[i:j] = c  (extraction from a constant bitvector)
00354     virtual Theorem extractConst(const Expr& e) = 0;
00355     //! t[n-1:0] = t  for n-bit t
00356     virtual Theorem extractWhole(const Expr& e) = 0;
00357     //! t[i:j][k:l] = t[k+j:l+j]  (eliminate double extraction)
00358     virtual Theorem extractExtract(const Expr& e) = 0;
00359     //! (t1 @ t2)[i:j] = t1[...] @ t2[...]  (push extraction through concat)
00360     virtual Theorem extractConcat(const Expr& e) = 0;
00361     //! (t1 & t2)[i:j] = t1[i:j] & t2[i:j]  (push extraction through OR)
00362     virtual Theorem extractAnd(const Expr& e) = 0;
00363     //! (t1 | t2)[i:j] = t1[i:j] | t2[i:j]  (push extraction through AND)
00364     virtual Theorem extractOr(const Expr& e) = 0;
00365     //! (~t)[i:j] = ~(t[i:j]) (push extraction through NEG)
00366     virtual Theorem extractNeg(const Expr& e) = 0;
00367     //! Auxiliary function: (t1 op t2)[i:j] = t1[i:j] op t2[i:j]
00368     virtual Theorem extractBitwise(const Expr& e,
00369            int kind, const std::string& name) = 0;
00370
00371     // Negation rules
00372
00373     //! ~c1 = c  (bit-wise negation of a constant bitvector)
00374     virtual Theorem negConst(const Expr& e) = 0;
00375     //! ~(t1\@...\@tn) = (~t1)\@...\@(~tn) -- push negation through concat
00376     virtual Theorem negConcat(const Expr& e) = 0;
00377     //! ~(~t) = t  -- eliminate double negation
00378     virtual Theorem negNeg(const Expr& e) = 0;
00379     //! ~t = -1*t + 1 -- eliminate negation
00380     virtual Theorem negElim(const Expr& e) = 0;
00381     //! ~(t1 & t2) <=> ~t1 | ~t2 -- DeMorgan's Laws
00382     virtual Theorem negBVand(const Expr& e) = 0;
00383     //! ~(t1 | t2) <=> ~t1 & ~t2 -- DeMorgan's Laws
00384     virtual Theorem negBVor(const Expr& e) = 0;
00385     //! ~(t1 xor t2) = ~t1 xor t2
00386     virtual Theorem negBVxor(const Expr& e) = 0;
00387     //! ~(t1 xnor t2) = t1 xor t2
00388     virtual Theorem negBVxnor(const Expr& e) = 0;
00389
00390     //! Combine constants in bitwise AND, OR, XOR
00391     virtual Theorem bitwiseConst(const Expr& e,
00392                                  const std::vector<int>& idxs,
00393                                  int kind) = 0;
00394     //! Lifts concatenation above bitwise operators.
00395     virtual Theorem bitwiseConcat(const Expr& e, int kind) = 0;
00396     //! Flatten bitwise operation
00397     virtual Theorem bitwiseFlatten(const Expr& e, int kind) = 0;
00398     //! Simplify bitwise operator containing a constant child
00399     /*! \param e is the bit-wise expr
00400      *  \param idx is the index of the constant bitvector
00401      *  \param kind is the kind of e
00402      */
00403     virtual Theorem bitwiseConstElim(const Expr& e, int idx, int kind) = 0;
00404
00405     // Concatenation rules
00406
00407     //! c1\@c2\@...\@cn = c  (concatenation of constant bitvectors)
00408     virtual Theorem concatConst(const Expr& e) = 0;
00409     //! Flatten one level of nested concatenation, e.g.: x\@(y\@z)\@w = x\@y\@z\@w
00410     virtual Theorem concatFlatten(const Expr& e) = 0;
00411     //! Merge n-ary concat. of adjacent extractions: x[15:8]\@x[7:0] = x[15:0]
00412     virtual Theorem concatMergeExtract(const Expr& e) = 0;
00413
00414     ///////////////////////////////////////////////////////////////////
00415     /////  Modulo arithmetic rules
00416     ///////////////////////////////////////////////////////////////////
00417
00418     //! BVPLUS(n, c1,c2,...,cn) = c  (bit-vector plus of constant bitvectors)
00419     virtual Theorem bvplusConst(const Expr& e) = 0;
00420     /*! @brief n*c1 = c, where n >= 0 (multiplication of a constant
00421      *  bitvector by a non-negative constant) */
00422     virtual Theorem bvmultConst(const Expr& e) = 0;
00423
00424     ///////////////////////////////////////////////////////////////////
00425     /////  Type predicate rules
00426     ///////////////////////////////////////////////////////////////////
00427
00428     //! |- t=0 OR t=1  for any 1-bit bitvector t
00429     virtual Theorem typePredBit(const Expr& e) = 0;
00430     //! Expand the type predicate wrapper (compute the actual type predicate)
00431     virtual Theorem expandTypePred(const Theorem& tp) = 0;
00432
00433     /*Beginning of Lorenzo PLatania's methods*/
00434
00435     //    virtual Theorem multiply_coeff( Rational mult_inv, const Expr& e)=0;
00436
00437     //! isolate a variable with coefficient = 1 on the Lhs of an
00438     //equality expression
00439     virtual Theorem isolate_var(const Expr& e)=0;
00440
00441     // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
00442     // where n = BVSize(b), a != 0
00443     virtual Theorem liftConcatBVMult(const Expr& e)=0;
00444
00445     //! canonize BVMult expressions in order to get one coefficient
00446     //multiplying the variable(s) in the expression
00447     virtual Theorem canonBVMult( const Expr& e )=0;
00448
00449     // BVPLUS(N, a@b, y) = BVPLUS(N-n,a,BVPLUS(N,b,y)[N-1:n])@BVPLUS(n,b,y)
00450     // where n = BVSize(b)
00451     virtual Theorem liftConcatBVPlus(const Expr& e)=0;
00452
00453     //! canonize BVPlus expressions in order to get just one
00454     //coefficient multiplying each variable in the expression
00455     virtual Theorem canonBVPlus( const Expr& e )=0;
00456     virtual Theorem canonBVUMinus( const Expr& e )=0;
00457     // Input: t[hi:lo] = rhs
00458     // if t appears as leaf in rhs, then:
00459     //    t[hi:lo] = rhs |- Exists x,y,z. (t = x @ y @ z AND y = rhs), solvedForm = false
00460     // else
00461     //    t[hi:lo] = rhs |- Exists x,y,z. (t = x @ rhs @ z AND y = rhs), solvedForm = true
00462     virtual Theorem processExtract(const Theorem& e, bool& solvedForm)=0;
00463     // normalizes equation
00464     virtual Theorem canonBVEQ( const Expr& e, int maxEffort = 3 )=0;
00465
00466     //! apply the distributive rule on the BVMULT expression e
00467     virtual Theorem distributive_rule( const Expr& e )=0;
00468     //    virtual Theorem BVMultConstTerm( const Expr& e1, const Expr& e2)=0;
00469     // recursively reorder subterms in a BVMULT term
00470     virtual Theorem BVMult_order_subterms( const Expr& e ) = 0;
00471     // rewrites the equation in the form 0 = Expr
00472     // this is needed for TheoryBitvector::solve
00473     virtual Theorem MarkNonSolvableEq( const Expr& e) = 0;
00474     /*End of Lorenzo PLatania's methods*/
00475
00476     // rewrite BVZEROEXTEND into CONCAT
00477     virtual Theorem zeroExtendRule(const Expr& e) = 0;
00478     // rewrite BVREPEAT into CONCAT
00479     virtual Theorem repeatRule(const Expr& e) = 0;
00480     // rewrite BVROTL into CONCAT
00481     virtual Theorem rotlRule(const Expr& e) = 0;
00482     // rewrite BVROTR into CONCAT
00483     virtual Theorem rotrRule(const Expr& e) = 0;
00484
00485     /**
00486      * Divide a with b unsigned and return the bit-vector constant result
00487      */
00488     virtual Theorem bvUDivConst(const Expr& divExpr) = 0;
00489
00490     /**
00491      * Rewrite a/b with a fresh variable d and add the constraints to make it be a divider.
00492      */
00493     virtual Theorem bvUDivTheorem(const Expr& divExpr) = 0;
00494
00495     /**
00496      * Divide a with b unsigned and return the bit-vector constant result
00497      */
00498     virtual Theorem bvURemConst(const Expr& remExpr) = 0;
00499
00500     /**
00501      * Rewrite a%b in terms of a/b, i.e. a - a/b
00502      */
00503     virtual Theorem bvURemRewrite(const Expr& divExpr) = 0;
00504
00505     /**
00506      * Rewrite the signed divide in terms of the unsigned one.
00507      */
00508     virtual Theorem bvSDivRewrite(const Expr& sDivExpr) = 0;
00509
00510     /**
00511      * Rewrite the signed remainder in terms of the unsigned one.
00512      */
00513     virtual Theorem bvSRemRewrite(const Expr& sRemExpr) = 0;
00514
00515     /**
00516      * Rewrite the signed mod in terms of the unsigned one.
00517      */
00518     virtual Theorem bvSModRewrite(const Expr& sModExpr) = 0;
00519
00520     /**
00521      * Bit-blast the multiplication a_times_b given the bits in a_bits and b_bits.
00522      * The resulting output bits will be in the vector output_bits. The return value
00523      * is a theorem saying there is no overflow for this multiplication. (TODO, it's
00524      * just an empty theorem for now).
00525      */
00526     virtual Theorem bitblastBVMult(const std::vector<Theorem>& a_bits,
00527                                const std::vector<Theorem>& b_bits,
00528                                const Expr& a_times_b,
00529                                std::vector<Theorem>& output_bits) = 0;
00530
00531     /**
00532      * Bit-blast the sum a_times_b given the bits in a_bits and b_bits.
00533      * The resulting output bits will be in the vector output_bits. The return value
00534      * is a theorem saying there is no overflow for this sum. (TODO, it's
00535      * just an empty theorem for now).
00536      */
00537     virtual Theorem bitblastBVPlus(const std::vector<Theorem>& a_bits,
00538                                const std::vector<Theorem>& b_bits,
00539                                const Expr& a_plus_b,
00540                                std::vector<Theorem>& output_bits) = 0;
00541
00542     /**
00543      * Rewrite x_1 \vee x_2 \vee \ldots \vee x_n = 0 into
00544      * x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0.
00545      */
00546     virtual Theorem zeroBVOR(const Expr& orEqZero) = 0;
00547
00548     /**
00549      * Rewrite x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n into
00550      * x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n.
00551      */
00552     virtual Theorem oneBVAND(const Expr& andEqOne) = 0;
00553
00554     /**
00555      * Equalities over constants go to true/false.
00556      */
00557     virtual Theorem constEq(const Expr& eq) = 0;
00558
00559     /**
00560      * Returns true if equation is of the form x[i:j] = x[k:l], where the
00561      * extracted segments overlap, i.e. i > j >= k > l or k > i >= l > j.
00562      */
00563     virtual bool solveExtractOverlapApplies(const Expr& eq) = 0;
00564
00565     /**
00566      * Returns the theorem that simplifies the equality of two overlapping
00567      * extracts over the same term.
00568      */
00569     virtual Theorem solveExtractOverlap(const Expr& eq) = 0;
00570
00571   }; // end of class BitvectorProofRules
00572 } // end of name-space CVC3
00573
00574 #endif