From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 7 Feb 2013 23:13:01 +0000 (-0500)
Subject: Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previousl... 
X-Git-Tag: cvc5-1.0.0~7354
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=994e6eb72e3475967a9a40a0566744ce1794f20a;p=cvc5.git

Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 21a37a43d..2b909a9a9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3369,7 +3369,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   // We have a "fake context" for the substitution map (we don't need it
   // to be context-dependent)
   context::Context fakeContext;
-  SubstitutionMap substitutions(&fakeContext);
+  SubstitutionMap substitutions(&fakeContext, /* substituteUnderQuantifiers = */ false);
 
   for(size_t k = 0; k < m->getNumCommands(); ++k) {
     const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k));
@@ -3457,13 +3457,13 @@ void SmtEngine::checkModel(bool hardFailure) {
     Notice() << "SmtEngine::checkModel(): -- simplifies to  " << n << endl;
 
     TheoryId thy = Theory::theoryOf(n);
-    if(thy == THEORY_QUANTIFIERS || thy == THEORY_REWRITERULES) {
+    if(thy == THEORY_REWRITERULES) {
       // Note this "skip" is done here, rather than above.  This is
       // because (1) the quantifier could in principle simplify to false,
       // which should be reported, and (2) checking for the quantifier
       // above, before simplification, doesn't catch buried quantifiers
       // anyway (those not at the top-level).
-      Notice() << "SmtEngine::checkModel(): -- skipping quantified assertion"
+      Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
                << endl;
       continue;
     }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 42a5380e4..2c5844cd4 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -78,7 +78,23 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
 Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
 {
   if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
-    CheckArgument(d_equalityEngine.hasTerm(n), n, "Cannot get the model value for a previously-unseen quantifier: %s", n.toString().c_str());
+    // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
+    // However, if the Decision Engine stops us early, there might be a
+    // quantifier that isn't assigned.  In conjunction with miniscoping, this
+    // might lead to a perfectly good model.  Think of
+    //     ASSERT FORALL(x) : p OR x=5
+    // The p is pulled out by miniscoping, and set to TRUE by the decision
+    // engine, then the quantifier's value in the model doesn't matter, so the
+    // Decision Engine stops.  So even though the top-level quantifier was
+    // asserted, it can't be checked directly: first, it doesn't "exist" in
+    // non-miniscoped form, and second, no quantifiers have been asserted, so
+    // none is in the model.  We used to fail an assertion here, but that's
+    // no good.  Instead, return the quantifier itself.  If we're in
+    // checkModel(), and the quantifier actually matters, we'll get an
+    // assert-fail since the quantifier isn't a constant.
+    if(!d_equalityEngine.hasTerm(n)) {
+      return n;
+    }
   } else {
     if(n.getKind() == kind::LAMBDA) {
       NodeManager* nm = NodeManager::currentNM();
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 96d07d7f3..48ac97294 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -145,6 +145,7 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
+	bug484.smt2 \
 	bug486.cvc \
 	bug497.cvc
 
@@ -152,8 +153,7 @@ TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
-	bug216.smt2.expect \
-	bug484.smt2
+	bug216.smt2.expect
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else