47 #ifndef _cvc3__expr_h_
51 #ifndef _cvc3__theorem_h_
52 #define _cvc3__theorem_h_
103 {
return (
compare(t1, t2)==0); }
106 {
return (
compare(t1, t2) != 0); }
113 const Proof& pf,
bool isAssump =
false,
int scope = -1);
126 void recursivePrint(
int& i)
const;
127 void getAssumptionsRec(std::set<Expr>& assumptions)
const;
128 void getAssumptionsAndCongRec(std::set<Expr>& assumptions,
129 std::vector<Expr>& congruences)
const;
130 void GetSatAssumptionsRec(std::vector<Theorem>& assumptions)
const;
161 bool withProof()
const;
162 bool withAssumptions()
const;
164 bool isNull()
const {
return d_thm == 0; }
167 bool isRewrite()
const;
169 bool isAssump()
const;
171 bool isRefl()
const {
return d_thm && !(d_thm & 0x1); }
174 Expr getExpr()
const;
175 const Expr& getLHS()
const;
176 const Expr& getRHS()
const;
178 void GetSatAssumptions(std::vector<Theorem>& assumptions)
const;
185 void getLeafAssumptions(std::vector<Expr>& assumptions,
186 bool negate =
false)
const;
188 void getAssumptionsAndCong(std::vector<Expr>& assumptions,
189 std::vector<Expr>& congruences,
190 bool negate =
false)
const;
194 Proof getProof()
const;
197 int getScope()
const;
199 unsigned getQuantLevel()
const;
201 unsigned getQuantLevelDebug()
const;
204 void setQuantLevel(
unsigned level);
210 std::string toString()
const;
214 void printxnodag()
const;
215 void pprintx()
const;
216 void pprintxnodag()
const;
227 bool isFlagged()
const;
229 void clearAllFlags()
const;
231 void setFlag()
const;
234 void setSubst()
const;
236 bool isSubst()
const;
238 void setExpandFlag(
bool val)
const;
240 bool getExpandFlag()
const;
244 void setLitFlag(
bool val)
const;
248 bool getLitFlag()
const;
250 bool isAbsLiteral()
const;
255 (e.
isNot() && e[0] == getExpr()) ||
256 (getExpr().isNot() && getExpr()[0] == e);
261 return getExpr() == e;
266 return proves(e) || refutes(e);
269 void setCachedValue(
int value)
const;
270 int getCachedValue()
const;
275 std::ostream& print(std::ostream& os,
const std::string& name)
const;
278 return t.
print(os,
"Theorem");
284 "AssumptionsValue() Null Theorem passed to constructor");
334 :
d_thm(tm, lhs, rhs, assump, pf) { }
405 std::ostringstream ss;
411 std::ostringstream ss;
428 {
return compare(t1, t2) < 0; }
430 {
return compare(t1, t2) <= 0; }
432 {
return compare(t1, t2) > 0; }
434 {
return compare(t1, t2) >= 0; }
442 template<>
struct hash<CVC3::Theorem>
Data structure of expressions in CVC3.
bool withAssumptions() const
std::map< Theorem, bool, TheoremLess > TheoremMap
friend std::ostream & operator<<(std::ostream &os, const Theorem3 &t)
bool operator<=(const Expr &e1, const Expr &e2)
int compare(const Expr &e1, const Expr &e2)
TheoremValue * thm() const
static bool TheoremEq(const Theorem &t1, const Theorem &t2)
bool withAssumptions() const
ExprValue * exprValue() const
Theorem(TheoremValue *thm)
Constructor only used by TheoremValue for assumptions.
bool proves(const Expr &e) const
Check if the flag attribute is set.
#define DebugAssert(cond, str)
bool operator>(const Expr &e1, const Expr &e2)
bool matches(const Expr &e) const
Check if the flag attribute is set.
bool refutes(const Expr &e) const
Check if the flag attribute is set.
friend bool operator==(const Theorem3 &t1, const Theorem3 &t2)
std::string toString() const
friend bool operator!=(const Theorem &t1, const Theorem &t2)
Disequality is w.r.t. compare()
friend bool operator==(const Theorem &t1, const Theorem &t2)
Equality is w.r.t. compare()
std::string toString() const
int compareByPtr(const Theorem &t1, const Theorem &t2)
Abstraction over different operating systems.
const Expr & getRHS() const
bool isAbsLiteral() const
Check if the theorem is a literal.
Theorem3(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
const Assumptions & getAssumptionsRef() const
bool operator<(const Expr &e1, const Expr &e2)
size_t operator()(const CVC3::Theorem &e) const
bool operator>=(const Expr &e1, const Expr &e2)
bool operator()(const Theorem &t1, const Theorem &t2) const
"Less" comparator for theorems by TheoremValue pointers
const Expr & getRHS() const
Theorem3(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
bool isAbsLiteral() const
Check if the theorem is a literal.
Definition of the API to expression package. See class Expr for details.
const Expr & getLHS() const
const Expr & getLHS() const
The base class for holding the actual data in expressions.
friend bool operator!=(const Theorem3 &t1, const Theorem3 &t2)
friend std::ostream & operator<<(std::ostream &os, const Theorem &t)
const Assumptions & getAssumptionsRef() const