summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/minisat/core/Solver.C6
-rw-r--r--src/prop/minisat/core/Solver.h25
-rw-r--r--src/prop/minisat/core/SolverTypes.h12
-rw-r--r--src/prop/minisat/mtl/Alg.h8
-rw-r--r--src/prop/minisat/mtl/BasicHeap.h6
-rw-r--r--src/prop/minisat/mtl/BoxedVec.h34
-rw-r--r--src/prop/minisat/mtl/Heap.h17
-rw-r--r--src/prop/minisat/mtl/Map.h10
-rw-r--r--src/prop/minisat/mtl/Queue.h6
-rw-r--r--src/prop/minisat/mtl/Sort.h6
-rw-r--r--src/prop/minisat/mtl/Vec.h6
-rw-r--r--src/prop/minisat/simp/SimpSolver.C12
-rw-r--r--src/prop/minisat/simp/SimpSolver.h19
-rw-r--r--src/prop/prop_engine.cpp123
-rw-r--r--src/prop/prop_engine.h23
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback