3 files changed, 49 insertions, 7 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index d220c4dbb..a260a8ca1 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -395,6 +395,7 @@ Lit Solver::pickBranchLit()
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
         Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
+        decisions++;
         return nextLit;
       } else {
         Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
@@ -414,14 +415,35 @@ Lit Solver::pickBranchLit()
             rnd_decisions++; }
 
     // Activity based decision:
-    while (next == var_Undef || value(next) != l_Undef || !decision[next])
+    while (next == var_Undef || value(next) != l_Undef || !decision[next]) {
         if (order_heap.empty()){
             next = var_Undef;
             break;
-        }else
+        }else {
             next = order_heap.removeMin();
+        }
+
+        if(!decision[next]) continue;
+        // Check with decision engine about relevancy
+        if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) {
+          next = var_Undef;
+        }
+    }
 
-    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
+    if(next == var_Undef) {
+      return lit_Undef;
+    } else {
+      decisions++;
+      // Check with decision engine if it can tell polarity
+      lbool dec_pol = MinisatSatSolver::toMinisatlbool
+        (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next)));
+      if(dec_pol != l_Undef) {
+        Assert(dec_pol == l_True || dec_pol == l_False);
+        return mkLit(next, (dec_pol == l_True) );
+      }
+      // If it can't use internal heuristic to do that
+      return mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
+    }
 }
 
 
@@ -1127,7 +1149,6 @@ lbool Solver::search(int nof_conflicts)
 
             if (next == lit_Undef) {
                 // New variable decision:
-                decisions++;
                 next = pickBranchLit();
 
                 if (next == lit_Undef) {
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;
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 19ade8ffa..9171bf232 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -45,8 +45,10 @@ public:
   static SatVariable     toSatVariable(Minisat::Var var);
   static Minisat::Lit    toMinisatLit(SatLiteral lit);
   static SatLiteral      toSatLiteral(Minisat::Lit lit);
-  static SatValue toSatLiteralValue(bool res);
-  static SatValue toSatLiteralValue(Minisat::lbool res);
+  static SatValue        toSatLiteralValue(bool res);
+  static SatValue        toSatLiteralValue(Minisat::lbool res);
+  static Minisat::lbool  toMinisatlbool(SatValue val);
+  //(Commented because not in use) static bool            tobool(SatValue val);
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
   static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);