00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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 {
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,
00082 BVTOINT,
00083
00084 BVTYPEPRED
00085 } BVKinds;
00086
00087
00088
00089
00090
00091
00092
00093
00094
00095
00096
00097
00098
00099 class TheoryBitvector :public Theory {
00100 BitvectorProofRules* d_rules;
00101
00102 size_t d_bvConstExprIndex;
00103 size_t d_bvPlusExprIndex;
00104 size_t d_bvParameterExprIndex;
00105 size_t d_bvTypePredExprIndex;
00106
00107
00108 StatCounter d_bvDelayEq;
00109
00110 StatCounter d_bvAssertEq;
00111
00112 StatCounter d_bvDelayDiseq;
00113
00114 StatCounter d_bvAssertDiseq;
00115
00116 StatCounter d_bvTypePreds;
00117
00118 StatCounter d_bvDelayTypePreds;
00119
00120 StatCounter d_bvBitBlastEq;
00121
00122 StatCounter d_bvBitBlastDiseq;
00123
00124
00125
00126 const bool* d_booleanRWFlag;
00127
00128 const bool* d_boolExtractCacheFlag;
00129
00130 const bool* d_bv32Flag;
00131
00132 const bool* d_rewriteFlag;
00133
00134 const bool* d_concatRewriteFlag;
00135
00136 const bool* d_bvplusRewriteFlag;
00137
00138 const bool* d_rwBitBlastFlag;
00139
00140 const bool* d_cnfBitBlastFlag;
00141
00142 const bool* d_lhsMinusRhsFlag;
00143
00144 const bool* d_pushNegationFlag;
00145
00146
00147 CDMap<Expr,Theorem> d_bitvecCache;
00148
00149
00150
00151
00152 ExprMap<Theorem> d_pushNegCache;
00153
00154
00155 CDList<Theorem> d_eq;
00156
00157 CDO<size_t> d_eqIdx;
00158
00159 CDO<size_t> d_eqBlastIdx;
00160
00161 CDList<Theorem> d_diseq;
00162
00163 CDO<size_t> d_diseqIdx;
00164
00165 CDMap<Expr,bool> d_staleDB;
00166
00167 CDList<Theorem> d_tccs;
00168
00169 CDO<size_t> d_tccsIdx;
00170
00171 CDMap<Expr,Expr> d_sharedSubterms;
00172
00173 CDList<Expr> d_sharedSubtermsList;
00174
00175 CDMap<Expr, Theorem> d_typePredsCache;
00176
00177
00178
00179
00180 Expr d_bvZero;
00181
00182 Expr d_bvOne;
00183
00184 const Expr& bvZero() const { return d_bvZero; }
00185
00186 const Expr& bvOne() const { return d_bvOne; }
00187
00188
00189 int d_maxLength;
00190
00191
00192 CDO<unsigned> d_index1;
00193
00194
00195 Theorem bitBlastEqn(const Expr& e);
00196
00197 Theorem bitBlastDisEqn(const Theorem& e);
00198 public:
00199
00200 Theorem bitBlastTerm(const Expr& t, int bitPosition);
00201 private:
00202
00203 Theorem bitBlastIneqn(const Expr& e);
00204
00205
00206 Theorem padBVPlus(const Expr& e);
00207
00208 Theorem flattenBVPlus(const Expr& e);
00209
00210
00211 Theorem normalizeConcat(const Expr& e, bool useFind);
00212
00213 Theorem normalizeBVArith(const Expr& e, bool useFind);
00214
00215 Theorem normalizeConcat(const Theorem& t, bool useFind) {
00216 return transitivityRule(t, normalizeConcat(t.getRHS(), useFind));
00217 }
00218
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
00229 virtual Theorem simplifyOp(const Expr& e);
00230
00231
00232
00233 Theorem rewriteConst(const Expr& e);
00234
00235 Theorem rewriteBV(const Expr& e, bool useFind);
00236
00237 Theorem rewriteBV(const Expr& e, int n, bool useFind);
00238
00239 Theorem rewriteBV(const Theorem& t, int n, bool useFind) {
00240 return transitivityRule(t, rewriteBV(t.getRHS(), n, useFind));
00241 }
00242
00243 Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, bool useFind);
00244
00245 Theorem rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n,
00246 bool useFind);
00247
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
00254 Theorem rewriteBoolean(const Expr& e);
00255
00256
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
00267
00268 BitvectorProofRules* createProofRules();
00269 Theorem pushNegationRec(const Expr& e, bool neg);
00270
00271
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
00291 Expr rat(const Rational& r) { return getEM()->newRatExpr(r); }
00292
00293 Expr pad(int len, const Expr& e);
00294
00295 bool comparebv(const Expr& e1, const Expr& e2);
00296
00297
00298 int BVSize(const Expr& e);
00299
00300
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
00341 Expr newBVConstExpr(const Rational& r, int len = 0);
00342 Expr newBVZeroString(int r);
00343 Expr newBVOneString(int r);
00344
00345 Expr newBVExtractExpr(const Expr& e,
00346 int hi, int low);
00347 Expr newBVSubExpr(const Expr& t1, const Expr& t2);
00348
00349 Expr newBVPlusExpr(int numbits, const std::vector<Expr>& k);
00350
00351 Expr newBVMultExpr(int bvLength,
00352 const Expr& t1, const Expr& t2);
00353
00354
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
00373 Rational computeBVConst(const Expr& e);
00374
00375 Rational computeNegBVConst(const Expr& e);
00376
00377 int getMaxSize() { return d_maxLength; }
00378
00379 };
00380
00381
00382 Rational computeBVConst(const Expr& e);
00383
00384 }
00385 #endif