summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.cproject2
-rw-r--r--src/parser/bounded_token_buffer.cpp2
-rw-r--r--src/prop/Makefile.am1
-rw-r--r--src/prop/prop_engine.cpp3
-rw-r--r--src/prop/sat.cpp43
-rw-r--r--src/prop/sat.h162
6 files changed, 122 insertions, 91 deletions
diff --git a/.cproject b/.cproject
index 488d7e4d4..df8183d4e 100644
--- a/.cproject
+++ b/.cproject
@@ -44,7 +44,7 @@
</toolChain>
</folderInfo>
<sourceEntries>
-<entry excluding="parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
+<entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
</sourceEntries>
</configuration>
</storageModule>
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 8bd896cd4..53b56dcdd 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -10,7 +10,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** An ANTLR3 bounded token stream implementation.
+ ** An ANTLR3 bounded token stream implementation.
** This code is largely based on the original token buffer implementation
** in libantlr3c, by Jim Idle.
**/
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 357818b32..2856cc065 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -9,6 +9,7 @@ libprop_la_SOURCES = \
prop_engine.cpp \
prop_engine.h \
sat.h \
+ sat.cpp \
cnf_stream.h \
cnf_stream.cpp \
cnf_conversion.h
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index ef28a4ac6..6b28e6f99 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -12,8 +12,9 @@
**
**/
+#include "cnf_stream.h"
+#include "prop_engine.h"
#include "sat.h"
-#include "prop/prop_engine.h"
#include "theory/theory_engine.h"
#include "util/decision_engine.h"
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
new file mode 100644
index 000000000..c578cf361
--- /dev/null
+++ b/src/prop/sat.cpp
@@ -0,0 +1,43 @@
+#include "cnf_stream.h"
+#include "prop_engine.h"
+#include "sat.h"
+#include "context/context.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace prop {
+
+void SatSolver::theoryCheck(SatClause& conflict) {
+ // Try theory propagation
+ if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) {
+ // We have a conflict, get it
+ Node conflictNode = d_theoryEngine->getConflict();
+ Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
+ // Go through the literals and construct the conflict clause
+ Node::const_iterator literal_it = conflictNode.begin();
+ Node::const_iterator literal_end = conflictNode.end();
+ while (literal_it != literal_end) {
+ // Get the literal corresponding to the node
+ SatLiteral l = d_cnfStream->getLiteral(*literal_it);
+ // Add the negation to the conflict clause and continue
+ conflict.push(~l);
+ literal_it ++;
+ }
+ }
+}
+
+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 */
+}/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 12aa82793..d5adedd20 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -18,15 +18,20 @@
#ifndef __CVC4__PROP__SAT_H
#define __CVC4__PROP__SAT_H
+// Just defining this for now, since there's no other SAT solver bindings.
+// Optional blocks below will be unconditionally included
#define __CVC4_USE_MINISAT
+#include "util/options.h"
+
#ifdef __CVC4_USE_MINISAT
-#include "util/options.h"
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/core/SolverTypes.h"
#include "prop/minisat/simp/SimpSolver.h"
+#endif /* __CVC4_USE_MINISAT */
+
namespace CVC4 {
class TheoryEngine;
@@ -36,6 +41,10 @@ namespace prop {
class PropEngine;
class CnfStream;
+/* Definitions of abstract types and conversion functions for SAT interface */
+
+#ifdef __CVC4_USE_MINISAT
+
/** Type of the SAT variables */
typedef minisat::Var SatVariable;
@@ -46,6 +55,25 @@ typedef minisat::Lit SatLiteral;
typedef minisat::vec<SatLiteral> SatClause;
/**
+ * Returns the variable of the literal.
+ * @param lit the literal
+ */
+inline SatVariable literalToVariable(SatLiteral lit) {
+ return minisat::var(lit);
+}
+
+inline bool literalSign(SatLiteral lit) {
+ return minisat::sign(lit);
+}
+
+static inline size_t
+hashSatLiteral(const SatLiteral& literal) {
+ return (size_t) minisat::toInt(literal);
+}
+
+#endif /* __CVC4_USE_MINISAT */
+
+/**
* 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.
@@ -64,83 +92,53 @@ class SatSolver {
/** Context we will be using to synchronzie the sat solver */
context::Context* d_context;
+ /** Remember the options */
+ Options* d_options;
+
+ /* Pointer to the concrete SAT solver. Including this via the
+ preprocessor saves us a level of indirection vs, e.g., defining a
+ sub-class for each solver. */
+
+#ifdef __CVC4_USE_MINISAT
+
/** Minisat solver */
minisat::SimpSolver* d_minisat;
- /** Remember the options */
- Options* d_options;
+#endif /* __CVC4_USE_MINISAT */
-public:
+protected:
+public:
/** Hash function for literals */
struct SatLiteralHashFunction {
inline size_t operator()(const SatLiteral& literal) const;
};
- inline SatSolver(PropEngine* propEngine,
+ SatSolver(PropEngine* propEngine,
TheoryEngine* theoryEngine,
context::Context* context,
const Options* options);
- inline ~SatSolver();
-
- inline bool solve();
-
- inline void addClause(SatClause& clause);
+ ~SatSolver();
- inline SatVariable newVar(bool theoryAtom = false);
+ bool solve();
+
+ void addClause(SatClause& clause);
- inline void theoryCheck(SatClause& conflict);
+ SatVariable newVar(bool theoryAtom = false);
- inline void enqueueTheoryLiteral(const SatLiteral& l);
+ void theoryCheck(SatClause& conflict);
- inline void setCnfStream(CnfStream* cnfStream);
+ void enqueueTheoryLiteral(const SatLiteral& l);
+
+ 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 {
+/* Functions that delegate to the concrete SAT solver. */
-/**
- * Returns the variable of the literal.
- * @param lit the literal
- */
-inline SatVariable literalToVariable(SatLiteral lit) {
- return minisat::var(lit);
-}
-
-inline bool literalSign(SatLiteral lit) {
- return minisat::sign(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) {
- out << "clause:";
- for(int i = 0; i < clause.size(); ++i) {
- out << " " << clause[i];
- }
- out << ";";
- return out;
-}
-
-inline size_t
-SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
- return (size_t) minisat::toInt(literal);
-}
+#ifdef __CVC4_USE_MINISAT
-SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
+inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
context::Context* context, const Options* options) :
d_propEngine(propEngine),
d_cnfStream(NULL),
@@ -157,57 +155,45 @@ SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
}
-SatSolver::~SatSolver() {
+inline SatSolver::~SatSolver() {
delete d_minisat;
}
-bool SatSolver::solve() {
+inline bool SatSolver::solve() {
return d_minisat->solve();
}
-void SatSolver::addClause(SatClause& clause) {
+inline void SatSolver::addClause(SatClause& clause) {
d_minisat->addClause(clause);
}
-SatVariable SatSolver::newVar(bool theoryAtom) {
+inline SatVariable SatSolver::newVar(bool theoryAtom) {
return d_minisat->newVar(true, true, theoryAtom);
}
-void SatSolver::theoryCheck(SatClause& conflict) {
- // Try theory propagation
- if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) {
- // We have a conflict, get it
- Node conflictNode = d_theoryEngine->getConflict();
- Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
- // Go through the literals and construct the conflict clause
- Node::const_iterator literal_it = conflictNode.begin();
- Node::const_iterator literal_end = conflictNode.end();
- while (literal_it != literal_end) {
- // Get the literal corresponding to the node
- SatLiteral l = d_cnfStream->getLiteral(*literal_it);
- // Add the negation to the conflict clause and continue
- conflict.push(~l);
- literal_it ++;
- }
- }
+#endif /* __CVC4_USE_MINISAT */
+
+inline size_t
+SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const {
+ return hashSatLiteral(literal);
}
-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);
- }
+inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) {
+ const char * s = (literalSign(lit)) ? "~" : " ";
+ out << s << literalToVariable(lit);
+ return out;
}
-void SatSolver::setCnfStream(CnfStream* cnfStream) {
- d_cnfStream = cnfStream;
+inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) {
+ out << "clause:";
+ for(int i = 0; i < clause.size(); ++i) {
+ out << " " << clause[i];
+ }
+ out << ";";
+ return out;
}
}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif
-
#endif /* __CVC4__PROP__SAT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback