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.
// PropEngine* d_propEngine;
CnfStream* d_cnfStream;
- DPLLSatSolverInterface* d_satSolver;
+ CDCLTSatSolverInterface* d_satSolver;
context::Context* d_satContext;
context::UserContext* d_userContext;
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);
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):
//
simpDB_props(0),
order_heap(VarOrderLt(activity)),
progress_estimate(0),
- remove_satisfied(!enable_incremental)
+ remove_satisfied(!enableIncremental)
// Resource constraints:
//
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 */
#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"
#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 */
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>;
/** 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; }
// 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 ();
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)
d_minisat = new Minisat::SimpSolver(
theoryProxy,
d_context,
+ userContext,
+ pnm,
options::incrementalSolving()
|| options::decisionMode() != options::DecisionMode::INTERNAL);
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 {
namespace CVC4 {
namespace prop {
-class MinisatSatSolver : public DPLLSatSolverInterface {
-public:
-
+class MinisatSatSolver : public CDCLTSatSolverInterface
+{
+ public:
MinisatSatSolver(StatisticsRegistry* registry);
~MinisatSatSolver() override;
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
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 */
};/* class MinisatSatSolver::Statistics */
Statistics d_statistics;
-};/* class MinisatSatSolver */
+}; /* class MinisatSatSolver */
}/* CVC4::prop namespace */
}/* CVC4 namespace */
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),
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)),
clauses_persistent.shrink(i - j);
}
-
//=================================================================================================
// Garbage Collection methods:
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);
// 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 {
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();
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();
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 */
Context* satContext,
UserContext* userContext,
ResourceManager* rm,
- OutputManager& outMgr)
+ OutputManager& outMgr,
+ ProofNodeManager* pnm)
: d_inCheckSat(false),
d_theoryEngine(te),
d_context(satContext),
d_registrar(NULL),
d_cnfStream(NULL),
d_pfCnfStream(nullptr),
+ d_ppm(nullptr),
d_interrupted(false),
d_resourceManager(rm),
d_outMgr(outMgr)
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(
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);
#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"
namespace prop {
class CnfStream;
-class DPLLSatSolverInterface;
+class CDCLTSatSolverInterface;
class PropEngine;
context::Context* satContext,
context::UserContext* userContext,
ResourceManager* rm,
- OutputManager& outMgr);
+ OutputManager& outMgr,
+ ProofNodeManager* pnm);
/**
* Destructor.
/** 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
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;
/** 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 */
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
{
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);
// 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"))
{
public:
PropPfManager(context::UserContext* userContext,
ProofNodeManager* pnm,
- SatProofManager* satPM,
+ CDCLTSatSolverInterface* satSolver,
ProofCnfStream* cnfProof);
/** Saves assertion for later checking whether refutation proof is closed.
/** 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
#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 {
};/* 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;
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();
return new BVMinisatSatSolver(registry, mainSatContext, name);
}
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
StatisticsRegistry* registry)
{
return new MinisatSatSolver(registry);
#include <vector>
#include "context/context.h"
+#include "prop/minisat/minisat.h"
#include "prop/sat_solver.h"
#include "util/statistics_registry.h"
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 = "");
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());
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
projects / cvc5.git / commitdiff