diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/theory/model.cpp | 18 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 4 |
3 files changed, 22 insertions, 6 deletions
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 |