CVC3 2.2
|
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 // New constants 00034 BVCONST = 80, 00035 00036 BITVECTOR = 8000, 00037 00038 CONCAT, 00039 EXTRACT, 00040 BOOLEXTRACT, 00041 00042 LEFTSHIFT, 00043 CONST_WIDTH_LEFTSHIFT, 00044 RIGHTSHIFT, 00045 BVSHL, 00046 BVLSHR, 00047 BVASHR, 00048 SX, 00049 BVREPEAT, 00050 BVZEROEXTEND, 00051 BVROTL, 00052 BVROTR, 00053 00054 BVAND, 00055 BVOR, 00056 BVXOR, 00057 BVXNOR, 00058 BVNEG, 00059 BVNAND, 00060 BVNOR, 00061 BVCOMP, 00062 00063 BVUMINUS, 00064 BVPLUS, 00065 BVSUB, 00066 BVMULT, 00067 BVUDIV, 00068 BVSDIV, 00069 BVUREM, 00070 BVSREM, 00071 BVSMOD, 00072 00073 BVLT, 00074 BVLE, 00075 BVGT, 00076 BVGE, 00077 BVSLT, 00078 BVSLE, 00079 BVSGT, 00080 BVSGE, 00081 00082 INTTOBV, // Not implemented yet 00083 BVTOINT, // Not implemented yet 00084 // A wrapper for delaying the construction of type predicates 00085 BVTYPEPRED 00086 } BVKinds; 00087 00088 /*****************************************************************************/ 00089 /*! 00090 *\class TheoryBitvector 00091 *\ingroup Theories 00092 *\brief Theory of bitvectors of known length \ 00093 * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG) 00094 * 00095 * Author: Vijay Ganesh 00096 * 00097 * Created:Wed May 5 15:35:07 PDT 2004 00098 */ 00099 /*****************************************************************************/ 00100 class TheoryBitvector :public Theory { 00101 BitvectorProofRules* d_rules; 00102 //! MemoryManager index for BVConstExpr subclass 00103 size_t d_bvConstExprIndex; 00104 size_t d_bvPlusExprIndex; 00105 size_t d_bvParameterExprIndex; 00106 size_t d_bvTypePredExprIndex; 00107 00108 //! counts delayed asserted equalities 00109 StatCounter d_bvDelayEq; 00110 //! counts asserted equalities 00111 StatCounter d_bvAssertEq; 00112 //! counts delayed asserted disequalities 00113 StatCounter d_bvDelayDiseq; 00114 //! counts asserted disequalities 00115 StatCounter d_bvAssertDiseq; 00116 //! counts type predicates 00117 StatCounter d_bvTypePreds; 00118 //! counts delayed type predicates 00119 StatCounter d_bvDelayTypePreds; 00120 //! counts bitblasted equalities 00121 StatCounter d_bvBitBlastEq; 00122 //! counts bitblasted disequalities 00123 StatCounter d_bvBitBlastDiseq; 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 00132 //! Cache for storing the results of the bitBlastTerm function 00133 CDMap<Expr,Theorem> d_bitvecCache; 00134 00135 //! Cache for pushNegation(). it is ok that this is cache is 00136 //ExprMap. it is cleared for each call of pushNegation. Does not add 00137 //value across calls of pushNegation 00138 ExprMap<Theorem> d_pushNegCache; 00139 00140 //! Backtracking queue for equalities 00141 CDList<Theorem> d_eq; 00142 //! Backtracking queue for unsolved equalities 00143 CDList<Theorem> d_eqPending; 00144 //! Index to current position in d_eqPending 00145 CDO<unsigned int> d_eq_index; 00146 //! Backtracking queue for all other assertions 00147 CDList<Theorem> d_bitblast; 00148 //! Index to current position in d_bitblast 00149 CDO<unsigned int> d_bb_index; 00150 //! Backtracking database of subterms of shared terms 00151 CDMap<Expr,Expr> d_sharedSubterms; 00152 //! Backtracking database of subterms of shared terms 00153 CDList<Expr> d_sharedSubtermsList; 00154 00155 //! Constant 1-bit bit-vector 0bin0 00156 Expr d_bvZero; 00157 //! Constant 1-bit bit-vector 0bin0 00158 Expr d_bvOne; 00159 //! Return cached constant 0bin0 00160 const Expr& bvZero() const { return d_bvZero; } 00161 //! Return cached constant 0bin1 00162 const Expr& bvOne() const { return d_bvOne; } 00163 00164 //! Max size of any bitvector we've seen 00165 int d_maxLength; 00166 00167 //! Used in checkSat 00168 CDO<unsigned> d_index1; 00169 CDO<unsigned> d_index2; 00170 00171 //! functions which implement the DP strategy for bitblasting 00172 Theorem bitBlastEqn(const Expr& e); 00173 //! bitblast disequation 00174 Theorem bitBlastDisEqn(const Theorem& notE); 00175 //! function which implements the DP strtagey to bitblast Inequations 00176 Theorem bitBlastIneqn(const Expr& e); 00177 //! functions which implement the DP strategy for bitblasting 00178 Theorem bitBlastTerm(const Expr& t, int bitPosition); 00179 00180 // //! strategy fucntions for BVPLUS NORMAL FORM 00181 // Theorem padBVPlus(const Expr& e); 00182 // //! strategy fucntions for BVPLUS NORMAL FORM 00183 // Theorem flattenBVPlus(const Expr& e); 00184 00185 // //! Implementation of the concatenation normal form 00186 // Theorem normalizeConcat(const Expr& e, bool useFind); 00187 // //! Implementation of the n-bit arithmetic normal form 00188 // Theorem normalizeBVArith(const Expr& e, bool useFind); 00189 // //! Helper method for composing normalizations 00190 // Theorem normalizeConcat(const Theorem& t, bool useFind) { 00191 // return transitivityRule(t, normalizeConcat(t.getRHS(), useFind)); 00192 // } 00193 // //! Helper method for composing normalizations 00194 // Theorem normalizeBVArith(const Theorem& t, bool useFind) { 00195 // return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind)); 00196 // } 00197 00198 // Theorem signExtendBVLT(const Expr& e, int len, bool useFind); 00199 00200 public: 00201 Theorem pushNegationRec(const Expr& e); 00202 private: 00203 Theorem pushNegation(const Expr& e); 00204 00205 //! Top down simplifier 00206 virtual Theorem simplifyOp(const Expr& e); 00207 00208 //! Internal rewrite method for constants 00209 // Theorem rewriteConst(const Expr& e); 00210 00211 //! Main rewrite method (implements the actual rewrites) 00212 Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n = 1); 00213 00214 //! Rewrite children 'n' levels down (n==1 means "only the top level") 00215 Theorem rewriteBV(const Expr& e, int n = 1); 00216 00217 // Shortcuts for theorems 00218 Theorem rewriteBV(const Theorem& t, ExprMap<Theorem>& cache, int n = 1) { 00219 return transitivityRule(t, rewriteBV(t.getRHS(), cache, n)); 00220 } 00221 Theorem rewriteBV(const Theorem& t, int n = 1) { 00222 return transitivityRule(t, rewriteBV(t.getRHS(), n)); 00223 } 00224 00225 //! rewrite input boolean expression e to a simpler form 00226 Theorem rewriteBoolean(const Expr& e); 00227 00228 /*Beginning of Lorenzo PLatania's methods*/ 00229 00230 Expr multiply_coeff( Rational mult_inv, const Expr& e); 00231 00232 // extract the min value from a Rational list 00233 int min(std::vector<Rational> list); 00234 00235 // evaluates the gcd of two integer coefficients 00236 // int gcd(int c1, int c2); 00237 00238 // converts a bv constant to an integer 00239 // int bv2int(const Expr& e); 00240 00241 // return the odd coefficient of a leaf for which we can solve the 00242 // equation, or zero if no one has been found 00243 Rational Odd_coeff( const Expr& e ); 00244 00245 00246 00247 // returns 1 if e is a linear term 00248 int check_linear( const Expr &e ); 00249 00250 bool isTermIn(const Expr& e1, const Expr& e2); 00251 00252 Theorem updateSubterms( const Expr& d ); 00253 00254 // returns how many times "term" appears in "e" 00255 int countTermIn( const Expr& term, const Expr& e); 00256 00257 Theorem simplifyPendingEq(const Theorem& thm, int maxEffort); 00258 Theorem generalBitBlast( const Theorem& thm ); 00259 /*End of Lorenzo PLatania's methods*/ 00260 00261 public: 00262 TheoryBitvector(TheoryCore* core); 00263 ~TheoryBitvector(); 00264 00265 ExprMap<Expr> d_bvPlusCarryCacheLeftBV; 00266 ExprMap<Expr> d_bvPlusCarryCacheRightBV; 00267 00268 // Trusted method that creates the proof rules class (used in constructor). 00269 // Implemented in bitvector_theorem_producer.cpp 00270 BitvectorProofRules* createProofRules(); 00271 00272 // Theory interface 00273 void addSharedTerm(const Expr& e); 00274 void assertFact(const Theorem& e); 00275 void assertTypePred(const Expr& e, const Theorem& pred); 00276 void checkSat(bool fullEffort); 00277 Theorem rewrite(const Expr& e); 00278 Theorem rewriteAtomic(const Expr& e); 00279 void setup(const Expr& e); 00280 void update(const Theorem& e, const Expr& d); 00281 Theorem solve(const Theorem& e); 00282 void checkType(const Expr& e); 00283 Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 00284 bool enumerate, bool computeSize); 00285 void computeType(const Expr& e); 00286 void computeModelTerm(const Expr& e, std::vector<Expr>& v); 00287 void computeModel(const Expr& e, std::vector<Expr>& vars); 00288 Expr computeTypePred(const Type& t, const Expr& e); 00289 Expr computeTCC(const Expr& e); 00290 ExprStream& print(ExprStream& os, const Expr& e); 00291 Expr parseExprOp(const Expr& e); 00292 00293 //helper functions 00294 00295 //! Return the number of bits in the bitvector expression 00296 int BVSize(const Expr& e); 00297 00298 Expr rat(const Rational& r) { return getEM()->newRatExpr(r); } 00299 //!pads e to be of length len 00300 Expr pad(int len, const Expr& e); 00301 00302 bool comparebv(const Expr& e1, const Expr& e2); 00303 00304 //helper functions: functions to construct exprs 00305 Type newBitvectorType(int i) 00306 { return newBitvectorTypeExpr(i); } 00307 Expr newBitvectorTypePred(const Type& t, const Expr& e); 00308 Expr newBitvectorTypeExpr(int i); 00309 00310 Expr newBVAndExpr(const Expr& t1, const Expr& t2); 00311 Expr newBVAndExpr(const std::vector<Expr>& kids); 00312 00313 Expr newBVOrExpr(const Expr& t1, const Expr& t2); 00314 Expr newBVOrExpr(const std::vector<Expr>& kids); 00315 00316 Expr newBVXorExpr(const Expr& t1, const Expr& t2); 00317 Expr newBVXorExpr(const std::vector<Expr>& kids); 00318 00319 Expr newBVXnorExpr(const Expr& t1, const Expr& t2); 00320 Expr newBVXnorExpr(const std::vector<Expr>& kids); 00321 00322 Expr newBVNandExpr(const Expr& t1, const Expr& t2); 00323 Expr newBVNorExpr(const Expr& t1, const Expr& t2); 00324 Expr newBVCompExpr(const Expr& t1, const Expr& t2); 00325 00326 Expr newBVLTExpr(const Expr& t1, const Expr& t2); 00327 Expr newBVLEExpr(const Expr& t1, const Expr& t2); 00328 Expr newSXExpr(const Expr& t1, int len); 00329 Expr newBVIndexExpr(int kind, const Expr& t1, int len); 00330 Expr newBVSLTExpr(const Expr& t1, const Expr& t2); 00331 Expr newBVSLEExpr(const Expr& t1, const Expr& t2); 00332 00333 Expr newBVNegExpr(const Expr& t1); 00334 Expr newBVUminusExpr(const Expr& t1); 00335 Expr newBoolExtractExpr(const Expr& t1, int r); 00336 Expr newFixedLeftShiftExpr(const Expr& t1, int r); 00337 Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r); 00338 Expr newFixedRightShiftExpr(const Expr& t1, int r); 00339 Expr newConcatExpr(const Expr& t1, const Expr& t2); 00340 Expr newConcatExpr(const Expr& t1, const Expr& t2, const Expr& t3); 00341 Expr newConcatExpr(const std::vector<Expr>& kids); 00342 Expr newBVConstExpr(const std::string& s, int base = 2); 00343 Expr newBVConstExpr(const std::vector<bool>& bits); 00344 // Lorenzo's wrapper 00345 // as computeBVConst can not give the BV expr of a negative rational, 00346 // I use this wrapper to do that 00347 Expr signed_newBVConstExpr( Rational c, int bv_size); 00348 // end of Lorenzo's wrapper 00349 00350 // Construct BVCONST of length 'len', or the min. needed length when len=0. 00351 Expr newBVConstExpr(const Rational& r, int len = 0); 00352 Expr newBVZeroString(int r); 00353 Expr newBVOneString(int r); 00354 //! hi and low are bit indices 00355 Expr newBVExtractExpr(const Expr& e, 00356 int hi, int low); 00357 Expr newBVSubExpr(const Expr& t1, const Expr& t2); 00358 //! 'numbits' is the number of bits in the result 00359 Expr newBVPlusExpr(int numbits, const Expr& k1, const Expr& k2); 00360 //! 'numbits' is the number of bits in the result 00361 Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k); 00362 //! pads children and then builds plus expr 00363 Expr newBVPlusPadExpr(int bvLength, const std::vector<Expr>& k); 00364 Expr newBVMultExpr(int bvLength, 00365 const Expr& t1, const Expr& t2); 00366 Expr newBVMultExpr(int bvLength, const std::vector<Expr>& kids); 00367 Expr newBVMultPadExpr(int bvLength, 00368 const Expr& t1, const Expr& t2); 00369 Expr newBVMultPadExpr(int bvLength, const std::vector<Expr>& kids); 00370 Expr newBVUDivExpr(const Expr& t1, const Expr& t2); 00371 Expr newBVURemExpr(const Expr& t1, const Expr& t2); 00372 Expr newBVSDivExpr(const Expr& t1, const Expr& t2); 00373 Expr newBVSRemExpr(const Expr& t1, const Expr& t2); 00374 Expr newBVSModExpr(const Expr& t1, const Expr& t2); 00375 00376 // Accessors for expression parameters 00377 int getBitvectorTypeParam(const Expr& e); 00378 int getBitvectorTypeParam(const Type& t) 00379 { return getBitvectorTypeParam(t.getExpr()); } 00380 Type getTypePredType(const Expr& tp); 00381 const Expr& getTypePredExpr(const Expr& tp); 00382 int getSXIndex(const Expr& e); 00383 int getBVIndex(const Expr& e); 00384 int getBoolExtractIndex(const Expr& e); 00385 int getFixedLeftShiftParam(const Expr& e); 00386 int getFixedRightShiftParam(const Expr& e); 00387 int getExtractHi(const Expr& e); 00388 int getExtractLow(const Expr& e); 00389 int getBVPlusParam(const Expr& e); 00390 int getBVMultParam(const Expr& e); 00391 00392 unsigned getBVConstSize(const Expr& e); 00393 bool getBVConstValue(const Expr& e, int i); 00394 //!computes the integer value of a bitvector constant 00395 Rational computeBVConst(const Expr& e); 00396 //!computes the integer value of ~c+1 or BVUMINUS(c) 00397 Rational computeNegBVConst(const Expr& e); 00398 00399 int getMaxSize() { return d_maxLength; } 00400 00401 /*Beginning of Lorenzo PLatania's public methods*/ 00402 00403 bool isLinearTerm( const Expr& e ); 00404 void extract_vars( const Expr& e, std::vector<Expr>& vars ); 00405 // checks whether e can be solved in term 00406 bool canSolveFor( const Expr& term, const Expr& e ); 00407 00408 // evaluates the multipicative inverse 00409 Rational multiplicative_inverse(Rational r, int n_bits); 00410 00411 00412 /*End of Lorenzo PLatania's public methods*/ 00413 00414 std::vector<Theorem> additionalRewriteConstraints; 00415 00416 }; //end of class TheoryBitvector 00417 00418 00419 }//end of namespace CVC3 00420 #endif