From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 17 Feb 2013 00:58:07 +0000 (-0500)
Subject: decision/ : jh: refactor embedded ITE, other minor
X-Git-Tag: cvc5-1.0.0~7407^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e495881142c623d9099869dba1147b6ea5ebae5;p=cvc5.git

decision/ : jh: refactor embedded ITE, other minor

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

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;
+}
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a1a39cd6a..4be436351 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -36,13 +36,6 @@ namespace CVC4 {
 
 namespace decision {
 
-class GiveUpException : public Exception {
-public:
-  GiveUpException() : 
-    Exception("justification heuristic: giving up") {
-  }
-};/* class GiveUpException */
-
 class JustificationHeuristic : public ITEDecisionStrategy {
   typedef std::vector<pair<TNode,TNode> > IteList;
   typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
@@ -138,11 +131,8 @@ public:
 
       SatValue desiredVal = SAT_VALUE_TRUE;
       SatLiteral litDecision;
-      try {
-        litDecision = findSplitter(d_assertions[i], desiredVal);
-      }catch(GiveUpException &e) {
-        return prop::undefSatLiteral;
-      }
+
+      litDecision = findSplitter(d_assertions[i], desiredVal);
 
       if(litDecision != undefSatLiteral) {
         d_prvsIndex = i;
@@ -234,6 +224,7 @@ private:
   bool handleBinaryHard(TNode node1, SatValue desiredVal1,
                         TNode node2, SatValue desiredVal2);
   bool handleITE(TNode node, SatValue desiredVal);
+  bool handleEmbeddedITEs(TNode node);
 };/* class JustificationHeuristic */
 
 }/* namespace decision */