diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-01 18:00:12 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-07 18:06:11 -0500 |
commit | d6a6ab61dbe64848b78b9ab8d07d95fc58b64e72 (patch) | |
tree | db3cb085ddd0c2aad7e8ee32cb5d0c4a428183c6 /src | |
parent | 822d66189bac649d1f04208f8f4f80e292403d40 (diff) |
Significant work on bug #491 (not yet closed).
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 37 | ||||
-rw-r--r-- | src/theory/substitutions.h | 6 |
4 files changed, 36 insertions, 16 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) { } |