diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:47:56 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:47:56 -0500 |
commit | 7f604fe97bd85efbe6ffcf17140905cdb34c7468 (patch) | |
tree | 75a2b26057b4bf0a9d08d519da5b4801f1322634 /src | |
parent | 42be934ef4d4430944ae9074c7202a7d130c75bb (diff) |
Fix bug 554 (nominally).
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 02542b640..1bbc99f09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3677,8 +3677,15 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); - n = d_private->rewriteBooleanTerms(n); - n = Rewriter::rewrite(n); + // There are two ways model values for terms are computed (for historical + // reasons). One way is that used in check-model; the other is that + // used by the Model classes. It's not clear to me exactly how these + // two are different, but they need to be unified. This ugly hack here + // is to fix bug 554 until we can revamp boolean-terms and models [MGD] + if(!n.getType().isFunction()) { + n = d_private->rewriteBooleanTerms(n); + n = Rewriter::rewrite(n); + } Trace("smt") << "--- getting value of " << n << endl; TheoryModel* m = d_theoryEngine->getModel(); |