decision/ : jh: refactor embedded ITE, other minor

other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.

1 files changed, 26 insertions, 18 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 4e924de9e..f2e5feee5 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -48,7 +48,7 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
 
 void JustificationHeuristic::computeITEs(TNode n, IteList &l)
 {
-  Trace("jh-ite") << " computeITEs( " << n << ", &l)\n";
+  Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n";
   d_visitedComputeITE.insert(n);
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
     SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
@@ -138,27 +138,13 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
                         << "litVal = " << litVal << std::endl;
 
   /**
-   * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
-   * then check if this is something to split-on.
+   * If not in theory of booleans, check if this is something to split-on.
    */
   if(tId != theory::THEORY_BOOL) {
 
     // if node has embedded ites, resolve that first
-    const IteList& l = getITEs(node);
-    Trace("jh-ite") << " ite size = " << l.size() << std::endl;
-    /*d_visited.insert(node);*/
-    for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
-      if(d_visited.find(i->first) == d_visited.end()) {
-        d_visited.insert(i->first);
-        Debug("jh-ite") << "jh-ite: adding visited " << i->first << std::endl;
-        if(findSplitterRec(i->second, SAT_VALUE_TRUE))
-          return true;
-        Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl;
-        d_visited.erase(i->first);
-      } else {
-        Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl;
-      }
-    }
+    if(handleEmbeddedITEs(node))
+      return true;
 
     if(litVal != SAT_VALUE_UNKNOWN) {
       setJustified(node);
@@ -353,3 +339,25 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
   }// else (...ifVal...)
   return false;
 }
+
+bool JustificationHeuristic::handleEmbeddedITEs(TNode node)
+{
+  const IteList& l = getITEs(node);
+  Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl;
+
+  for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) {
+    if(d_visited.find(i->first) == d_visited.end()) {
+      d_visited.insert(i->first);
+      Debug("decision::jh::ite") << "jh-ite: adding visited "
+                                 << i->first << std::endl;
+      if(findSplitterRec(i->second, SAT_VALUE_TRUE))
+        return true;
+      Debug("decision::jh::ite") << "jh-ite: removing visited "
+                                 << i->first << std::endl;
+      d_visited.erase(i->first);
+    } else {
+      Debug("decision::jh::ite") << "jh-ite: already visited " << i->first << std::endl;
+    }
+  }
+  return false;
+}