From 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 5 Oct 2012 22:07:16 +0000 Subject: [PATCH] BoolExpr removed and replaced with Expr --- .cproject | 13 +- .settings/language.settings.xml | 9 ++ examples/hashsmt/sha1smt.cpp | 6 +- examples/hashsmt/word.cpp | 2 +- examples/hashsmt/word.h | 2 +- examples/nra-translate/normalize.cpp | 2 +- examples/nra-translate/smt2info.cpp | 2 +- examples/nra-translate/smt2todreal.cpp | 2 +- examples/nra-translate/smt2toisat.cpp | 8 +- examples/nra-translate/smt2tomathematica.cpp | 8 +- examples/nra-translate/smt2toqepcad.cpp | 8 +- examples/nra-translate/smt2toredlog.cpp | 8 +- examples/simple_vc_cxx.cpp | 6 +- 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 +----- 28 files changed, 151 insertions(+), 223 deletions(-) create mode 100644 .settings/language.settings.xml diff --git a/.cproject b/.cproject index bcc6a9ca5..299de0591 100644 --- a/.cproject +++ b/.cproject @@ -1,7 +1,5 @@ - - - + @@ -319,6 +317,14 @@ false true + + make + -j10 + all + true + true + true + make -j2 @@ -344,4 +350,5 @@ + diff --git a/.settings/language.settings.xml b/.settings/language.settings.xml new file mode 100644 index 000000000..e0bae153a --- /dev/null +++ b/.settings/language.settings.xml @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/examples/hashsmt/sha1smt.cpp b/examples/hashsmt/sha1smt.cpp index 3a33a4bc2..97b79a7d0 100644 --- a/examples/hashsmt/sha1smt.cpp +++ b/examples/hashsmt/sha1smt.cpp @@ -46,7 +46,7 @@ int main(int argc, char* argv[]) { output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; // Ouput the solution also - BoolExpr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i])); + Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i])); output << "; " << AssertCommand(solution) << endl; } @@ -65,9 +65,9 @@ int main(int argc, char* argv[]) { sha1encoder.get_digest(sha1digest); // Create the assertion - BoolExpr assertion; + Expr assertion; for (unsigned i = 0; i < 5; ++ i) { - BoolExpr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i])); + Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i])); if (i > 0) { assertion = assertion.andExpr(conjunct); } else { diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index d1b8e2fef..c6cb8caf2 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -34,7 +34,7 @@ ExprManager* Word::em() { return s_manager; } -BoolExpr Word::operator == (const Word& b) const { +Expr Word::operator == (const Word& b) const { return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr()); } diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index 50fdee0c0..e8d6053c0 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -61,7 +61,7 @@ public: } /** Returns the comparison expression */ - CVC4::BoolExpr operator == (const Word& b) const; + CVC4::Expr operator == (const Word& b) const; }; inline std::ostream& operator << (std::ostream& out, const Word& word) { diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index ac5780439..d38da7616 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -40,7 +40,7 @@ int main(int argc, char* argv[]) SmtEngine engine(&exprManager); // Variables and assertions - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index b14f8fa8f..0ccf9d669 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -72,7 +72,7 @@ int main(int argc, char* argv[]) vector variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 8bdb27181..6fcf5c565 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -42,7 +42,7 @@ int main(int argc, char* argv[]) std::map variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index e2b55b4b9..b44339309 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -23,7 +23,7 @@ void translate_to_isat( const vector& info_tags, const vector& info_data, const map& variables, - const vector& assertions); + const vector& assertions); int main(int argc, char* argv[]) { @@ -47,7 +47,7 @@ int main(int argc, char* argv[]) std::map variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { @@ -148,7 +148,7 @@ void translate_to_isat_term(const map& variables, const Expr& te } } -void translate_to_isat(const map& variables, const BoolExpr& assertion) { +void translate_to_isat(const map& variables, const Expr& assertion) { bool first; unsigned n = assertion.getNumChildren(); @@ -260,7 +260,7 @@ void translate_to_isat( const vector& info_tags, const vector& info_data, const std::map& variables, - const vector& assertions) + const vector& assertions) { bool first; diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 9da21b69b..bfee27310 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -22,7 +22,7 @@ void translate_to_mathematica( const vector& info_tags, const vector& info_data, const map& variables, - const vector& assertions); + const vector& assertions); int main(int argc, char* argv[]) { @@ -43,7 +43,7 @@ int main(int argc, char* argv[]) std::map variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { @@ -150,7 +150,7 @@ void translate_to_mathematica_term(const map& variables, const E } } -void translate_to_mathematica(const map& variables, const BoolExpr& assertion) { +void translate_to_mathematica(const map& variables, const Expr& assertion) { bool first; unsigned n = assertion.getNumChildren(); @@ -255,7 +255,7 @@ void translate_to_mathematica( const vector& info_tags, const vector& info_data, const std::map& variables, - const vector& assertions) + const vector& assertions) { bool first; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index bed9b42ea..fc43c4c7b 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -22,7 +22,7 @@ void translate_to_qepcad( const vector& info_tags, const vector& info_data, const map& variables, - const vector& assertions); + const vector& assertions); int main(int argc, char* argv[]) { @@ -44,7 +44,7 @@ int main(int argc, char* argv[]) std::map variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { @@ -152,7 +152,7 @@ void translate_to_qepcad_term(const std::map& variables, const E } } -void translate_to_qepcad(const std::map& variables, const BoolExpr& assertion) { +void translate_to_qepcad(const std::map& variables, const Expr& assertion) { bool first; unsigned n = assertion.getNumChildren(); @@ -251,7 +251,7 @@ void translate_to_qepcad( const vector& info_tags, const vector& info_data, const std::map& variables, - const vector& assertions) + const vector& assertions) { bool first; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index da34ca4da..b2717c157 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -24,7 +24,7 @@ void translate_to_redlog( const vector& info_tags, const vector& info_data, const map& variables, - const vector& assertions); + const vector& assertions); int main(int argc, char* argv[]) { @@ -50,7 +50,7 @@ int main(int argc, char* argv[]) std::map variables; vector info_tags; vector info_data; - vector assertions; + vector assertions; Command* cmd; while ((cmd = parser->nextCommand())) { @@ -155,7 +155,7 @@ void translate_to_redlog_term(const map& variables, const Expr& } } -void translate_to_redlog(const map& variables, const BoolExpr& assertion) { +void translate_to_redlog(const map& variables, const Expr& assertion) { bool first; unsigned n = assertion.getNumChildren(); @@ -269,7 +269,7 @@ void translate_to_redlog( const vector& info_tags, const vector& info_data, const std::map& variables, - const vector& assertions) + const vector& assertions) { bool first; diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 557199e75..92714ebc7 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -49,9 +49,9 @@ int main() { Expr three = em.mkConst(Rational(3)); Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); - BoolExpr formula = - BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)). - impExpr(BoolExpr(twox_plus_y_geq_3)); + Expr formula = + em.mkExpr(kind::AND, x_positive, y_positive). + impExpr(twox_plus_y_geq_3); cout << "Checking validity of formula " << formula << " with CVC4." << endl; cout << "CVC4 should report VALID." << endl; 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(); } } -- 2.30.2