From 16c0d86ae359fc16064e29ed7545db5896366c9b Mon Sep 17 00:00:00 2001 From: guykatzz Date: Thu, 23 Mar 2017 14:13:46 -0700 Subject: [PATCH] support incremental unsat cores --- src/proof/bitvector_proof.cpp | 2 +- src/proof/bitvector_proof.h | 1 + src/proof/proof_manager.cpp | 61 ++++++++++++++++++++++---- src/proof/proof_manager.h | 27 ++++++++---- src/proof/sat_proof.h | 19 +++++--- src/proof/sat_proof_implementation.h | 65 ++++++++++++++++++++-------- src/proof/unsat_core.h | 3 +- src/prop/minisat/core/Solver.cc | 2 +- src/smt/smt_engine.cpp | 6 +-- 9 files changed, 139 insertions(+), 47 deletions(-) diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 926dae9fd..ebe82cd91 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -47,7 +47,7 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proo void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { Assert (d_resolutionProof == NULL); - d_resolutionProof = new LFSCBVSatProof(solver, "bb", true); + d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true); } void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 6b952e35c..fcd1d2584 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -85,6 +85,7 @@ protected: std::map d_constantLetMap; bool d_useConstantLetification; + context::Context d_fakeContext; public: BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d8eefdcf0..cbc7f591a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -56,17 +56,18 @@ std::string append(const std::string& str, uint64_t num) { return os.str(); } -ProofManager::ProofManager(ProofFormat format): +ProofManager::ProofManager(context::Context* context, ProofFormat format): + d_context(context), d_satProof(NULL), d_cnfProof(NULL), d_theoryProof(NULL), d_inputFormulas(), - d_inputCoreFormulas(), - d_outputCoreFormulas(), + d_inputCoreFormulas(context), + d_outputCoreFormulas(context), d_nextId(0), d_fullProof(NULL), d_format(format), - d_deps() + d_deps(context) { } @@ -141,7 +142,7 @@ SkolemizationManager* ProofManager::getSkolemizationManager() { void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); - currentPM()->d_satProof = new LFSCCoreSatProof(solver, ""); + currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, ""); } void ProofManager::initCnfProof(prop::CnfStream* cnfStream, @@ -293,13 +294,45 @@ void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) { } } +void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) { + Debug("cores") << "trace deps " << n << std::endl; + if ((n.isConst() && n == NodeManager::currentNM()->mkConst(true)) || + (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst(false))) { + return; + } + if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { + // originating formula was in core set + Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; + coreAssertions->insert(n.toExpr()); + } else { + Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; + if(d_deps.find(n) == d_deps.end()) { + if (options::allowEmptyDependencies()) { + Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl; + return; + } + 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; + if( !(*i).isNull() ){ + traceDeps(*i, coreAssertions); + } + } + } +} + void ProofManager::traceUnsatCore() { Assert (options::unsatCores()); - constructSatProof(); + d_satProof->refreshProof(); IdToSatClause used_lemmas; IdToSatClause used_inputs; d_satProof->collectClausesUsed(used_inputs, used_lemmas); + IdToSatClause::const_iterator it = used_inputs.begin(); for(; it != used_inputs.end(); ++it) { Node node = d_cnfProof->getAssertionForClause(it->first); @@ -320,6 +353,17 @@ bool ProofManager::unsatCoreAvailable() const { return d_satProof->derivedEmptyClause(); } +std::vector ProofManager::extractUnsatCore() { + std::vector result; + output_core_iterator it = begin_unsat_core(); + output_core_iterator end = end_unsat_core(); + while ( it != end ) { + result.push_back(*it); + ++it; + } + return result; +} + void ProofManager::constructSatProof() { if (!d_satProof->proofConstructed()) { d_satProof->constructProof(); @@ -476,8 +520,9 @@ void ProofManager::addDependence(TNode n, TNode dep) { if( !dep.isNull() && 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); + std::vector deps = d_deps[n].get(); + deps.push_back(dep); + d_deps[n].set(deps); } } diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 19215589f..31638e8ee 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -22,6 +22,8 @@ #include #include #include "expr/node.h" +#include "context/cdhashset.h" +#include "context/cdhashmap.h" #include "proof/clause_id.h" #include "proof/proof.h" #include "proof/proof_utils.h" @@ -95,9 +97,11 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; -typedef __gnu_cxx::hash_set ExprSet; +typedef __gnu_cxx::hash_set ExprSet; +typedef context::CDHashSet CDExprSet; typedef __gnu_cxx::hash_set NodeSet; typedef __gnu_cxx::hash_map, NodeHashFunction > NodeToNodes; +typedef context::CDHashMap, NodeHashFunction > CDNodeToNodes; typedef std::hash_set IdHashSet; enum ProofRule { @@ -139,6 +143,8 @@ private: }; class ProofManager { + context::Context* d_context; + CoreSatProof* d_satProof; CnfProof* d_cnfProof; TheoryProofEngine* d_theoryProof; @@ -146,8 +152,8 @@ class ProofManager { // information that will need to be shared across proofs ExprSet d_inputFormulas; std::map d_inputFormulaToName; - ExprSet d_inputCoreFormulas; - ExprSet d_outputCoreFormulas; + CDExprSet d_inputCoreFormulas; + CDExprSet d_outputCoreFormulas; SkolemizationManager d_skolemizationManager; @@ -156,7 +162,7 @@ class ProofManager { Proof* d_fullProof; ProofFormat d_format; // used for now only in debug builds - NodeToNodes d_deps; + CDNodeToNodes d_deps; std::set d_printedTypes; @@ -169,13 +175,13 @@ protected: LogicInfo d_logic; public: - ProofManager(ProofFormat format = LFSC); + ProofManager(context::Context* context, ProofFormat format = LFSC); ~ProofManager(); static ProofManager* currentPM(); // initialization - static void initSatProof(Minisat::Solver* solver); + void initSatProof(Minisat::Solver* solver); static void initCnfProof(CVC4::prop::CnfStream* cnfStream, context::Context* ctx); static void initTheoryProofEngine(); @@ -248,10 +254,15 @@ public: // trace dependences back to unsat core void traceDeps(TNode n, ExprSet* coreAssertions); + void traceDeps(TNode n, CDExprSet* coreAssertions); void traceUnsatCore(); - assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } - assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } + + typedef CDExprSet::const_iterator output_core_iterator; + + output_core_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } + output_core_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } + std::vector extractUnsatCore(); bool unsatCoreAvailable() const; void getLemmasInUnsatCore(theory::TheoryId theory, std::vector &lemmas); diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 52e059e95..5691d1bd2 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -28,6 +28,7 @@ #include #include +#include "context/cdhashmap.h" #include "expr/expr.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" @@ -101,9 +102,9 @@ class TSatProof { typedef std::set VarSet; typedef std::hash_map IdCRefMap; typedef std::hash_map ClauseIdMap; - typedef std::hash_map IdUnitMap; - typedef std::hash_map UnitIdMap; - typedef std::hash_map IdResMap; + typedef context::CDHashMap IdUnitMap; + typedef context::CDHashMap UnitIdMap; + typedef context::CDHashMap IdResMap; typedef std::hash_map IdProofRuleMap; typedef std::vector ResStack; typedef std::set IdSet; @@ -113,7 +114,8 @@ class TSatProof { typedef __gnu_cxx::hash_map IdToConflicts; public: - TSatProof(Solver* solver, const std::string& name, bool checkRes = false); + TSatProof(Solver* solver, context::Context* context, + const std::string& name, bool checkRes = false); virtual ~TSatProof(); void setCnfProof(CnfProof* cnf_proof); @@ -198,6 +200,8 @@ class TSatProof { */ void constructProof(ClauseId id); void constructProof() { constructProof(d_emptyClauseId); } + void refreshProof(ClauseId id); + void refreshProof() { refreshProof(d_emptyClauseId); } bool proofConstructed() const; void collectClauses(ClauseId id); bool derivedEmptyClause() const; @@ -298,6 +302,7 @@ class TSatProof { // Internal data. typename Solver::Solver* d_solver; + context::Context* d_context; CnfProof* d_cnfProof; // clauses @@ -389,9 +394,9 @@ template class LFSCSatProof : public TSatProof { private: public: - LFSCSatProof(SatSolver* solver, const std::string& name, - bool checkRes = false) - : TSatProof(solver, name, checkRes) {} + LFSCSatProof(SatSolver* solver, context::Context* context, + const std::string& name, bool checkRes = false) + : TSatProof(solver, context, name, checkRes) {} virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); virtual void printResolutions(std::ostream& out, std::ostream& paren); diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 603559da1..bcc849906 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -196,20 +196,22 @@ void ProofProxy::updateCRef(typename Solver::TCRef oldref, /// SatProof template -TSatProof::TSatProof(Solver* solver, const std::string& name, - bool checkRes) +TSatProof::TSatProof(Solver* solver, context::Context* context, + const std::string& name, bool checkRes) : d_solver(solver), + d_context(context), d_cnfProof(NULL), d_idClause(), d_clauseId(), - d_idUnit(), + d_idUnit(context), + d_unitId(context), d_deleted(), d_inputClauses(), d_lemmaClauses(), d_assumptions(), d_assumptionConflicts(), d_assumptionConflictsDebug(), - d_resolutionChains(), + d_resolutionChains(d_context), d_resStack(), d_checkRes(checkRes), d_emptyClauseId(ClauseIdEmpty), @@ -263,7 +265,7 @@ TSatProof::~TSatProof() { ResolutionChainIterator resolution_it = d_resolutionChains.begin(); ResolutionChainIterator resolution_it_end = d_resolutionChains.end(); for (; resolution_it != resolution_it_end; ++resolution_it) { - ResChain* current = resolution_it->second; + ResChain* current = (*resolution_it).second; delete current; } @@ -378,7 +380,7 @@ template ClauseId TSatProof::getClauseIdForLiteral( typename Solver::TLit lit) const { Assert(hasClauseIdForLiteral(lit)); - return d_unitId.find(toInt(lit))->second; + return (*d_unitId.find(toInt(lit))).second; } template @@ -432,7 +434,7 @@ bool TSatProof::isUnit(ClauseId id) const { template typename Solver::TLit TSatProof::getUnit(ClauseId id) const { Assert(isUnit(id)); - return d_idUnit.find(id)->second; + return (*d_idUnit.find(id)).second; } template @@ -443,7 +445,7 @@ bool TSatProof::isUnit(typename Solver::TLit lit) const { template ClauseId TSatProof::getUnitId(typename Solver::TLit lit) const { Assert(isUnit(lit)); - return d_unitId.find(toInt(lit))->second; + return (*d_unitId.find(toInt(lit))).second; } template @@ -455,7 +457,7 @@ template const typename TSatProof::ResolutionChain& TSatProof::getResolutionChain(ClauseId id) const { Assert(hasResolutionChain(id)); - const ResolutionChain* chain = d_resolutionChains.find(id)->second; + const ResolutionChain* chain = (*d_resolutionChains.find(id)).second; return *chain; } @@ -535,6 +537,7 @@ ClauseId TSatProof::registerClause(typename Solver::TCRef clause, typename ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); + d_clauseId.insert(std::make_pair(clause, newId)); d_idClause.insert(std::make_pair(newId, clause)); if (kind == INPUT) { @@ -568,8 +571,11 @@ ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); if (it == d_unitId.end()) { ClauseId newId = ProofManager::currentPM()->nextId(); - d_unitId.insert(std::make_pair(toInt(lit), newId)); - d_idUnit.insert(std::make_pair(newId, lit)); + + if (d_unitId.find(toInt(lit)) == d_unitId.end()) + d_unitId[toInt(lit)] = newId; + if (d_idUnit.find(newId) == d_idUnit.end()) + d_idUnit[newId] = lit; if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); @@ -719,13 +725,12 @@ void TSatProof::registerResolution(ClauseId id, ResChain* res) { // could be the case that a resolution chain for this clause already // exists (e.g. when removing units in addClause). if (hasResolutionChain(id)) { - ResChain* current = d_resolutionChains.find(id)->second; + ResChain* current = (*d_resolutionChains.find(id)).second; delete current; - d_resolutionChains.erase(id); } - Assert(!hasResolutionChain(id)); + if (d_resolutionChains.find(id) == d_resolutionChains.end()) + d_resolutionChains.insert(id, res); - d_resolutionChains.insert(std::make_pair(id, res)); if (Debug.isOn("proof:sat")) { printRes(id); } @@ -823,6 +828,7 @@ void TSatProof::storeUnitResolution(typename Solver::TLit lit) { template ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { // first check if we already have a resolution for lit + if (isUnit(lit)) { ClauseId id = getClauseIdForLiteral(lit); Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id)); @@ -882,10 +888,9 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { typename Solver::TLit lit = d_idUnit[conflict_id]; ClauseId res_id = resolveUnit(~lit); res->addStep(lit, res_id, !sign(lit)); - registerResolution(d_emptyClauseId, res); - return; + } else { Assert(!d_storedUnitConflict); conflict_id = registerClause(conflict_ref, LEARNT); // FIXME @@ -894,6 +899,7 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { if (Debug.isOn("proof:sat")) { Debug("proof:sat") << "proof::finalizeProof Final Conflict "; print(conflict_id); + Debug("proof:sat") << std::endl; } ResChain* res = new ResChain(conflict_id); @@ -907,6 +913,7 @@ void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { res->addStep(lit, res_id, !sign(lit)); conflict_size = conflict.size(); } + registerResolution(d_emptyClauseId, res); } @@ -962,6 +969,30 @@ void TSatProof::constructProof(ClauseId conflict) { collectClauses(conflict); } +template +void TSatProof::refreshProof(ClauseId conflict) { + IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin(); + IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end(); + + for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) { + if (d_deletedTheoryLemmas.find(seen_lemma_it->first) == d_deletedTheoryLemmas.end()) + delete seen_lemma_it->second; + } + + IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin(); + IdToSatClause::const_iterator seen_input_end = d_seenInputs.end(); + + for (; seen_input_it != seen_input_end; ++seen_input_it) { + delete seen_input_it->second; + } + + d_seenInputs.clear(); + d_seenLemmas.clear(); + d_seenLearnt.clear(); + + collectClauses(conflict); +} + template bool TSatProof::proofConstructed() const { return d_satProofConstructed; diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h index a238f0a6a..50a01bedb 100644 --- a/src/proof/unsat_core.h +++ b/src/proof/unsat_core.h @@ -45,8 +45,7 @@ class CVC4_PUBLIC UnsatCore { public: UnsatCore() : d_smt(NULL) {} - template - UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) { + UnsatCore(SmtEngine* smt, std::vector core) : d_smt(smt), d_core(core) { initMessage(); } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d898b66a2..26af5f146 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -131,7 +131,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, , propagation_budget (-1) , asynch_interrupt (false) { - PROOF(ProofManager::initSatProof(this);) + PROOF(ProofManager::currentPM()->initSatProof(this);) // Create the constant variables varTrue = newVar(true, false, false); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 998967c5e..911728cb1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1012,7 +1012,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : // being parsed from the input file. Because of this, we cannot trust // that options::proof() is set correctly yet. #ifdef CVC4_PROOF - d_proofManager = new ProofManager(); + d_proofManager = new ProofManager(d_userContext); #endif // We have mutual dependency here, so we add the prop engine to the theory @@ -1996,7 +1996,7 @@ void SmtEngine::setDefaults() { } } - if(options::incrementalSolving() && (options::proof() || options::unsatCores())) { + if(options::incrementalSolving() && options::proof()) { Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof or --produce-unsat-cores, try --tear-down-incremental instead)" << endl; setOption("incremental", SExpr("false")); } @@ -5054,7 +5054,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti } d_proofManager->traceUnsatCore();// just to trigger core creation - return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core()); + return UnsatCore(this, d_proofManager->extractUnsatCore()); #else /* IS_PROOFS_BUILD */ throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores)."); #endif /* IS_PROOFS_BUILD */ -- 2.30.2