45 #ifndef _cvc3__theorem_value_h_
46 #define _cvc3__theorem_value_h_
118 FatalAssert(
false,
"TheoremValue() copy constructor called");
121 FatalAssert(
false,
"TheoremValue assignment operator called");
301 "TheoremValue::getLHS() called on non-rewrite theorem:\n"
308 "TheoremValue::getRHS() called on non-rewrite theorem:\n"
322 "Thm::TheoremValue::~TheoremValue(): refcount != 0.");)
374 if (!d_assump.empty()) {
387 TRACE(
"quantlevel",
"empty assumptions found ", thm ,
"");
401 d_assump.getFirst().d_thm = 0;
414 mm->deleteData(pMem);
417 void operator delete(
void* d) { }
461 if (!assump.
empty()) {
476 TRACE(
"quantlevel",
"RW empty assup found lhs << " , d_lhs,
"" );
477 TRACE(
"quantlevel",
"RW empty assup found rhs >> " , d_rhs,
"" );
490 :
TheoremValue(tm,
Expr(), pf, isAssump), d_lhs(lhs), d_rhs(rhs), d_assump(NULL)
491 { init(assump, scope); }
497 :
TheoremValue(tm, thm, pf, isAssump), d_lhs(thm[0]), d_rhs(thm[1]), d_assump(NULL)
498 { init(assump, scope); }
505 *pexpr = isBool ? d_lhs.
iffExpr(d_rhs) : d_lhs.
eqExpr(d_rhs);
520 d_assump->getFirst().d_thm = 0;
522 if (d_assump)
delete d_assump;
527 if (d_assump)
return *d_assump;
538 mm->deleteData(pMem);
541 void operator delete(
void* d) { }
bool d_expand
whether it should this be expanded in graph traversal
int d_cachedValue
Temporary cache used during traversals.
unsigned findQuantLevelDebug()
std::string toString() const
Data structure of expressions in CVC3.
int getCachedValue() const
virtual const Expr & getExpr() const
virtual const Expr & getLHS() const
bool d_clauselit
whether it belongs to the conflict clause
TheoremValue(TheoremManager *tm, const Expr &thm, const Proof &pf, bool isAssump)
Expr eqExpr(const Expr &right) const
MemoryManager * getMM() const
Expr d_thm
The expression representing a theorem.
#define DebugAssert(cond, str)
virtual const Assumptions & getAssumptionsRef() const =0
RegTheoremValue(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
bool d_isSubst
whether this theorem was generated by substitution
const Expr & getExpr() const
Proof d_proof
Proof of the theorem.
RWTheoremValue(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
ContextManager * getCM() const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
std::string toString() const
Print the expression to a string.
MemoryManager * getRWMM() const
const Assumptions & getAssumptionsRef() const
virtual const Expr & getRHS() const
Expr iffExpr(const Expr &right) const
RWTheoremValue(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
int d_scopeLevel
Largest scope level of the assumptions.
void init(const Assumptions &assump, int scope)
unsigned d_refcount
How many pointers to this theorem value.
void setLitFlag(bool val)
virtual MemoryManager * getMM()=0
unsigned getQuantLevelDebug()
const Assumptions & getAssumptionsRef() const
const Expr & getRHS() const
TheoremValue(const TheoremValue &t)
void setQuantLevel(unsigned level)
virtual void * newData(size_t size)=0
unsigned d_quantLevel
Quantification level of this theorem.
Assumptions d_assump
The assumptions for the theorem.
Iterator for the Assumptions: points to class Theorem.
const Expr & getLHS() const
void setCachedValue(int value)
TheoremValue & operator=(const TheoremValue &t)
Type getType() const
Get the type. Recursively compute if necessary.
bool isActive()
Test whether the TheoremManager is still active.
void setExpandFlag(bool val)
std::string toString() const
static const Assumptions & emptyAssump()
TheoremManager * d_tm
Theorem Manager.
unsigned recQuantLevel(Expr proof)
unsigned d_flag
debug quantlevel, this one is from proof, not from assumption list
virtual bool isRewrite() const