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";