00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047 #ifndef _cvc3__expr_h_
00048 #include "expr.h"
00049 #endif
00050
00051 #ifndef _cvc3__theorem_h_
00052 #define _cvc3__theorem_h_
00053
00054 #include "os.h"
00055 #include "proof.h"
00056 #include "assumptions.h"
00057
00058 namespace CVC3 {
00059
00060
00061 class TheoremManager;
00062 class TheoremValue;
00063 class Assumptions;
00064
00065
00066
00067
00068
00069
00070
00071
00072
00073
00074
00075
00076
00077 class CVC_DLL Theorem {
00078 private:
00079
00080
00081 friend class TheoremProducer;
00082
00083 friend class Theorem3;
00084
00085 friend class RegTheoremValue;
00086 friend class RWTheoremValue;
00087
00088
00089
00090
00091 union {
00092 intptr_t d_thm;
00093 ExprValue* d_expr;
00094 };
00095
00096
00097 friend int compare(const Theorem& t1, const Theorem& t2);
00098
00099 friend int compare(const Theorem& t1, const Expr& e2);
00100
00101 friend int compareByPtr(const Theorem& t1, const Theorem& t2);
00102
00103 friend bool operator==(const Theorem& t1, const Theorem& t2)
00104 { return (compare(t1, t2)==0); }
00105
00106 friend bool operator!=(const Theorem& t1, const Theorem& t2)
00107 { return (compare(t1, t2) != 0); }
00108
00109
00110 Theorem(TheoremValue* thm) :d_thm(((intptr_t)thm) | 0x1) {}
00111
00112
00113 Theorem(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
00114 const Proof& pf, bool isAssump = false, int scope = -1);
00115
00116
00117
00118
00119
00120 Theorem(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00121 const Assumptions& assump, const Proof& pf, bool isAssump = false,
00122 int scope = -1);
00123
00124
00125 Theorem(const Expr& e);
00126
00127 void recursivePrint(int& i) const;
00128 void getAssumptionsRec(std::set<Expr>& assumptions) const;
00129
00130 ExprValue* exprValue() const { return d_expr; }
00131 TheoremValue* thm() const { return (TheoremValue*)(d_thm & (~(0x1))); }
00132
00133 public:
00134
00135
00136
00137
00138 void printDebug() const {
00139 clearAllFlags();
00140 setCachedValue(0);
00141 setFlag();
00142 int i = 1;
00143 recursivePrint(i);
00144 }
00145
00146
00147
00148
00149 Theorem(): d_thm(0) { }
00150
00151 Theorem(const Theorem &th);
00152
00153 Theorem& operator=(const Theorem &th);
00154
00155
00156 ~Theorem();
00157
00158
00159 bool withProof() const;
00160 bool withAssumptions() const;
00161
00162 bool isNull() const { return d_thm == 0; }
00163
00164
00165 bool isRewrite() const;
00166
00167 bool isAssump() const;
00168
00169 bool isRefl() const { return d_thm && !(d_thm & 0x1); }
00170
00171
00172 Expr getExpr() const;
00173 const Expr& getLHS() const;
00174 const Expr& getRHS() const;
00175
00176
00177
00178
00179 void getLeafAssumptions(std::vector<Expr>& assumptions,
00180 bool negate = false) const;
00181 const Assumptions& getAssumptionsRef() const;
00182
00183
00184 Proof getProof() const;
00185
00186
00187 int getScope() const;
00188
00189 unsigned getQuantLevel() const;
00190
00191 void setQuantLevel(unsigned level);
00192
00193
00194 size_t hash() const;
00195
00196
00197 std::string toString() const;
00198
00199
00200 void printx() const;
00201 void printxnodag() const;
00202 void pprintx() const;
00203 void pprintxnodag() const;
00204
00205 void print() const;
00206
00207
00208
00209
00210
00211
00212
00213
00214 bool isFlagged() const;
00215
00216 void clearAllFlags() const;
00217
00218 void setFlag() const;
00219
00220
00221 void setExpandFlag(bool val) const;
00222
00223 bool getExpandFlag() const;
00224
00225
00226
00227 void setLitFlag(bool val) const;
00228
00229
00230
00231 bool getLitFlag() const;
00232
00233 bool isAbsLiteral() const;
00234
00235 bool refutes(const Expr& e) const
00236 {
00237 return
00238 (e.isNot() && e[0] == getExpr()) ||
00239 (getExpr().isNot() && getExpr()[0] == e);
00240 }
00241
00242 bool proves(const Expr& e) const
00243 {
00244 return getExpr() == e;
00245 }
00246
00247 bool matches(const Expr& e) const
00248 {
00249 return proves(e) || refutes(e);
00250 }
00251
00252 void setCachedValue(int value) const;
00253 int getCachedValue() const;
00254
00255
00256
00257
00258 std::ostream& print(std::ostream& os, const std::string& name) const;
00259
00260 friend std::ostream& operator<<(std::ostream& os, const Theorem& t) {
00261 return t.print(os, "Theorem");
00262 }
00263
00264 static bool TheoremEq(const Theorem& t1, const Theorem& t2)
00265 {
00266 DebugAssert(!t1.isNull() && !t2.isNull(),
00267 "AssumptionsValue() Null Theorem passed to constructor");
00268 return t1 == t2;
00269 }
00270 };
00271
00272
00273
00274
00275
00276
00277
00278
00279
00280
00281
00282
00283
00284
00285
00286
00287
00288
00289
00290
00291 class Theorem3 {
00292 private:
00293
00294
00295 friend class TheoremProducer;
00296
00297 Theorem d_thm;
00298
00299 friend bool operator==(const Theorem3& t1, const Theorem3& t2) {
00300 return t1.d_thm == t2.d_thm;
00301 }
00302 friend bool operator!=(const Theorem3& t1, const Theorem3& t2) {
00303 return t1.d_thm != t2.d_thm;
00304 }
00305
00306
00307
00308 Theorem3(TheoremManager* tm, const Expr &thm, const Assumptions& assump,
00309 const Proof& pf, bool isAssump = false, int scope = -1)
00310 : d_thm(tm, thm, assump, pf, isAssump, scope) { }
00311
00312
00313
00314
00315 Theorem3(TheoremManager* tm, const Expr& lhs, const Expr& rhs,
00316 const Assumptions& assump, const Proof& pf)
00317 : d_thm(tm, lhs, rhs, assump, pf) { }
00318
00319 public:
00320
00321
00322
00323
00324 void printDebug() const { d_thm.printDebug(); }
00325
00326
00327
00328
00329 Theorem3() { }
00330
00331
00332 virtual ~Theorem3() { }
00333
00334 bool isNull() const { return d_thm.isNull(); }
00335
00336
00337 bool isRewrite() const { return d_thm.isRewrite(); }
00338 bool isAssump() const { return d_thm.isAssump(); }
00339
00340
00341 Expr getExpr() const { return d_thm.getExpr(); }
00342 const Expr& getLHS() const { return d_thm.getLHS(); }
00343 const Expr& getRHS() const { return d_thm.getRHS(); }
00344
00345
00346
00347
00348 const Assumptions& getAssumptionsRef() const {
00349 return d_thm.getAssumptionsRef();
00350 }
00351
00352
00353 Proof getProof() const { return d_thm.getProof(); }
00354
00355
00356
00357 int getScope() const { return d_thm.getScope(); }
00358
00359
00360 bool withProof() const { return d_thm.withProof(); }
00361 bool withAssumptions() const { return d_thm.withAssumptions(); }
00362
00363
00364 std::string toString() const;
00365
00366
00367 void printx() const { d_thm.printx(); }
00368 void print() const { d_thm.print(); }
00369
00370
00371 bool isAbsLiteral() const { return d_thm.isAbsLiteral(); }
00372
00373 friend std::ostream& operator<<(std::ostream& os, const Theorem3& t) {
00374 return t.d_thm.print(os, "Theorem3");
00375 }
00376 };
00377
00378
00379 class TheoremLess {
00380 public:
00381 bool operator()(const Theorem& t1, const Theorem& t2) const {
00382 return (compareByPtr(t1, t2) < 0);
00383 }
00384 };
00385 typedef std::map<Theorem,bool, TheoremLess> TheoremMap;
00386
00387 inline std::string Theorem::toString() const {
00388 std::ostringstream ss;
00389 ss << (*this);
00390 return ss.str();
00391 }
00392
00393 inline std::string Theorem3::toString() const {
00394 std::ostringstream ss;
00395 ss << (*this);
00396 return ss.str();
00397 }
00398
00399
00400
00401
00402
00403
00404
00405
00406
00407
00408
00409
00410 inline bool operator<(const Theorem& t1, const Theorem& t2)
00411 { return compare(t1, t2) < 0; }
00412 inline bool operator<=(const Theorem& t1, const Theorem& t2)
00413 { return compare(t1, t2) <= 0; }
00414 inline bool operator>(const Theorem& t1, const Theorem& t2)
00415 { return compare(t1, t2) > 0; }
00416 inline bool operator>=(const Theorem& t1, const Theorem& t2)
00417 { return compare(t1, t2) >= 0; }
00418
00419 }
00420
00421 #include "hash_fun.h"
00422 namespace Hash
00423 {
00424
00425 template<> struct hash<CVC3::Theorem>
00426 {
00427 size_t operator()(const CVC3::Theorem& e) const { return e.hash(); }
00428 };
00429
00430 }
00431
00432 #endif