From 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Fri, 5 Oct 2012 22:07:16 +0000 Subject: BoolExpr removed and replaced with Expr --- src/compat/cvc3_compat.cpp | 6 +- src/expr/command.cpp | 12 ++-- src/expr/command.h | 18 +++--- src/expr/expr_template.cpp | 33 +++------- src/expr/expr_template.h | 128 +++++++++++++------------------------- src/printer/ast/ast_printer.cpp | 2 +- src/printer/cvc/cvc_printer.cpp | 4 +- src/printer/smt2/smt2_printer.cpp | 4 +- src/prop/cnf_stream.cpp | 4 +- src/prop/cnf_stream.h | 1 + src/prop/minisat/core/Solver.cc | 24 ++++--- src/prop/prop_engine.cpp | 4 +- src/smt/smt_engine.cpp | 10 +-- src/smt/smt_engine.h | 8 +-- src/theory/theory_engine.cpp | 40 +----------- 15 files changed, 105 insertions(+), 193 deletions(-) (limited to 'src') diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 8ba91b419..2ed3c0a7f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -2071,7 +2071,7 @@ void ValidityChecker::setTimeLimit(unsigned limit) { } void ValidityChecker::assertFormula(const Expr& e) { - d_smt->assertFormula(CVC4::BoolExpr(e)); + d_smt->assertFormula(e); } void ValidityChecker::registerAtom(const Expr& e) { @@ -2107,11 +2107,11 @@ static QueryResult cvc4resultToCvc3result(CVC4::Result r) { } QueryResult ValidityChecker::query(const Expr& e) { - return cvc4resultToCvc3result(d_smt->query(CVC4::BoolExpr(e))); + return cvc4resultToCvc3result(d_smt->query(e)); } QueryResult ValidityChecker::checkUnsat(const Expr& e) { - return cvc4resultToCvc3result(d_smt->checkSat(CVC4::BoolExpr(e))); + return cvc4resultToCvc3result(d_smt->checkSat(e)); } QueryResult ValidityChecker::checkContinue() { diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a62a9421f..220629cfd 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -177,11 +177,11 @@ Command* EchoCommand::clone() const { /* class AssertCommand */ -AssertCommand::AssertCommand(const BoolExpr& e) throw() : +AssertCommand::AssertCommand(const Expr& e) throw() : d_expr(e) { } -BoolExpr AssertCommand::getExpr() const throw() { +Expr AssertCommand::getExpr() const throw() { return d_expr; } @@ -248,11 +248,11 @@ Command* PopCommand::clone() const { /* class CheckSatCommand */ -CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : +CheckSatCommand::CheckSatCommand(const Expr& expr) throw() : d_expr(expr) { } -BoolExpr CheckSatCommand::getExpr() const throw() { +Expr CheckSatCommand::getExpr() const throw() { return d_expr; } @@ -291,11 +291,11 @@ Command* CheckSatCommand::clone() const { /* class QueryCommand */ -QueryCommand::QueryCommand(const BoolExpr& e) throw() : +QueryCommand::QueryCommand(const Expr& e) throw() : d_expr(e) { } -BoolExpr QueryCommand::getExpr() const throw() { +Expr QueryCommand::getExpr() const throw() { return d_expr; } diff --git a/src/expr/command.h b/src/expr/command.h index 6f5b0bd4c..9fabf129e 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -290,11 +290,11 @@ public: class CVC4_PUBLIC AssertCommand : public Command { protected: - BoolExpr d_expr; + Expr d_expr; public: - AssertCommand(const BoolExpr& e) throw(); + AssertCommand(const Expr& e) throw(); ~AssertCommand() throw() {} - BoolExpr getExpr() const throw(); + Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; @@ -423,13 +423,13 @@ public: class CVC4_PUBLIC CheckSatCommand : public Command { protected: - BoolExpr d_expr; + Expr d_expr; Result d_result; public: CheckSatCommand() throw(); - CheckSatCommand(const BoolExpr& expr) throw(); + CheckSatCommand(const Expr& expr) throw(); ~CheckSatCommand() throw() {} - BoolExpr getExpr() const throw(); + Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); @@ -439,12 +439,12 @@ public: class CVC4_PUBLIC QueryCommand : public Command { protected: - BoolExpr d_expr; + Expr d_expr; Result d_result; public: - QueryCommand(const BoolExpr& e) throw(); + QueryCommand(const Expr& e) throw(); ~QueryCommand() throw() {} - BoolExpr getExpr() const throw(); + Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); Result getResult() const throw(); void printResult(std::ostream& out) const throw(); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 2f9e27c0c..d535beec2 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -467,20 +467,13 @@ TNode Expr::getTNode() const throw() { return *d_node; } -BoolExpr::BoolExpr() { -} - -BoolExpr::BoolExpr(const Expr& e) : - Expr(e) { -} - -BoolExpr BoolExpr::notExpr() const { +Expr Expr::notExpr() const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); return d_exprManager->mkExpr(NOT, *this); } -BoolExpr BoolExpr::andExpr(const BoolExpr& e) const { +Expr Expr::andExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == e.d_exprManager, e, @@ -488,7 +481,7 @@ BoolExpr BoolExpr::andExpr(const BoolExpr& e) const { return d_exprManager->mkExpr(AND, *this, e); } -BoolExpr BoolExpr::orExpr(const BoolExpr& e) const { +Expr Expr::orExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == e.d_exprManager, e, @@ -496,7 +489,7 @@ BoolExpr BoolExpr::orExpr(const BoolExpr& e) const { return d_exprManager->mkExpr(OR, *this, e); } -BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const { +Expr Expr::xorExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == e.d_exprManager, e, @@ -504,7 +497,7 @@ BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const { return d_exprManager->mkExpr(XOR, *this, e); } -BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const { +Expr Expr::iffExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == e.d_exprManager, e, @@ -512,7 +505,7 @@ BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const { return d_exprManager->mkExpr(IFF, *this, e); } -BoolExpr BoolExpr::impExpr(const BoolExpr& e) const { +Expr Expr::impExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == e.d_exprManager, e, @@ -520,8 +513,8 @@ BoolExpr BoolExpr::impExpr(const BoolExpr& e) const { return d_exprManager->mkExpr(IMPLIES, *this, e); } -BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, - const BoolExpr& else_e) const { +Expr Expr::iteExpr(const Expr& then_e, + const Expr& else_e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); CheckArgument(d_exprManager == then_e.d_exprManager, then_e, @@ -531,16 +524,6 @@ BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } -Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == then_e.getExprManager(), then_e, - "Different expression managers!"); - CheckArgument(d_exprManager == else_e.getExprManager(), else_e, - "Different expression managers!"); - return d_exprManager->mkExpr(ITE, *this, then_e, else_e); -} - void Expr::printAst(std::ostream & o, int indent) const { ExprManagerScope ems(*this); getNode().printAst(o, indent); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 4255e3454..b530d13b2 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -161,16 +161,12 @@ struct ExprHashFunction { size_t operator()(CVC4::Expr e) const; };/* struct ExprHashFunction */ -class BoolExpr; - /** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. */ class CVC4_PUBLIC Expr { - friend class BoolExpr; - /** The internal expression representation */ NodeTemplate* d_node; @@ -312,6 +308,48 @@ public: return std::vector(begin(), end()); } + /** + * Returns the Boolean negation of this Expr. + */ + Expr notExpr() const; + + /** + * Returns the conjunction of this expression and + * the given expression. + */ + Expr andExpr(const Expr& e) const; + + /** + * Returns the disjunction of this expression and + * the given expression. + */ + Expr orExpr(const Expr& e) const; + + /** + * Returns the exclusive disjunction of this expression and + * the given expression. + */ + Expr xorExpr(const Expr& e) const; + + /** + * Returns the Boolean equivalence of this expression and + * the given expression. + */ + Expr iffExpr(const Expr& e) const; + + /** + * Returns the implication of this expression and + * the given expression. + */ + Expr impExpr(const Expr& e) const; + + /** + * Returns the if-then-else expression with this expression + * as the Boolean condition and the given expressions as + * the "then" and "else" expressions. + */ + Expr iteExpr(const Expr& then_e, const Expr& else_e) const; + /** * Iterator type for the children of an Expr. */ @@ -562,86 +600,6 @@ private: };/* class Expr */ -/** - * Extending the expression with the capability to construct Boolean - * expressions. - */ -class CVC4_PUBLIC BoolExpr : public Expr { - -public: - - /** Default constructor, makes a null expression */ - BoolExpr(); - - /** - * Convert an expression to a Boolean expression - */ - BoolExpr(const Expr& e); - - /** - * Negate this expression. - * @return the logical negation of this expression. - */ - BoolExpr notExpr() const; - - /** - * Conjunct the given expression to this expression. - * @param e the expression to conjunct - * @return the conjunction of this expression and e - */ - BoolExpr andExpr(const BoolExpr& e) const; - - /** - * Disjunct the given expression to this expression. - * @param e the expression to disjunct - * @return the disjunction of this expression and e - */ - BoolExpr orExpr(const BoolExpr& e) const; - - /** - * Make an exclusive or expression out of this expression and the given - * expression. - * @param e the right side of the xor - * @return the xor of this expression and e - */ - BoolExpr xorExpr(const BoolExpr& e) const; - - /** - * Make an equivalence expression out of this expression and the given - * expression. - * @param e the right side of the equivalence - * @return the equivalence expression - */ - BoolExpr iffExpr(const BoolExpr& e) const; - - /** - * Make an implication expression out of this expression and the given - * expression. - * @param e the right side of the equivalence - * @return the equivalence expression - */ - BoolExpr impExpr(const BoolExpr& e) const; - - /** - * Make a Boolean if-then-else expression using this expression as the - * condition, and given the then and else parts. - * @param then_e the then branch expression - * @param else_e the else branch expression - * @return the if-then-else expression - */ - BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const; - - /** - * Make a term if-then-else expression using this expression as the - * condition, and given the then and else parts. - * @param then_e the then branch expression - * @param else_e the else branch expression - * @return the if-then-else expression - */ - Expr iteExpr(const Expr& then_e, const Expr& else_e) const; - -};/* class BoolExpr */ - namespace expr { /** @@ -968,7 +926,7 @@ public: ${getConst_instantiations} -#line 959 "${template}" +#line 930 "${template}" namespace expr { diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 4ae66f510..34bf0bb6d 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -208,7 +208,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() { } static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { - BoolExpr e = c->getExpr(); + Expr e = c->getExpr(); if(e.isNull()) { out << "CheckSat()"; } else { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 56d9a20b0..5d2ffb9db 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -821,7 +821,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() { } static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { - BoolExpr e = c->getExpr(); + Expr e = c->getExpr(); if(!e.isNull()) { out << "CHECKSAT " << e << ";"; } else { @@ -830,7 +830,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { } static void toStream(std::ostream& out, const QueryCommand* c) throw() { - BoolExpr e = c->getExpr(); + Expr e = c->getExpr(); if(!e.isNull()) { out << "QUERY " << e << ";"; } else { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5d9a13786..31754cb3a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -615,7 +615,7 @@ static void toStream(std::ostream& out, const PopCommand* c) throw() { } static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { - BoolExpr e = c->getExpr(); + Expr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl << AssertCommand(e) << endl @@ -627,7 +627,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { } static void toStream(std::ostream& out, const QueryCommand* c) throw() { - BoolExpr e = c->getExpr(); + Expr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl << AssertCommand(BooleanSimplification::negate(e)) << endl diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f47637b72..e7c74525d 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -75,7 +75,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; if(Dump.isOn("clauses")) { if(c.size() == 1) { - Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())); + Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr())); } else { Assert(c.size() > 1); NodeBuilder<> b(kind::OR); @@ -83,7 +83,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { b << getNode(c[i]); } Node n = b; - Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())); + Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } d_satSolver->addClause(c, d_removable); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 5efedd4ca..a6e2b2e02 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -30,6 +30,7 @@ #include "expr/node.h" #include "prop/theory_proxy.h" #include "prop/registrar.h" +#include "context/cdlist.h" #include diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 5e19eb776..7fc7a1d9c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -349,11 +349,11 @@ void Solver::cancelUntil(int level) { } for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) + polarity[x] = sign(trail[c]); if(intro_level(x) != -1) {// might be unregistered - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0) - polarity[x] = sign(trail[c]); insertVarOrder(x); } } @@ -1409,6 +1409,9 @@ void Solver::push() trail_ok.push(ok); trail_user_lim.push(trail.size()); assert(trail_user_lim.size() == assertionLevel); + + context->push(); + Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl; } @@ -1438,10 +1441,10 @@ void Solver::pop() while(downto < trail.size()) { Debug("minisat") << "== unassigning " << trail.last() << std::endl; Var x = var(trail.last()); + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + polarity[x] = sign(trail.last()); if(intro_level(x) != -1) {// might be unregistered - assigns [x] = l_Undef; - vardata[x].trail_index = -1; - polarity[x] = sign(trail.last()); insertVarOrder(x); } trail.pop(); @@ -1458,9 +1461,12 @@ void Solver::pop() Debug("minisat") << "== unassigning " << l << std::endl; Var x = var(l); assigns [x] = l_Undef; + vardata[x].trail_index = -1; if (phase_saving >= 1 && (polarity[x] & 0x2) == 0) polarity[x] = sign(l); - insertVarOrder(x); + if(intro_level(x) != -1) {// might be unregistered + insertVarOrder(x); + } trail_user.pop(); } trail_user.pop(); @@ -1470,6 +1476,8 @@ void Solver::pop() Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl; + context->pop(); + // Notify the cnf proxy->removeClausesAboveLevel(assertionLevel); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 973adc67f..12e85de13 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -111,9 +111,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; if(!d_inCheckSat && Dump.isOn("learned")) { - Dump("learned") << AssertCommand(BoolExpr(node.toExpr())); + Dump("learned") << AssertCommand(node.toExpr()); } else if(Dump.isOn("lemmas")) { - Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())); + Dump("lemmas") << AssertCommand(node.toExpr()); } // Assert as removable diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 878588d15..2d83b7960 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1770,7 +1770,7 @@ void SmtEnginePrivate::processAssertions() { // Push the simplified assertions to the dump output stream for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { Dump("assertions") - << AssertCommand(BoolExpr(d_assertionsToCheck[i].toExpr())); + << AssertCommand(d_assertionsToCheck[i].toExpr()); } } @@ -1812,7 +1812,7 @@ void SmtEnginePrivate::addFormula(TNode n) } } -void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) { +void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { Type type = e.getType(options::typeChecking()); Type boolType = d_exprManager->booleanType(); if(type != boolType) { @@ -1824,7 +1824,7 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { +Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) { Assert(e.isNull() || e.getExprManager() == d_exprManager); @@ -1891,7 +1891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { return r; }/* SmtEngine::checkSat() */ -Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { +Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) { Assert(!e.isNull()); Assert(e.getExprManager() == d_exprManager); @@ -1955,7 +1955,7 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { return r; }/* SmtEngine::query() */ -Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException) { +Result SmtEngine::assertFormula(const Expr& e) throw(TypeCheckingException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f30a98935..df2e47b5b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -263,7 +263,7 @@ class CVC4_PUBLIC SmtEngine { * Fully type-check the argument, and also type-check that it's * actually Boolean. */ - void ensureBoolean(const BoolExpr& e) throw(TypeCheckingException); + void ensureBoolean(const Expr& e) throw(TypeCheckingException); void internalPush(); @@ -362,20 +362,20 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(const BoolExpr& e) throw(TypeCheckingException); + Result assertFormula(const Expr& e) throw(TypeCheckingException); /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const BoolExpr& e) throw(TypeCheckingException); + Result query(const Expr& e) throw(TypeCheckingException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const BoolExpr& e = BoolExpr()) throw(TypeCheckingException); + Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException); /** * Simplify a formula without doing "much" work. Does not involve 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::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); - for (; it != it_end; ++ it) { - TNode t1 = (*it); - context::CDList::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(); } } -- cgit v1.2.3