93 if(
this == &th)
return *
this;
94 if(d_thm == th.
d_thm)
return *
this;
102 "Theorem::operator=: invariant violated");
113 "Theorem::operator=: invariant violated");
120 else if (d_thm != 0) {
121 exprValue()->decRefcount();
133 bool isAssump,
int scope) {
136 if (thm[0] == thm[1]) {
146 d_thm = ((intptr_t)tv)|0x1;
149 "Null proof in theorem:\n"+toString());
163 d_thm = ((long)tv)|0x1;
165 "Null proof in theorem:\n"+toString());
173 "Theorem(const Theorem&): refcount = "
177 }
else if (
d_thm != 0) {
193 "~Theorem(): refcount = "
202 else if (
d_thm != 0) {
269 (*i).getAssumptionsRec(assumptions);
282 for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
284 assumptions.push_back(negate ? (*i).negate() : *i);
297 assumptions.push_back(*
this);
303 if ((*i).isRefl() || (*i).isFlagged())
continue;
304 (*i).GetSatAssumptionsRec(assumptions);
314 if ((*i).isRefl() || (*i).isFlagged())
continue;
315 (*i).GetSatAssumptionsRec(assumptions);
321 vector<Expr>& congruences)
const
343 hyp.push_back(e[1].eqExpr(e[0]));
348 congruences.push_back(
Expr(
OR, hyp));
350 else if (e[0].isAtomicFormula() && !e[0].isEq()) {
351 hyp.push_back(!e[0]);
353 congruences.push_back(
Expr(
OR, hyp));
357 hyp.push_back(!e[1]);
358 congruences.push_back(
Expr(
OR, hyp));
364 (*i).getAssumptionsAndCongRec(assumptions, congruences);
371 vector<Expr>& congruences,
379 for(set<Expr>::iterator i=assumpSet.begin(), iend=assumpSet.end();
381 assumptions.push_back(negate ? (*i).negate() : *i);
454 if (
isRefl())
return false;
520 for (; it != iend; ++it) {
529 <<
"]@" <<
getScope() <<
"\tTheorem: {";
544 if (
isSubst()) cout <<
" [[Subst]]";
581 if(
isNull())
return os << name <<
"(Null)";
590 if(
thm()->d_tm->getFlags()[
"print-assump"].getBool()
594 os <<
"<assumptions>";
599 else os <<
"(being destructed)";
608 else os <<
"being destructed";
void setCachedValue(int value) const
Check if the flag attribute is set.
bool getExpandFlag() const
Check the "expand" attribute.
void setSubst() const
Set flag stating that theorem is an instance of substitution.
bool isAtomic() const
Test if e is atomic.
ExprValue * d_expr
The value. This is the only data member in this class.
Data structure of expressions in CVC3.
ExprManager * getEM() const
void clearAllFlags() const
Clear the flag attribute in all the theorems.
int getCachedValue() const
virtual const Expr & getExpr() const
void recursivePrint(int &i) const
int compare(const Expr &e1, const Expr &e2)
TheoremValue * thm() const
void pprintnodag() const
Pretty-print without dagifying.
virtual const Expr & getLHS() const
int incIndent(int n, bool permanent=false)
Increment the current transient indentation by n.
bool withAssumptions() const
bool isActive()
Check if the ExprManager is still active (clear() was not called)
void getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const
ExprValue * exprValue() const
void printnodag() const
Print the expression as AST without dagifying.
Expr eqExpr(const Expr &right) const
MemoryManager * getMM() const
#define DebugAssert(cond, str)
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Theorem & operator=(const Theorem &th)
virtual const Assumptions & getAssumptionsRef() const =0
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void setExpandFlag(bool val) const
Set the "expand" attribute.
int getCachedValue() const
Check if the flag attribute is set.
int getCachedValue(long ptr)
void getAssumptionsAndCongRec(std::set< Expr > &assumptions, std::vector< Expr > &congruences) const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
TheoremManager * getTM() const
Fetch the TheoremManager.
std::string toString() const
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
MemoryManager * getRWMM() const
void setLitFlag(bool val) const
Set the "literal" attribute.
int compareByPtr(const Theorem &t1, const Theorem &t2)
void pprintxnodag() const
bool isFlagged() const
Check if the flag attribute is set.
virtual const Expr & getRHS() const
Expr iffExpr(const Expr &right) const
unsigned getQuantLevel() const
Return quantification level for this theorem.
void setExpandFlag(long ptr, bool value)
bool getLitFlag(long ptr)
std::string int2string(int n)
unsigned getQuantLevelDebug() const
const Expr & getRHS() const
bool isAbsLiteral() const
Check if the theorem is a literal.
void incRefcount()
Increment reference counter.
void setCachedValue(long ptr, int value)
const Assumptions & getAssumptionsRef() const
unsigned d_refcount
How many pointers to this theorem value.
virtual void deleteData(void *d)=0
void getAssumptionsRec(std::set< Expr > &assumptions) const
void setLitFlag(bool val)
void GetSatAssumptionsRec(std::vector< Theorem > &assumptions) const
int indent() const
Get initial indentation.
void decRefcount()
Decrement reference counter.
virtual MemoryManager * getMM()=0
void getAssumptionsAndCong(std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const
ExprManager * d_em
Our expr. manager.
bool isRegisteredAtom() const
unsigned getQuantLevelDebug()
void setQuantLevel(unsigned level)
bool isAbsLiteral() const
Test if e is an abstract literal.
bool getExpandFlag(long ptr)
const Expr & getLHS() const
Iterator for the Assumptions: points to class Theorem.
void pprint() const
Pretty-print the expression.
void setCachedValue(int value)
bool isAtomicFormula() const
Test if e is an atomic formula.
bool isSubst() const
Is theorem an instance of substitution.
void GetSatAssumptions(std::vector< Theorem > &assumptions) const
void setExpandFlag(bool val)
static const Assumptions & emptyAssump()
TheoremManager * d_tm
Theorem Manager.
virtual bool isRewrite() const
bool getLitFlag() const
Check the "literal" attribute.
void setFlag() const
Set the flag attribute.
void setLitFlag(long ptr, bool value)