theory_bitvector.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_bitvector.h
00004  * 
00005  * Author: Vijay Ganesh
00006  * 
00007  * Created: Wed May 05 18:34:55 PDT 2004
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__theory_bitvector_h_
00022 #define _cvc3__include__theory_bitvector_h_
00023 
00024 #include "theory_core.h"
00025 #include "statistics.h"
00026 
00027 namespace CVC3 {
00028 
00029   class VCL;
00030   class BitvectorProofRules;
00031   
00032   typedef enum { //some new BV kinds
00033     BITVECTOR = 8000,
00034 
00035     BVCONST,
00036 
00037     CONCAT,
00038     EXTRACT,
00039     BOOLEXTRACT,
00040 
00041     LEFTSHIFT,
00042     CONST_WIDTH_LEFTSHIFT,
00043     RIGHTSHIFT,
00044     BVSHL,
00045     BVLSHR,
00046     BVASHR,
00047     SX,
00048     BVREPEAT,
00049     BVZEROEXTEND,
00050     BVROTL,
00051     BVROTR,
00052 
00053     BVAND,
00054     BVOR,
00055     BVXOR,
00056     BVXNOR,
00057     BVNEG,
00058     BVNAND,
00059     BVNOR,
00060     BVCOMP,
00061 
00062     BVUMINUS,
00063     BVPLUS,
00064     BVSUB,
00065     BVMULT,
00066     BVUDIV,
00067     BVSDIV,
00068     BVUREM,
00069     BVSREM,
00070     BVSMOD,
00071 
00072     BVLT,
00073     BVLE,
00074     BVGT,
00075     BVGE,
00076     BVSLT,
00077     BVSLE,
00078     BVSGT,
00079     BVSGE,
00080 
00081     INTTOBV, // Not implemented yet
00082     BVTOINT, // Not implemented yet
00083     // A wrapper for delaying the construction of type predicates
00084     BVTYPEPRED
00085   } BVKinds;
00086 
00087 /*****************************************************************************/
00088 /*!
00089  *\class TheoryBitvector
00090  *\ingroup Theories
00091  *\brief Theory of bitvectors of known length \
00092  * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)
00093  *
00094  * Author: Vijay Ganesh
00095  *
00096  * Created:Wed May  5 15:35:07 PDT 2004
00097  */
00098 /*****************************************************************************/
00099 class TheoryBitvector :public Theory {
00100   BitvectorProofRules* d_rules;
00101   //! MemoryManager index for BVConstExpr subclass
00102   size_t d_bvConstExprIndex;
00103   size_t d_bvPlusExprIndex;
00104   size_t d_bvParameterExprIndex;
00105   size_t d_bvTypePredExprIndex;
00106 
00107   //! counts delayed asserted equalities
00108   StatCounter d_bvDelayEq;
00109   //! counts asserted equalities
00110   StatCounter d_bvAssertEq;
00111   //! counts delayed asserted disequalities
00112   StatCounter d_bvDelayDiseq;
00113   //! counts asserted disequalities
00114   StatCounter d_bvAssertDiseq;
00115   //! counts type predicates
00116   StatCounter d_bvTypePreds;
00117   //! counts delayed type predicates
00118   StatCounter d_bvDelayTypePreds;
00119   //! counts bitblasted equalities
00120   StatCounter d_bvBitBlastEq;
00121   //! counts bitblasted disequalities
00122   StatCounter d_bvBitBlastDiseq;
00123 
00124 
00125   //! boolean on the fly rewrite flag
00126   const bool* d_booleanRWFlag;
00127   //! bool extract cache flag
00128   const bool* d_boolExtractCacheFlag;
00129   //! flag which indicates that all arithmetic is 32 bit with no overflow
00130   const bool* d_bv32Flag;
00131   //! Command line flag: rewrite bitvector expressions
00132   const bool* d_rewriteFlag;
00133   //! Command line flag: concatenation normal form rewrite bitvector expressions
00134   const bool* d_concatRewriteFlag;
00135   //! Command line flag: bvplus normal form rewrite bitvector expressions
00136   const bool* d_bvplusRewriteFlag;
00137   //! Commant line flag: rewrite while bit-blasting
00138   const bool* d_rwBitBlastFlag;
00139   //! Commant line flag: bit-blast equalities in CNF converter
00140   const bool* d_cnfBitBlastFlag;
00141   //! Command line flag: enable lhs-minus-rhs-rule for lhs=rhs
00142   const bool* d_lhsMinusRhsFlag;
00143   //! Command line flag: enable pushnegation
00144   const bool* d_pushNegationFlag;
00145 
00146   //! Cache for storing the results of the bitBlastTerm function
00147   CDMap<Expr,Theorem> d_bitvecCache;
00148 
00149   //! Cache for pushNegation(). it is ok that this is cache is
00150   //ExprMap. it is cleared for each call of pushNegation. Does not add
00151   //value across calls of pushNegation
00152   ExprMap<Theorem> d_pushNegCache;
00153 
00154   //! Backtracking queue for equalities (to delay them till checkSat() call)
00155   CDList<Theorem> d_eq;
00156   //! Pointer to the next unasserted equality in d_eq
00157   CDO<size_t> d_eqIdx;
00158   //! Pointer to the next equality in d_eq which is not bit-blasted yet
00159   CDO<size_t> d_eqBlastIdx;
00160   //! Backtracking queue for disequalities (to delay them till checkSat() call)
00161   CDList<Theorem> d_diseq;
00162   //! Pointer to the next unasserted disequality in d_diseq
00163   CDO<size_t> d_diseqIdx;
00164   //! Database of stale bit-expansions for update()
00165   CDMap<Expr,bool> d_staleDB;
00166   //! Backtracking queue for TCCs on individual bits
00167   CDList<Theorem> d_tccs;
00168   //! Pointer to the next unasserted TCC in d_tccs
00169   CDO<size_t> d_tccsIdx;
00170   //! Backtracking database of subterms of shared terms
00171   CDMap<Expr,Expr> d_sharedSubterms;
00172   //! Backtracking database of subterms of shared terms
00173   CDList<Expr> d_sharedSubtermsList;
00174   //! Cache for typePredicates of non shared terms
00175   CDMap<Expr, Theorem> d_typePredsCache;
00176   //! cache for rewriteBoolean
00177   //CDMap<Expr, Theorem> d_rewriteBooleanCache;
00178   
00179   //! Constant 1-bit bit-vector 0bin0
00180   Expr d_bvZero;
00181   //! Constant 1-bit bit-vector 0bin0
00182   Expr d_bvOne;
00183   //! Return cached constant 0bin0
00184   const Expr& bvZero() const { return d_bvZero; }
00185   //! Return cached constant 0bin1
00186   const Expr& bvOne() const { return d_bvOne; }
00187 
00188   //! Max size of any bitvector we've seen
00189   int d_maxLength;
00190 
00191   //! Used in checkSat
00192   CDO<unsigned> d_index1;
00193 
00194   //! functions which implement the DP strategy for bitblasting
00195   Theorem bitBlastEqn(const Expr& e);
00196   //! functions which implement the DP strategy for bitblasting
00197   Theorem bitBlastDisEqn(const Theorem& e);
00198   public:
00199   //! functions which implement the DP strategy for bitblasting
00200   Theorem bitBlastTerm(const Expr& t, int bitPosition);
00201   private:
00202   //! function which implements the DP strtagey to bitblast Inequations
00203   Theorem bitBlastIneqn(const Expr& e);
00204 
00205   //! strategy fucntions for BVPLUS NORMAL FORM
00206   Theorem padBVPlus(const Expr& e);
00207   //! strategy fucntions for BVPLUS NORMAL FORM
00208   Theorem flattenBVPlus(const Expr& e);
00209   
00210   //! Implementation of the concatenation normal form
00211   Theorem normalizeConcat(const Expr& e, bool useFind);
00212   //! Implementation of the n-bit arithmetic normal form
00213   Theorem normalizeBVArith(const Expr& e, bool useFind);
00214   //! Helper method for composing normalizations
00215   Theorem normalizeConcat(const Theorem& t, bool useFind) {
00216     return transitivityRule(t, normalizeConcat(t.getRHS(), useFind));
00217   }
00218   //! Helper method for composing normalizations
00219   Theorem normalizeBVArith(const Theorem& t, bool useFind) {
00220     return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind));
00221   }
00222 
00223   Theorem signExtendBVLT(const Expr& e, int len, bool useFind);
00224 
00225   Theorem pushNegationRec(const Theorem& thm, bool neg);
00226   Theorem pushNegation(const Expr& e);
00227 
00228   //! Top down simplifier
00229   virtual Theorem simplifyOp(const Expr& e);
00230 
00231 
00232   //! Internal rewrite method for constants
00233   Theorem rewriteConst(const Expr& e);
00234   //! Internal rewrite method
00235   Theorem rewriteBV(const Expr& e, bool useFind);
00236   //! Rewrite children 'n' levels down (n==1 means "only the top level")
00237   Theorem rewriteBV(const Expr& e, int n, bool useFind);
00238   //! Rewrite children 'n' levels down (n==1 means "only the top level")
00239   Theorem rewriteBV(const Theorem& t, int n, bool useFind) {
00240     return transitivityRule(t, rewriteBV(t.getRHS(), n, useFind));
00241   }
00242   //! Internal rewrite method (implements the actual rewrites)
00243   Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, bool useFind);
00244   //! Rewrite children 'n' levels down (n==1 means "only the top level")
00245   Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n,
00246         bool useFind);
00247   //! Rewrite children 'n' levels down (n==1 means "only the top level")
00248   Theorem rewriteBV(const Theorem& t, ExprMap<Theorem>& cache, int n,
00249         bool useFind) {
00250     return transitivityRule(t, rewriteBV(t.getRHS(), cache, n, useFind));
00251   }
00252 
00253   //! rewrite input boolean expression e to a simpler form
00254   Theorem rewriteBoolean(const Expr& e);
00255   
00256   //! Setup the NotifyList mechanism for the Expr e
00257   void setupExpr(const Expr& e);
00258 public:
00259   TheoryBitvector(TheoryCore* core);
00260   ~TheoryBitvector();
00261 
00262 
00263   ExprMap<Expr> d_bvPlusCarryCacheLeftBV;
00264   ExprMap<Expr> d_bvPlusCarryCacheRightBV;
00265 
00266   // Trusted method that creates the proof rules class (used in constructor).
00267   // Implemented in bitvector_theorem_producer.cpp
00268   BitvectorProofRules* createProofRules();
00269   Theorem pushNegationRec(const Expr& e, bool neg);
00270 
00271   // Theory interface
00272   void addSharedTerm(const Expr& e);
00273   void assertFact(const Theorem& e);
00274   void assertTypePred(const Expr& e, const Theorem& pred);
00275   void checkSat(bool fullEffort);
00276   Theorem rewrite(const Expr& e);
00277   Theorem rewriteAtomic(const Expr& e);
00278   void setup(const Expr& e);
00279   void update(const Theorem& e, const Expr& d);
00280   Theorem solve(const Theorem& e);
00281   void checkType(const Expr& e);
00282   void computeType(const Expr& e);
00283   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00284   void computeModel(const Expr& e, std::vector<Expr>& vars);
00285   Expr computeTypePred(const Type& t, const Expr& e);
00286   Expr computeTCC(const Expr& e);
00287   ExprStream& print(ExprStream& os, const Expr& e);
00288   Expr parseExprOp(const Expr& e);
00289 
00290   //helper functions
00291   Expr rat(const Rational& r) { return getEM()->newRatExpr(r); }
00292   //!pads e to be of length len
00293   Expr pad(int len, const Expr& e);
00294 
00295   bool comparebv(const Expr& e1, const Expr& e2);
00296 
00297   //! Return the number of bits in the bitvector expression
00298   int BVSize(const Expr& e);
00299 
00300   //helper functions: functions to construct exprs
00301   Type newBitvectorType(int i) 
00302     { return newBitvectorTypeExpr(i); }
00303   Expr newBitvectorTypePred(const Type& t, const Expr& e);
00304   Expr newBitvectorTypeExpr(int i);
00305 
00306   Expr newBVAndExpr(const Expr& t1, const Expr& t2);
00307   Expr newBVAndExpr(const std::vector<Expr>& kids);
00308 
00309   Expr newBVOrExpr(const Expr& t1, const Expr& t2);
00310   Expr newBVOrExpr(const std::vector<Expr>& kids);
00311 
00312   Expr newBVXorExpr(const Expr& t1, const Expr& t2);
00313   Expr newBVXorExpr(const std::vector<Expr>& kids);
00314 
00315   Expr newBVXnorExpr(const Expr& t1, const Expr& t2);
00316   Expr newBVXnorExpr(const std::vector<Expr>& kids);
00317 
00318   Expr newBVNandExpr(const Expr& t1, const Expr& t2);
00319   Expr newBVNorExpr(const Expr& t1, const Expr& t2);
00320   Expr newBVCompExpr(const Expr& t1, const Expr& t2);
00321   
00322   Expr newBVLTExpr(const Expr& t1, const Expr& t2);
00323   Expr newBVLEExpr(const Expr& t1, const Expr& t2);  
00324   Expr newSXExpr(const Expr& t1, int len);
00325   Expr newBVIndexExpr(int kind, const Expr& t1, int len);
00326   Expr newBVSLTExpr(const Expr& t1, const Expr& t2);
00327   Expr newBVSLEExpr(const Expr& t1, const Expr& t2);
00328 
00329   Expr newBVNegExpr(const Expr& t1);
00330   Expr newBVUminusExpr(const Expr& t1);
00331   Expr newBoolExtractExpr(const Expr& t1, int r);
00332   Expr newFixedLeftShiftExpr(const Expr& t1, int r);
00333   Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r);
00334   Expr newFixedRightShiftExpr(const Expr& t1, int r);
00335   Expr newConcatExpr(const Expr& t1, const Expr& t2);
00336   Expr newConcatExpr(const Expr& t1, const Expr& t2, const Expr& t3);
00337   Expr newConcatExpr(const std::vector<Expr>& kids);
00338   Expr newBVConstExpr(const std::string& s, int base = 2);
00339   Expr newBVConstExpr(const std::vector<bool>& bits);
00340   // Construct BVCONST of length 'len', or the min. needed length when len=0.
00341   Expr newBVConstExpr(const Rational& r, int len = 0);
00342   Expr newBVZeroString(int r);
00343   Expr newBVOneString(int r);
00344   //! hi and low are bit indices
00345   Expr newBVExtractExpr(const Expr& e, 
00346       int hi, int low);
00347   Expr newBVSubExpr(const Expr& t1, const Expr& t2);
00348   //! 'numbits' is the number of bits in the result
00349   Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
00350   //! accepts an integer, r, and bitvector, t1, and returns r.t1
00351   Expr newBVMultExpr(int bvLength,
00352          const Expr& t1, const Expr& t2);
00353 
00354   // Accessors for expression parameters
00355   int getBitvectorTypeParam(const Expr& e);
00356   int getBitvectorTypeParam(const Type& t) 
00357     { return getBitvectorTypeParam(t.getExpr()); }
00358   Type getTypePredType(const Expr& tp);
00359   const Expr& getTypePredExpr(const Expr& tp);
00360   int getSXIndex(const Expr& e);
00361   int getBVIndex(const Expr& e);
00362   int getBoolExtractIndex(const Expr& e);
00363   int getFixedLeftShiftParam(const Expr& e);
00364   int getFixedRightShiftParam(const Expr& e);
00365   int getExtractHi(const Expr& e);
00366   int getExtractLow(const Expr& e);
00367   int getBVPlusParam(const Expr& e);
00368   int getBVMultParam(const Expr& e);
00369 
00370   unsigned getBVConstSize(const Expr& e);
00371   bool getBVConstValue(const Expr& e, int i);
00372   //!computes the integer value of a bitvector constant
00373   Rational computeBVConst(const Expr& e);
00374   //!computes the integer value of ~c+1 or BVUMINUS(c)
00375   Rational computeNegBVConst(const Expr& e);
00376  
00377   int getMaxSize() { return d_maxLength; }
00378 
00379 }; //end of class TheoryBitvector
00380 
00381   //!computes the integer value of a bitvector constant
00382   Rational computeBVConst(const Expr& e);
00383 
00384 }//end of namespace CVC3
00385 #endif

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