This is an attempt to fix the bug in the justification heuristic. The

other minor change is removing dependency of header file in
theory_engine.h

It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a
wrong answer for QF_AUFLIA -- it is currently unclear what is the cause
of this bug, could be sharing.

Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of
course, those for which the answer was wrong earlier; and also perhaps
one or two off-cases)

The issue was with how the infinite loop in justification stuff was prevented.
To keep it short, I skip what was wrong earlier, and this is what is done
now:
* whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable,
  AssertionCorrespondingToIteSkolem> is created for each skolem occuring in
  the atom.
* we iterate over this list, doing the following: check if skolem is marked
  as visited. if not, mark visited, recurse, when back unmark.

I lied, I will tell you what was being done earlier was -- 1. the check for
not being visited was being done in each recursive call, not just for atoms.
2. The AssertionCorrespondingToIteSkolem was being used to check if something
is visited and not IteSkolemVariable. I don't know if this makes any
difference, but anyhow, I think this is cleaner & clearer, so I keep this.

4 files changed, 51 insertions, 104 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 93ff65e6d..065d40a9a 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -96,16 +96,18 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n)
 
 void JustificationHeuristic::computeITEs(TNode n, IteList &l)
 {
-  Debug("jh-ite") << " computeITEs( " << n << ", &l)\n";
+  Trace("jh-ite") << " computeITEs( " << n << ", &l)\n";
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
     SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
-    if(it2 != d_iteAssertions.end())
-      l.push_back(it2->second);
+    if(it2 != d_iteAssertions.end()) {
+      l.push_back(make_pair(n[i], it2->second));
+      Assert(n[i].getNumChildren() == 0);
+    }
     computeITEs(n[i], l);
   }
 }
 
-const IteList& JustificationHeuristic::getITEs(TNode n)
+const JustificationHeuristic::IteList& JustificationHeuristic::getITEs(TNode n)
 {
   IteCache::iterator it = d_iteCache.find(n);
   if(it != d_iteCache.end()) {
@@ -113,7 +115,7 @@ const IteList& JustificationHeuristic::getITEs(TNode n)
   } else {
     // Compute the list of ITEs
     // TODO: optimize by avoiding multiple lookup for d_iteCache[n]
-    d_iteCache[n] = vector<TNode>();
+    d_iteCache[n] = IteList();
     computeITEs(n, d_iteCache[n]);
     return d_iteCache[n];
   }
@@ -123,7 +125,7 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
                                              SatValue desiredVal,
                                              SatLiteral* litDecision)
 {
-  Trace("decision") 
+  Trace("jh-findSplitterRec") 
     << "findSplitterRec(" << node << ", " 
     << desiredVal << ", .. )" << std::endl; 
 
@@ -136,36 +138,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
   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))
+  if (checkJustified(node)) {
     return false;
-  if(d_visited.find(node) != d_visited.end()) {
-
-    if(tryGetSatValue(node) != SAT_VALUE_UNKNOWN) {
-      setJustified(node);
-      return false;
-    } else {
-      Assert(d_decisionEngine->hasSatLiteral(node));
-      SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable();
-      *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE );
-      Trace("decision") << "decision " << *litDecision << std::endl;
-      Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl;
-      return true;
-    }
-
   }
 
-#if defined CVC4_ASSERTIONS || defined CVC4_TRACING
+#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
   // We don't always have a sat literal, so remember that. Will need
   // it for some assertions we make.
   bool litPresent = d_decisionEngine->hasSatLiteral(node);
-  if(Trace.isOn("decision")) {
+  if(Debug.isOn("decision")) {
     if(!litPresent) {
-      Trace("decision") << "no sat literal for this node" << std::endl;
+      Debug("decision") << "no sat literal for this node" << std::endl;
     }
   }
   //Assert(litPresent); -- fails
@@ -186,10 +172,10 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
   theory::TheoryId tId = theory::kindToTheoryId(k);
 
   /* Some debugging stuff */
-  Trace("jh-findSplitterRec") << "kind = " << k << std::endl;
-  Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
-  Trace("jh-findSplitterRec") << "node = " << node << std::endl;
-  Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
+  Debug("jh-findSplitterRec") << "kind = " << k << std::endl;
+  Debug("jh-findSplitterRec") << "theoryId = " << tId << std::endl;
+  Debug("jh-findSplitterRec") << "node = " << node << std::endl;
+  Debug("jh-findSplitterRec") << "litVal = " << litVal << std::endl;
 
   /**
    * If not in theory of booleans, and not a "boolean" EQUAL (IFF),
@@ -202,73 +188,20 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
     // if node has embedded ites -- which currently happens iff it got
     // replaced during ite removal -- then try to resolve that first
     const IteList& l = getITEs(node);
-    Debug("jh-ite") << " ite size = " << l.size() << std::endl;
-    d_visited.insert(node);
-    for(unsigned i = 0; i < l.size(); ++i) {
-      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]);
-#endif
-
-      // Handle the ITE to catch the case when a variable is its own
-      // fanin
-      SatValue ifVal = tryGetSatValue(l[i][0]);
-      if (ifVal == SAT_VALUE_UNKNOWN) {
-        // are we better off trying false? if not, try true
-        SatValue ifDesiredVal = 
-          (tryGetSatValue(l[i][2]) == desiredVal ||
-           tryGetSatValue(l[i][1]) == invertValue(desiredVal))
-          ? SAT_VALUE_FALSE : SAT_VALUE_TRUE;
-
-        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 );
+    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, litDecision))
           return true;
-        }
-
-        Assert(false, "No controlling input found (1)");
+        Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl;
+        d_visited.erase(i->first);
       } else {
-
-        // Try to justify 'if'
-        if (findSplitterRec(l[i][0], ifVal, litDecision)) {
-          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(l[i][ch]);
-        if( d_visited.find(l[i]) == d_visited.end()
-            && (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal)
-            && findSplitterRec(l[i][ch], desiredVal, litDecision) ) {
-          return true;
-        }
+        Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl;
       }
-      Assert(litPresent == false || litVal == desiredVal,
-             "Output should be justified");
-      setJustified(l[i]);
     }
-    d_visited.erase(node);
 
     if(litVal != SAT_VALUE_UNKNOWN) {
       setJustified(node);
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 6c470e6df..1dc7a85d7 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -34,8 +34,6 @@ namespace CVC4 {
 
 namespace decision {
 
-typedef std::vector<TNode> IteList;
-
 class GiveUpException : public Exception {
 public:
   GiveUpException() : 
@@ -44,11 +42,13 @@ public:
 };/* class GiveUpException */
 
 class JustificationHeuristic : public ITEDecisionStrategy {
+  typedef std::vector<pair<TNode,TNode> > IteList;
   typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
   typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
 
   // being 'justified' is monotonic with respect to decisions
-  context::CDHashSet<TNode,TNodeHashFunction> d_justified;
+  typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
+  JustifiedSet d_justified;
   context::CDO<unsigned>  d_prvsIndex;
 
   IntStat d_helfulness;
@@ -99,8 +99,19 @@ public:
 
     d_visited.clear();
 
+    if(Trace.isOn("justified")) {
+      for(JustifiedSet::iterator i = d_justified.begin();
+          i != d_justified.end(); ++i) {
+        TNode n = *i;
+        SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
+          d_decisionEngine->getSatLiteral(n) : -1;
+        SatValue v = tryGetSatValue(n);
+        Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
+      }
+    }
+
     for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
-      Trace("decision") << d_assertions[i] << std::endl;
+      Debug("decision") << d_assertions[i] << std::endl;
 
       // Sanity check: if it was false, aren't we inconsistent?
       Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
@@ -153,7 +164,7 @@ public:
     // Save mapping between ite skolems and ite assertions
     for(IteSkolemMap::iterator i = iteSkolemMap.begin();
         i != iteSkolemMap.end(); ++i) {
-      Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to "
+      Trace("jh-ite") << " jh-ite: " << (i->first) << " maps to "
                       << assertions[(i->second)] << std::endl;
       Assert(i->second >= assertionsEnd && i->second < assertions.size());
       d_iteAssertions[i->first] = assertions[i->second];
@@ -175,7 +186,7 @@ private:
       return prop::undefSatLiteral;
     }
     if(ret == true) {
-      Trace("decision") << "Yippee!!" << std::endl;
+      Debug("decision") << "Yippee!!" << std::endl;
       //d_prvsIndex = i;
       ++d_helfulness;
       return litDecision;
@@ -199,7 +210,7 @@ private:
   SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
-  const IteList& getITEs(TNode n);
+  const JustificationHeuristic::IteList& getITEs(TNode n);
 
   /* Compute all term-ITEs in a node recursively */
   void computeITEs(TNode n, IteList &l);
diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp
index c5e1f7fbc..f73337c8f 100644
--- a/src/decision/relevancy.cpp
+++ b/src/decision/relevancy.cpp
@@ -68,7 +68,7 @@ void Relevancy::computeITEs(TNode n, IteList &l)
   }
 }
 
-const IteList& Relevancy::getITEs(TNode n)
+const Relevancy::IteList& Relevancy::getITEs(TNode n)
 {
   IteCache::iterator it = d_iteCache.find(n);
   if(it != d_iteCache.end()) {
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index 3a33a5cb8..f45ce2e8f 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -46,8 +46,6 @@ namespace CVC4 {
 
 namespace decision {
 
-typedef std::vector<TNode> IteList;
-
 class RelGiveUpException : public Exception {
 public:
   RelGiveUpException() : 
@@ -56,6 +54,7 @@ public:
 };/* class GiveUpException */
 
 class Relevancy : public RelevancyStrategy {
+  typedef std::vector<TNode> IteList;
   typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
   typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
   typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache;
@@ -139,6 +138,10 @@ public:
     d_maxTimeAsPercentageOfTotalTime(decOpt.maxRelTimeAsPermille*1.0/10.0),
     d_curDecision(NULL)
   {
+    Warning() << "There are known bugs in this Relevancy code which we know"
+              << "how to fix (but haven't yet)." << std::endl
+              << "Please bug kshitij if you wish to use." << std::endl;
+
     StatisticsRegistry::registerStat(&d_helfulness);
     StatisticsRegistry::registerStat(&d_polqueries);
     StatisticsRegistry::registerStat(&d_polhelp);
@@ -350,7 +353,7 @@ private:
   SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
-  const IteList& getITEs(TNode n);
+  const Relevancy::IteList& getITEs(TNode n);
 
   /* Compute all term-ITEs in a node recursively */
   void computeITEs(TNode n, IteList &l);