Merge from decision branch -- partially working justification heuristic

Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
  revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
  unknown and smtEngine queries DE to get the answer
  relevant stat: smt::resultSource
* there are known bugs

Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A

1 files changed, 179 insertions, 150 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 4b017ef45..e86b03258 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -41,6 +41,7 @@
 
 #include "justification_heuristic.h"
 
+#include "expr/kind.h"
 
 /***
 
@@ -59,14 +60,14 @@ CVC3 code <---->  this code
 
 ***/
 
-void JustificationHeuristic::setJustified(SatVariable v)
+void JustificationHeuristic::setJustified(TNode n)
 {
-  d_justified.insert(v);
+  d_justified.insert(n);
 }
 
-bool JustificationHeuristic::checkJustified(SatVariable v)
+bool JustificationHeuristic::checkJustified(TNode n)
 {
-  return d_justified.find(v) != d_justified.end();
+  return d_justified.find(n) != d_justified.end();
 }
 
 SatValue invertValue(SatValue v)
@@ -76,50 +77,53 @@ SatValue invertValue(SatValue v)
   else return SAT_VALUE_TRUE;
 }
 
-bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision)
+bool JustificationHeuristic::findSplitterRec(Node node, SatValue desiredVal, SatLiteral* litDecision)
 //bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision)
 {
-  // if(not ) {
-  //   //    Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl;
-  //   return false;
-  //   //    Assert(not lit.isNull());
-  // }
-
-  /** 
-   * TODO -- Base case. Way CVC3 seems to handle is that it has
-   * literals correpsonding to true and false. We'll have to take care
-   * somewhere else.
-   */
+  Trace("decision") 
+    << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; 
 
-  // Var v = lit.getVar();
-  SatVariable v = lit.getSatVariable();
-  SatValue litVal =  d_decisionEngine->getSatValue(lit);
+  /* Handle NOT as a special case */
+  if (node.getKind() == kind::NOT) {
+    desiredVal = invertValue(desiredVal);
+    node = node[0];
+  }
 
-  // if (lit.isFalse() || lit.isTrue()) return false;
-  if (v == 0) return false;
+  if (checkJustified(node)) return false;
+
+  SatValue litVal = tryGetSatValue(node);
+  bool litPresent = false;
+  if(d_decisionEngine->hasSatLiteral(node) ) {
+    SatLiteral lit = d_decisionEngine->getSatLiteral(node);
+    litPresent = true;
+
+    SatVariable v = lit.getSatVariable();
+    // if (lit.isFalse() || lit.isTrue()) return false;
+    if (v == 0) {
+      setJustified(node);
+      return false;
+    }
+  } else {
+    Trace("decision") << "no sat literal for this node" << std::endl;
+  }
 
 
   /* You'd better know what you want */
-  // DebugAssert(value != Var::UNKNOWN, "expected known value");
   Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value");
 
   /* Good luck, hope you can get what you want */
-  // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN,
-  //             "invariant violated");
   Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, 
          "invariant voilated");
 
+  /* What type of node is this */
+  Kind k = node.getKind();
+  theory::TheoryId tId = theory::kindToTheoryId(k);
 
-  if (checkJustified(v)) return false;
-
-  if (lit.isNegated()) {
-    desiredVal = invertValue(desiredVal);
-  }
-
-  Node node = d_decisionEngine->getNode(lit);
-  Trace("decision") << "lit = " << lit << std::endl;
-  Trace("decision") << node.getKind() << std::endl;
-  Trace("decision") << node << std::endl;
+  /* Some debugging stuff */
+  Trace("findSpitterRec") << "kind = " << k << std::endl;
+  Trace("findSplitterRec") << "theoryId = " << tId << std::endl;
+  Trace("findSplitterRec") << "node = " << node << std::endl;
+  Trace("findSplitterRec") << "litVal = " << litVal << std::endl;
 
   /*
   if (d_cnfManager->numFanins(v) == 0) {
@@ -133,17 +137,32 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
     }
   }
   */
-  if(node.getNumChildren() == 0) {
+
+
+  /**
+   * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
+   * then check if this is something to split-on? 
+   */
+  if(tId != theory::THEORY_BOOL
+     //      && !(k == kind::EQUAL && node[0].getType().isBoolean()) 
+     ) {
     if(litVal != SAT_VALUE_UNKNOWN) {
-      setJustified(v);
+      setJustified(node);
       return false;
     } else {
-      *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE );
+      if(not d_decisionEngine->hasSatLiteral(node))
+        throw GiveUpException();
+      Assert(d_decisionEngine->hasSatLiteral(node));
+      SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
+      *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
+      Trace("decision") << "decision " << *litDecision << std::endl;
+      Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
       return true;
     }
   }
 
 
+  /*** TODO: Term ITEs ***/
   /*
   else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
     // This node represents a predicate with embedded ITE's
@@ -208,134 +227,143 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
       return true;
     }
   }
+  */
 
-  int kind = d_cnfManager->concreteVar(v).getKind();
-  Var::Val valHard = Var::FALSE_VAL;
-  switch (kind) {
-    case AND:
-      valHard = Var::TRUE_VAL;
-    case OR:
-      if (value == valHard) {
-        n = d_cnfManager->numFanins(v);
-        for (i=0; i < n; ++i) {
-          litTmp = d_cnfManager->getFanin(v, i);
-          if (findSplitterRec(litTmp, valHard, litDecision)) {
-            return true;
-          }
-        }
-        DebugAssert(getValue(v) == valHard, "Output should be justified");
-        setJustified(v);
-        return false;
-      }
-      else {
-        Var::Val valEasy = Var::invertValue(valHard);
-        n = d_cnfManager->numFanins(v);
-        for (i=0; i < n; ++i) {
-          litTmp = d_cnfManager->getFanin(v, i);
-          if (getValue(litTmp) != valHard) {
-            if (findSplitterRec(litTmp, valEasy, litDecision)) {
-              return true;
-            }
-            DebugAssert(getValue(v) == valEasy, "Output should be justified");
-            setJustified(v);
-            return false;
-          }
-        }
-        DebugAssert(false, "No controlling input found (2)");
-      }
-      break;
-    case IMPLIES:
-      DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins");
-      if (value == Var::FALSE_VAL) {
-        litTmp = d_cnfManager->getFanin(v, 0);
-        if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+  SatValue valHard = SAT_VALUE_FALSE;
+  switch (k) {
+  case kind::AND:
+    valHard = SAT_VALUE_TRUE;
+  case kind::OR:
+    if (desiredVal == valHard) {
+      int n = node.getNumChildren();
+      for(int i = 0; i < n; ++i) {
+        if (findSplitterRec(node[i], valHard, litDecision)) {
           return true;
         }
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
-          return true;
-        }
-        DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified");
-        setJustified(v);
-        return false;
       }
-      else {
-        litTmp = d_cnfManager->getFanin(v, 0);
-        if (getValue(litTmp) != Var::TRUE_VAL) {
-          if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) {
-            return true;
-          }
-          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
-          setJustified(v);
-          return false;
-        }
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (getValue(litTmp) != Var::FALSE_VAL) {
-          if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) {
+      Assert(litPresent == false || litVal == valHard, "Output should be justified");
+      setJustified(node);
+      return false;
+    }
+    else {
+      SatValue valEasy = invertValue(valHard);
+      int n = node.getNumChildren();
+      for(int i = 0; i < n; ++i) {
+        Trace("findSplitterRec") << " node[i] = " << node[i] << " " << tryGetSatValue(node[i]) << std::endl;
+        if ( tryGetSatValue(node[i]) != valHard) {
+          Trace("findSplitterRec") << "hi"<< std::endl;
+          if (findSplitterRec(node[i], valEasy, litDecision)) {
             return true;
           }
-          DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified");
-          setJustified(v);
+          Assert(litPresent == false || litVal == valEasy, "Output should be justified");
+          setJustified(node);
           return false;
         }
-        DebugAssert(false, "No controlling input found (3)");
       }
-      break;
-    case IFF: {
-      litTmp = d_cnfManager->getFanin(v, 0);
-      Var::Val val = getValue(litTmp);
-      if (val != Var::UNKNOWN) {
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
-        litTmp = d_cnfManager->getFanin(v, 1);
+      Trace("findSplitterRec") << " * ** " << std::endl;
+      Trace("findSplitterRec") << node.getKind() << " " << node << std::endl;
+      for(unsigned i = 0; i < node.getNumChildren(); ++i) 
+        Trace("findSplitterRec") << "child: " << tryGetSatValue(node[i]) << std::endl;
+      Trace("findSplitterRec") << "node: " << tryGetSatValue(node) << std::endl;
+      Assert(false, "No controlling input found (2)");
+    }
+    break;
 
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        DebugAssert(getValue(v) == value, "Output should be justified");
-        setJustified(v);
-        return false;
+  case kind::IMPLIES:
+    //throw GiveUpException();
+    Assert(node.getNumChildren() == 2, "Expected 2 fanins");
+    if (desiredVal == SAT_VALUE_FALSE) {
+      if (findSplitterRec(node[0], SAT_VALUE_TRUE, litDecision)) {
+        return true;
       }
-      else {
-        val = getValue(d_cnfManager->getFanin(v, 1));
-        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
-        if (value == Var::FALSE_VAL) val = Var::invertValue(val);
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        DebugAssert(false, "Unable to find controlling input (4)");
+      if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) {
+        return true;
       }
-      break;
+      Assert(litPresent == false || litVal == SAT_VALUE_FALSE, "Output should be justified");
+      setJustified(node);
+      return false;
     }
-    case XOR: {
-      litTmp = d_cnfManager->getFanin(v, 0);
-      Var::Val val = getValue(litTmp);
-      if (val != Var::UNKNOWN) {
-        if (findSplitterRec(litTmp, val, litDecision)) {
-          return true;
-        }
-        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
-        litTmp = d_cnfManager->getFanin(v, 1);
-        if (findSplitterRec(litTmp, val, litDecision)) {
+    else {
+      if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) {
+        if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) {
           return true;
         }
-        DebugAssert(getValue(v) == value, "Output should be justified");
-        setJustified(v);
+        Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+        setJustified(node);
         return false;
       }
-      else {
-        val = getValue(d_cnfManager->getFanin(v, 1));
-        if (val == Var::UNKNOWN) val = Var::FALSE_VAL;
-        if (value == Var::TRUE_VAL) val = Var::invertValue(val);
-        if (findSplitterRec(litTmp, val, litDecision)) {
+      if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) {
+        if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) {
           return true;
         }
-        DebugAssert(false, "Unable to find controlling input (5)");
+        Assert(litPresent == false || litVal == SAT_VALUE_TRUE, "Output should be justified");
+        setJustified(node);
+        return false;
+      }
+      Assert(false, "No controlling input found (3)");
+    }
+    break;
+  case kind::IFF: 
+    //throw GiveUpException();
+    {
+    SatValue val = tryGetSatValue(node[0]);
+    if (val != SAT_VALUE_UNKNOWN) {
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
       }
-      break;
+      if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+
+      if (findSplitterRec(node[1], val, litDecision)) {
+        return true;
+      }
+      Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+      setJustified(node);
+      return false;
     }
+    else {
+      val = tryGetSatValue(node[1]);
+      if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+      if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val);
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      Assert(false, "Unable to find controlling input (4)");
+    }
+    break;
+  }
+    
+  case kind::XOR:
+    //throw GiveUpException();
+    {
+    SatValue val = tryGetSatValue(node[0]);
+    if (val != SAT_VALUE_UNKNOWN) {
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+
+      if (findSplitterRec(node[1], val, litDecision)) {
+        return true;
+      }
+      Assert(litPresent == false || litVal == desiredVal, "Output should be justified");
+      setJustified(node);
+      return false;
+    }
+    else {
+      SatValue val = tryGetSatValue(node[1]);
+      if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE;
+      if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val);
+      if (findSplitterRec(node[0], val, litDecision)) {
+        return true;
+      }
+      Assert(false, "Unable to find controlling input (5)");
+    }
+    break;
+  }
+
+  case kind::ITE:
+    throw GiveUpException();
+    /*
     case ITE: {
       Lit cIf = d_cnfManager->getFanin(v, 0);
       Lit cThen = d_cnfManager->getFanin(v, 1);
@@ -380,14 +408,15 @@ bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal
       setJustified(v);
       return false;
     }
-    default:
-      DebugAssert(false, "Unexpected Boolean operator");
-      break;
+      */
+  default:
+    Assert(false, "Unexpected Boolean operator");
+    break;
   }
-  FatalAssert(false, "Should be unreachable");
-  ------------------------------------------------  */
-  return false;
 
+  /* Swap order of these two once we handle all cases */
+  return false;
   Unreachable();
 
+
 }/* findRecSplit method */