diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-05 22:07:16 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-10-05 22:07:16 +0000 |
commit | 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 (patch) | |
tree | d0cfcf60cbf9600c52dcb728744802ad27a5c3e1 /src/theory | |
parent | 7a9899f394476e53b7f759e698c7e10c8388fd57 (diff) |
BoolExpr removed and replaced with Expr
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_engine.cpp | 40 |
1 files changed, 1 insertions, 39 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 61b66ba3e..de32409c5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -211,53 +211,15 @@ void TheoryEngine::dumpAssertions(const char* tag) { Node assertionNode = (*it).assertion; // Purify all the terms - BoolExpr assertionExpr(assertionNode.toExpr()); if ((*it).isPreregistered) { Dump(tag) << CommentCommand("Preregistered"); } else { Dump(tag) << CommentCommand("Shared assertion"); } - Dump(tag) << AssertCommand(assertionExpr); + Dump(tag) << AssertCommand(assertionNode.toExpr()); } Dump(tag) << CheckSatCommand(); - // Check for any missed propagations of shared terms - if (d_logicInfo.isSharingEnabled()) { - Dump(tag) << CommentCommand("Shared term equalities"); - context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); - for (; it != it_end; ++ it) { - TNode t1 = (*it); - context::CDList<TNode>::const_iterator it2 = it; - for (++ it2; it2 != it_end; ++ it2) { - TNode t2 = (*it2); - if (t1.getType() == t2.getType()) { - Node equality = t1.eqNode(t2); - if (d_sharedTerms.isKnown(equality)) { - continue; - } - Node disequality = equality.notNode(); - if (d_sharedTerms.isKnown(disequality)) { - continue; - } - - // Check equality - Dump(tag) << PushCommand(); - BoolExpr eqExpr(equality.toExpr()); - Dump(tag) << AssertCommand(eqExpr); - Dump(tag) << CheckSatCommand(); - Dump(tag) << PopCommand(); - - // Check disequality - Dump(tag) << PushCommand(); - BoolExpr diseqExpr(disequality.toExpr()); - Dump(tag) << AssertCommand(diseqExpr); - Dump(tag) << CheckSatCommand(); - Dump(tag) << PopCommand(); - } - } - } - } - Dump(tag) << PopCommand(); } } |