45 vector<Expr> operatorStack;
46 vector<int> childStack;
49 operatorStack.push_back(e);
50 childStack.push_back(0);
52 while (!operatorStack.empty()) {
53 DebugAssert(operatorStack.size() == childStack.size(),
"Invariant violated");
54 if (childStack.back() < operatorStack.back().arity()) {
55 e2 = operatorStack.back()[childStack.back()++];
59 if (operatorStack.size() >= 5000) {
64 operatorStack.push_back(e2);
65 childStack.push_back(0);
69 cache[operatorStack.back()] =
true;
70 operatorStack.pop_back();
71 childStack.pop_back();
74 DebugAssert(childStack.empty(),
"Invariant violated");
104 if (ppRes.
isRefl())
break;
142 TRACE(
"pushNegation",
"pushNegationRec(", e,
143 ", neg=" +
string(neg?
"true":
"false") +
") {");
147 TRACE(
"pushNegation",
"pushNegationRec [cached] => ", (*i).second,
"}");
153 switch(e.getKind()) {
166 vector<Theorem> thms;
186 vector<Theorem> thms;
196 switch(e.getKind()) {
203 vector<Theorem> thms;
219 TRACE(
"pushNegation",
"pushNegationRec => ", res,
"}");
231 "pushNegationRec(Theorem, neg = true): bad Theorem: "
240 TRACE(
"pushNegation1",
"pushNegation1(", e,
") {");
243 switch(e[0].getKind()) {
256 vector<Theorem> thms;
268 vector<Theorem> thms;
277 TRACE(
"pushNegation1",
"pushNegation1 => ", res.getExpr(),
" }");
301 if (it != cache.
end())
return (*it).second;
306 if (thm.getRHS().isBoolConst()) {
314 vector<Theorem> newChildrenThm;
315 vector<unsigned> changed;
317 for(
int k = 0; k < ar; ++k) {
321 newChildrenThm.push_back(thm2);
322 changed.push_back(k);
325 if(changed.size() > 0) {
358 vector<Theorem> newChildrenThm;
359 vector<unsigned> changed;
360 int ar = current.
arity();
361 for(
int k = 0; k < ar; ++k) {
365 newChildrenThm.push_back(thm);
366 changed.push_back(k);
369 if(changed.size() > 0) {
386 if ((newExpr[0].isLiteral() || newExpr[0].isAnd())) {
415 const set<Expr>& careSet)
421 set<Expr>* cs2 = (*it).second;
422 set<Expr>* csNew =
new set<Expr>;
423 set_intersection(careSet.begin(), careSet.end(), cs2->begin(), cs2->end(),
424 inserter(*csNew, csNew->begin()));
425 (*it).second = csNew;
429 queue[e] =
new set<Expr>(careSet);
449 it = substTable.
find(e);
450 iend = substTable.
end();
458 vector<Theorem> newChildrenThm;
459 vector<unsigned> changed;
460 for(
int k = 0; k < ar; ++k) {
463 newChildrenThm.push_back(thm);
464 changed.push_back(k);
467 if(changed.size() > 0) {
489 while (!queue.
empty()) {
530 set<Expr>::iterator iCare, iCareEnd = cs.end();
534 iCare = cs.find(v[0]);
535 if (iCare != iCareEnd) {
543 iCare = cs.find(v[0].negate());
544 if (iCare != iCareEnd) {
556 cs.insert(v[0].negate());
562 for (i = 0; i < v.
arity(); ++i) {
563 iCare = cs.find(v[i].negate());
564 if (iCare != iCareEnd) {
578 for (i = 1; i < v.
arity(); ++i) {
585 for (i = 0; i < v.
arity(); ++i) {
586 iCare = cs.find(v[i]);
587 if (iCare != iCareEnd) {
596 cs.insert(v[1].negate());
598 cs.erase(v[1].negate());
599 cs.insert(v[0].negate());
600 for (i = 1; i < v.
arity(); ++i) {
612 for (
int i = 0; i < v.
arity(); ++i) {
bool isAtomic() const
Test if e is atomic.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
const CLFlags & getFlags() const
virtual Theorem rewriteIteThen(const Expr &e, const Theorem &thenThm)=0
a |- b == d ==> ITE(a, b, c) == ITE(a, d, c)
iterator find(const Expr &e)
virtual Theorem dummyTheorem(const Expr &e)=0
Temporary cheat for building theorems.
virtual Theorem assumpRule(const Expr &a, int scope=-1)=0
virtual Theorem rewriteIteCond(const Expr &e)=0
==> ITE(a, b(a), c(a)) IFF ITE(a, b(TRUE), c(FALSE))
bool isPropAtom() const
True iff expr is not a Bool connective.
bool containsTermITE() const
Return whether Expr contains a non-bool type ITE as a sub-term.
Expr eqExpr(const Expr &right) const
virtual Theorem reflexivityRule(const Expr &a)=0
#define DebugAssert(cond, str)
bool isTerm() const
Test if e is a term (as opposed to a predicate/formula)
Theorem callTheoryPreprocess(const Expr &e)
Call theory-specific preprocess routines.
virtual Theorem rewriteNotFalse(const Expr &e)=0
==> NOT FALSE IFF TRUE
virtual Theorem rewriteNotNot(const Expr &e)=0
==> NOT NOT e IFF e, takes !!e
Op getOp() const
Get operator from expression.
CoreProofRules * getCoreRules() const
CommonProofRules * getCommonRules()
Get a pointer to common proof rules.
void setInPP()
Set the flag for the preprocessor.
Theorem simplify(const Expr &e)
Top-level simplifier.
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
std::string toString() const
std::string toString() const
Print the expression to a string.
bool validSimpCache() const
Return true if there is a valid cached value for calling simplify on this Expr.
Expr iffExpr(const Expr &right) const
const Expr & falseExpr()
FALSE Expr.
const Expr & getRHS() const
virtual Theorem rewriteNotOr(const Expr &e)=0
==> NOT (OR e1 ... en) IFF (AND !e1 ... !en), takes (OR ...)
const Expr & trueExpr()
TRUE Expr.
virtual Theorem rewriteNotAnd(const Expr &e)=0
==> NOT (AND e1 ... en) IFF (OR !e1 ... !en), takes (AND ...)
ExprManager * getEM()
Access to ExprManager.
bool leavesAreNumConst(const Expr &e)
virtual Theorem rewriteLetDecl(const Expr &e)=0
Replace LETDECL with its definition.
ContextManager * getCM() const
virtual Theorem liftOneITE(const Expr &e)=0
virtual Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0
(same for IFF)
virtual Theorem rewriteIteElse(const Expr &e, const Theorem &elseThm)=0
!a |- c == d ==> ITE(a, b, c) == ITE(a, b, d)
virtual Theorem rewriteNotIte(const Expr &e)=0
==> NOT ITE(a,b,c) IFF ITE(a,NOT b,NOT c)
iterator find(const Expr &e)
Proof rules used by theory_core.
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
void invalidateSimpCache()
Invalidate the simplifier's cache tag.
bool isAtomicFormula() const
Test if e is an atomic formula.
Theorem reflexivityRule(const Expr &a)
==> a == a
Theory * theoryOf(int kind)
Return the theory associated with a kind.
Type getType() const
Get the type. Recursively compute if necessary.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
virtual Theorem rewriteNotTrue(const Expr &e)=0
==> NOT TRUE IFF FALSE
void erase(const Expr &e)
virtual Theorem rewriteImplies(const Expr &e)=0
==> IMPLIES(e1,e2) IFF OR(!e1, e2)