1 /*****************************************************************************/ 2 /*! 3 * \file theory_bitvector.h 4 * 5 * Author: Vijay Ganesh 6 * 7 * Created: Wed May 05 18:34:55 PDT 2004 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 */ 19 /*****************************************************************************/ 20 21 #ifndef _cvc3__include__theory_bitvector_h_ 22 #define _cvc3__include__theory_bitvector_h_ 23 24 #include "theory_core.h" 25 #include "statistics.h" 26 27 namespace CVC3 { 28 29 class VCL; 30 class BitvectorProofRules; 31 32 typedef enum { //some new BV kinds 33 // New constants 34 BVCONST = 80, 35 36 BITVECTOR = 8000, 37 38 CONCAT, 39 EXTRACT, 40 BOOLEXTRACT, 41 42 LEFTSHIFT, 43 CONST_WIDTH_LEFTSHIFT, 44 RIGHTSHIFT, 45 BVSHL, 46 BVLSHR, 47 BVASHR, 48 SX, 49 BVREPEAT, 50 BVZEROEXTEND, 51 BVROTL, 52 BVROTR, 53 54 BVAND, 55 BVOR, 56 BVXOR, 57 BVXNOR, 58 BVNEG, 59 BVNAND, 60 BVNOR, 61 BVCOMP, 62 63 BVUMINUS, 64 BVPLUS, 65 BVSUB, 66 BVMULT, 67 BVUDIV, 68 BVSDIV, 69 BVUREM, 70 BVSREM, 71 BVSMOD, 72 73 BVLT, 74 BVLE, 75 BVGT, 76 BVGE, 77 BVSLT, 78 BVSLE, 79 BVSGT, 80 BVSGE, 81 82 INTTOBV, // Not implemented yet 83 BVTOINT, // Not implemented yet 84 // A wrapper for delaying the construction of type predicates 85 BVTYPEPRED 86 } BVKinds; 87 88 /*****************************************************************************/ 89 /*! 90 *\class TheoryBitvector 91 *\ingroup Theories 92 *\brief Theory of bitvectors of known length \ 93 * (operations include: @,[i:j],[i],+,.,BVAND,BVNEG) 94 * 95 * Author: Vijay Ganesh 96 * 97 * Created:Wed May 5 15:35:07 PDT 2004 98 */ 99 /*****************************************************************************/ 100 class TheoryBitvector :public Theory { 101 BitvectorProofRules* d_rules; 102 //! MemoryManager index for BVConstExpr subclass 103 size_t d_bvConstExprIndex; 104 size_t d_bvPlusExprIndex; 105 size_t d_bvParameterExprIndex; 106 size_t d_bvTypePredExprIndex; 107 108 //! counts delayed asserted equalities 109 StatCounter d_bvDelayEq; 110 //! counts asserted equalities 111 StatCounter d_bvAssertEq; 112 //! counts delayed asserted disequalities 113 StatCounter d_bvDelayDiseq; 114 //! counts asserted disequalities 115 StatCounter d_bvAssertDiseq; 116 //! counts type predicates 117 StatCounter d_bvTypePreds; 118 //! counts delayed type predicates 119 StatCounter d_bvDelayTypePreds; 120 //! counts bitblasted equalities 121 StatCounter d_bvBitBlastEq; 122 //! counts bitblasted disequalities 123 StatCounter d_bvBitBlastDiseq; 124 125 //! boolean on the fly rewrite flag 126 const bool* d_booleanRWFlag; 127 //! bool extract cache flag 128 const bool* d_boolExtractCacheFlag; 129 //! flag which indicates that all arithmetic is 32 bit with no overflow 130 const bool* d_bv32Flag; 131 132 //! Cache for storing the results of the bitBlastTerm function 133 CDMap<Expr,Theorem> d_bitvecCache; 134 135 //! Cache for pushNegation(). it is ok that this is cache is 136 //ExprMap. it is cleared for each call of pushNegation. Does not add 137 //value across calls of pushNegation 138 ExprMap<Theorem> d_pushNegCache; 139 140 //! Backtracking queue for equalities 141 CDList<Theorem> d_eq; 142 //! Backtracking queue for unsolved equalities 143 CDList<Theorem> d_eqPending; 144 //! Index to current position in d_eqPending 145 CDO<unsigned int> d_eq_index; 146 //! Backtracking queue for all other assertions 147 CDList<Theorem> d_bitblast; 148 //! Index to current position in d_bitblast 149 CDO<unsigned int> d_bb_index; 150 //! Backtracking database of subterms of shared terms 151 CDMap<Expr,Expr> d_sharedSubterms; 152 //! Backtracking database of subterms of shared terms 153 CDList<Expr> d_sharedSubtermsList; 154 155 //! Constant 1-bit bit-vector 0bin0 156 Expr d_bvZero; 157 //! Constant 1-bit bit-vector 0bin0 158 Expr d_bvOne; 159 //! Return cached constant 0bin0 bvZero()160 const Expr& bvZero() const { return d_bvZero; } 161 //! Return cached constant 0bin1 bvOne()162 const Expr& bvOne() const { return d_bvOne; } 163 164 //! Max size of any bitvector we've seen 165 int d_maxLength; 166 167 //! Used in checkSat 168 CDO<unsigned> d_index1; 169 CDO<unsigned> d_index2; 170 171 //! functions which implement the DP strategy for bitblasting 172 Theorem bitBlastEqn(const Expr& e); 173 //! bitblast disequation 174 Theorem bitBlastDisEqn(const Theorem& notE); 175 //! function which implements the DP strtagey to bitblast Inequations 176 Theorem bitBlastIneqn(const Expr& e); 177 //! functions which implement the DP strategy for bitblasting 178 Theorem bitBlastTerm(const Expr& t, int bitPosition); 179 180 // //! strategy fucntions for BVPLUS NORMAL FORM 181 // Theorem padBVPlus(const Expr& e); 182 // //! strategy fucntions for BVPLUS NORMAL FORM 183 // Theorem flattenBVPlus(const Expr& e); 184 185 // //! Implementation of the concatenation normal form 186 // Theorem normalizeConcat(const Expr& e, bool useFind); 187 // //! Implementation of the n-bit arithmetic normal form 188 // Theorem normalizeBVArith(const Expr& e, bool useFind); 189 // //! Helper method for composing normalizations 190 // Theorem normalizeConcat(const Theorem& t, bool useFind) { 191 // return transitivityRule(t, normalizeConcat(t.getRHS(), useFind)); 192 // } 193 // //! Helper method for composing normalizations 194 // Theorem normalizeBVArith(const Theorem& t, bool useFind) { 195 // return transitivityRule(t, normalizeBVArith(t.getRHS(), useFind)); 196 // } 197 198 // Theorem signExtendBVLT(const Expr& e, int len, bool useFind); 199 200 public: 201 Theorem pushNegationRec(const Expr& e); 202 private: 203 Theorem pushNegation(const Expr& e); 204 205 //! Top down simplifier 206 virtual Theorem simplifyOp(const Expr& e); 207 208 //! Internal rewrite method for constants 209 // Theorem rewriteConst(const Expr& e); 210 211 //! Main rewrite method (implements the actual rewrites) 212 Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n = 1); 213 214 //! Rewrite children 'n' levels down (n==1 means "only the top level") 215 Theorem rewriteBV(const Expr& e, int n = 1); 216 217 // Shortcuts for theorems 218 Theorem rewriteBV(const Theorem& t, ExprMap<Theorem>& cache, int n = 1) { 219 return transitivityRule(t, rewriteBV(t.getRHS(), cache, n)); 220 } 221 Theorem rewriteBV(const Theorem& t, int n = 1) { 222 return transitivityRule(t, rewriteBV(t.getRHS(), n)); 223 } 224 225 //! rewrite input boolean expression e to a simpler form 226 Theorem rewriteBoolean(const Expr& e); 227 228 /*Beginning of Lorenzo PLatania's methods*/ 229 230 Expr multiply_coeff( Rational mult_inv, const Expr& e); 231 232 // extract the min value from a Rational list 233 int min(std::vector<Rational> list); 234 235 // evaluates the gcd of two integer coefficients 236 // int gcd(int c1, int c2); 237 238 // converts a bv constant to an integer 239 // int bv2int(const Expr& e); 240 241 // return the odd coefficient of a leaf for which we can solve the 242 // equation, or zero if no one has been found 243 Rational Odd_coeff( const Expr& e ); 244 245 246 247 // returns 1 if e is a linear term 248 int check_linear( const Expr &e ); 249 250 bool isTermIn(const Expr& e1, const Expr& e2); 251 252 Theorem updateSubterms( const Expr& d ); 253 254 // returns how many times "term" appears in "e" 255 int countTermIn( const Expr& term, const Expr& e); 256 257 Theorem simplifyPendingEq(const Theorem& thm, int maxEffort); 258 Theorem generalBitBlast( const Theorem& thm ); 259 /*End of Lorenzo PLatania's methods*/ 260 261 ExprStream& printSmtLibShared(ExprStream& os, const Expr& e); 262 263 public: 264 TheoryBitvector(TheoryCore* core); 265 ~TheoryBitvector(); 266 267 ExprMap<Expr> d_bvPlusCarryCacheLeftBV; 268 ExprMap<Expr> d_bvPlusCarryCacheRightBV; 269 270 // Trusted method that creates the proof rules class (used in constructor). 271 // Implemented in bitvector_theorem_producer.cpp 272 BitvectorProofRules* createProofRules(); 273 274 // Theory interface 275 void addSharedTerm(const Expr& e); 276 void assertFact(const Theorem& e); 277 void assertTypePred(const Expr& e, const Theorem& pred); 278 void checkSat(bool fullEffort); 279 Theorem rewrite(const Expr& e); 280 Theorem rewriteAtomic(const Expr& e); 281 void setup(const Expr& e); 282 void update(const Theorem& e, const Expr& d); 283 Theorem solve(const Theorem& e); 284 void checkType(const Expr& e); 285 Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 286 bool enumerate, bool computeSize); 287 void computeType(const Expr& e); 288 void computeModelTerm(const Expr& e, std::vector<Expr>& v); 289 void computeModel(const Expr& e, std::vector<Expr>& vars); 290 Expr computeTypePred(const Type& t, const Expr& e); 291 Expr computeTCC(const Expr& e); 292 ExprStream& print(ExprStream& os, const Expr& e); 293 Expr parseExprOp(const Expr& e); 294 295 //helper functions 296 297 //! Return the number of bits in the bitvector expression 298 int BVSize(const Expr& e); 299 rat(const Rational & r)300 Expr rat(const Rational& r) { return getEM()->newRatExpr(r); } 301 //!pads e to be of length len 302 Expr pad(int len, const Expr& e); 303 304 bool comparebv(const Expr& e1, const Expr& e2); 305 306 //helper functions: functions to construct exprs newBitvectorType(int i)307 Type newBitvectorType(int i) 308 { return newBitvectorTypeExpr(i); } 309 Expr newBitvectorTypePred(const Type& t, const Expr& e); 310 Expr newBitvectorTypeExpr(int i); 311 312 Expr newBVAndExpr(const Expr& t1, const Expr& t2); 313 Expr newBVAndExpr(const std::vector<Expr>& kids); 314 315 Expr newBVOrExpr(const Expr& t1, const Expr& t2); 316 Expr newBVOrExpr(const std::vector<Expr>& kids); 317 318 Expr newBVXorExpr(const Expr& t1, const Expr& t2); 319 Expr newBVXorExpr(const std::vector<Expr>& kids); 320 321 Expr newBVXnorExpr(const Expr& t1, const Expr& t2); 322 Expr newBVXnorExpr(const std::vector<Expr>& kids); 323 324 Expr newBVNandExpr(const Expr& t1, const Expr& t2); 325 Expr newBVNorExpr(const Expr& t1, const Expr& t2); 326 Expr newBVCompExpr(const Expr& t1, const Expr& t2); 327 328 Expr newBVLTExpr(const Expr& t1, const Expr& t2); 329 Expr newBVLEExpr(const Expr& t1, const Expr& t2); 330 Expr newSXExpr(const Expr& t1, int len); 331 Expr newBVIndexExpr(int kind, const Expr& t1, int len); 332 Expr newBVSLTExpr(const Expr& t1, const Expr& t2); 333 Expr newBVSLEExpr(const Expr& t1, const Expr& t2); 334 335 Expr newBVNegExpr(const Expr& t1); 336 Expr newBVUminusExpr(const Expr& t1); 337 Expr newBoolExtractExpr(const Expr& t1, int r); 338 Expr newFixedLeftShiftExpr(const Expr& t1, int r); 339 Expr newFixedConstWidthLeftShiftExpr(const Expr& t1, int r); 340 Expr newFixedRightShiftExpr(const Expr& t1, int r); 341 Expr newConcatExpr(const Expr& t1, const Expr& t2); 342 Expr newConcatExpr(const Expr& t1, const Expr& t2, const Expr& t3); 343 Expr newConcatExpr(const std::vector<Expr>& kids); 344 Expr newBVConstExpr(const std::string& s, int base = 2); 345 Expr newBVConstExpr(const std::vector<bool>& bits); 346 // Lorenzo's wrapper 347 // as computeBVConst can not give the BV expr of a negative rational, 348 // I use this wrapper to do that 349 Expr signed_newBVConstExpr( Rational c, int bv_size); 350 // end of Lorenzo's wrapper 351 352 // Construct BVCONST of length 'len', or the min. needed length when len=0. 353 Expr newBVConstExpr(const Rational& r, int len = 0); 354 Expr newBVZeroString(int r); 355 Expr newBVOneString(int r); 356 //! hi and low are bit indices 357 Expr newBVExtractExpr(const Expr& e, 358 int hi, int low); 359 Expr newBVSubExpr(const Expr& t1, const Expr& t2); 360 //! 'numbits' is the number of bits in the result 361 Expr newBVPlusExpr(int numbits, const Expr& k1, const Expr& k2); 362 //! 'numbits' is the number of bits in the result 363 Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k); 364 //! pads children and then builds plus expr 365 Expr newBVPlusPadExpr(int bvLength, const std::vector<Expr>& k); 366 Expr newBVMultExpr(int bvLength, 367 const Expr& t1, const Expr& t2); 368 Expr newBVMultExpr(int bvLength, const std::vector<Expr>& kids); 369 Expr newBVMultPadExpr(int bvLength, 370 const Expr& t1, const Expr& t2); 371 Expr newBVMultPadExpr(int bvLength, const std::vector<Expr>& kids); 372 Expr newBVUDivExpr(const Expr& t1, const Expr& t2); 373 Expr newBVURemExpr(const Expr& t1, const Expr& t2); 374 Expr newBVSDivExpr(const Expr& t1, const Expr& t2); 375 Expr newBVSRemExpr(const Expr& t1, const Expr& t2); 376 Expr newBVSModExpr(const Expr& t1, const Expr& t2); 377 378 // Accessors for expression parameters 379 int getBitvectorTypeParam(const Expr& e); getBitvectorTypeParam(const Type & t)380 int getBitvectorTypeParam(const Type& t) 381 { return getBitvectorTypeParam(t.getExpr()); } 382 Type getTypePredType(const Expr& tp); 383 const Expr& getTypePredExpr(const Expr& tp); 384 int getSXIndex(const Expr& e); 385 int getBVIndex(const Expr& e); 386 int getBoolExtractIndex(const Expr& e); 387 int getFixedLeftShiftParam(const Expr& e); 388 int getFixedRightShiftParam(const Expr& e); 389 int getExtractHi(const Expr& e); 390 int getExtractLow(const Expr& e); 391 int getBVPlusParam(const Expr& e); 392 int getBVMultParam(const Expr& e); 393 394 unsigned getBVConstSize(const Expr& e); 395 bool getBVConstValue(const Expr& e, int i); 396 //!computes the integer value of a bitvector constant 397 Rational computeBVConst(const Expr& e); 398 //!computes the integer value of ~c+1 or BVUMINUS(c) 399 Rational computeNegBVConst(const Expr& e); 400 getMaxSize()401 int getMaxSize() { return d_maxLength; } 402 403 /*Beginning of Lorenzo PLatania's public methods*/ 404 405 bool isLinearTerm( const Expr& e ); 406 void extract_vars( const Expr& e, std::vector<Expr>& vars ); 407 // checks whether e can be solved in term 408 bool canSolveFor( const Expr& term, const Expr& e ); 409 410 // evaluates the multipicative inverse 411 Rational multiplicative_inverse(Rational r, int n_bits); 412 413 414 /*End of Lorenzo PLatania's public methods*/ 415 416 std::vector<Theorem> additionalRewriteConstraints; 417 418 }; //end of class TheoryBitvector 419 420 421 }//end of namespace CVC3 422 #endif 423