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;
252 bool refutes(
const Expr& e)
const
255 (e.
isNot() && e[0] == getExpr()) ||
256 (getExpr().isNot() && getExpr()[0] == e);
259 bool proves(
const Expr& e)
const
261 return getExpr() == e;
264 bool matches(
const Expr& e)
const
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>