From c51920039f10864f813ae1a4b4e765264a322256 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 14 Dec 2020 13:14:59 -0300 Subject: [PATCH] [proof-new] Updating interfaces between prop engine and minisat (#5664) This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface". Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code. --- src/decision/decision_engine.h | 5 +- src/prop/minisat/core/Solver.cc | 19 +++- src/prop/minisat/core/Solver.h | 114 ++++++++++++++---------- src/prop/minisat/minisat.cpp | 19 +++- src/prop/minisat/minisat.h | 22 +++-- src/prop/minisat/simp/SimpSolver.cc | 12 +-- src/prop/minisat/simp/SimpSolver.h | 129 ++++++++++++++++++---------- src/prop/prop_engine.cpp | 8 +- src/prop/prop_engine.h | 22 ++++- src/prop/prop_proof_manager.cpp | 8 +- src/prop/prop_proof_manager.h | 8 +- src/prop/sat_solver.h | 16 ++-- src/prop/sat_solver_factory.cpp | 2 +- src/prop/sat_solver_factory.h | 4 +- src/smt/smt_solver.cpp | 6 +- 15 files changed, 258 insertions(+), 136 deletions(-) diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index afa16397d..15dbf0d79 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -46,7 +46,7 @@ class DecisionEngine { // PropEngine* d_propEngine; CnfStream* d_cnfStream; - DPLLSatSolverInterface* d_satSolver; + CDCLTSatSolverInterface* d_satSolver; context::Context* d_satContext; context::UserContext* d_userContext; @@ -75,7 +75,8 @@ class DecisionEngine { Trace("decision") << "Destroying decision engine" << std::endl; } - void setSatSolver(DPLLSatSolverInterface* ss) { + void setSatSolver(CDCLTSatSolverInterface* ss) + { // setPropEngine should not be called more than once Assert(d_satSolver == NULL); Assert(ss != NULL); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e769ba6cc..c5158bb4f 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -148,11 +148,14 @@ class ScopedBool Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, - bool enable_incremental) + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm, + bool enableIncremental) : d_proxy(proxy), d_context(context), assertionLevel(0), - d_enable_incremental(enable_incremental), + d_pfManager(nullptr), + d_enable_incremental(enableIncremental), minisat_busy(false) // Parameters (user settable): // @@ -209,7 +212,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, simpDB_props(0), order_heap(VarOrderLt(activity)), progress_estimate(0), - remove_satisfied(!enable_incremental) + remove_satisfied(!enableIncremental) // Resource constraints: // @@ -2118,5 +2121,15 @@ inline bool Solver::withinBudget(ResourceManager::Resource r) const return within_budget; } +SatProofManager* Solver::getProofManager() +{ + return d_pfManager ? d_pfManager.get() : nullptr; +} + +std::shared_ptr Solver::getProof() +{ + return d_pfManager ? d_pfManager->getProof() : nullptr; +} + } /* CVC4::Minisat namespace */ } /* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index f3bcfb67e..270cc9308 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "context/context.h" +#include "expr/proof_node_manager.h" #include "proof/clause_id.h" #include "prop/minisat/core/SolverTypes.h" #include "prop/minisat/mtl/Alg.h" @@ -36,12 +37,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/sat_proof_manager.h" #include "theory/theory.h" - namespace CVC4 { template class TSatProof; namespace prop { - class TheoryProxy; +class PropEngine; +class TheoryProxy; }/* CVC4::prop namespace */ }/* CVC4 namespace */ @@ -55,6 +56,7 @@ namespace Minisat { class Solver { /** The only two CVC4 entry points to the private solver data */ + friend class CVC4::prop::PropEngine; friend class CVC4::prop::TheoryProxy; friend class CVC4::prop::SatProofManager; friend class CVC4::TSatProof; @@ -85,6 +87,9 @@ public: /** Variable representing false */ Var varFalse; + /** The resolution proof manager */ + std::unique_ptr d_pfManager; + public: /** Returns the current user assertion level */ int getAssertionLevel() const { return assertionLevel; } @@ -129,51 +134,66 @@ public: // Constructor/Destructor: // - Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false); - CVC4_PUBLIC virtual ~Solver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); // Add a new variable with parameters specifying variable mode. - Var trueVar() const { return varTrue; } - Var falseVar() const { return varFalse; } - - // Less than for literals in a lemma - struct lemma_lt { - Solver& d_solver; - lemma_lt(Solver& solver) : d_solver(solver) {} - bool operator()(Lit x, Lit y) - { - lbool x_value = d_solver.value(x); - lbool y_value = d_solver.value(y); - // Two unassigned literals are sorted arbitrarily - if (x_value == l_Undef && y_value == l_Undef) - { - return x < y; - } - // Unassigned literals are put to front - if (x_value == l_Undef) return true; - if (y_value == l_Undef) return false; - // Literals of the same value are sorted by decreasing levels - if (x_value == y_value) - { - return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y)); - } - else - { - // True literals go up front - if (x_value == l_True) - { - return true; - } - else - { - return false; - } - } - } - }; - + Solver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm, + bool enableIncremental = false); + CVC4_PUBLIC virtual ~Solver(); + + // Problem specification: + // + Var newVar(bool polarity = true, + bool dvar = true, + bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true); // Add a new variable with parameters + // specifying variable mode. + Var trueVar() const { return varTrue; } + Var falseVar() const { return varFalse; } + + /** Retrive the SAT proof manager */ + CVC4::prop::SatProofManager* getProofManager(); + + /** Retrive the refutation proof */ + std::shared_ptr getProof(); + + // Less than for literals in a lemma + struct lemma_lt + { + Solver& d_solver; + lemma_lt(Solver& solver) : d_solver(solver) {} + bool operator()(Lit x, Lit y) + { + lbool x_value = d_solver.value(x); + lbool y_value = d_solver.value(y); + // Two unassigned literals are sorted arbitrarily + if (x_value == l_Undef && y_value == l_Undef) + { + return x < y; + } + // Unassigned literals are put to front + if (x_value == l_Undef) return true; + if (y_value == l_Undef) return false; + // Literals of the same value are sorted by decreasing levels + if (x_value == y_value) + { + return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y)); + } + else + { + // True literals go up front + if (x_value == l_True) + { + return true; + } + else + { + return false; + } + } + } + }; // CVC4 context push/pop void push (); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index aae347caf..8af73140e 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -102,8 +102,11 @@ void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, Assert((unsigned)clause.size() == sat_clause.size()); } -void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { - +void MinisatSatSolver::initialize(context::Context* context, + TheoryProxy* theoryProxy, + context::UserContext* userContext, + ProofNodeManager* pnm) +{ d_context = context; if (options::decisionMode() != options::DecisionMode::INTERNAL) @@ -116,6 +119,8 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_minisat = new Minisat::SimpSolver( theoryProxy, d_context, + userContext, + pnm, options::incrementalSolving() || options::decisionMode() != options::DecisionMode::INTERNAL); @@ -218,6 +223,16 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const { return d_minisat->isDecision( decn ); } +SatProofManager* MinisatSatSolver::getProofManager() +{ + return d_minisat->getProofManager(); +} + +std::shared_ptr MinisatSatSolver::getProof() +{ + return d_minisat->getProof(); +} + /** Incremental interface */ unsigned MinisatSatSolver::getAssertionLevel() const { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index e2b5699f7..959095757 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -23,9 +23,9 @@ namespace CVC4 { namespace prop { -class MinisatSatSolver : public DPLLSatSolverInterface { -public: - +class MinisatSatSolver : public CDCLTSatSolverInterface +{ + public: MinisatSatSolver(StatisticsRegistry* registry); ~MinisatSatSolver() override; @@ -38,7 +38,10 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); - void initialize(context::Context* context, TheoryProxy* theoryProxy) override; + void initialize(context::Context* context, + TheoryProxy* theoryProxy, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm) override; ClauseId addClause(SatClause& clause, bool removable) override; ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override @@ -79,6 +82,15 @@ public: bool isDecision(SatVariable decn) const override; + /** Retrieve a pointer to the unerlying solver. */ + Minisat::SimpSolver* getSolver() { return d_minisat; } + + /** Retrieve the proof manager of this SAT solver. */ + SatProofManager* getProofManager(); + + /** Retrieve the refutation proof of this SAT solver. */ + std::shared_ptr getProof() override; + private: /** The SatSolver used */ @@ -104,7 +116,7 @@ public: };/* class MinisatSatSolver::Statistics */ Statistics d_statistics; -};/* class MinisatSatSolver */ +}; /* class MinisatSatSolver */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 0ec8981ca..5c8922360 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -49,8 +49,10 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm, bool enableIncremental) - : Solver(proxy, context, enableIncremental), + : Solver(proxy, context, userContext, pnm, enableIncremental), grow(opt_grow), clause_lim(opt_clause_lim), subsumption_lim(opt_subsumption_lim), @@ -62,10 +64,9 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, asymm_lits(0), eliminated_vars(0), elimorder(1), - use_simplification( - !enableIncremental - && !options::unsatCores()) // TODO: turn off simplifications if - // proofs are on initially + use_simplification(!enableIncremental && !options::unsatCores() + && !pnm) // TODO: turn off simplifications if + // proofs are on initially , occurs(ClauseDeleted(ca)), elim_heap(ElimLt(n_occ)), @@ -733,7 +734,6 @@ void SimpSolver::cleanUpClauses() clauses_persistent.shrink(i - j); } - //================================================================================================= // Garbage Collection methods: diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index c13ee5583..f952aee1e 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -43,41 +43,66 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false); - CVC4_PUBLIC ~SimpSolver(); - - // 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, ClauseId& id); - bool addEmptyClause(bool removable); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver. - bool addClause_(vec& ps, bool removable, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may cause a contradiction). - - // Variable mode: - // - void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. - bool isEliminated(Var v) const; - - // Solving: - // - lbool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solve ( bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); - bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. - - // Memory managment: - // - void garbageCollect() override; - - // Generate a (possibly simplified) DIMACS file: - // + SimpSolver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm, + bool enableIncremental = false); + CVC4_PUBLIC ~SimpSolver(); + + // 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, ClauseId& id); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause(Lit p, + bool removable, + ClauseId& id); // Add a unit clause to the solver. + bool addClause(Lit p, + Lit q, + bool removable, + ClauseId& id); // Add a binary clause to the solver. + bool addClause(Lit p, + Lit q, + Lit r, + bool removable, + ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec& ps, bool removable, ClauseId& id); + bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may + // cause a contradiction). + + // Variable mode: + // + void setFrozen(Var v, + bool b); // If a variable is frozen it will not be eliminated. + bool isEliminated(Var v) const; + + // Solving: + // + lbool solve(const vec& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(const vec& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solve(bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + lbool solve( + Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + bool eliminate(bool turn_off_elim = false); // Perform variable elimination + // based simplification. + + // Memory managment: + // + void garbageCollect() override; + + // Generate a (possibly simplified) DIMACS file: + // #if 0 void toDimacs (const char* file, const vec& assumps); void toDimacs (const char* file); @@ -118,11 +143,13 @@ class SimpSolver : public Solver { // old ordering function // bool operator()(Var x, Var y) const { return cost(x) < cost(y); } - - bool operator()(Var x, Var y) const { - int c_x = cost(x); - int c_y = cost(y); - return c_x < c_y || (c_x == c_y && x < y); } + + bool operator()(Var x, Var y) const + { + int c_x = cost(x); + int c_y = cost(y); + return c_x < c_y || (c_x == c_y && x < y); + } }; struct ClauseDeleted { @@ -200,14 +227,14 @@ inline lbool SimpSolver::solve ( bool do_simp, bool t assumptions.clear(); return solve_(do_simp, turn_off_simp); } - + inline lbool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp); } - + inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); @@ -215,7 +242,7 @@ inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool t assumptions.push(q); return solve_(do_simp, turn_off_simp); } - + inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); @@ -225,16 +252,24 @@ inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool t return solve_(do_simp, turn_off_simp); } - inline lbool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ + inline lbool SimpSolver::solve(const vec& assumps, + bool do_simp, + bool turn_off_simp) + { budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } -inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bool turn_off_simp){ - assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } + inline lbool SimpSolver::solveLimited(const vec& assumps, + bool do_simp, + bool turn_off_simp) + { + assumps.copyTo(assumptions); + return solve_(do_simp, turn_off_simp); + } -//================================================================================================= + //================================================================================================= } /* CVC4::Minisat namespace */ } /* CVC4 namespace */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e5efcbf8f..fee73babb 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -70,7 +70,8 @@ PropEngine::PropEngine(TheoryEngine* te, Context* satContext, UserContext* userContext, ResourceManager* rm, - OutputManager& outMgr) + OutputManager& outMgr, + ProofNodeManager* pnm) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), @@ -79,6 +80,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar(NULL), d_cnfStream(NULL), d_pfCnfStream(nullptr), + d_ppm(nullptr), d_interrupted(false), d_resourceManager(rm), d_outMgr(outMgr) @@ -89,7 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies - d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); + d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( @@ -97,7 +99,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); - d_satSolver->initialize(d_context, d_theoryProxy); + d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index b36b9d22a..b311558ab 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,7 +28,12 @@ #include "options/options.h" #include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" +#include "prop/minisat/core/Solver.h" +#include "prop/minisat/minisat.h" #include "prop/proof_cnf_stream.h" +#include "prop/prop_proof_manager.h" +#include "prop/sat_solver_types.h" +#include "theory/trust_node.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -47,7 +52,7 @@ namespace theory { namespace prop { class CnfStream; -class DPLLSatSolverInterface; +class CDCLTSatSolverInterface; class PropEngine; @@ -65,7 +70,8 @@ class PropEngine context::Context* satContext, context::UserContext* userContext, ResourceManager* rm, - OutputManager& outMgr); + OutputManager& outMgr, + ProofNodeManager* pnm); /** * Destructor. @@ -239,6 +245,10 @@ class PropEngine /** Retrieve this modules proof CNF stream. */ ProofCnfStream* getProofCnfStream(); + /** Checks that the proof is closed w.r.t. asserted formulas to this engine as + * well as to the given assertions. */ + void checkProof(context::CDList* assertions); + /** * Return the prop engine proof. This should be called only when proofs are * enabled. Returns a proof of false whose free assumptions are the @@ -268,7 +278,7 @@ class PropEngine TheoryProxy* d_theoryProxy; /** The SAT solver proxy */ - DPLLSatSolverInterface* d_satSolver; + CDCLTSatSolverInterface* d_satSolver; /** List of all of the assertions that need to be made */ std::vector d_assertionList; @@ -276,11 +286,17 @@ class PropEngine /** Theory registrar; kept around for destructor cleanup */ theory::TheoryRegistrar* d_registrar; + /** A pointer to the proof node maneger to be used by this engine. */ + ProofNodeManager* d_pnm; + /** The CNF converter in use */ CnfStream* d_cnfStream; /** Proof-producing CNF converter */ std::unique_ptr d_pfCnfStream; + /** The proof manager for prop engine */ + std::unique_ptr d_ppm; + /** Whether we were just interrupted (or not) */ bool d_interrupted; /** Pointer to resource manager for associated SmtEngine */ diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 3b1df8a00..3c18dc896 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -22,11 +22,11 @@ namespace prop { PropPfManager::PropPfManager(context::UserContext* userContext, ProofNodeManager* pnm, - SatProofManager* satPM, + CDCLTSatSolverInterface* satSolver, ProofCnfStream* cnfProof) : d_pnm(pnm), d_pfpp(new ProofPostproccess(pnm, cnfProof)), - d_satPM(satPM), + d_satSolver(satSolver), d_assertions(userContext) { // add trivial assumption. This is so that we can check the that the prop @@ -47,7 +47,7 @@ void PropPfManager::checkProof(context::CDList* assertions) { Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution " "proof of false is closed\n"; - std::shared_ptr conflictProof = d_satPM->getProof(); + std::shared_ptr conflictProof = d_satSolver->getProof(); Assert(conflictProof); // connect it with CNF proof d_pfpp->process(conflictProof); @@ -66,7 +66,7 @@ std::shared_ptr PropPfManager::getProof() // retrieve the SAT solver's refutation proof Trace("sat-proof") << "PropPfManager::getProof: Getting resolution proof of false\n"; - std::shared_ptr conflictProof = d_satPM->getProof(); + std::shared_ptr conflictProof = d_satSolver->getProof(); Assert(conflictProof); if (Trace.isOn("sat-proof")) { diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index f3deee5bc..fc0151bcd 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -39,7 +39,7 @@ class PropPfManager public: PropPfManager(context::UserContext* userContext, ProofNodeManager* pnm, - SatProofManager* satPM, + CDCLTSatSolverInterface* satSolver, ProofCnfStream* cnfProof); /** Saves assertion for later checking whether refutation proof is closed. @@ -78,9 +78,9 @@ class PropPfManager /** The proof post-processor */ std::unique_ptr d_pfpp; /** - * The SAT solver's proof manager, which will provide a refutation - * proofresolution proof when requested */ - SatProofManager* d_satPM; + * The SAT solver of this prop engine, which should provide a refutation + * proof when requested */ + CDCLTSatSolverInterface* d_satSolver; /** Assertions corresponding to the leaves of the prop engine's proof. * * These are kept in a context-dependent manner since the prop engine's proof diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index a842647bd..10ee843df 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -24,9 +24,10 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" +#include "expr/proof_node_manager.h" #include "proof/clause_id.h" -#include "prop/sat_solver_types.h" #include "prop/bv_sat_solver_notify.h" +#include "prop/sat_solver_types.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -122,13 +123,15 @@ public: };/* class BVSatSolverInterface */ -class DPLLSatSolverInterface : public SatSolver +class CDCLTSatSolverInterface : public SatSolver { public: - virtual ~DPLLSatSolverInterface(){}; + virtual ~CDCLTSatSolverInterface(){}; virtual void initialize(context::Context* context, - prop::TheoryProxy* theoryProxy) = 0; + prop::TheoryProxy* theoryProxy, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm) = 0; virtual void push() = 0; @@ -145,7 +148,10 @@ class DPLLSatSolverInterface : public SatSolver virtual void requirePhase(SatLiteral lit) = 0; virtual bool isDecision(SatVariable decn) const = 0; -}; /* class DPLLSatSolverInterface */ + + virtual std::shared_ptr getProof() = 0; + +}; /* class CDCLTSatSolverInterface */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { out << lit.toString(); diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index cfdbc8b04..c6213f5a0 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -33,7 +33,7 @@ BVSatSolverInterface* SatSolverFactory::createMinisat( return new BVMinisatSatSolver(registry, mainSatContext, name); } -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat( +MinisatSatSolver* SatSolverFactory::createCDCLTMinisat( StatisticsRegistry* registry) { return new MinisatSatSolver(registry); diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 75069e63b..0bf6116cb 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -23,6 +23,7 @@ #include #include "context/context.h" +#include "prop/minisat/minisat.h" #include "prop/sat_solver.h" #include "util/statistics_registry.h" @@ -36,8 +37,7 @@ class SatSolverFactory StatisticsRegistry* registry, const std::string& name = ""); - static DPLLSatSolverInterface* createDPLLMinisat( - StatisticsRegistry* registry); + static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry* registry); static SatSolver* createCryptoMinisat(StatisticsRegistry* registry, const std::string& name = ""); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c18dfe8ac..e53401f79 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -71,7 +71,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_smt.getContext(), d_smt.getUserContext(), d_rm, - d_smt.getOutputManager())); + d_smt.getOutputManager(), + d_pnm)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -91,7 +92,8 @@ void SmtSolver::resetAssertions() d_smt.getContext(), d_smt.getUserContext(), d_rm, - d_smt.getOutputManager())); + d_smt.getOutputManager(), + d_pnm)); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not -- 2.30.2