Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

1 files changed, 20 insertions, 1 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4f2a16670..6b02153c7 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -69,6 +69,20 @@ SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
   return SAT_VALUE_FALSE;
 }
 
+Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
+{
+  if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
+  if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
+  Assert(val == SAT_VALUE_FALSE);
+  return Minisat::lbool((uint8_t)1);
+}
+
+/*bool MinisatSatSolver::tobool(SatValue val)
+{
+  if(val == SAT_VALUE_TRUE) return true;
+  Assert(val == SAT_VALUE_FALSE);
+  return false;
+  }*/
 
 void MinisatSatSolver::toMinisatClause(SatClause& clause,
                                            Minisat::vec<Minisat::Lit>& minisat_clause) {
@@ -92,10 +106,15 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
 
   d_context = context;
 
+  if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) {
+    Notice() << "minisat: Incremental solving is disabled"
+             << " unless using internal decision strategy." << std::endl;
+  }
+
   // Create the solver
   d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
                                       Options::current()->incrementalSolving || 
-                                      Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION );
+                                      Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL );
   // Setup the verbosity
   d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1;