summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cnf_stream.cpp13
-rw-r--r--src/prop/cnf_stream.h25
-rw-r--r--src/prop/minisat/core/Solver.C12
-rw-r--r--src/prop/minisat/core/Solver.h3
-rw-r--r--src/prop/minisat/simp/SimpSolver.C4
-rw-r--r--src/prop/minisat/simp/SimpSolver.h2
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/prop_engine.h2
-rw-r--r--src/prop/sat.h172
9 files changed, 163 insertions, 73 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 612b00bcf..2efad3cb2 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -14,6 +14,7 @@
** of given an equisatisfiable stream of assertions to PropEngine.
**/
+#include "sat.h"
#include "prop/cnf_stream.h"
#include "prop/prop_engine.h"
#include "expr/node.h"
@@ -71,12 +72,18 @@ SatLiteral CnfStream::lookupInCache(const TNode& n) const {
void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) {
Debug("cnf") << "caching translation " << node << " to " << lit << endl;
+ // We always cash bot the node and the negation at the same time
d_translationCache[node] = lit;
+ d_translationCache[node.notNode()] = ~lit;
}
-SatLiteral CnfStream::newLiteral(const TNode& node) {
- SatLiteral lit = SatLiteral(d_satSolver->newVar());
+SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) {
+ SatLiteral lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
cacheTranslation(node, lit);
+ if (theoryLiteral) {
+ d_nodeCache[lit] = node;
+ d_nodeCache[~lit] = node.notNode();
+ }
return lit;
}
@@ -86,7 +93,7 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
Debug("cnf") << "handleAtom(" << node << ")" << endl;
- SatLiteral lit = newLiteral(node);
+ SatLiteral lit = newLiteral(node, true);
switch(node.getKind()) {
case TRUE:
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9af15ba31..93c1f529a 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -46,7 +46,12 @@ private:
SatSolver *d_satSolver;
/** Cache of what literal have been registered to a node. */
- __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> d_translationCache;
+ typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> TranslationCache;
+ TranslationCache d_translationCache;
+
+ /** Cache of what nodes have been registered to a literal. */
+ typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFcn> NodeCache;
+ NodeCache d_nodeCache;
protected:
@@ -103,9 +108,11 @@ protected:
* Acquires a new variable from the SAT solver to represent the node and
* inserts the necessary data it into the mapping tables.
* @param node a formula
+ * @param theoryLiteral is this literal a theory literal (i.e. theory to be
+ * informed when set to true/false
* @return the literal corresponding to the formula
*/
- SatLiteral newLiteral(const TNode& node);
+ SatLiteral newLiteral(const TNode& node, bool theoryLiteral = false);
public:
@@ -131,6 +138,20 @@ public:
*/
virtual void convertAndAssert(const TNode& node) = 0;
+ /**
+ * Returns a node the is represented by a give SatLiteral literal.
+ * @param literal the literal from the sat solver
+ * @return the actual node
+ */
+ Node getNode(const SatLiteral& literal) {
+ Node node;
+ NodeCache::iterator find = d_nodeCache.find(literal);
+ if (find != d_nodeCache.end()) {
+ node = find->second;
+ }
+ return node;
+ }
+
}; /* class CnfStream */
/**
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index dd5e1e667..e3ce088b1 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -77,7 +77,7 @@ Solver::~Solver()
// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
//
-Var Solver::newVar(bool sign, bool dvar)
+Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
{
int v = nVars();
watches .push(); // (list for positive literal)
@@ -88,6 +88,8 @@ Var Solver::newVar(bool sign, bool dvar)
activity .push(0);
seen .push(0);
+ theory .push(theoryAtom);
+
polarity .push((char)sign);
decision_var.push((char)dvar);
@@ -394,11 +396,17 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
void Solver::uncheckedEnqueue(Lit p, Clause* from)
{
assert(value(p) == l_Undef);
- assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient
+ assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost efficient
level [var(p)] = decisionLevel();
reason [var(p)] = from;
+ // Added for phase-caching
polarity [var(p)] = sign(p);
trail.push(p);
+
+ if (theory[var(p)]) {
+ // Enqueue to the theory
+ proxy->enqueueTheoryLiteral(p);
+ }
}
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index c593d8b2c..131999e38 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -65,7 +65,7 @@ public:
// Problem specification:
//
- Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+ Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
bool addClause (vec<Lit>& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method!
// Solving:
@@ -144,6 +144,7 @@ protected:
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<char> assigns; // The current assignments (lbool:s stored as char:s).
vec<char> polarity; // The preferred polarity of each variable.
+ vec<bool> theory; // Is the variable representing a theory atom
vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C
index 124849155..a2e46e2e4 100644
--- a/src/prop/minisat/simp/SimpSolver.C
+++ b/src/prop/minisat/simp/SimpSolver.C
@@ -58,8 +58,8 @@ SimpSolver::~SimpSolver()
}
-Var SimpSolver::newVar(bool sign, bool dvar) {
- Var v = Solver::newVar(sign, dvar);
+Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) {
+ Var v = Solver::newVar(sign, dvar,theoryAtom);
if (use_simplification){
n_occ .push(0);
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 67d0d2b95..38d51206d 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -44,7 +44,7 @@ class SimpSolver : public Solver {
// Problem specification:
//
- Var newVar (bool polarity = true, bool dvar = true);
+ Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false);
bool addClause (vec<Lit>& ps);
// Variable mode:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 32be206b0..96154063d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -12,8 +12,8 @@
**
**/
+#include "sat.h"
#include "prop/prop_engine.h"
-#include "prop/cnf_stream.h"
#include "theory/theory_engine.h"
#include "util/decision_engine.h"
@@ -42,6 +42,7 @@ PropEngine::PropEngine(const Options* opts, DecisionEngine* de,
Debug("prop") << "Constructing the PropEngine" << endl;
d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver);
+ d_satSolver->setCnfStream(d_cnfStream);
}
PropEngine::~PropEngine() {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 0c3916162..2ddbd24fc 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,12 +25,12 @@
#include "util/options.h"
#include "util/decision_engine.h"
#include "theory/theory_engine.h"
-#include "prop/sat.h"
namespace CVC4 {
namespace prop {
class CnfStream;
+class SatSolver;
/**
* PropEngine is the abstraction of a Sat Solver, providing methods for
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 2468990f2..fb8930910 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -13,13 +13,11 @@
** SAT Solver.
**/
-#include "cvc4_private.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-
#ifndef __CVC4__PROP__SAT_H
#define __CVC4__PROP__SAT_H
+#include "cvc4_private.h"
+
#define __CVC4_USE_MINISAT
#ifdef __CVC4_USE_MINISAT
@@ -36,6 +34,7 @@ class TheoryEngine;
namespace prop {
class PropEngine;
+class CnfStream;
/** Type of the SAT variables */
typedef minisat::Var SatVariable;
@@ -47,6 +46,67 @@ typedef minisat::Lit SatLiteral;
typedef minisat::vec<SatLiteral> SatClause;
/**
+ * The proxy class that allows us to modify the internals of the SAT solver.
+ * It's only accessible from the PropEngine, and should be treated with major
+ * care.
+ */
+class SatSolver {
+
+ /** The prop engine we are using */
+ PropEngine* d_propEngine;
+
+ /** The CNF engine we are using */
+ CnfStream* d_cnfStream;
+
+ /** The theory engine we are using */
+ TheoryEngine* d_theoryEngine;
+
+ /** Context we will be using to synchronzie the sat solver */
+ context::Context* d_context;
+
+ /** Minisat solver */
+ minisat::SimpSolver* d_minisat;
+
+ /** Remember the options */
+ Options* d_options;
+
+public:
+
+ /** Hash function for literals */
+ struct SatLiteralHashFcn {
+ inline size_t operator()(const SatLiteral& literal) const;
+ };
+
+ inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context,
+ const Options* options);
+
+ inline ~SatSolver();
+
+ inline bool solve();
+
+ inline void addClause(SatClause& clause);
+
+ inline SatVariable newVar(bool theoryAtom = false);
+
+ inline void theoryCheck(SatClause& conflict);
+
+ inline void enqueueTheoryLiteral(const SatLiteral& l);
+
+ inline void setCnfStream(CnfStream* cnfStream);
+};
+
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
+
+#include "context/context.h"
+#include "theory/theory_engine.h"
+#include "prop/prop_engine.h"
+#include "prop/cnf_stream.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
* Returns the variable of the literal.
* @param lit the literal
*/
@@ -58,13 +118,13 @@ inline bool literalSign(SatLiteral lit) {
return minisat::sign(lit);
}
-inline std::ostream& operator << (std::ostream& out, SatLiteral lit) {
+inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) {
const char * s = (literalSign(lit)) ? "~" : " ";
out << s << literalToVariable(lit);
return out;
}
-inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
+inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
out << "clause:";
for(int i = 0; i < clause.size(); ++i) {
out << " " << clause[i];
@@ -73,66 +133,59 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) {
return out;
}
-/**
- * The proxy class that allows us to modify the internals of the SAT solver.
- * It's only accessible from the PropEngine, and should be treated with major
- * care.
- */
-class SatSolver {
+size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const {
+ return (size_t) minisat::toInt(literal);
+}
- /** The prop engine we are using */
- PropEngine* d_propEngine;
+SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
+ context::Context* context, const Options* options) :
+ d_propEngine(propEngine),
+ d_cnfStream(NULL),
+ d_theoryEngine(theoryEngine),
+ d_context(context)
+{
+ // Create the solver
+ d_minisat = new minisat::SimpSolver(this, d_context);
+ // Setup the verbosity
+ d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
+ // Do not delete the satisfied clauses, just the learnt ones
+ d_minisat->remove_satisfied = false;
+ // Make minisat reuse the literal values
+ d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
+}
- /** The theory engine we are using */
- TheoryEngine* d_theoryEngine;
+SatSolver::~SatSolver() {
+ delete d_minisat;
+}
- /** Context we will be using to synchronzie the sat solver */
- context::Context* d_context;
+bool SatSolver::solve() {
+ return d_minisat->solve();
+}
- /** Minisat solver */
- minisat::SimpSolver* d_minisat;
+void SatSolver::addClause(SatClause& clause) {
+ d_minisat->addClause(clause);
+}
- /** Remember the options */
- Options* d_options;
+SatVariable SatSolver::newVar(bool theoryAtom) {
+ return d_minisat->newVar(true, true, theoryAtom);
+}
- 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
- d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
- // Do not delete the satisfied clauses, just the learnt ones
- d_minisat->remove_satisfied = false;
- // Make minisat reuse the literal values
- d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
- }
-
- ~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) {
- }
-};
+void SatSolver::theoryCheck(SatClause& conflict) {
+ d_theoryEngine->check(theory::Theory::STANDARD);
+}
+void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
+ Node literalNode = d_cnfStream->getNode(l);
+ // We can get null from the prop engine if the literal is useless (i.e.)
+ // the expression is not in context anyomore
+ if(!literalNode.isNull()) {
+ d_theoryEngine->assertFact(literalNode);
+ }
+}
+
+void SatSolver::setCnfStream(CnfStream* cnfStream) {
+ d_cnfStream = cnfStream;
+}
}/* CVC4::prop namespace */
@@ -140,5 +193,4 @@ class SatSolver {
#endif
-
#endif /* __CVC4__PROP__SAT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback