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) { }