diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 89 |
1 files changed, 54 insertions, 35 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 88cefbdc2..0fadca424 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -313,7 +313,6 @@ class SmtEnginePrivate : public NodeManagerListener { hash_map<unsigned, Node> d_BVDivByZero; hash_map<unsigned, Node> d_BVRemByZero; - /** * Function symbol used to implement uninterpreted * int-division-by-zero semantics. Needed to deal with partial @@ -560,6 +559,11 @@ public: throw(TypeCheckingException, LogicException); /** + * Rewrite Boolean terms in a Node. + */ + Node rewriteBooleanTerms(TNode n); + + /** * Simplify node "in" by expanding definitions and applying any * substitutions learned from preprocessing. */ @@ -2899,6 +2903,39 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, return false; } +Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); + if(d_booleanTermConverter == NULL) { + // This needs to be initialized _after_ the whole SMT framework is in place, subscribed + // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype + // definition, and not dump it properly. + d_booleanTermConverter = new BooleanTermConverter(d_smt); + } + Node retval = d_booleanTermConverter->rewriteBooleanTerms(n); + if(retval != n) { + switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { + case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + case booleans::BOOLEAN_TERM_CONVERT_NATIVE: + if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_BV); + d_smt.d_logic.lock(); + } + break; + case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_DATATYPES); + d_smt.d_logic.lock(); + } + break; + default: + Unhandled(mode); + } + } + return retval; +} + void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); @@ -2956,37 +2993,8 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess); { Chat() << "rewriting Boolean terms..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); - if(d_booleanTermConverter == NULL) { - // This needs to be initialized _after_ the whole SMT framework is in place, subscribed - // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype - // definition, and not dump it properly. - d_booleanTermConverter = new BooleanTermConverter(d_smt); - } for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { - Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]); - if(n != d_assertionsToPreprocess[i]) { - switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { - case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - case booleans::BOOLEAN_TERM_CONVERT_NATIVE: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_BV); - d_smt.d_logic.lock(); - } - break; - case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_DATATYPES); - d_smt.d_logic.lock(); - } - break; - default: - Unhandled(mode); - } - } - d_assertionsToPreprocess[i] = n; + d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]); } } dumpAssertions("post-boolean-terms", d_assertionsToPreprocess); @@ -3529,9 +3537,14 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // do not need to apply preprocessing substitutions (should be recorded // in model already) + Node n = Node::fromExpr(e); + Trace("smt") << "--- getting value of " << n << endl; + TypeNode expectedType = n.getType(); + // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; - Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); + n = d_private->expandDefinitions(n, cache); + n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; @@ -3541,13 +3554,13 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin resultNode = m->getValue(n); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; - resultNode = postprocess(resultNode, n.getType()); + resultNode = postprocess(resultNode, expectedType); Trace("smt") << "--- model-post returned " << resultNode << endl; Trace("smt") << "--- model-post returned " << resultNode.getType() << endl; - Trace("smt") << "--- model-post expected " << n.getType() << endl; + Trace("smt") << "--- model-post expected " << expectedType << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); + Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType)); // ensure it's a constant Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); @@ -3625,9 +3638,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { ++i) { Assert((*i).getType() == boolType); + Trace("smt") << "--- getting value of " << *i << endl; + // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(*i, cache); + n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; @@ -3639,6 +3655,9 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { // type-check the result we got Assert(resultNode.isNull() || resultNode.getType() == boolType); + // ensure it's a constant + Assert(resultNode.isConst()); + vector<SExpr> v; if((*i).getKind() == kind::APPLY) { Assert((*i).getNumChildren() == 0); |