bug fixes in justification heuristic

* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp

1 files changed, 26 insertions, 1 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 68c11295f..cd69eeb74 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -133,6 +133,13 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
     node = node[0];
   }
 
+  if(Debug.isOn("decision")) {
+    if(checkJustified(node))
+      Debug("decision") << "  justified, returning" << std::endl; 
+    if(d_visited.find(node) != d_visited.end())
+      Debug("decision") << "  visited, returning" << std::endl;       
+  }
+
   /* Base case */
   if (checkJustified(node) || d_visited.find(node) != d_visited.end())
     return false;
@@ -183,11 +190,19 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
     Debug("jh-ite") << " ite size = " << l.size() << std::endl;
     d_visited.insert(node);
     for(unsigned i = 0; i < l.size(); ++i) {
-      Assert(l[i].getKind() == kind::ITE, "Expected ITE");
       Debug("jh-ite") << " i = " << i 
                       << " l[i] = " << l[i] << std::endl;
       if (checkJustified(l[i])) continue;
 
+      // Assert(l[i].getKind() == kind::ITE, "Expected ITE");
+      if(l[i].getKind() != kind::ITE) {
+        //this might happen because of repeatSimp
+        Debug("jh-ite") << " not an ite, must have got repeatSimp-ed"
+                        << std::endl;
+        findSplitterRec(l[i], SAT_VALUE_TRUE, litDecision);
+        continue;
+      }
+
       SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable
 #ifdef CVC4_ASSERTIONS
       bool litPresent = d_decisionEngine->hasSatLiteral(l[i]);
@@ -206,6 +221,16 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
         if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) {
           return true;
         }
+
+        // Handle special case when if node itself is visited. Decide
+        // on it.
+        if(d_visited.find(l[i][0]) != d_visited.end()) {
+          Assert(d_decisionEngine->hasSatLiteral(l[i][0]));
+          SatVariable v = d_decisionEngine->getSatLiteral(l[i][0]).getSatVariable();
+          *litDecision = SatLiteral(v, ifDesiredVal != SAT_VALUE_TRUE );
+          return true;
+        }
+
         Assert(false, "No controlling input found (1)");
       } else {