diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-16 18:28:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-17 17:21:26 -0400 |
commit | 004bcc12f592991db93ffd92cfb5925940c80980 (patch) | |
tree | 1bb1db6b03f80b4833a681622f211b6bfaa911b9 /src | |
parent | cffc449795c777217c6412998c7900ad80c389e8 (diff) |
Fix bug 516; include some bug testcases.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/model.cpp | 13 |
2 files changed, 14 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b72f52092..2cddc29cf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3541,6 +3541,12 @@ void SmtEngine::checkModel(bool hardFailure) { Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; + if(Theory::theoryOf(n) != THEORY_REWRITERULES) { + // In case it's a quantifier (or contains one), look up its value before + // simplifying, or the quantifier might be irreparably altered. + n = m->getValue(n); + } + // Simplify the result. n = d_private->simplify(n); Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; @@ -3562,6 +3568,7 @@ void SmtEngine::checkModel(bool hardFailure) { // but don't show up in our substitution map above. n = m->getValue(n); Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl; + AlwaysAssert(n.isConst() || n.getKind() == kind::LAMBDA); // The result should be == true. if(n != NodeManager::currentNM()->mkConst(true)) { diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 75187b7bd..234b137c8 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -28,7 +28,7 @@ using namespace CVC4::context; using namespace CVC4::theory; TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels) : - d_substitutions(c), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) + d_substitutions(c, false), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -48,14 +48,13 @@ void TheoryModel::reset(){ d_uf_models.clear(); } -Node TheoryModel::getValue( TNode n ) const{ +Node TheoryModel::getValue(TNode n) const { //apply substitutions - Node nn = d_substitutions.apply( n ); + Node nn = d_substitutions.apply(n); //get value in model - nn = getModelValue( nn ); + nn = getModelValue(nn); //normalize nn = Rewriter::rewrite(nn); - Assert(nn.isConst() || nn.getKind() == kind::LAMBDA); return nn; } @@ -97,8 +96,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // 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)) { + if(!d_equalityEngine.hasTerm(Rewriter::rewrite(n))) { return n; + } else { + n = Rewriter::rewrite(n); } } else { if(n.getKind() == kind::LAMBDA) { |