AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+ -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include
AM_CXXFLAGS = -Wall -fvisibility=hidden -DNDEBUG
noinst_LTLIBRARIES = libminisat.la
#include "Solver.h"
#include "Sort.h"
+#include "prop/sat.h"
#include <cmath>
//=================================================================================================
namespace prop {
namespace minisat {
-Solver::Solver() :
+Solver::Solver(SatSolver* proxy, context::Context* context) :
+
+ // SMT stuff
+ proxy(proxy)
+ , context(context)
// Parameters: (formerly in 'SearchParams')
- var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
+ , var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02)
, restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
// More parameters:
//
void Solver::cancelUntil(int level) {
if (decisionLevel() > level){
- for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+ // Pop the SMT context
+ for (int l = trail_lim.size() - level; l > 0; --l)
+ context->pop();
+ // Now the minisat stuff
+ for (int c = trail.size()-1; c >= trail_lim[level]; c--) {
Var x = var(trail[c]);
assigns[x] = toInt(l_Undef);
- insertVarOrder(x); }
+ insertVarOrder(x);
+ }
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
- } }
+ }
+}
//=================================================================================================
}
+Clause* Solver::propagate()
+{
+ Clause* confl = NULL;
+
+ while(qhead < trail.size()) {
+ confl = propagateBool();
+ if (confl != NULL) break;
+ confl = propagateTheory();
+ if (confl != NULL) break;
+ }
+
+ return confl;
+}
+
/*_________________________________________________________________________________________________
|
-| propagate : [void] -> [Clause*]
+| propagateTheory : [void] -> [Clause*]
+|
+| Description:
+| Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned,
+| otherwise NULL.
+|
+| Note: the propagation queue might be NOT empty
+|________________________________________________________________________________________________@*/
+Clause* Solver::propagateTheory()
+{
+ SatClause clause;
+ proxy->theoryCheck(clause);
+ return NULL;
+}
+
+/*_________________________________________________________________________________________________
+|
+| propagateBool : [void] -> [Clause*]
|
| Description:
| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
| Post-conditions:
| * the propagation queue is empty, even if there was a conflict.
|________________________________________________________________________________________________@*/
-Clause* Solver::propagate()
+Clause* Solver::propagateBool()
{
Clause* confl = NULL;
int num_props = 0;
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#include "cvc4_private.h"
-
#ifndef __CVC4__PROP__MINISAT__SOLVER_H
#define __CVC4__PROP__MINISAT__SOLVER_H
+#include "cvc4_private.h"
+#include "context/context.h"
+
#include <cstdio>
#include <cassert>
#include "SolverTypes.h"
-
//=================================================================================================
// Solver -- the main class:
namespace CVC4 {
namespace prop {
-class SatSolverProxy;
+class SatSolver;
namespace minisat {
class Solver {
/** The only CVC4 entry point to the private solver data */
- friend class CVC4::prop::SatSolverProxy;
+ friend class CVC4::prop::SatSolver;
+
+protected:
+
+ /** The pointer to the proxy that provides interfaces to the SMT engine */
+ SatSolver* proxy;
+
+ /** The context from the SMT solver */
+ context::Context* context;
public:
// Constructor/Destructor:
//
- Solver();
+ Solver(SatSolver* proxy, context::Context* context);
CVC4_PUBLIC ~Solver();
// Problem specification:
void newDecisionLevel (); // Begins a new decision level.
void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined.
bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise.
- Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause.
+ Clause* propagate (); // Perform Boolean and Theory. Returns possibly conflicting clause.
+ Clause* propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause.
+ Clause* propagateTheory (); // Perform Theory propagation. Returns possibly conflicting clause.
void cancelUntil (int level); // Backtrack until a certain level.
void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
return (int)(drand(seed) * size); }
};
-
//=================================================================================================
// Implementation of inline methods:
-
inline void Solver::insertVarOrder(Var x) {
if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); }
inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
-inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
+inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); }
inline int Solver::decisionLevel () const { return trail_lim.size(); }
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); }
namespace prop {
namespace minisat {
-SimpSolver::SimpSolver() :
- grow (0)
+SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) :
+ Solver(proxy, context)
+ , grow (0)
, asymm_mode (false)
, redundancy_check (false)
, merges (0)
namespace CVC4 {
namespace prop {
+
+class SatSolver;
+
namespace minisat {
class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
- SimpSolver();
+ SimpSolver(SatSolver* proxy, context::Context* context);
CVC4_PUBLIC ~SimpSolver();
// Problem specification:
#include <map>
using namespace std;
+using namespace CVC4::context;
namespace CVC4 {
namespace prop {
PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
- TheoryEngine* te)
+ TheoryEngine* te, Context* context)
: d_inCheckSat(false),
d_options(opts),
d_decisionEngine(de),
- d_theoryEngine(te)
+ d_theoryEngine(te),
+ d_context(context)
{
Debug("prop") << "Constructing the PropEngine" << endl;
- d_satSolver = new SatSolver();
- SatSolverProxy::initSatSolver(d_satSolver, d_options);
+ d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
}
/** The theory engine we will be using */
TheoryEngine *d_theoryEngine;
- /** The SAT solver*/
+ context::Context* d_context;
+
+ /** The SAT solver proxy */
SatSolver* d_satSolver;
/** List of all of the assertions that need to be made */
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(const Options*, DecisionEngine*, TheoryEngine*);
+ PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*);
/**
* Destructor.
**/
#include "cvc4_private.h"
+#include "context/context.h"
+#include "theory/theory_engine.h"
#ifndef __CVC4__PROP__SAT_H
#define __CVC4__PROP__SAT_H
#include "prop/minisat/simp/SimpSolver.h"
namespace CVC4 {
+
+class TheoryEngine;
+
namespace prop {
-/** The solver we are using */
-typedef minisat::SimpSolver SatSolver;
+class PropEngine;
/** Type of the SAT variables */
typedef minisat::Var SatVariable;
* It's only accessible from the PropEngine, and should be treated with major
* care.
*/
-class SatSolverProxy {
+class SatSolver {
+
+ /** The prop engine we are using */
+ PropEngine* d_propEngine;
+
+ /** The theory engine we are using */
+ TheoryEngine* d_theoryEngine;
- /** Only the prop engine can modify the internals of the SAT solver */
- friend class PropEngine;
+ /** Context we will be using to synchronzie the sat solver */
+ context::Context* d_context;
- private:
+ /** Minisat solver */
+ minisat::SimpSolver* d_minisat;
- /**
- * Initializes the given sat solver with the given options.
- * @param satSolver the SAT solver
- * @param options the options
- */
- inline static void initSatSolver(SatSolver* satSolver,
- const Options* options) {
+ /** Remember the options */
+ Options* d_options;
+
+ public:
+
+ SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
+ context::Context* context, const Options* options)
+ : d_propEngine(propEngine),
+ d_theoryEngine(theoryEngine),
+ d_context(context)
+ {
+ // Create the solver
+ d_minisat = new minisat::SimpSolver(this, d_context);
// Setup the verbosity
- satSolver->verbosity = (options->verbosity > 0) ? 1 : -1;
+ d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
// Do not delete the satisfied clauses, just the learnt ones
- satSolver->remove_satisfied = false;
+ d_minisat->remove_satisfied = false;
+ }
+
+ ~SatSolver() {
+ delete d_minisat;
+ }
+
+ inline bool solve() {
+ return d_minisat->solve();
+ }
+
+ inline void addClause(SatClause& clause) {
+ d_minisat->addClause(clause);
+ }
+
+ inline SatVariable newVar() {
+ return d_minisat->newVar();
+ }
+
+ inline void theoryCheck(SatClause& conflict) {
}
};
NodeManagerScope nms(d_nodeManager);
d_decisionEngine = new DecisionEngine;
d_theoryEngine = new TheoryEngine(this, d_ctxt);
- d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine);
+ d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
}
SmtEngine::~SmtEngine() {
projects / cvc5.git / commitdiff