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.

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 93ff65e6dc265fe466c5c58f27d1fd5220dcde21..065d40a9ac07f1f009ceeb98037c82ea42829e28 100644 (file)
--- 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 6c470e6df6605c7c3d06bf806a600bb50c5b3630..1dc7a85d742fd255b71f4492cd9067b056350baf 100644 (file)
--- 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 c5e1f7fbc6d41af321ab2a8a7979962dfe246c0e..f73337c8f537ee79fce78d3dd6cceb357334d32f 100644 (file)
--- 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 3a33a5cb804d940b81076de5ba65f2bc498d64f3..f45ce2e8fe80856166e2192b038c7a225ac1216a 100644 (file)
--- 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);

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2bdf7b71f1529bd744498b609040690a333fb5f6..5e8d711986f398bfebd8d4896705c4dc18b62b8a 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1267,7 +1267,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
-    Debug("smt") << "POST nonClasualSimplify" << std::endl;
+    Trace("smt") << "POST nonClasualSimplify" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1283,7 +1283,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    Debug("smt") << "POST theoryPP" << std::endl;
+    Trace("smt") << "POST theoryPP" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1292,7 +1292,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
-    Debug("smt") << "POST iteSimp" << std::endl;
+    Trace("smt") << "POST iteSimp" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1301,7 +1301,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       unconstrainedSimp();
     }
 
-    Debug("smt") << "POST unconstraintedSimp" << std::endl;
+    Trace("smt") << "POST unconstraintedSimp" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1313,7 +1313,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       if(!noConflict) return false;
     }
 
-    Debug("smt") << "POST repeatSimp" << std::endl;
+    Trace("smt") << "POST repeatSimp" << std::endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -1480,7 +1480,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
+  Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0c0d65d743f3bef9e0f4969e40646dc27d7123de..92e4b17df45e7376ac6141444e4a65822fd9813e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -19,6 +19,8 @@
 #include <vector>
 #include <list>
 
+#include "decision/decision_engine.h"
+
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2440a2e53ba1aedd1a27a53819e27e4b4bc6f171..0452d13aa0c0c34571a4c016049fc8f0f396a1e2 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -25,7 +25,6 @@
 #include <vector>
 #include <utility>
 
-#include "decision/decision_engine.h"
 #include "expr/node.h"
 #include "expr/command.h"
 #include "prop/prop_engine.h"
@@ -76,6 +75,8 @@ namespace theory {
   class Instantiator;
 }/* CVC4::theory namespace */
 
+class DecisionEngine;
+
 /**
  * This is essentially an abstraction for a collection of theories.  A
  * TheoryEngine provides services to a PropEngine, making various