diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 18:13:01 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-01 15:38:14 -0400 |
commit | 994e6eb72e3475967a9a40a0566744ce1794f20a (patch) | |
tree | fec05368ea52fbb00204ee3f3a168c2434610eae /src/theory | |
parent | bf7f728381bb27163f3e056d698ba4da6316b9c8 (diff) |
Fix bug 491 and related issues with checkModel() and quantifiers. Enabling previously-failing testcase.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/model.cpp | 18 |
1 files changed, 17 insertions, 1 deletions
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(); |