From 2dbe1f150d30f0fb0c8522f891104270ce09db4c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 22 Aug 2014 16:59:28 -0400 Subject: Unsat core infrastruture and API (SMT-LIB compliance to come). --- src/expr/command.cpp | 37 +- src/expr/command.h | 12 +- src/parser/smt2/Smt2.g | 16 +- src/parser/smt2/smt2.h | 9 + src/printer/smt2/smt2_printer.cpp | 5 + src/proof/cnf_proof.cpp | 128 +++++-- src/proof/cnf_proof.h | 40 +-- src/proof/proof.h | 6 +- src/proof/proof_manager.cpp | 119 ++++-- src/proof/proof_manager.h | 63 +++- src/proof/sat_proof.cpp | 77 ++-- src/proof/sat_proof.h | 16 +- src/prop/bvminisat/bvminisat.cpp | 4 +- src/prop/bvminisat/bvminisat.h | 4 +- src/prop/cnf_stream.cpp | 28 +- src/prop/cnf_stream.h | 28 +- src/prop/minisat/core/Solver.cc | 32 +- src/prop/minisat/core/Solver.h | 38 +- src/prop/minisat/minisat.cpp | 6 +- src/prop/minisat/minisat.h | 2 +- src/prop/minisat/simp/SimpSolver.cc | 8 +- src/prop/minisat/simp/SimpSolver.h | 26 +- src/prop/prop_engine.cpp | 9 +- src/prop/prop_engine.h | 3 +- src/prop/sat_solver.h | 3 +- src/prop/theory_proxy.cpp | 2 +- src/smt/options | 8 +- src/smt/options_handlers.h | 12 - src/smt/simplification_mode.cpp | 3 - src/smt/simplification_mode.h | 2 - src/smt/smt_engine.cpp | 598 ++++++++++++++++++------------- src/smt/smt_engine.h | 26 +- src/smt/smt_engine_scope.h | 7 +- src/theory/booleans/circuit_propagator.h | 2 +- src/theory/bv/eager_bitblaster.cpp | 4 +- src/theory/bv/lazy_bitblaster.cpp | 4 +- src/theory/theory_engine.cpp | 8 +- src/util/Makefile.am | 7 +- src/util/ite_removal.cpp | 13 +- src/util/ite_removal.h | 5 +- src/util/unsat_core.cpp | 41 +++ src/util/unsat_core.h | 54 +++ src/util/unsat_core.i | 5 + 43 files changed, 974 insertions(+), 546 deletions(-) create mode 100644 src/util/unsat_core.cpp create mode 100644 src/util/unsat_core.h create mode 100644 src/util/unsat_core.i (limited to 'src') diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 33be85d11..a07076281 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -189,8 +189,8 @@ std::string EchoCommand::getCommandName() const throw() { /* class AssertCommand */ -AssertCommand::AssertCommand(const Expr& e) throw() : - d_expr(e) { +AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { } Expr AssertCommand::getExpr() const throw() { @@ -199,7 +199,7 @@ Expr AssertCommand::getExpr() const throw() { void AssertCommand::invoke(SmtEngine* smtEngine) throw() { try { - smtEngine->assertFormula(d_expr); + smtEngine->assertFormula(d_expr, d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); @@ -207,18 +207,17 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() { } Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new AssertCommand(d_expr.exportTo(exprManager, variableMap)); + return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); } Command* AssertCommand::clone() const { - return new AssertCommand(d_expr); + return new AssertCommand(d_expr, d_inUnsatCore); } std::string AssertCommand::getCommandName() const throw() { return "assert"; } - /* class PushCommand */ void PushCommand::invoke(SmtEngine* smtEngine) throw() { @@ -271,8 +270,8 @@ CheckSatCommand::CheckSatCommand() throw() : d_expr() { } -CheckSatCommand::CheckSatCommand(const Expr& expr) throw() : - d_expr(expr) { +CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : + d_expr(expr), d_inUnsatCore(inUnsatCore) { } Expr CheckSatCommand::getExpr() const throw() { @@ -301,13 +300,13 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const t } Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap)); + CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); c->d_result = d_result; return c; } Command* CheckSatCommand::clone() const { - CheckSatCommand* c = new CheckSatCommand(d_expr); + CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); c->d_result = d_result; return c; } @@ -318,8 +317,8 @@ std::string CheckSatCommand::getCommandName() const throw() { /* class QueryCommand */ -QueryCommand::QueryCommand(const Expr& e) throw() : - d_expr(e) { +QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : + d_expr(e), d_inUnsatCore(inUnsatCore) { } Expr QueryCommand::getExpr() const throw() { @@ -348,13 +347,13 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const thro } Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap)); + QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); c->d_result = d_result; return c; } Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_expr); + QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); c->d_result = d_result; return c; } @@ -1123,35 +1122,31 @@ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { } void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { - /* try { d_result = smtEngine->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } - */ - d_commandStatus = new CommandUnsupported(); } void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { if(! ok()) { this->Command::printResult(out, verbosity); } else { - //do nothing -- unsat cores not yet supported - // d_result->toStream(out); + d_result.toStream(out); } } Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); - //c->d_result = d_result; + c->d_result = d_result; return c; } Command* GetUnsatCoreCommand::clone() const { GetUnsatCoreCommand* c = new GetUnsatCoreCommand(); - //c->d_result = d_result; + c->d_result = d_result; return c; } diff --git a/src/expr/command.h b/src/expr/command.h index c4e7fbf89..e84c53d09 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -35,6 +35,7 @@ #include "util/sexpr.h" #include "util/datatype.h" #include "util/proof.h" +#include "util/unsat_core.h" namespace CVC4 { @@ -309,8 +310,9 @@ public: class CVC4_PUBLIC AssertCommand : public Command { protected: Expr d_expr; + bool d_inUnsatCore; public: - AssertCommand(const Expr& e) throw(); + AssertCommand(const Expr& e, bool inUnsatCore = true) throw(); ~AssertCommand() throw() {} Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); @@ -457,9 +459,10 @@ class CVC4_PUBLIC CheckSatCommand : public Command { protected: Expr d_expr; Result d_result; + bool d_inUnsatCore; public: CheckSatCommand() throw(); - CheckSatCommand(const Expr& expr) throw(); + CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw(); ~CheckSatCommand() throw() {} Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); @@ -474,8 +477,9 @@ class CVC4_PUBLIC QueryCommand : public Command { protected: Expr d_expr; Result d_result; + bool d_inUnsatCore; public: - QueryCommand(const Expr& e) throw(); + QueryCommand(const Expr& e, bool inUnsatCore = true) throw(); ~QueryCommand() throw() {} Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine) throw(); @@ -597,7 +601,7 @@ public: class CVC4_PUBLIC GetUnsatCoreCommand : public Command { protected: - //UnsatCore* d_result; + UnsatCore d_result; public: GetUnsatCoreCommand() throw(); ~GetUnsatCoreCommand() throw() {} diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bd7c96dce..e1547d23d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -378,7 +378,9 @@ command returns [CVC4::Command* cmd = NULL] | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[expr, expr2] - { cmd = new AssertCommand(expr); } + { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr); + PARSER_STATE->setLastNamedTerm(Expr()); + } | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( term[expr, expr2] @@ -684,7 +686,7 @@ rewriterulesCommand[CVC4::Command*& cmd] }; args.push_back(expr); expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd = new AssertCommand(expr); } + cmd = new AssertCommand(expr, false); } /* propagation rule */ | rewritePropaKind[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK @@ -735,7 +737,7 @@ rewriterulesCommand[CVC4::Command*& cmd] }; args.push_back(expr); expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd = new AssertCommand(expr); } + cmd = new AssertCommand(expr, false); } ; rewritePropaKind[CVC4::Kind& kind] @@ -1035,8 +1037,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] - ( attribute[expr, attexpr,attr] - { if( attr == ":pattern" && ! attexpr.isNull()) { + ( attribute[expr, attexpr, attr] + { if(attr == ":pattern" && ! attexpr.isNull()) { patexprs.push_back( attexpr ); } } @@ -1074,7 +1076,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } } expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); - }else{ + } else { expr2 = f2; } } @@ -1210,6 +1212,8 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] PARSER_STATE->reserveSymbolAtAssertionLevel(name); // define it Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + // remember the last term to have been given a :named attribute + PARSER_STATE->setLastNamedTerm(expr); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand(name, func, std::vector(), expr); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 71161be94..7ecd2e5b1 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -54,6 +54,7 @@ private: bool d_logicSet; LogicInfo d_logic; std::hash_map operatorKindMap; + Expr d_lastNamedTerm; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -105,6 +106,14 @@ public: void includeFile(const std::string& filename); + void setLastNamedTerm(Expr e) { + d_lastNamedTerm = e; + } + + Expr lastNamedTerm() { + return d_lastNamedTerm; + } + bool isAbstractValue(const std::string& name) { return name.length() >= 2 && name[0] == '@' && name[1] != '0' && name.find_first_not_of("0123456789", 1) == std::string::npos; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c9db1eece..766db729a 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -702,6 +702,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c, d_variant) || tryToStream(out, c) || @@ -1025,6 +1026,10 @@ static void toStream(std::ostream& out, const GetProofCommand* c) throw() { out << "(get-proof)"; } +static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() { + out << "(get-unsat-core)"; +} + static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "(set-info :status " << c->getStatus() << ")"; } diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 3dfb61428..22a40ff69 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -30,6 +30,8 @@ CnfProof::CnfProof(CnfStream* stream) : d_cnfStream(stream) {} +CnfProof::~CnfProof() { +} Expr CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); @@ -38,34 +40,33 @@ Expr CnfProof::getAtom(prop::SatVariable var) { return atom; } -CnfProof::~CnfProof() { -} - -LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() { - return iterator(*this, ProofManager::currentPM()->begin_vars()); +prop::SatLiteral CnfProof::getLiteral(TNode atom) { + return d_cnfStream->getLiteral(atom); } -LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() { - return iterator(*this, ProofManager::currentPM()->end_vars()); +Expr CnfProof::getAssertion(uint64_t id) { + return d_cnfStream->getAssertion(id).toExpr(); } -void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { - ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars(); - ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); - - for (;it != end; ++it) { - os << "(decl_atom "; - - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { - Expr atom = getAtom(*it); - LFSCTheoryProof::printTerm(atom, os); - } else { - // print fake atoms for all other logics - os << "true "; +void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { + for (unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = clause->operator[](i); + if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) { + d_atomsDeclared.insert(lit.getSatVariable()); + os << "(decl_atom "; + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 || + ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 || + ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) { + Expr atom = getAtom(lit.getSatVariable()); + LFSCTheoryProof::printTerm(atom, os); + } else { + // print fake atoms for all other logics (for now) + os << "true "; + } + + os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n"; + paren << ")))"; } - - os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; - paren << ")))"; } } @@ -75,36 +76,93 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { } void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { - os << " ;; Input Clauses \n"; + os << " ;; Clauses\n"; ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; + printAtomMapping(clause, os, paren); os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); - os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; + os << "(clausify_false trust)" << clause_paren.str() + << " (\\ " << ProofManager::getInputClauseName(id) << "\n"; paren << "))"; } } - void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas \n"; - ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas(); - ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas(); + os << " ;; Theory Lemmas\n"; + ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas(); + ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas(); + + for(size_t n = 0; it != end; ++it, ++n) { + if(n % 100 == 0) { + Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl; + } - for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; + NodeBuilder<> c(kind::AND); + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + prop::SatVariable var = lit.getSatVariable(); + if(lit.isNegated()) { + c << Node::fromExpr(getAtom(var)); + } else { + c << Node::fromExpr(getAtom(var)).notNode(); + } + } + Node cl = c; + if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { + uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; + TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); + if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { + Debug("cores") << "; extensional lemma!" << std::endl; + Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT); + TNode myk = cl[0][0][1]; + Debug("cores") << "; so my skolemized k is " << myk << std::endl; + os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n"; + paren << ")))"; + } + } + printAtomMapping(clause, os, paren); os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); - os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; + + Debug("cores") << "\n;id is " << id << std::endl; + if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { + uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; + Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl; + Assert(int32_t(proof_id & 0xffffffff) != -1); + TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); + Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl; + Debug("cores") << "; that means the lemma was " << orig << std::endl; + if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { + Debug("cores") << "; extensional" << std::endl; + os << "(clausify_false trust)\n"; + } else if(proof_id == 0) { + // theory propagation caused conflict + //ProofManager::currentPM()->printProof(os, cl); + os << "(clausify_false trust)\n"; + } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) { + os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; + //ProofManager::currentPM()->printProof(os, cl); + os << "(clausify_false trust)\n"; + } else { + os << "\n;; need to generate a (lemma) proof of " << cl; + os << "\n;; DON'T KNOW HOW !!\n"; + os << "(clausify_false trust)\n"; + } + } else { + os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; + ProofManager::currentPM()->printProof(os, cl); + } + os << clause_paren.str() + << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n"; paren << "))"; } } @@ -114,10 +172,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { - os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } else { - os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; + os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index b2c35c4f7..459815e60 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -30,62 +30,38 @@ namespace CVC4 { namespace prop { class CnfStream; -} +}/* CVC4::prop namespace */ class CnfProof; -class AtomIterator { - CnfProof& d_cnf; - ProofManager::var_iterator d_it; - -public: - AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it) - : d_cnf(cnf), d_it(it) - {} - inline Expr operator*(); - AtomIterator& operator++() { ++d_it; return *this; } - AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; } - bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; } - bool operator!=(const AtomIterator& it) const { return !(*this == it); } -};/* class AtomIterator */ - class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - Expr getAtom(prop::SatVariable var); - friend class AtomIterator; + VarSet d_atomsDeclared; public: CnfProof(CVC4::prop::CnfStream* cnfStream); - typedef AtomIterator iterator; - virtual iterator begin_atom_mapping() = 0; - virtual iterator end_atom_mapping() = 0; + Expr getAtom(prop::SatVariable var); + Expr getAssertion(uint64_t id); + prop::SatLiteral getLiteral(TNode atom); - virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; virtual ~CnfProof(); -}; +};/* class CnfProof */ class LFSCCnfProof : public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); + virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren); public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) {} - virtual iterator begin_atom_mapping(); - virtual iterator end_atom_mapping(); - - virtual void printAtomMapping(std::ostream& os, std::ostream& paren); virtual void printClauses(std::ostream& os, std::ostream& paren); -}; - -inline Expr AtomIterator::operator*() { - return d_cnf.getAtom(*d_it); -} +};/* class LFSCCnfProof */ } /* CVC4 namespace */ diff --git a/src/proof/proof.h b/src/proof/proof.h index 174913755..440279dbc 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -22,9 +22,9 @@ #include "smt/options.h" #ifdef CVC4_PROOF -# define PROOF(x) if(options::proof()) { x; } -# define NULLPROOF(x) (options::proof()) ? x : NULL -# define PROOF_ON() options::proof() +# define PROOF(x) if(options::proof() || options::unsatCores()) { x; } +# define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL +# define PROOF_ON() (options::proof() || options::unsatCores()) #else /* CVC4_PROOF */ # define PROOF(x) # define NULLPROOF(x) NULL diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 680e57d39..0cca16574 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -23,6 +23,15 @@ #include "util/cvc4_assert.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "theory/output_channel.h" +#include "theory/valuation.h" +#include "util/node_visitor.h" +#include "theory/term_registration_visitor.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine.h" +#include "theory/arrays/theory_arrays.h" +#include "context/context.h" +#include "util/hash.h" namespace CVC4 { @@ -37,7 +46,8 @@ ProofManager::ProofManager(ProofFormat format): d_cnfProof(NULL), d_theoryProof(NULL), d_fullProof(NULL), - d_format(format) + d_format(format), + d_deps() { } @@ -53,7 +63,7 @@ ProofManager::~ProofManager() { delete it->second; } - for(IdToClause::iterator it = d_theoryLemmas.begin(); + for(OrderedIdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { delete it->second; @@ -91,11 +101,10 @@ CnfProof* ProofManager::getCnfProof() { } TheoryProof* ProofManager::getTheoryProof() { - Assert (currentPM()->d_theoryProof); + //Assert (currentPM()->d_theoryProof); return currentPM()->d_theoryProof; } - void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); @@ -114,35 +123,101 @@ void ProofManager::initTheoryProof() { currentPM()->d_theoryProof = new LFSCTheoryProof(); } - -std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); } -std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); } +std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); } std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); } -std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); } -std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); } -std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } +std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); } +std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); } +std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); } + +std::string ProofManager::getAtomName(TNode atom) { + prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom); + Assert(!lit.isNegated()); + return getAtomName(lit.getSatVariable()); +} +std::string ProofManager::getLitName(TNode lit) { + return getLitName(currentPM()->d_cnfProof->getLiteral(lit)); +} + +void ProofManager::traceDeps(TNode n) { + Debug("cores") << "trace deps " << n << std::endl; + if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { + // originating formula was in core set + Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; + d_outputCoreFormulas.insert(n.toExpr()); + } else { + Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; + if(d_deps.find(n) == d_deps.end()) { + InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str()); + } + Assert(d_deps.find(n) != d_deps.end()); + std::vector deps = (*d_deps.find(n)).second; + for(std::vector::const_iterator i = deps.begin(); i != deps.end(); ++i) { + Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; + traceDeps(*i); + } + } +} void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { - for (unsigned i = 0; i < clause->size(); ++i) { + /*for (unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = clause->operator[](i); d_propVars.insert(lit.getSatVariable()); - } + }*/ if (kind == INPUT) { d_inputClauses.insert(std::make_pair(id, clause)); - return; + Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end()); + Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl; + if(d_satProof->d_inputClauses[id] == uint64_t(-1)) { + Debug("cores") << " + constant unit (true or false)" << std::endl; + } else if(options::unsatCores()) { + Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff); + Debug("cores") << "core input assertion from CnfStream is " << e << std::endl; + Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl; + // Invalid proof rules are currently used for parts of CVC4 that don't + // support proofs (these are e.g. unproven theory lemmas) or don't need + // proofs (e.g. split lemmas). We can ignore these safely when + // constructing unsat cores. + if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) { + // trace dependences back to actual assertions + traceDeps(Node::fromExpr(e)); + } + } + } else { + Assert(kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); } - Assert (kind == THEORY_LEMMA); - d_theoryLemmas.insert(std::make_pair(id, clause)); } -void ProofManager::addAssertion(Expr formula) { +void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { + Debug("cores") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); + d_deps[Node::fromExpr(formula)]; // empty vector of deps + if(inUnsatCore || options::dumpUnsatCores()) { + Debug("cores") << "adding to input core forms: " << formula << std::endl; + d_inputCoreFormulas.insert(formula); + } } -void ProofManager::setLogic(const std::string& logic_string) { - d_logic = logic_string; +void ProofManager::addDependence(TNode n, TNode dep) { + if(dep != n) { + Debug("cores") << "dep: " << n << " : " << dep << std::endl; + if(d_deps.find(dep) == d_deps.end()) { + Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl; + } + //Assert(d_deps.find(dep) != d_deps.end()); + d_deps[n].push_back(dep); + } +} + +void ProofManager::setLogic(const LogicInfo& logic) { + d_logic = logic; } +void ProofManager::printProof(std::ostream& os, TNode n) { + // no proofs here yet +} LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) @@ -157,17 +232,18 @@ void LFSCProof::toStream(std::ostream& out) { smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; + out << " ;; Declarations\n"; if (d_theoryProof == NULL) { d_theoryProof = new LFSCTheoryProof(); } - for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); + /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); i != d_cnfProof->end_atom_mapping(); ++i) { d_theoryProof->addDeclaration(*i); - } + }*/ d_theoryProof->printAssertions(out, paren); + out << " ;; Proof of empty clause follows\n"; out << "(: (holds cln)\n"; - d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); d_satProof->printResolutions(out, paren); paren <<")))\n;;"; @@ -175,5 +251,4 @@ void LFSCProof::toStream(std::ostream& out) { out << "\n"; } - } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index f428de36d..d60a3f6e3 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -20,9 +20,12 @@ #define __CVC4__PROOF_MANAGER_H #include +#include #include "proof/proof.h" #include "util/proof.h" - +#include "expr/node.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" // forward declarations namespace Minisat { @@ -63,6 +66,7 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause; typedef __gnu_cxx::hash_set VarSet; typedef __gnu_cxx::hash_set ExprSet; @@ -74,6 +78,18 @@ enum ClauseKind { LEARNT };/* enum ClauseKind */ +enum ProofRule { + RULE_GIVEN, /* input assertion */ + RULE_DERIVED, /* a "macro" rule */ + RULE_RECONSTRUCT, /* prove equivalence using another method */ + RULE_TRUST, /* trust without evidence (escape hatch until proofs are fully supported) */ + RULE_INVALID, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */ + RULE_CONFLICT, /* re-construct as a conflict */ + + RULE_ARRAYS_EXT, /* arrays, extensional */ + RULE_ARRAYS_ROW, /* arrays, read-over-write */ +};/* enum ProofRules */ + class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; @@ -81,15 +97,25 @@ class ProofManager { // information that will need to be shared across proofs IdToClause d_inputClauses; - IdToClause d_theoryLemmas; + OrderedIdToClause d_theoryLemmas; + IdToClause d_theoryPropagations; ExprSet d_inputFormulas; - VarSet d_propVars; + ExprSet d_inputCoreFormulas; + ExprSet d_outputCoreFormulas; + //VarSet d_propVars; + + int d_nextId; Proof* d_fullProof; ProofFormat d_format; // used for now only in debug builds + __gnu_cxx::hash_map< Node, std::vector, NodeHashFunction > d_deps; + + // trace dependences back to unsat core + void traceDeps(TNode n); + protected: - std::string d_logic; + LogicInfo d_logic; public: ProofManager(ProofFormat format = LFSC); @@ -109,35 +135,50 @@ public: // iterators over data shared by proofs typedef IdToClause::const_iterator clause_iterator; + typedef OrderedIdToClause::const_iterator ordered_clause_iterator; typedef ExprSet::const_iterator assertions_iterator; typedef VarSet::const_iterator var_iterator; clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } clause_iterator end_input_clauses() const { return d_inputClauses.end(); } + size_t num_input_clauses() const { return d_inputClauses.size(); } - clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } - clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } + ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } + ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } + size_t num_lemmas() const { return d_theoryLemmas.size(); } assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } + size_t num_assertions() const { return d_inputFormulas.size(); } - var_iterator begin_vars() const { return d_propVars.begin(); } - var_iterator end_vars() const { return d_propVars.end(); } + void printProof(std::ostream& os, TNode n); - void addAssertion(Expr formula); + void addAssertion(Expr formula, bool inUnsatCore); void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + // note that n depends on dep (for cores) + void addDependence(TNode n, TNode dep); + + assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } + assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } + size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } + + int nextId() { return d_nextId++; } // variable prefixes static std::string getInputClauseName(ClauseId id); + static std::string getLemmaName(ClauseId id); static std::string getLemmaClauseName(ClauseId id); static std::string getLearntClauseName(ClauseId id); static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); + static std::string getAtomName(TNode atom); static std::string getLitName(prop::SatLiteral lit); + static std::string getLitName(TNode lit); + + void setLogic(const LogicInfo& logic); + const std::string getLogic() const { return d_logic.getLogicString(); } - void setLogic(const std::string& logic_string); - const std::string getLogic() const { return d_logic; } };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 0ace84b4d..f7b9c4889 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -57,9 +57,6 @@ void printDebug (Minisat::Clause& c) { Debug("proof:sat") << endl; } - -int SatProof::d_idCounter = 0; - /** * Converts the clause associated to id to a set of literals * @@ -274,7 +271,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { Minisat::CRef SatProof::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { - Debug("proof:sat") << "proof:getClauseRef cannot find clause "<nextId(); d_clauseId[clause] = newId; d_idClause[newId] = clause; if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + d_inputClauses[newId] = proof_id; } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + d_lemmaClauses[newId] = proof_id; } } - Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; + Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n"; return d_clauseId[clause]; } -ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) { +ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) { + Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl; UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { - ClauseId newId = d_idCounter++; + ClauseId newId = ProofManager::currentPM()->nextId(); d_unitId[toInt(lit)] = newId; d_idUnit[newId] = lit; if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); - d_inputClauses.insert(newId); + d_inputClauses[newId] = proof_id; } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - d_lemmaClauses.insert(newId); + d_lemmaClauses[newId] = proof_id; } } - Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; + Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n"; return d_unitId[toInt(lit)]; } @@ -445,7 +442,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { removedDfs(*it, removed, removeStack, inClause, seen); } - for (int i = removeStack.size()-1; i >= 0; --i) { + for (int i = removeStack.size() - 1; i >= 0; --i) { Lit lit = removeStack[i]; CRef reason_ref = d_solver->reason(var(lit)); ClauseId reason_id; @@ -454,7 +451,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { Assert(isUnit(~lit)); reason_id = getUnitId(~lit); } else { - reason_id = registerClause(reason_ref); + reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1)); } res->addStep(lit, reason_id, !sign(lit)); } @@ -486,14 +483,14 @@ void SatProof::startResChain(::Minisat::CRef start) { } void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) { - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); res->addStep(lit, id, sign); } void SatProof::endResChain(CRef clause) { Assert(d_resStack.size() > 0); - ClauseId id = registerClause(clause); + ClauseId id = registerClause(clause, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); @@ -502,7 +499,7 @@ void SatProof::endResChain(CRef clause) { void SatProof::endResChain(::Minisat::Lit lit) { Assert(d_resStack.size() > 0); - ClauseId id = registerUnitClause(lit); + ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1)); ResChain* res = d_resStack.back(); registerResolution(id, res); d_resStack.pop_back(); @@ -523,6 +520,7 @@ void SatProof::resolveOutUnit(::Minisat::Lit lit) { } void SatProof::storeUnitResolution(::Minisat::Lit lit) { + Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; resolveUnit(lit); } @@ -536,7 +534,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { CRef reason_ref = d_solver->reason(var(lit)); Assert(reason_ref != CRef_Undef); - ClauseId reason_id = registerClause(reason_ref); + ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1)); ResChain* res = new ResChain(reason_id); // Here, the call to resolveUnit() can reallocate memory in the @@ -551,7 +549,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) { res->addStep(l, res_id, !sign(l)); } } - ClauseId unit_id = registerUnitClause(lit); + ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1)); registerResolution(unit_id, res); return unit_id; } @@ -561,11 +559,12 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } -void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) { +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) { + Debug("cores") << "STORE UNIT CONFLICT" << std::endl; Assert(!d_storedUnitConflict); - d_unitConflictId = registerUnitClause(conflict_lit, kind); + d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id); d_storedUnitConflict = true; - Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n"; } void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { @@ -586,7 +585,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { return; } else { Assert(!d_storedUnitConflict); - conflict_id = registerClause(conflict_ref); //FIXME + conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME } if(Debug.isOn("proof:sat")) { @@ -652,11 +651,10 @@ std::string SatProof::clauseName(ClauseId id) { if (isInputClause(id)) { os << ProofManager::getInputClauseName(id); return os.str(); - } else - if (isLemmaClause(id)) { + } else if (isLemmaClause(id)) { os << ProofManager::getLemmaClauseName(id); return os.str(); - }else { + } else { os << ProofManager::getLearntClauseName(id); return os.str(); } @@ -728,10 +726,9 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); - for (int i = steps.size()-1; i >= 0; i--) { + for (int i = steps.size() - 1; i >= 0; --i) { out << "("; out << (steps[i].sign? "R" : "Q") << " _ _ "; - } ClauseId start_id = res->getStart(); @@ -742,11 +739,13 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "< IdUnitMap; typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; +typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; typedef std::vector < ResChain* > ResStack; typedef std::hash_map IdToSatClause; typedef std::set < ClauseId > IdSet; @@ -115,14 +116,15 @@ protected: UnitIdMap d_unitId; IdHashSet d_deleted; IdToSatClause d_deletedTheoryLemmas; - IdHashSet d_inputClauses; - IdHashSet d_lemmaClauses; +public: + IdProofRuleMap d_inputClauses; + IdProofRuleMap d_lemmaClauses; +protected: // resolutions IdResMap d_resChains; ResStack d_resStack; bool d_checkRes; - static ClauseId d_idCounter; const ClauseId d_emptyClauseId; const ClauseId d_nullId; // proxy class to break circular dependencies @@ -144,6 +146,7 @@ protected: void printRes(ResChain* res); bool isInputClause(ClauseId id); + bool isTheoryConflict(ClauseId id); bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); bool isUnit(::Minisat::Lit lit); @@ -207,10 +210,10 @@ public: void finalizeProof(::Minisat::CRef conflict); /// clause registration methods - ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); - ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); + ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id); + ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); - void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT); + void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); /** * Marks the deleted clauses as deleted. Note we may still use them in the final @@ -242,6 +245,7 @@ public: protected: IdSet d_seenLearnt; IdHashSet d_seenInput; + IdHashSet d_seenTheoryConflicts; IdHashSet d_seenLemmas; inline std::string varName(::Minisat::Lit lit); diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 2121d7366..498b31ce5 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -45,7 +45,7 @@ void BVMinisatSatSolver::setNotify(Notify* notify) { d_minisat->setNotify(d_minisatNotify); } -void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) { +void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { Debug("sat::minisat") << "Add clause " << clause <<"\n"; BVMinisat::vec minisat_clause; toMinisatClause(clause, minisat_clause); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 0101c5d62..04f21e761 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -76,7 +76,7 @@ public: void setNotify(Notify* notify); - void addClause(SatClause& clause, bool removable); + void addClause(SatClause& clause, bool removable, uint64_t proof_id); SatValue propagate(); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e0697735f..0d133aa13 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,7 +44,6 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { - CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : d_satSolver(satSolver), d_booleanVariables(context), @@ -52,6 +51,7 @@ CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Contex d_literalToNodeMap(context), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar), + d_assertionTable(context), d_removable(false) { } @@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } - d_satSolver->addClause(c, d_removable); + d_satSolver->addClause(c, d_removable, d_proofId); } void CnfStream::assertClause(TNode node, SatLiteral a) { @@ -104,9 +104,9 @@ bool CnfStream::hasLiteral(TNode n) const { } void TseitinCnfStream::ensureLiteral(TNode n) { - - // These are not removable + // These are not removable and have no proof ID d_removable = false; + d_proofId = uint64_t(-1); Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { @@ -188,9 +188,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister // If a theory literal, we pre-register it if (preRegister) { - bool backup = d_removable; + // In case we are re-entered due to lemmas, save our state + bool backupRemovable = d_removable; + uint64_t backupProofId= d_proofId; d_registrar->preRegister(node); - d_removable = backup; + d_removable = backupRemovable; + d_proofId = backupProofId; } // Here, you can have it @@ -642,9 +645,20 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) { +void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; d_removable = removable; + if(options::proof() || options::unsatCores()) { + // Encode the assertion ID in the proof_id to store with generated clauses. + uint64_t assertionTableIndex = d_assertionTable.size(); + Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision"); + d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); + d_assertionTable.push_back(from.isNull() ? node : from); + Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; + } else { + // We aren't producing proofs or unsat cores; use an invalid proof id. + d_proofId = uint64_t(-1); + } convertAndAssert(node, negated); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 266362ef5..b76051279 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -28,6 +28,7 @@ #include "expr/node.h" #include "prop/theory_proxy.h" #include "prop/registrar.h" +#include "proof/proof_manager.h" #include "context/cdlist.h" #include "context/cdinsert_hashmap.h" @@ -36,7 +37,6 @@ namespace CVC4 { namespace prop { - class PropEngine; /** @@ -77,6 +77,9 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; + /** A table of assertions, used for regenerating proofs. */ + context::CDList d_assertionTable; + /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -103,11 +106,19 @@ protected: return node; } + /** + * A reference into the assertion table, used to map clauses back to + * their "original" input assertion/lemma. This variable is manipulated + * by the top-level convertAndAssert(). This is needed in proofs-enabled + * runs, to justify where the SAT solver's clauses came from. + */ + uint64_t d_proofId; + /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't - * need to be passed on over the stack. Only pure clauses can be asserted as - * removable. + * need to be passed on over the stack. Only pure clauses can be asserted + * as removable. */ bool d_removable; @@ -190,7 +201,7 @@ public: * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated */ - virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -222,6 +233,13 @@ public: */ SatLiteral getLiteral(TNode node); + /** + * Get the assertion with a given ID. (Used for reconstructing proofs.) + */ + TNode getAssertion(uint64_t id) { + return d_assertionTable[id]; + } + /** * Returns the Boolean variables from the input problem. */ @@ -258,7 +276,7 @@ public: * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated); + void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b0d710d66..5403b992e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -135,8 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); ) } @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -271,7 +271,7 @@ CRef Solver::reason(Var x) { return real_reason; } -bool Solver::addClause_(vec& ps, bool removable) +bool Solver::addClause_(vec& ps, bool removable, uint64_t proof_id) { if (!ok) return false; @@ -321,6 +321,8 @@ bool Solver::addClause_(vec& ps, bool removable) lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); + Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; + lemmas_proof_id.push(proof_id); } else { // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { @@ -329,7 +331,7 @@ bool Solver::addClause_(vec& ps, bool removable) // construct the clause below to give to the proof manager // as the final conflict. if(falseLiteralsCount == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); ) + PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); ) PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) return ok = false; } @@ -351,7 +353,7 @@ bool Solver::addClause_(vec& ps, bool removable) attachClause(cr); if(PROOF_ON()) { - PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); ) if(ps.size() == falseLiteralsCount) { PROOF( ProofManager::getSatProof()->finalizeProof(cr); ) return ok = false; @@ -364,11 +366,12 @@ bool Solver::addClause_(vec& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ); + Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl; + PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } ); CRef confl = propagate(CHECK_WITHOUT_THEORY); if(! (ok = (confl == CRef_Undef)) ) { if(ca[confl].size() == 1) { - PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); ); + PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); ); PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); ) } else { PROOF( ProofManager::getSatProof()->finalizeProof(confl); ); @@ -842,7 +845,7 @@ CRef Solver::propagate(TheoryCheckType type) propagateTheory(); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { - confl = updateLemmas(); + confl = updateLemmas(); } } else { // Even though in conflict, we still need to discharge the lemmas @@ -891,7 +894,7 @@ void Solver::propagateTheory() { proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); vec explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); - addClause(explanation, true); + addClause(explanation, true, 0); } } } @@ -1645,6 +1648,8 @@ CRef Solver::updateLemmas() { // The current lemma vec& lemma = lemmas[i]; bool removable = lemmas_removable[i]; + uint64_t proof_id = lemmas_proof_id[i]; + Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl; // Attach it if non-unit CRef lemma_ref = CRef_Undef; @@ -1659,7 +1664,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1667,7 +1672,7 @@ CRef Solver::updateLemmas() { } attachClause(lemma_ref); } else { - PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ); + PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); ); } // If the lemma is propagating enqueue its literal (or set the conflict) @@ -1681,7 +1686,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; - PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0]); ); + PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); ); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; @@ -1694,6 +1699,7 @@ CRef Solver::updateLemmas() { // Clear the lemmas lemmas.clear(); lemmas_removable.clear(); + lemmas_proof_id.clear(); if (conflict != CRef_Undef) { theoryConflict = true; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 7831f211b..2d70cfeef 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -37,12 +37,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "expr/command.h" namespace CVC4 { -class SatProof; - -namespace prop { - class TheoryProxy; -}/* CVC4::prop namespace */ + class SatProof; + namespace prop { + class TheoryProxy; + }/* CVC4::prop namespace */ }/* CVC4 namespace */ namespace Minisat { @@ -85,6 +84,9 @@ protected: /** Is the lemma removable */ vec lemmas_removable; + /** Proof IDs for lemmas */ + vec lemmas_proof_id; + /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -154,12 +156,14 @@ public: void push (); void pop (); - bool addClause (const vec& ps, bool removable); // Add a clause to the solver. + // CVC4 adds the "proof_id" here to refer to the input assertion/lemma + // that produced this clause + bool addClause (const vec& ps, bool removable, uint64_t proof_id); // Add a clause to the solver. bool addEmptyClause(bool removable); // Add the empty clause, making the solver contradictory. - bool addClause (Lit p, bool removable); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. - bool addClause_( vec& ps, bool removable); // Add a clause to the solver without making superflous internal copy. Will + bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. + bool addClause_( vec& ps, bool removable, uint64_t proof_id); // Add a clause to the solver without making superflous internal copy. Will // change the passed vector 'ps'. // Solving: @@ -489,11 +493,15 @@ inline void Solver::checkGarbage(double gf){ // NOTE: enqueue does not set the ok flag! (only public methods do) inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } -inline bool Solver::addClause (const vec& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } -inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } -inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } +inline bool Solver::addClause (const vec& ps, bool removable, uint64_t proof_id) + { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } +inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); } +inline bool Solver::addClause (Lit p, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } +inline bool Solver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } +inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 4a192d0d2..b50c1c09f 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -149,10 +149,10 @@ void MinisatSatSolver::setupOptions() { d_minisat->restart_inc = options::satRestartInc(); } -void MinisatSatSolver::addClause(SatClause& clause, bool removable) { +void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) { Minisat::vec minisat_clause; toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable); + d_minisat->addClause(minisat_clause, removable, proof_id); } SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { @@ -228,7 +228,7 @@ void MinisatSatSolver::push() { d_minisat->push(); } -void MinisatSatSolver::pop(){ +void MinisatSatSolver::pop() { d_minisat->pop(); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index b37371d98..3992f1adb 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -53,7 +53,7 @@ public: static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); - void addClause(SatClause& clause, bool removable); + void addClause(SatClause& clause, bool removable, uint64_t proof_id); SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 6dcdb76c7..71e747f72 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -159,7 +159,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec& ps, bool removable) +bool SimpSolver::addClause_(vec& ps, bool removable, uint64_t proof_id) { #ifndef NDEBUG if (use_simplification) { @@ -173,7 +173,7 @@ bool SimpSolver::addClause_(vec& ps, bool removable) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable)) + if (!Solver::addClause_(ps, removable, proof_id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -545,7 +545,7 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) { bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { return false; } } @@ -585,7 +585,7 @@ bool SimpSolver::substitute(Var v, Lit x) removeClause(cls[i]); - if (!addClause_(subst_clause, c.removable())) { + if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { return ok = false; } } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 878d799a5..041309546 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -47,12 +47,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); - bool addClause (const vec& ps, bool removable); - bool addEmptyClause(bool removable); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. - bool addClause_(vec& ps, bool removable); + bool addClause (const vec& ps, bool removable, uint64_t proof_id); + bool addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. + bool addClause_(vec& ps, bool removable, uint64_t proof_id); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (const vec& ps, bool removable, uint64_t proof_id) + { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id) { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 82c0bae1a..a02e40e32 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,6 +25,7 @@ #include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" +#include "proof/proof_manager.h" #include "util/cvc4_assert.h" #include "options/options.h" #include "smt/options.h" @@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable) { +void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as removable - d_cnfStream->convertAndAssert(node, removable, negated); + // Assert as (possibly) removable + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a5132e3da..ed022a64f 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,6 +25,7 @@ #include "options/options.h" #include "util/result.h" #include "smt/modal_exception.h" +#include "proof/proof_manager.h" #include namespace CVC4 { @@ -199,7 +200,7 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable); + void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 8e7e53474..e3b0f3449 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -24,6 +24,7 @@ #include "util/statistics_registry.h" #include "context/cdlist.h" #include "prop/sat_solver_types.h" +#include "expr/node.h" namespace CVC4 { namespace prop { @@ -38,7 +39,7 @@ public: virtual ~SatSolver() { } /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool removable) = 0; + virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0; /** * Create a new boolean variable in the solver. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 67325cb18..2bcd48099 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -122,7 +122,7 @@ void TheoryProxy::notifyRestart() { if(lemmaCount % 1 == 0) { Debug("shared") << "=) " << asNode << std::endl; } - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true); + d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); } else { Debug("shared") << "=(" << asNode << std::endl; } diff --git a/src/smt/options b/src/smt/options index 9c7eea12f..3ee3dbecb 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,9 +37,11 @@ option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response -# this is just a placeholder for later; it doesn't show up in command-line options listings -undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - turn on unsat core generation (NOT YET SUPPORTED) +option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + turn on unsat core generation +option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + output unsat cores after every UNSAT/VALID response + option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" support the get-assignment command diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 61e17801d..fcd625267 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -153,10 +153,6 @@ batch (default) \n\ (MiniSat) propagation for all of them only after reaching a querying command\n\ (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ \n\ -incremental\n\ -+ run nonclausal simplification and clausal propagation at each ASSERT\n\ - (and at CHECKSAT/QUERY/SUBTYPE)\n\ -\n\ none\n\ + do not perform nonclausal simplification\n\ "; @@ -283,8 +279,6 @@ inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEn inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "batch") { return SIMPLIFICATION_MODE_BATCH; - } else if(optarg == "incremental") { - return SIMPLIFICATION_MODE_INCREMENTAL; } else if(optarg == "none") { return SIMPLIFICATION_MODE_NONE; } else if(optarg == "help") { @@ -316,12 +310,6 @@ inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) th #endif /* CVC4_PROOF */ } -inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { - if(value) { - throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores"); - } -} - // This macro is used for setting :regular-output-channel and :diagnostic-output-channel // to redirect a stream. It maintains all attributes set on the stream. #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \ diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp index f728fa862..be46badfc 100644 --- a/src/smt/simplification_mode.cpp +++ b/src/smt/simplification_mode.cpp @@ -21,9 +21,6 @@ namespace CVC4 { std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { switch(mode) { - case SIMPLIFICATION_MODE_INCREMENTAL: - out << "SIMPLIFICATION_MODE_INCREMENTAL"; - break; case SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break; diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h index 2242e8bdf..b0b78d318 100644 --- a/src/smt/simplification_mode.h +++ b/src/smt/simplification_mode.h @@ -26,8 +26,6 @@ namespace CVC4 { /** Enumeration of simplification modes (when to simplify). */ typedef enum { - /** Simplify the assertions as they come in */ - SIMPLIFICATION_MODE_INCREMENTAL, /** Simplify the assertions all together once a check is requested */ SIMPLIFICATION_MODE_BATCH, /** Don't do simplification */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 77ee362c0..7b1f99403 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -48,6 +48,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "main/options.h" +#include "util/unsat_core.h" #include "util/proof.h" #include "proof/proof.h" #include "proof/proof_manager.h" @@ -137,6 +138,30 @@ public: Node getFormula() const { return d_formula; } };/* class DefinedFunction */ +class AssertionPipeline { + vector d_nodes; + +public: + + size_t size() const { return d_nodes.size(); } + + void resize(size_t n) { d_nodes.resize(n); } + void clear() { d_nodes.clear(); } + + Node& operator[](size_t i) { return d_nodes[i]; } + const Node& operator[](size_t i) const { return d_nodes[i]; } + void push_back(Node n) { d_nodes.push_back(n); } + + vector& ref() { return d_nodes; } + const vector& ref() const { return d_nodes; } + + void replace(size_t i, Node n) { + PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); ); + d_nodes[i] = n; + } + +};/* class AssertionPipeline */ + struct SmtEngineStatistics { /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; @@ -160,6 +185,8 @@ struct SmtEngineStatistics { TimerStat d_iteRemovalTime; /** time spent in theory preprocessing */ TimerStat d_theoryPreprocessTime; + /** time spent in theory preprocessing */ + TimerStat d_rewriteApplyToConstTime; /** time spent converting to CNF */ TimerStat d_cnfConversionTime; /** Num of assertions before ite removal */ @@ -192,6 +219,7 @@ struct SmtEngineStatistics { d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), + d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"), d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), @@ -214,10 +242,12 @@ struct SmtEngineStatistics { StatisticsRegistry::registerStat(&d_unconstrainedSimpTime); StatisticsRegistry::registerStat(&d_iteRemovalTime); StatisticsRegistry::registerStat(&d_theoryPreprocessTime); + StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime); StatisticsRegistry::registerStat(&d_cnfConversionTime); StatisticsRegistry::registerStat(&d_numAssertionsPre); StatisticsRegistry::registerStat(&d_numAssertionsPost); StatisticsRegistry::registerStat(&d_checkModelTime); + StatisticsRegistry::registerStat(&d_checkProofTime); StatisticsRegistry::registerStat(&d_solveTime); StatisticsRegistry::registerStat(&d_pushPopTime); StatisticsRegistry::registerStat(&d_processAssertionsTime); @@ -236,10 +266,12 @@ struct SmtEngineStatistics { StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime); StatisticsRegistry::unregisterStat(&d_iteRemovalTime); StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime); + StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime); StatisticsRegistry::unregisterStat(&d_cnfConversionTime); StatisticsRegistry::unregisterStat(&d_numAssertionsPre); StatisticsRegistry::unregisterStat(&d_numAssertionsPost); StatisticsRegistry::unregisterStat(&d_checkModelTime); + StatisticsRegistry::unregisterStat(&d_checkProofTime); StatisticsRegistry::unregisterStat(&d_solveTime); StatisticsRegistry::unregisterStat(&d_pushPopTime); StatisticsRegistry::unregisterStat(&d_processAssertionsTime); @@ -264,9 +296,6 @@ struct SmtEngineStatistics { class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; - /** The assertions yet to be preprocessed */ - vector d_assertionsToPreprocess; - /** Learned literals */ vector d_nonClausalLearnedLiterals; @@ -281,8 +310,8 @@ class SmtEnginePrivate : public NodeManagerListener { bool d_propagatorNeedsFinish; std::vector d_boolVars; - /** Assertions to push to sat */ - vector d_assertionsToCheck; + /** Assertions in the preprocessing pipeline */ + AssertionPipeline d_assertions; /** Whether any assertions have been processed */ CDO d_assertionsProcessed; @@ -319,7 +348,7 @@ class SmtEnginePrivate : public NodeManagerListener { public: /** - * Map from skolem variables to index in d_assertionsToCheck containing + * Map from skolem variables to index in d_assertions containing * corresponding introduced Boolean ite */ IteSkolemMap d_iteSkolemMap; @@ -375,7 +404,7 @@ private: bool simpITE(); // Simplify based on unconstrained values - void unconstrainedSimp(std::vector& assertions); + void unconstrainedSimp(); // Ensures the assertions asserted after before now // effectively come before d_realAssertionsEnd @@ -386,7 +415,7 @@ private: * (predicate subtype or integer subrange type) must be constrained * to be in that type. */ - void constrainSubtypes(TNode n, std::vector& assertions) + void constrainSubtypes(TNode n, AssertionPipeline& assertions) throw(); // trace nodes back to their assertions using CircuitPropagator's BackEdgesMap @@ -410,13 +439,12 @@ public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), - d_assertionsToPreprocess(), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), d_booleanTermConverter(NULL), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), - d_assertionsToCheck(), + d_assertions(), d_assertionsProcessed(smt.d_userContext, false), d_substitutionsIndex(smt.d_userContext, 0), d_fakeContext(), @@ -508,9 +536,8 @@ public: * someone does a push-assert-pop without a check-sat. */ void notifyPop() { - d_assertionsToPreprocess.clear(); + d_assertions.clear(); d_nonClausalLearnedLiterals.clear(); - d_assertionsToCheck.clear(); d_realAssertionsEnd = 0; d_iteSkolemMap.clear(); } @@ -546,7 +573,7 @@ public: hash_map cache; Node n = expandDefinitions(in, cache).toExpr(); // Make sure we've done all preprocessing, etc. - Assert(d_assertionsToCheck.size() == 0 && d_assertionsToPreprocess.size() == 0); + Assert(d_assertions.size() == 0); return applySubstitutions(n).toExpr(); } @@ -919,6 +946,64 @@ void SmtEngine::setDefaults() { } } + if(options::unsatCores()) { + if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { + if(options::simplificationMode.wasSetByUser()) { + throw OptionException("simplification not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl; + options::simplificationMode.set(SIMPLIFICATION_MODE_NONE); + } + + if(options::unconstrainedSimp()) { + if(options::unconstrainedSimp.wasSetByUser()) { + throw OptionException("unconstrained simplification not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl; + options::unconstrainedSimp.set(false); + } + + if(options::pbRewrites()) { + if(options::pbRewrites.wasSetByUser()) { + throw OptionException("pseudoboolean rewrites not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl; + setOption("pb-rewrites", false); + } + + if(options::sortInference()) { + if(options::sortInference.wasSetByUser()) { + throw OptionException("sort inference not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl; + options::sortInference.set(false); + } + + if(options::preSkolemQuant()) { + if(options::preSkolemQuant.wasSetByUser()) { + throw OptionException("pre-skolemization not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl; + options::preSkolemQuant.set(false); + } + + if(options::bitvectorToBool()) { + if(options::bitvectorToBool.wasSetByUser()) { + throw OptionException("bv-to-bool not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl; + options::bitvectorToBool.set(false); + } + + if(options::bvIntroducePow2()) { + if(options::bvIntroducePow2.wasSetByUser()) { + throw OptionException("bv-intro-pow2 not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl; + setOption("bv-intro-pow2", false); + } + } + if(options::produceAssignments() && !options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; setOption("produce-models", SExpr("true")); @@ -1626,11 +1711,10 @@ void SmtEnginePrivate::removeITEs() { Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; // Remove all of the ITE occurrences and normalize - d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]); + d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); } - } void SmtEnginePrivate::staticLearning() { @@ -1640,22 +1724,21 @@ void SmtEnginePrivate::staticLearning() { Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl; - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + for (unsigned i = 0; i < d_assertions.size(); ++ i) { NodeBuilder<> learned(kind::AND); - learned << d_assertionsToCheck[i]; - d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned); + learned << d_assertions[i]; + d_smt.d_theoryEngine->ppStaticLearn(d_assertions[i], learned); if(learned.getNumChildren() == 1) { learned.clear(); } else { - d_assertionsToCheck[i] = learned; + d_assertions.replace(i, learned); } } } // do dumping (before/after any preprocessing pass) -static void dumpAssertions(const char* key, - const std::vector& assertionList) { +static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) { if( Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key) ) { // Push the simplified assertions to the dump output stream @@ -1684,14 +1767,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); // Don't reprocess substitutions if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) { continue; } - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl; - d_propagator.assertTrue(d_assertionsToPreprocess[i]); + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl; + Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl; + d_propagator.assertTrue(d_assertions[i]); } Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -1700,8 +1784,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { // If in conflict, just return false Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict in non-clausal propagation" << endl; - d_assertionsToPreprocess.clear(); - d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + Node falseNode = NodeManager::currentNM()->mkConst(false); + Assert(!options::unsatCores()); + d_assertions.clear(); + d_assertions.push_back(falseNode); d_propagatorNeedsFinish = true; return false; } @@ -1738,8 +1824,9 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict with " << d_nonClausalLearnedLiterals[i] << endl; - d_assertionsToPreprocess.clear(); - d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + Assert(!options::unsatCores()); + d_assertions.clear(); + d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); d_propagatorNeedsFinish = true; return false; } @@ -1773,8 +1860,9 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict while solving " << learnedLiteral << endl; - d_assertionsToPreprocess.clear(); - d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + Assert(!options::unsatCores()); + d_assertions.clear(); + d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); d_propagatorNeedsFinish = true; return false; default: @@ -1799,8 +1887,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { // constantPropagations.simplifyLHS(t, c, equations, true); // if (!equations.empty()) { // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); - // d_assertionsToPreprocess.clear(); - // d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + // d_assertions.clear(); + // d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); // return; // } // d_topLevelSubstitutions.simplifyRHS(constantPropagations); @@ -1849,8 +1937,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { hash_set s; Trace("debugging") << "NonClausal simplify pre-preprocess\n"; - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Node assertion = d_assertionsToPreprocess[i]; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node assertion = d_assertions[i]; Node assertionNew = newSubstitutions.apply(assertion); Trace("debugging") << "assertion = " << assertion << endl; Trace("debugging") << "assertionNew = " << assertionNew << endl; @@ -1871,17 +1959,16 @@ bool SmtEnginePrivate::nonClausalSimplify() { } Trace("debugging") << "\n"; s.insert(assertion); - d_assertionsToCheck.push_back(assertion); + d_assertions.replace(i, assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal preprocessed: " << assertion << endl; } - d_assertionsToPreprocess.clear(); // If in incremental mode, add substitutions to the list of assertions if (d_substitutionsIndex > 0) { NodeBuilder<> substitutionsBuilder(kind::AND); - substitutionsBuilder << d_assertionsToCheck[d_substitutionsIndex]; + substitutionsBuilder << d_assertions[d_substitutionsIndex]; pos = newSubstitutions.begin(); for (; pos != newSubstitutions.end(); ++pos) { // Add back this substitution as an assertion @@ -1891,8 +1978,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; } if (substitutionsBuilder.getNumChildren() > 1) { - d_assertionsToCheck[d_substitutionsIndex] = - Rewriter::rewrite(Node(substitutionsBuilder)); + d_assertions.replace(d_substitutionsIndex, + Rewriter::rewrite(Node(substitutionsBuilder))); } } else { // If not in incremental mode, must add substitutions to model @@ -1908,8 +1995,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { } NodeBuilder<> learnedBuilder(kind::AND); - Assert(d_realAssertionsEnd <= d_assertionsToCheck.size()); - learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1]; + Assert(d_realAssertionsEnd <= d_assertions.size()); + learnedBuilder << d_assertions[d_realAssertionsEnd - 1]; for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { Node learned = d_nonClausalLearnedLiterals[i]; @@ -1938,7 +2025,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { } d_nonClausalLearnedLiterals.clear(); - for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { Node cProp = (*pos).first.eqNode((*pos).second); Assert(d_topLevelSubstitutions.apply(cProp) == cProp); @@ -1963,8 +2049,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { d_topLevelSubstitutions.addSubstitutions(newSubstitutions); if(learnedBuilder.getNumChildren() > 1) { - d_assertionsToCheck[d_realAssertionsEnd - 1] = - Rewriter::rewrite(Node(learnedBuilder)); + d_assertions.replace(d_realAssertionsEnd - 1, + Rewriter::rewrite(Node(learnedBuilder))); } d_propagatorNeedsFinish = true; @@ -1974,9 +2060,9 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvAbstraction() { Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl; std::vector new_assertions; - bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertionsToPreprocess, new_assertions); - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]); + bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, Rewriter::rewrite(new_assertions[i])); } // if we are using the lazy solver and the abstraction // applies, then UF symbols were introduced @@ -1991,9 +2077,9 @@ void SmtEnginePrivate::bvAbstraction() { void SmtEnginePrivate::bvToBool() { Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; std::vector new_assertions; - d_smt.d_theoryEngine->ppBvToBool(d_assertionsToPreprocess, new_assertions); - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]); + d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, Rewriter::rewrite(new_assertions[i])); } } @@ -2002,23 +2088,23 @@ bool SmtEnginePrivate::simpITE() { Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; - unsigned numAssertionOnEntry = d_assertionsToCheck.size(); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { - Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]); - d_assertionsToCheck[i] = result; + unsigned numAssertionOnEntry = d_assertions.size(); + for (unsigned i = 0; i < d_assertions.size(); ++i) { + Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]); + d_assertions.replace(i, result); if(result.isConst() && !result.getConst()){ return false; } } - bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck); - if(numAssertionOnEntry < d_assertionsToCheck.size()){ + bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref()); + if(numAssertionOnEntry < d_assertions.size()){ compressBeforeRealAssertions(numAssertionOnEntry); } return result; } void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ - size_t curr = d_assertionsToCheck.size(); + size_t curr = d_assertions.size(); if(before >= curr || d_realAssertionsEnd <= 0 || d_realAssertionsEnd >= curr){ @@ -2038,24 +2124,24 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ std::vector intoConjunction; for(size_t i = before; i& assertions) { +void SmtEnginePrivate::unconstrainedSimp() { TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; - d_smt.d_theoryEngine->ppUnconstrainedSimp(assertions); + d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref()); } -void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector& assertions) +void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions) throw() { Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl; @@ -2177,8 +2263,7 @@ size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_setmkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); - d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq))); + d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq))); SubstitutionMap nullMap(&d_fakeContext); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions status = d_smt.d_theoryEngine->solve(geq, nullMap); @@ -2460,7 +2545,7 @@ void SmtEnginePrivate::doMiplibTrick() { } newAssertion = Rewriter::rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; - d_assertionsToCheck.push_back(newAssertion); + d_assertions.push_back(newAssertion); Debug("miplib") << " assertions to remove: " << endl; for(vector::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) { Debug("miplib") << " " << *k << endl; @@ -2473,26 +2558,26 @@ void SmtEnginePrivate::doMiplibTrick() { if(!removeAssertions.empty()) { Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl; for(size_t i = 0; i < d_realAssertionsEnd; ++i) { - if(removeAssertions.find(d_assertionsToCheck[i].getId()) != removeAssertions.end()) { - Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertionsToCheck[i] << endl; - d_assertionsToCheck[i] = d_true; + if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) { + Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl; + d_assertions[i] = d_true; ++d_smt.d_stats->d_numMiplibAssertionsRemoved; - } else if(d_assertionsToCheck[i].getKind() == kind::AND) { - size_t removals = removeFromConjunction(d_assertionsToCheck[i], removeAssertions); + } else if(d_assertions[i].getKind() == kind::AND) { + size_t removals = removeFromConjunction(d_assertions[i], removeAssertions); if(removals > 0) { - Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertionsToCheck[i] << endl; + Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl; Debug("miplib") << "SmtEnginePrivate::simplify(): - by " << removals << " conjuncts" << endl; d_smt.d_stats->d_numMiplibAssertionsRemoved += removals; } } - Debug("miplib") << "had: " << d_assertionsToCheck[i] << endl; - d_assertionsToCheck[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToCheck[i])); - Debug("miplib") << "now: " << d_assertionsToCheck[i] << endl; + Debug("miplib") << "had: " << d_assertions[i] << endl; + d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])); + Debug("miplib") << "now: " << d_assertions[i] << endl; } } else { Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl; } - d_realAssertionsEnd = d_assertionsToCheck.size(); + d_realAssertionsEnd = d_assertions.size(); } @@ -2526,7 +2611,7 @@ bool SmtEnginePrivate::simplifyAssertions() // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) - d_realAssertionsEnd == d_assertionsToCheck.size() ) { + d_realAssertionsEnd == d_assertions.size() ) { Chat() << "...fixing miplib encodings..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "looking for miplib pseudobooleans..." << endl; @@ -2538,18 +2623,16 @@ bool SmtEnginePrivate::simplifyAssertions() Trace("simplify") << "SmtEnginePrivate::simplify(): " << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl; } - } else { - Assert(d_assertionsToCheck.empty()); - d_assertionsToCheck.swap(d_assertionsToPreprocess); } - dumpAssertions("post-nonclausal", d_assertionsToCheck); + dumpAssertions("post-nonclausal", d_assertions); Trace("smt") << "POST nonClausalSimplify" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; // before ppRewrite check if only core theory for BV theory - d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck); + d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref()); + + dumpAssertions("pre-theorypp", d_assertions); // Theory preprocessing if (d_smt.d_earlyTheoryPP) { @@ -2557,17 +2640,16 @@ bool SmtEnginePrivate::simplifyAssertions() TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); // Call the theory preprocessors d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]); - d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); - Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); + d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); + Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); } } - dumpAssertions("post-theorypp", d_assertionsToCheck); + dumpAssertions("post-theorypp", d_assertions); Trace("smt") << "POST theoryPP" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; // ITE simplification if(options::doITESimp() && @@ -2580,38 +2662,33 @@ bool SmtEnginePrivate::simplifyAssertions() } } - dumpAssertions("post-itesimp", d_assertionsToCheck); + dumpAssertions("post-itesimp", d_assertions); Trace("smt") << "POST iteSimp" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; // Unconstrained simplification if(options::unconstrainedSimp()) { Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(d_assertionsToCheck); + unconstrainedSimp(); } - dumpAssertions("post-unconstrained", d_assertionsToCheck); + dumpAssertions("post-unconstrained", d_assertions); Trace("smt") << "POST unconstrainedSimp" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << " doing repeated simplification" << endl; - d_assertionsToCheck.swap(d_assertionsToPreprocess); - Assert(d_assertionsToCheck.empty()); bool noConflict = nonClausalSimplify(); if(!noConflict) { return false; } } - dumpAssertions("post-repeatsimp", d_assertionsToCheck); + dumpAssertions("post-repeatsimp", d_assertions); Trace("smt") << "POST repeatSimp" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any @@ -2797,52 +2874,45 @@ void SmtEnginePrivate::processAssertions() { Assert(d_smt.d_pendingPops == 0); // Dump the assertions - dumpAssertions("pre-everything", d_assertionsToPreprocess); + dumpAssertions("pre-everything", d_assertions); Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - - Assert(d_assertionsToCheck.size() == 0); + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if (d_assertionsToPreprocess.size() == 0) { + if (d_assertions.size() == 0) { // nothing to do return; } - if (d_assertionsProcessed && - ( options::incrementalSolving() || - options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL )) { + if (d_assertionsProcessed && options::incrementalSolving()) { // Placeholder for storing substitutions - d_substitutionsIndex = d_assertionsToPreprocess.size(); - d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst(true)); + d_substitutionsIndex = d_assertions.size(); + d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); } // Add dummy assertion in last position - to be used as a // placeholder for any new assertions to get added - d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst(true)); + d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); // any assertions added beyond realAssertionsEnd must NOT affect the // equisatisfiability - d_realAssertionsEnd = d_assertionsToPreprocess.size(); + d_realAssertionsEnd = d_assertions.size(); // Assertions are NOT guaranteed to be rewritten by this point - dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess); + dumpAssertions("pre-definition-expansion", d_assertions); { Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); hash_map cache; - for(unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = - expandDefinitions(d_assertionsToPreprocess[i], cache); + for(unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, expandDefinitions(d_assertions[i], cache)); } } - dumpAssertions("post-definition-expansion", d_assertionsToPreprocess); + dumpAssertions("post-definition-expansion", d_assertions); - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && !d_smt.d_logic.isPure(THEORY_BV)) { @@ -2852,146 +2922,153 @@ void SmtEnginePrivate::processAssertions() { } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess); + d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref()); } if ( options::bvAbstraction() && !options::incrementalSolving()) { - dumpAssertions("pre-bv-abstraction", d_assertionsToPreprocess); + dumpAssertions("pre-bv-abstraction", d_assertions); bvAbstraction(); - dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess); + dumpAssertions("post-bv-abstraction", d_assertions); } - dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess); + dumpAssertions("pre-boolean-terms", d_assertions); { Chat() << "rewriting Boolean terms..." << endl; - for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { - d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]); + for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { + d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i])); } } - dumpAssertions("post-boolean-terms", d_assertionsToPreprocess); + dumpAssertions("post-boolean-terms", d_assertions); - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess); + dumpAssertions("pre-constrain-subtypes", d_assertions); { // Any variables of subtype types need to be constrained properly. // Careful, here: constrainSubtypes() adds to the back of - // d_assertionsToPreprocess, but we don't need to reprocess those. + // d_assertions, but we don't need to reprocess those. // We also can't use an iterator, because the vector may be moved in // memory during this loop. Chat() << "constraining subtypes..." << endl; - for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { - constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess); + for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { + constrainSubtypes(d_assertions[i], d_assertions); } } - dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess); + dumpAssertions("post-constrain-subtypes", d_assertions); - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + bool noConflict = true; // Unconstrained simplification if(options::unconstrainedSimp()) { - dumpAssertions("pre-unconstrained-simp", d_assertionsToPreprocess); + dumpAssertions("pre-unconstrained-simp", d_assertions); Chat() << "...doing unconstrained simplification..." << endl; - unconstrainedSimp(d_assertionsToPreprocess); - dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess); + unconstrainedSimp(); + dumpAssertions("post-unconstrained-simp", d_assertions); } if(options::bvIntroducePow2()){ - theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess); + theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref()); } - dumpAssertions("pre-substitution", d_assertionsToPreprocess); + dumpAssertions("pre-substitution", d_assertions); - // Apply the substitutions we already have, and normalize - Chat() << "applying substitutions..." << endl; - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " - << "applying substitutions" << endl; - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl; - d_assertionsToPreprocess[i] = - Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); - Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; + if(options::unsatCores()) { + // special rewriting pass for unsat cores, since many of the passes below are skipped + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); + } + } else { + // Apply the substitutions we already have, and normalize + if(!options::unsatCores()) { + Chat() << "applying substitutions..." << endl; + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "applying substitutions" << endl; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Trace("simplify") << "applying to " << d_assertions[i] << endl; + d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); + Trace("simplify") << " got " << d_assertions[i] << endl; + } + } } - dumpAssertions("post-substitution", d_assertionsToPreprocess); - // Assertions ARE guaranteed to be rewritten by this point + dumpAssertions("post-substitution", d_assertions); + // Assertions ARE guaranteed to be rewritten by this point // Lift bit-vectors of size 1 to bool if(options::bitvectorToBool()) { - dumpAssertions("pre-bv-to-bool", d_assertionsToPreprocess); + dumpAssertions("pre-bv-to-bool", d_assertions); Chat() << "...doing bvToBool..." << endl; bvToBool(); - dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess); + dumpAssertions("post-bv-to-bool", d_assertions); } if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); + dumpAssertions("pre-strings-pp", d_assertions); CVC4::theory::strings::StringsPreprocess sp; std::vector newNodes; - newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]); - sp.simplify( d_assertionsToPreprocess, newNodes ); + newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]); + sp.simplify( d_assertions.ref(), newNodes ); if(newNodes.size() > 1) { - d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); + d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); } - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions[i] = Rewriter::rewrite( d_assertions[i] ); } - dumpAssertions("post-strings-pp", d_assertionsToPreprocess); + dumpAssertions("post-strings-pp", d_assertions); } if( d_smt.d_logic.isQuantified() ){ //remove rewrite rules - for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) { - if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){ - Node prev = d_assertionsToPreprocess[i]; + for( unsigned i=0; i < d_assertions.size(); i++ ) { + if( d_assertions[i].getKind() == kind::REWRITE_RULE ){ + Node prev = d_assertions[i]; Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; - d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) ); + d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) ); Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; } } - dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); + dumpAssertions("pre-skolem-quant", d_assertions); if( options::preSkolemQuant() ){ //apply pre-skolemization to existential quantifiers - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Node prev = d_assertionsToPreprocess[i]; + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Node prev = d_assertions[i]; Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; vector< TypeNode > fvTypes; vector< TNode > fvs; - d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - if( prev!=d_assertionsToPreprocess[i] ){ - d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); + d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs )); + if( prev!=d_assertions[i] ){ + d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] )); Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; } } } - dumpAssertions("post-skolem-quant", d_assertionsToPreprocess); + dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion bool success; do{ quantifiers::QuantifierMacros qm; - success = qm.simplify( d_assertionsToPreprocess, true ); + success = qm.simplify( d_assertions.ref(), true ); }while( success ); } Trace("fo-rsn-enable") << std::endl; if( options::foPropQuant() ){ quantifiers::FirstOrderPropagation fop; - fop.simplify( d_assertionsToPreprocess ); + fop.simplify( d_assertions.ref() ); } } if( options::sortInference() ){ //sort inference technique SortInference * si = d_smt.d_theoryEngine->getSortInference(); - si->simplify( d_assertionsToPreprocess ); + si->simplify( d_assertions.ref() ); for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){ d_smt.setPrintFuncInModel( it->first.toExpr(), false ); d_smt.setPrintFuncInModel( it->second.toExpr(), true ); @@ -2999,25 +3076,25 @@ void SmtEnginePrivate::processAssertions() { } //if( options::quantConflictFind() ){ - // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess ); + // d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions ); //} if( options::pbRewrites() ){ - d_pbsProcessor.learn(d_assertionsToPreprocess); + d_pbsProcessor.learn(d_assertions.ref()); if(d_pbsProcessor.likelyToHelp()){ - d_pbsProcessor.applyReplacements(d_assertionsToPreprocess); + d_pbsProcessor.applyReplacements(d_assertions.ref()); } } - dumpAssertions("pre-simplify", d_assertionsToPreprocess); + dumpAssertions("pre-simplify", d_assertions); Chat() << "simplifying assertions..." << endl; - bool noConflict = simplifyAssertions(); + noConflict = simplifyAssertions(); if(!noConflict){ ++(d_smt.d_stats->d_simplifiedToFalse); } - dumpAssertions("post-simplify", d_assertionsToCheck); + dumpAssertions("post-simplify", d_assertions); - dumpAssertions("pre-static-learning", d_assertionsToCheck); + dumpAssertions("pre-static-learning", d_assertions); if(options::doStaticLearning()) { // Perform static learning Chat() << "doing static learning..." << endl; @@ -3025,27 +3102,25 @@ void SmtEnginePrivate::processAssertions() { << "performing static learning" << endl; staticLearning(); } - dumpAssertions("post-static-learning", d_assertionsToCheck); + dumpAssertions("post-static-learning", d_assertions); Trace("smt") << "POST bvToBool" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-ite-removal", d_assertionsToCheck); + dumpAssertions("pre-ite-removal", d_assertions); { Chat() << "removing term ITEs..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime); // Remove ITEs, updating d_iteSkolemMap - d_smt.d_stats->d_numAssertionsPre += d_assertionsToCheck.size(); + d_smt.d_stats->d_numAssertionsPre += d_assertions.size(); removeITEs(); - d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size(); + d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } - dumpAssertions("post-ite-removal", d_assertionsToCheck); + dumpAssertions("post-ite-removal", d_assertions); - dumpAssertions("pre-repeat-simplify", d_assertionsToCheck); + dumpAssertions("pre-repeat-simplify", d_assertions); if(options::repeatSimp()) { - d_assertionsToCheck.swap(d_assertionsToPreprocess); Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(); @@ -3074,11 +3149,11 @@ void SmtEnginePrivate::processAssertions() { IteSkolemMap::iterator it = d_iteSkolemMap.begin(); IteSkolemMap::iterator iend = d_iteSkolemMap.end(); NodeBuilder<> builder(kind::AND); - builder << d_assertionsToCheck[d_realAssertionsEnd - 1]; + builder << d_assertions[d_realAssertionsEnd - 1]; vector toErase; for (; it != iend; ++it) { if (skolemSet.find((*it).first) == skolemSet.end()) { - TNode iteExpr = d_assertionsToCheck[(*it).second]; + TNode iteExpr = d_assertions[(*it).second]; if (iteExpr.getKind() == kind::ITE && iteExpr[1].getKind() == kind::EQUAL && iteExpr[1][0] == (*it).first && @@ -3094,8 +3169,8 @@ void SmtEnginePrivate::processAssertions() { } } // Move this iteExpr into the main assertions - builder << d_assertionsToCheck[(*it).second]; - d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst(true); + builder << d_assertions[(*it).second]; + d_assertions[(*it).second] = NodeManager::currentNM()->mkConst(true); toErase.push_back((*it).first); } if(builder.getNumChildren() > 1) { @@ -3103,60 +3178,58 @@ void SmtEnginePrivate::processAssertions() { d_iteSkolemMap.erase(toErase.back()); toErase.pop_back(); } - d_assertionsToCheck[d_realAssertionsEnd - 1] = + d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); } // For some reason this is needed for some benchmarks, such as // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 // Figure it out later removeITEs(); - // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); + // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } } - dumpAssertions("post-repeat-simplify", d_assertionsToCheck); + dumpAssertions("post-repeat-simplify", d_assertions); - dumpAssertions("pre-rewrite-apply-to-const", d_assertionsToCheck); + dumpAssertions("pre-rewrite-apply-to-const", d_assertions); if(options::rewriteApplyToConst()) { Chat() << "Rewriting applies to constants..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertionsToCheck[i])); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i])); } } - dumpAssertions("post-rewrite-apply-to-const", d_assertionsToCheck); + dumpAssertions("post-rewrite-apply-to-const", d_assertions); // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones #ifdef CVC4_ASSERTIONS - unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); + unsigned iteRewriteAssertionsEnd = d_assertions.size(); #endif - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck); + dumpAssertions("pre-theory-preprocessing", d_assertions); { Chat() << "theory preprocessing..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); // Call the theory preprocessors d_smt.d_theoryEngine->preprocessStart(); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i])); } } - dumpAssertions("post-theory-preprocessing", d_assertionsToCheck); + dumpAssertions("post-theory-preprocessing", d_assertions); // If we are using eager bit-blasting wrap assertions in fake atom so that // everything gets bit-blasted to internal SAT solver if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) { - TNode atom = d_assertionsToCheck[i]; + for (unsigned i = 0; i < d_assertions.size(); ++i) { + TNode atom = d_assertions[i]; Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom); - d_assertionsToCheck[i] = eager_atom; + d_assertions.replace(i, eager_atom); TheoryModel* m = d_smt.d_theoryEngine->getModel(); m->addSubstitution(eager_atom, atom); } @@ -3165,36 +3238,36 @@ void SmtEnginePrivate::processAssertions() { // Push the formula to decision engine if(noConflict) { Chat() << "pushing to decision engine..." << endl; - Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); + Assert(iteRewriteAssertionsEnd == d_assertions.size()); d_smt.d_decisionEngine->addAssertions - (d_assertionsToCheck, d_realAssertionsEnd, d_iteSkolemMap); + (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap); } // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones - dumpAssertions("post-everything", d_assertionsToCheck); + dumpAssertions("post-everything", d_assertions); //set instantiation level of everything to zero if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ - for( unsigned i=0; i < d_assertionsToCheck.size(); i++ ) { - theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertionsToCheck[i], 0 ); + for( unsigned i=0; i < d_assertions.size(); i++ ) { + theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 ); } } - // Push the formula to SAT { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); + for (unsigned i = 0; i < d_assertions.size(); ++ i) { + Chat() << "+ " << d_assertions[i] << std::endl; + d_smt.d_propEngine->assertFormula(d_assertions[i]); } } d_assertionsProcessed = true; - d_assertionsToCheck.clear(); + d_assertions.clear(); d_iteSkolemMap.clear(); } @@ -3209,13 +3282,8 @@ void SmtEnginePrivate::addFormula(TNode n) Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; // Add the normalized formula to the queue - d_assertionsToPreprocess.push_back(n); - //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n)); - - // If the mode of processing is incremental prepreocess and assert immediately - if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) { - processAssertions(); - } + d_assertions.push_back(n); + //d_assertions.push_back(Rewriter::rewrite(n)); } void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { @@ -3230,7 +3298,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { +Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { Assert(ex.isNull() || ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -3251,7 +3319,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Ensure expr is type-checked at this point. ensureBoolean(e); // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e); ); + PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); ); } // check to see if a postsolve() is pending @@ -3313,7 +3381,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc return r; }/* SmtEngine::checkSat() */ -Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { +Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { Assert(!ex.isNull()); Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -3332,7 +3400,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3391,13 +3459,13 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept return r; }/* SmtEngine::query() */ -Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) { +Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex); ); + PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); ); Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; @@ -3410,7 +3478,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log } d_private->addFormula(e.getNode()); return quickCheck().asValidityResult(); -} +}/* SmtEngine::assertFormula() */ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { ModelPostprocessor mpost; @@ -3880,6 +3948,30 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } +UnsatCore SmtEngine::getUnsatCore() throw(ModalException) { + Trace("smt") << "SMT getUnsatCore()" << endl; + SmtScope smts(this); + finalOptionsAreSet(); + if(Dump.isOn("benchmark")) { + Dump("benchmark") << GetUnsatCoreCommand(); + } +#ifdef CVC4_PROOF + if(!options::unsatCores()) { + throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off."); + } + if(d_status.isNull() || + d_status.asSatisfiabilityResult() != Result::UNSAT || + d_problemExtended) { + throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); + } + + delete d_proofManager->getProof(this);// just to trigger core creation + return UnsatCore(d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core()); +#else /* CVC4_PROOF */ + throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores)."); +#endif /* CVC4_PROOF */ +} + Proof* SmtEngine::getProof() throw(ModalException) { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); @@ -3889,16 +3981,12 @@ Proof* SmtEngine::getProof() throw(ModalException) { } #ifdef CVC4_PROOF if(!options::proof()) { - const char* msg = - "Cannot get a proof when produce-proofs option is off."; - throw ModalException(msg); + throw ModalException("Cannot get a proof when produce-proofs option is off."); } if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - const char* msg = - "Cannot get a proof unless immediately preceded by UNSAT/VALID response."; - throw ModalException(msg); + throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); } return ProofManager::getProof(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1671654d1..ac0170f3b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,6 +28,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/proof.h" +#include "util/unsat_core.h" #include "smt/modal_exception.h" #include "smt/logic_exception.h" #include "options/options.h" @@ -255,7 +256,7 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEnginePrivate* d_private; /** - * Check that a generated Proof (via getProof()) checks. + * Check that a generated proof (via getProof()) checks. */ void checkProof(); @@ -424,8 +425,8 @@ public: /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for - * literals and conjunction of literals. Returns false iff - * inconsistent. + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. */ void defineFunction(Expr func, const std::vector& formals, @@ -434,23 +435,25 @@ public: /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for - * literals and conjunction of literals. Returns false iff - * inconsistent. + * literals and conjunction of literals. Returns false if + * immediately determined to be inconsistent. This version + * takes a Boolean flag to determine whether to include this asserted + * formula in an unsat core (if one is later requested). */ - Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException); + Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException); /** * 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 Expr& e) throw(TypeCheckingException, ModalException, LogicException); + Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException); + Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException); /** * Simplify a formula without doing "much" work. Does not involve @@ -506,6 +509,13 @@ public: */ void printInstantiations( std::ostream& out ); + /** + * Get an unsatisfiable core (only if immediately preceded by an + * UNSAT or VALID query). Only permitted if CVC4 was built with + * unsat-core support and produce-unsat-cores is on. + */ + UnsatCore getUnsatCore() throw(ModalException); + /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 54b9fa1d0..fb5810fd5 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -40,9 +40,14 @@ inline SmtEngine* currentSmtEngine() { } inline ProofManager* currentProofManager() { - Assert(PROOF_ON()); +#ifdef CVC4_PROOF + Assert(options::proof() || options::unsatCores()); Assert(s_smtEngine_current != NULL); return s_smtEngine_current->d_proofManager; +#else /* CVC4_PROOF */ + InternalError("proofs/unsat cores are not on, but ProofManager requested"); + return NULL; +#endif /* CVC4_PROOF */ } class SmtScope : public NodeManagerScope { diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 7dbef4041..169ac6fa7 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -144,7 +144,7 @@ private: } } - // Get the current assignement + // Get the current assignment AssignmentStatus state = d_state[n]; if(state != UNASSIGNED) { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 38b9a1a0a..877baec4e 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -56,7 +56,7 @@ EagerBitblaster::~EagerBitblaster() { } void EagerBitblaster::bbFormula(TNode node) { - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, TNode::null()); } /** @@ -85,7 +85,7 @@ void EagerBitblaster::bbAtom(TNode node) { AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); storeBBAtom(node, atom_definition); - d_cnfStream->convertAndAssert(atom_definition, false, false); + d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 101d8b082..f8927284f 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -114,7 +114,7 @@ void TLazyBitblaster::bbAtom(TNode node) { Assert (!atom_bb.isNull()); Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false); + d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); return; } @@ -126,7 +126,7 @@ void TLazyBitblaster::bbAtom(TNode node) { // asserting that the atom is true iff the definition holds Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false); + d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1b0270b94..53a529325 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -34,6 +34,8 @@ #include "smt/logic_exception.h" +#include "proof/proof_manager.h" + #include "util/node_visitor.h" #include "util/ite_removal.h" @@ -168,7 +170,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - PROOF (ProofManager::currentPM()->initTheoryProof(); ); + PROOF (ProofManager::initTheoryProof(); ); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); @@ -1385,10 +1387,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 5cf5da1e0..fc9192dd9 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -97,7 +97,9 @@ libutil_la_SOURCES = \ regexp.cpp \ bin_heap.h \ didyoumean.h \ - didyoumean.cpp + didyoumean.cpp \ + unsat_core.h \ + unsat_core.cpp libstatistics_la_SOURCES = \ statistics_registry.h \ @@ -156,7 +158,8 @@ EXTRA_DIST = \ uninterpreted_constant.i \ chain.i \ regexp.i \ - proof.i + proof.i \ + unsat_core.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 68d7d9a34..97a6338ce 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -19,6 +19,7 @@ #include "util/ite_removal.h" #include "expr/command.h" #include "theory/ite_utilities.h" +#include "proof/proof_manager.h" using namespace CVC4; using namespace std; @@ -47,13 +48,23 @@ size_t RemoveITE::collectedCacheSizes() const{ return d_containsVisitor->cache_size() + d_iteCache.size(); } -void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap) +void RemoveITE::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) { + size_t n = output.size(); for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { // Do this in two steps to avoid Node problems(?) // Appears related to bug 512, splitting this into two lines // fixes the bug on clang on Mac OS Node itesRemoved = run(output[i], output, iteSkolemMap, false); + // In some calling contexts, not necessary to report dependence information. + if(reportDeps && options::unsatCores()) { + // new assertions have a dependence on the node + PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) + while(n < output.size()) { + PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) + ++n; + } + } output[i] = itesRemoved; } } diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 83c55dab7..d71f9b13d 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -50,8 +50,11 @@ public: * contains a map from introduced skolem variables to the index in * assertions containing the new Boolean ite created in conjunction * with that skolem variable. + * + * With reportDeps true, report reasoning dependences to the proof + * manager (for unsat cores). */ - void run(std::vector& assertions, IteSkolemMap& iteSkolemMap); + void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); /** * Removes the ITE from the node by introducing skolem diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp new file mode 100644 index 000000000..27261635d --- /dev/null +++ b/src/util/unsat_core.cpp @@ -0,0 +1,41 @@ +/********************* */ +/*! \file unsat_core.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of unsat cores + ** + ** Representation of unsat cores. + **/ + +#include "util/unsat_core.h" +#include "expr/command.h" + +namespace CVC4 { + +UnsatCore::const_iterator UnsatCore::begin() const { + return d_core.begin(); +} + +UnsatCore::const_iterator UnsatCore::end() const { + return d_core.end(); +} + +void UnsatCore::toStream(std::ostream& out) const { + for(UnsatCore::const_iterator i = begin(); i != end(); ++i) { + out << AssertCommand(*i) << std::endl; + } +} + +std::ostream& operator<<(std::ostream& out, const UnsatCore& core) { + core.toStream(out); + return out; +} + +}/* CVC4 namespace */ diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h new file mode 100644 index 000000000..51724b33b --- /dev/null +++ b/src/util/unsat_core.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file unsat_core.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__UNSAT_CORE_H +#define __CVC4__UNSAT_CORE_H + +#include +#include +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC UnsatCore { + std::vector d_core; + +public: + UnsatCore() {} + + template + UnsatCore(T begin, T end) : d_core(begin, end) {} + + ~UnsatCore() {} + + typedef std::vector::const_iterator iterator; + typedef std::vector::const_iterator const_iterator; + + const_iterator begin() const; + const_iterator end() const; + + void toStream(std::ostream& out) const; + +};/* class UnsatCore */ + +std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__UNSAT_CORE_H */ diff --git a/src/util/unsat_core.i b/src/util/unsat_core.i new file mode 100644 index 000000000..78b1360e7 --- /dev/null +++ b/src/util/unsat_core.i @@ -0,0 +1,5 @@ +%{ +#include "util/unsat_core.h" +%} + +%include "util/unsat_core.h" -- cgit v1.2.3