decision/: justification: refactor ITE out

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index d384e2b7820b929755b3e9c6b082ba1757986b87..4e924de9e2f9dd69159ce2383c4d3eb6f2fd8903 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -256,42 +256,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
     break;
   }
 
-  case kind::ITE: {
-    //[0]: if, [1]: then, [2]: else
-    SatValue ifVal = tryGetSatValue(node[0]);
-    if (ifVal == SAT_VALUE_UNKNOWN) {
-      
-      // are we better off trying false? if not, try true
-      SatValue ifDesiredVal = 
-        (tryGetSatValue(node[2]) == desiredVal ||
-        tryGetSatValue(node[1]) == invertValue(desiredVal))
-       ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
-
-      if(findSplitterRec(node[0], ifDesiredVal)) {
-       return true;
-      }
-      Assert(false, "No controlling input found (6)");
-    } else {
-
-      // Try to justify 'if'
-      if (findSplitterRec(node[0], ifVal)) {
-       return true;
-      }
-
-      // If that was successful, we need to go into only one of 'then'
-      // or 'else'
-      int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
-      int chVal = tryGetSatValue(node[ch]);
-      if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal)
-         && findSplitterRec(node[ch], desiredVal) ) {
-       return true;
-      }
-    }
-    Assert(litPresent == false || litVal == desiredVal,
-          "Output should be justified");
-    setJustified(node);
-    return false;
-  }
+  case kind::ITE:
+    ret = handleITE(node, desiredVal);
+    break;
 
   default:
     Assert(false, "Unexpected Boolean operator");
@@ -348,3 +315,41 @@ bool JustificationHeuristic::handleBinaryHard
     return true;
   return findSplitterRec(node2, desiredVal2);
 }
+
+bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
+{
+  Debug("decision::jh") << " handleITE (" << node << ", "
+                              << desiredVal << std::endl;
+
+  //[0]: if, [1]: then, [2]: else
+  SatValue ifVal = tryGetSatValue(node[0]);
+  if (ifVal == SAT_VALUE_UNKNOWN) {
+      
+    // are we better off trying false? if not, try true [CHOICE]
+    SatValue ifDesiredVal = 
+      (tryGetSatValue(node[2]) == desiredVal ||
+       tryGetSatValue(node[1]) == invertValue(desiredVal))
+      ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
+
+    if(findSplitterRec(node[0], ifDesiredVal)) return true;
+    
+    Assert(false, "No controlling input found (6)");
+  } else {
+    // Try to justify 'if'
+    if(findSplitterRec(node[0], ifVal)) return true;
+
+    // If that was successful, we need to go into only one of 'then'
+    // or 'else'
+    int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
+
+    // STALE code: remove after tests or mar 2013, whichever earlier
+    // int chVal = tryGetSatValue(node[ch]);
+    // Assert(chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal);
+    // end STALE code: remove
+
+    if( findSplitterRec(node[ch], desiredVal) ) {
+      return true;
+    }
+  }// else (...ifVal...)
+  return false;
+}

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index b0f42c583d0d8eb43d505cad0923684ebd71e37b..a1a39cd6a0c9bc6668cac10ebec82dcad0202409 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -233,7 +233,7 @@ private:
                         TNode node2, SatValue desiredVal2);
   bool handleBinaryHard(TNode node1, SatValue desiredVal1,
                         TNode node2, SatValue desiredVal2);
-
+  bool handleITE(TNode node, SatValue desiredVal);
 };/* class JustificationHeuristic */
 
 }/* namespace decision */