Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 24 insertions, 0 deletions

diff --git a/src/prop/sat.h b/src/prop/sat.h
index a6bdcb309..14b42e445 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -49,6 +49,30 @@ class PropEngine;
 class CnfStream;
 
 /* Definitions of abstract types and conversion functions for SAT interface */
+/*
+inline SatLiteral variableToLiteral(SatVariable var) {
+  return Minisat::mkLit(var);
+}
+
+inline bool literalSign(SatLiteral lit) {
+  return Minisat::sign(lit);
+}
+
+static inline size_t
+hashSatLiteral(const SatLiteral& literal) {
+  return (size_t) Minisat::toInt(literal);
+}
+
+inline std::string stringOfLiteralValue(SatLiteralValue val) {
+  if( val == l_False ) {
+    return "0";
+  } else if (val == l_True ) {
+    return "1";
+  } else { // unknown
+    return "_";
+  }
+}
+*/
 
 /**
  * The proxy class that allows the SatSolver to communicate with the theories