summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.h5
-rw-r--r--src/prop/minisat/core/Solver.cc19
-rw-r--r--src/prop/minisat/core/Solver.h114
-rw-r--r--src/prop/minisat/minisat.cpp19
-rw-r--r--src/prop/minisat/minisat.h22
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc12
-rw-r--r--src/prop/minisat/simp/SimpSolver.h129
-rw-r--r--src/prop/prop_engine.cpp8
-rw-r--r--src/prop/prop_engine.h22
-rw-r--r--src/prop/prop_proof_manager.cpp8
-rw-r--r--src/prop/prop_proof_manager.h8
-rw-r--r--src/prop/sat_solver.h16
-rw-r--r--src/prop/sat_solver_factory.cpp2
-rw-r--r--src/prop/sat_solver_factory.h4
-rw-r--r--src/smt/smt_solver.cpp6
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<ProofNode> 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 Solver> 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<Minisat::Solver>;
@@ -85,6 +87,9 @@ public:
/** Variable representing false */
Var varFalse;
+ /** The resolution proof manager */
+ std::unique_ptr<CVC4::prop::SatProofManager> 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<ProofNode> 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<ProofNode> 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::Lit>& 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<ProofNode> 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<Lit>& 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<Lit>& 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<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
- lbool solveLimited(const vec<Lit>& 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<Lit>& 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<Lit>& 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<Lit>& assumps,
+ bool do_simp = true,
+ bool turn_off_simp = false);
+ lbool solveLimited(const vec<Lit>& 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<Lit>& 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<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ inline lbool SimpSolver::solve(const vec<Lit>& 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<Lit>& assumps, bool do_simp, bool turn_off_simp){
- assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+ inline lbool SimpSolver::solveLimited(const vec<Lit>& 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<Node>* 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<Node> 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<ProofCnfStream> d_pfCnfStream;
+ /** The proof manager for prop engine */
+ std::unique_ptr<PropPfManager> 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<Node>* assertions)
{
Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution "
"proof of false is closed\n";
- std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+ std::shared_ptr<ProofNode> conflictProof = d_satSolver->getProof();
Assert(conflictProof);
// connect it with CNF proof
d_pfpp->process(conflictProof);
@@ -66,7 +66,7 @@ std::shared_ptr<ProofNode> PropPfManager::getProof()
// retrieve the SAT solver's refutation proof
Trace("sat-proof")
<< "PropPfManager::getProof: Getting resolution proof of false\n";
- std::shared_ptr<ProofNode> conflictProof = d_satPM->getProof();
+ std::shared_ptr<ProofNode> 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<prop::ProofPostproccess> 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<ProofNode> 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 <vector>
#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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback