Significant work on bug #491 (not yet closed).

5 files changed, 38 insertions, 18 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1d98ce115..09fed4f9f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2908,6 +2908,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       hash_map<Node, Node, NodeHashFunction> cache;
       n = d_private->expandDefinitions(n, cache);
     }
+    Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
 
     // Apply our model value substitutions.
     n = substitutions.apply(n);
@@ -2929,6 +2930,12 @@ void SmtEngine::checkModel(bool hardFailure) {
       continue;
     }
 
+    // As a last-ditch effort, ask model to simplify it.
+    // Presently, this is only an issue for quantifiers, which can have a value
+    // but don't show up in our substitution map above.
+    n = m->getValue(n);
+    Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
+
     // The result should be == true.
     if(n != NodeManager::currentNM()->mkConst(true)) {
       Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 2e33c7c4a..a1f8e32fe 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -95,8 +95,10 @@ Node TheoryQuantifiers::getValue(TNode n) {
 void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
     if((*i).assertion.getKind() == kind::NOT) {
+      Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
       m->assertPredicate((*i).assertion[0], false);
     } else {
+      Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
       m->assertPredicate(*i, true);
     }
   }
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 0cc64e403..8858cc34b 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -27,12 +27,11 @@ struct substitution_stack_element {
   bool children_added;
   substitution_stack_element(TNode node)
   : node(node), children_added(false) {}
-};
-
+};/* struct substitution_stack_element */
 
 Node SubstitutionMap::internalSubstitute(TNode t) {
 
-  Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
+  Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
 
   if (d_substitutions.empty()) {
     return t;
@@ -48,7 +47,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
     substitution_stack_element& stackHead = toVisit.back();
     TNode current = stackHead.node;
 
-    Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
+    Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
 
     // If node already in the cache we're done, pop from the stack
     NodeCache::iterator find = d_substitutionCache.find(current);
@@ -57,6 +56,14 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
       continue;
     }
 
+    if (!d_substituteUnderQuantifiers &&
+        (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) {
+      Debug("substitution::internal") << "--not substituting under quantifier" << endl;
+      d_substitutionCache[current] = current;
+      toVisit.pop_back();
+      continue;
+    }
+
     NodeMap::iterator find2 = d_substitutions.find(current);
     if (find2 != d_substitutions.end()) {
       Node rhs = (*find2).second;
@@ -98,7 +105,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
           }
         }
       }
-      Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
+      Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
       d_substitutionCache[current] = result;
       toVisit.pop_back();
     } else {
@@ -123,7 +130,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
         }
       } else {
         // No children, so we're done
-        Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl;
+        Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
         d_substitutionCache[current] = current;
         toVisit.pop_back();
       }
@@ -132,7 +139,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) {
 
   // Return the substituted version
   return d_substitutionCache[t];
-}
+}/* SubstitutionMap::internalSubstitute() */
 
 
   /*
@@ -258,7 +265,7 @@ void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, boo
 
 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
 {
-  Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
+  Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
   // this causes a later assert-fail (the rhs != current one, above) anyway
@@ -280,32 +287,32 @@ static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
-  Debug("substitution") << "checking " << node << std::endl;
+  Debug("substitution") << "checking " << node << endl;
   for (; it != it_end; ++ it) {
-    Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl;
+    Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl;
     if (node.hasSubterm((*it).first)) {
-      Debug("substitution") << "-- FAIL" << std::endl;
+      Debug("substitution") << "-- FAIL" << endl;
       return false;
     }
   }
-  Debug("substitution") << "-- SUCCEED" << std::endl;
+  Debug("substitution") << "-- SUCCEED" << endl;
   return true;
 }
 
 Node SubstitutionMap::apply(TNode t) {
 
-  Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl;
+  Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
 
   // Setup the cache
   if (d_cacheInvalidated) {
     d_substitutionCache.clear();
     d_cacheInvalidated = false;
-    Debug("substitution") << "-- reset the cache" << std::endl;
+    Debug("substitution") << "-- reset the cache" << endl;
   }
 
   // Perform the substitution
   Node result = internalSubstitute(t);
-  Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
+  Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 
   //  Assert(check(result, d_substitutions));
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 31a6b9141..a199256e7 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -62,6 +62,9 @@ private:
   /** Cache of the already performed substitutions */
   NodeCache d_substitutionCache;
 
+  /** Whether or not to substitute under quantifiers */
+  bool d_substituteUnderQuantifiers;
+
   /** Has the cache been invalidated? */
   bool d_cacheInvalidated;
 
@@ -95,10 +98,11 @@ private:
 
 public:
 
-  SubstitutionMap(context::Context* context) :
+  SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) :
     d_context(context),
     d_substitutions(context),
     d_substitutionCache(),
+    d_substituteUnderQuantifiers(substituteUnderQuantifiers),
     d_cacheInvalidated(false),
     d_cacheInvalidator(context, d_cacheInvalidated) {
   }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 4f473212c..00f75313e 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -144,14 +144,14 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
-	bug484.smt2 \
 	bug486.cvc
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
-	bug216.smt2.expect
+	bug216.smt2.expect \
+	bug484.smt2
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else