diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/prop | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.C | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 25 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 12 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Alg.h | 8 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BasicHeap.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BoxedVec.h | 34 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Heap.h | 17 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Map.h | 10 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Sort.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 12 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 19 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 123 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 23 |
15 files changed, 240 insertions, 73 deletions
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index d7a7bf8e1..4ea33e101 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Constructor/Destructor: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { Solver::Solver() : @@ -741,6 +742,7 @@ void Solver::checkLiteralCount() } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index e53cefc24..2383fd68c 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,14 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef CVC4_MiniSat_Solver_h -#define CVC4_MiniSat_Solver_h +#ifndef __CVC4__PROP__MINISAT__SOLVER_H +#define __CVC4__PROP__MINISAT__SOLVER_H #include <cstdio> +#include <cassert> -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" +#include "cvc4_config.h" +#include "../mtl/Vec.h" +#include "../mtl/Heap.h" +#include "../mtl/Alg.h" #include "SolverTypes.h" @@ -33,7 +35,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Solver -- the main class: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { class Solver { public: @@ -41,7 +44,7 @@ public: // Constructor/Destructor: // Solver(); - ~Solver(); + CVC4_PUBLIC ~Solver(); // Problem specification: // @@ -56,7 +59,7 @@ public: bool okay () const; // FALSE means solver is in a conflicting state // Variable mode: - // + // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. @@ -258,6 +261,7 @@ inline bool Solver::okay () const { return ok; } #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) ) +//#define reportf(format, args...) do {} while(0) static inline void logLit(FILE* f, Lit l) { @@ -299,8 +303,9 @@ inline void Solver::printClause(const C& c) } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= -#endif /* CVC4_MiniSat_Solver_h */ +#endif /* __CVC4__PROP__MINISAT__SOLVER_H */ diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 55e6d75fd..8860693e6 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -17,14 +17,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef CVC4_MiniSat_SolverTypes_h -#define CVC4_MiniSat_SolverTypes_h +#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H +#define __CVC4__PROP__MINISAT__SOLVERTYPES_H #include <cassert> #include <stdint.h> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Variables, literals, lifted booleans, clauses: @@ -196,7 +197,8 @@ inline void Clause::strengthen(Lit p) calcAbstraction(); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* CVC4_MiniSat_SolverTypes_h */ +#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */ diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index a4ca4403b..0fe6d84c7 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -20,8 +20,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef CVC4_MiniSat_Alg_h #define CVC4_MiniSat_Alg_h +#include <cassert> + namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Useful functions on vectors @@ -57,7 +60,8 @@ static inline bool find(V& ts, const T& t) return j < ts.size(); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Alg_h */ diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index b22a35ada..39d825411 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -99,7 +100,8 @@ class BasicHeap { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BasicHeap_h */ diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index 7c5b10e4c..05b801004 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -53,7 +54,7 @@ class bvec { x->cap = size; return x; } - + }; Vec_t* ref; @@ -79,16 +80,16 @@ class bvec { altvec (altvec<T>& other) { assert(0); } public: - void clear (bool dealloc = false) { + void clear (bool dealloc = false) { if (ref != NULL){ - for (int i = 0; i < ref->sz; i++) + for (int i = 0; i < ref->sz; i++) (*ref).data[i].~T(); - if (dealloc) { - free(ref); ref = NULL; - }else + if (dealloc) { + free(ref); ref = NULL; + }else ref->sz = 0; - } + } } // Constructors: @@ -110,11 +111,11 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - //new (&ref->data[size]) T(elem); - ref->data[size] = elem; - ref->sz = size+1; + //new (&ref->data[size]) T(elem); + ref->data[size] = elem; + ref->sz = size+1; } void push () { @@ -122,10 +123,10 @@ public: int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; - ref = Vec_t::alloc(ref, cap); + ref = Vec_t::alloc(ref, cap); } - new (&ref->data[size]) T(); - ref->sz = size+1; + new (&ref->data[size]) T(); + ref->sz = size+1; } void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } @@ -146,7 +147,8 @@ public: }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BoxedVec_h */ diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 84234705c..0c2019b65 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -21,9 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define CVC4_MiniSat_Heap_h #include "Vec.h" +#include <cassert> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -95,7 +97,7 @@ class Heap { indices[n] = heap.size(); heap.push(n); - percolateUp(indices[n]); + percolateUp(indices[n]); } @@ -107,19 +109,19 @@ class Heap { indices[x] = -1; heap.pop(); if (heap.size() > 1) percolateDown(0); - return x; + return x; } - void clear(bool dealloc = false) - { + void clear(bool dealloc = false) + { for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1; #ifdef NDEBUG for (int i = 0; i < indices.size(); i++) assert(indices[i] == -1); #endif - heap.clear(dealloc); + heap.clear(dealloc); } @@ -167,7 +169,8 @@ class Heap { }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index f69fca6d5..9168dde0e 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Default hash/equals functions @@ -83,7 +84,7 @@ class Map { cap = newsize; } - + public: Map () : table(NULL), cap(0), size(0) {} @@ -97,7 +98,7 @@ class Map { for (int i = 0; i < ps.size(); i++) if (equals(ps[i].key, k)){ d = ps[i].data; - return true; } + return true; } return false; } @@ -118,7 +119,8 @@ class Map { } }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Map_h */ diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index e4e7e2159..e02ac7222 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= @@ -83,7 +84,8 @@ public: //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Queue_h */ diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index df5261a06..2b9d5bb15 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Some sorting algorithms for vec's @@ -94,7 +95,8 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Sort_h */ diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 1a07cc334..fae1d0c5d 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -132,7 +133,8 @@ void vec<T>::clear(bool dealloc) { sz = 0; if (dealloc) free(data), data = NULL, cap = 0; } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Vec_h */ diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 14b64b555..063332e74 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Constructor/Destructor: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { SimpSolver::SimpSolver() : grow (0) @@ -226,11 +227,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou for (int i = 0; i < qs.size(); i++){ if (var(qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) + if (var(ps[j]) == var(qs[i])) { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -258,11 +260,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v) for (int i = 0; i < qs.size(); i++){ if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) + if (var(__ps[j]) == var(__qs[i])) { if (__ps[j] == ~__qs[i]) return false; else goto next; + } } next:; } @@ -701,5 +704,6 @@ void SimpSolver::toDimacs(const char* file) fprintf(stderr, "could not open file %s\n", file); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 221b4c6e2..f9e9b0387 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -17,23 +17,25 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#ifndef CVC4_MiniSat_SimpSolver_h -#define CVC4_MiniSat_SimpSolver_h +#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H +#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H #include <cstdio> +#include <cassert> -#include "Queue.h" -#include "Solver.h" +#include "../mtl/Queue.h" +#include "../core/Solver.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { class SimpSolver : public Solver { public: // Constructor/Destructor: // SimpSolver(); - ~SimpSolver(); + CVC4_PUBLIC ~SimpSolver(); // Problem specification: // @@ -159,8 +161,9 @@ inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size( inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } } inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= -#endif /* CVC4_MiniSat_SimpSolver_h */ +#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e69de29bb..2fb73cbed 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -0,0 +1,123 @@ +/********************* -*- C++ -*- */ +/** prop_engine.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#include "prop/prop_engine.h" +#include "theory/theory_engine.h" +#include "util/decision_engine.h" +#include "prop/minisat/mtl/Vec.h" +#include "prop/minisat/simp/SimpSolver.h" +#include "prop/minisat/core/SolverTypes.h" +#include "util/Assert.h" +#include "util/output.h" + +#include <utility> +#include <map> + +using namespace CVC4::prop::minisat; +using namespace std; + +namespace CVC4 { + +PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) : + d_de(de), d_te(te), d_sat() { +} + +void PropEngine::addVars(Expr e) { + Debug("prop") << "adding vars to " << e << endl; + for(Expr::iterator i = e.begin(); i != e.end(); ++i) { + Debug("prop") << "expr " << *i << endl; + if(i->getKind() == VARIABLE) { + if(d_vars.find(*i) == d_vars.end()) { + Var v = d_sat.newVar(); + Debug("prop") << "adding var " << *i << " <--> " << v << endl; + d_vars.insert(make_pair(*i, v)); + d_varsReverse.insert(make_pair(v, *i)); + } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl; + } else addVars(*i); + } +} + +static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) { + if(e.getKind() == VARIABLE) { + map<Expr, Var>::iterator v = vars->find(e); + Assert(v != vars->end()); + c->push(Lit(v->second, false)); + return; + } + if(e.getKind() == NOT) { + Assert(e.numChildren() == 1); + Expr child = *e.begin(); + Assert(child.getKind() == VARIABLE); + map<Expr, Var>::iterator v = vars->find(child); + Assert(v != vars->end()); + c->push(Lit(v->second, true)); + return; + } + Unhandled(); +} + +static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) { + vec<Lit> c; + Debug("prop") << " " << e << endl; + if(e.getKind() == VARIABLE || e.getKind() == NOT) { + doAtom(minisat, vars, e, &c); + } else { + Assert(e.getKind() == OR); + for(Expr::iterator i = e.begin(); i != e.end(); ++i) { + Debug("prop") << " " << *i << endl; + doAtom(minisat, vars, *i, &c); + } + } + Notice() << "added clause of length " << c.size() << endl; + for(int i = 0; i < c.size(); ++i) + Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]); + Notice() << " [["; + for(int i = 0; i < c.size(); ++i) + Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])]; + Notice() << " ]] " << endl; + minisat->addClause(c); +} + +void PropEngine::solve(Expr e) { + Debug("prop") << "SOLVING " << e << endl; + addVars(e); + if(e.getKind() == AND) { + Debug("prop") << "AND" << endl; + for(Expr::iterator i = e.begin(); i != e.end(); ++i) + doClause(&d_sat, &d_vars, &d_varsReverse, *i); + } else doClause(&d_sat, &d_vars, &d_varsReverse, e); + + d_sat.verbosity = 1; + bool result = d_sat.solve(); + + Notice() << "result is " << (result ? "sat" : "unsat") << endl; + if(result) { + Notice() << "model:" << endl; + for(int i = 0; i < d_sat.model.size(); ++i) + Notice() << " " << toInt(d_sat.model[i]); + Notice() << endl; + for(int i = 0; i < d_sat.model.size(); ++i) + Notice() << " " << d_varsReverse[i] << " is " + << (d_sat.model[i] == l_False ? "FALSE" : + (d_sat.model[i] == l_Undef ? "UNDEF" : + "TRUE")) << endl; + } else { + Notice() << "conflict:" << endl; + for(int i = 0; i < d_sat.conflict.size(); ++i) + Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]); + Notice() << " [["; + for(int i = 0; i < d_sat.conflict.size(); ++i) + Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])]; + Notice() << " ]] " << endl; + } +} + +}/* CVC4 namespace */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 5969e82d1..a3355bf89 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -9,28 +9,38 @@ ** **/ -#ifndef __CVC4__PROP__PROP_ENGINE_H -#define __CVC4__PROP__PROP_ENGINE_H +#ifndef __CVC4__PROP_ENGINE_H +#define __CVC4__PROP_ENGINE_H +#include "cvc4_config.h" #include "expr/expr.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" +#include "prop/minisat/simp/SimpSolver.h" +#include "prop/minisat/core/SolverTypes.h" + +#include <map> namespace CVC4 { -namespace prop { // In terms of abstraction, this is below (and provides services to) // Prover and above (and requires the services of) a specific // propositional solver, DPLL or otherwise. class PropEngine { - DecisionEngine* d_de; + DecisionEngine &d_de; + TheoryEngine &d_te; + CVC4::prop::minisat::SimpSolver d_sat; + std::map<Expr, CVC4::prop::minisat::Var> d_vars; + std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse; + + void addVars(Expr); public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(DecisionEngine*, TheoryEngine*); + CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&); /** * Converts to CNF if necessary. @@ -39,7 +49,6 @@ public: };/* class PropEngine */ -}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PROP__PROP_ENGINE_H */ +#endif /* __CVC4__PROP_ENGINE_H */ |