Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

8 files changed, 77 insertions, 9 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 62d885c06..485ddbb55 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -120,6 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const {
 }
 
 void TseitinCnfStream::ensureLiteral(TNode n) {
+  Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
   if(hasLiteral(n)) {
     // Already a literal!
     // newLiteral() may be necessary to renew a previously-extant literal
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);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 58270b4d0..702a530cf 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -77,7 +77,11 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
   d_satSolver = SatSolverFactory::createDPLLMinisat(); 
 
   theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
+  d_cnfStream = new CVC4::prop::TseitinCnfStream
+    (d_satSolver, registrar, 
+     // fullLitToNode Map = 
+     Options::current()->threads > 1 || 
+     Options::current()->decisionMode == Options::DECISION_STRATEGY_RELEVANCY);
 
   d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
 
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 0da4d7a6a..9dcc1c4bf 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): barrett, cconway
+ ** Minor contributors (to current version): barrett, cconway, kshitij
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -41,6 +41,15 @@ enum SatValue {
   SAT_VALUE_FALSE
 };
 
+/** Helper function for inverting a SatValue */
+inline SatValue invertValue(SatValue v)
+{
+  if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN;
+  else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE;
+  else return SAT_VALUE_TRUE;
+}
+
+
 /**
  * A variable of the SAT solver.
  */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index ccb26b6f0..93f8c0a5d 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -188,9 +188,17 @@ void TheoryProxy::checkTime() {
   d_propEngine->checkTime();
 }
 
+bool TheoryProxy::isDecisionRelevant(SatVariable var) {
+  return d_decisionEngine->isRelevant(var);
+}
+
 bool TheoryProxy::isDecisionEngineDone() {
   return d_decisionEngine->isDone();
 }
 
+SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
+  return d_decisionEngine->getPolarity(var);
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 2fac0ab7b..99aab8286 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -119,6 +119,10 @@ public:
 
   bool isDecisionEngineDone();
 
+  bool isDecisionRelevant(SatVariable var);
+
+  SatValue getDecisionPolarity(SatVariable var);
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */