From 8f341b6dc401a780f4a84fd4c51063242e885149 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sat, 16 Feb 2013 19:22:31 -0500
Subject: [PATCH] decision/: justification: refactor ITE out

---
 src/decision/justification_heuristic.cpp | 77 +++++++++++++-----------
 src/decision/justification_heuristic.h   |  2 +-
 2 files changed, 42 insertions(+), 37 deletions(-)

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index d384e2b78..4e924de9e 100644
--- 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 b0f42c583..a1a39cd6a 100644
--- 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 */
-- 
2.30.2