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.

1 files changed, 18 insertions, 7 deletions

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);