From ce6d5ca3fac179c2b5846df5c2661c4f26384425 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 16 Dec 2013 07:30:06 -0500 Subject: [PATCH] Fix for bug 544. --- src/smt/boolean_terms.cpp | 54 +++++++++++-------- src/smt/boolean_terms.h | 5 ++ src/smt/smt_engine.cpp | 89 +++++++++++++++++++------------ test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug544.smt2 | 10 ++++ 5 files changed, 102 insertions(+), 59 deletions(-) create mode 100644 test/regress/regress0/bug544.smt2 diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 30aa79aca..c1596dddc 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -43,8 +43,10 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : d_tt(), d_ffDt(), d_ttDt(), + d_varCache(), d_termCache(), - d_typeCache() { + d_typeCache(), + d_datatypeCache() { // set up our "false" and "true" conversions based on command-line option if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || @@ -250,10 +252,10 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl; Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr? Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl; - d_termCache[make_pair(Node::fromExpr((*c).getConstructor()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); - d_termCache[make_pair(Node::fromExpr((*c).getTester()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); + d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); + d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); + d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); } } out = &newD; @@ -400,12 +402,18 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa if(!childrenPushed) { Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; - BooleanTermCache::iterator i = d_termCache.find(pair(top, parentTheory)); - if(i != d_termCache.end()) { + BooleanTermVarCache::iterator i = d_varCache.find(top); + if(i != d_varCache.end()) { result.top() << ((*i).second.isNull() ? Node(top) : (*i).second); worklist.pop(); goto next_worklist; } + BooleanTermCache::iterator j = d_termCache.find(pair(top, parentTheory)); + if(j != d_termCache.end()) { + result.top() << ((*j).second.isNull() ? Node(top) : (*j).second); + worklist.pop(); + goto next_worklist; + } if(quantBoolVars.find(top) != quantBoolVars.end()) { // this Bool variable is quantified over and we're changing it to a BitVector var @@ -511,7 +519,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; @@ -536,7 +544,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa nm->mkConst(false), n_ff); Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; @@ -548,7 +556,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa top.setAttribute(BooleanTermAttr(), n); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; @@ -568,12 +576,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa nm->mkNode(kind::EQUAL, n_tt, d_tt)); Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; } - d_termCache[make_pair(top, parentTheory)] = Node::null(); + d_varCache[top] = Node::null(); result.top() << top; worklist.pop(); goto next_worklist; @@ -588,12 +596,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; } - d_termCache[make_pair(top, parentTheory)] = Node::null(); + d_varCache[top] = Node::null(); result.top() << top; worklist.pop(); goto next_worklist; @@ -601,7 +609,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa Debug("boolean-terms") << "found a var of datatype type" << endl; TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES); if(t != newT) { - Assert(d_termCache.find(make_pair(top, parentTheory)) == d_termCache.end(), + Assert(d_varCache.find(top) == d_varCache.end(), "Node `%s' already in cache ?!", top.toString().c_str()); Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", newT, "a datatype variable introduced by Boolean-term conversion", @@ -610,12 +618,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa top.setAttribute(BooleanTermAttr(), n); d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl; - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; } else { - d_termCache[make_pair(top, parentTheory)] = Node::null(); + d_varCache[top] = Node::null(); result.top() << top; worklist.pop(); goto next_worklist; @@ -630,13 +638,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst(); if(dt != dt2) { - Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), + Assert(d_varCache.find(top) != d_varCache.end(), "constructor `%s' not in cache", top.toString().c_str()); - result.top() << d_termCache[make_pair(top, parentTheory)]; + result.top() << d_varCache[top]; worklist.pop(); goto next_worklist; } - d_termCache[make_pair(top, parentTheory)] = Node::null(); + d_varCache[top] = Node::null(); result.top() << top; worklist.pop(); goto next_worklist; @@ -648,13 +656,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst(); if(dt != dt2) { - Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), + Assert(d_varCache.find(top) != d_varCache.end(), "tester or selector `%s' not in cache", top.toString().c_str()); - result.top() << d_termCache[make_pair(top, parentTheory)]; + result.top() << d_varCache[top]; worklist.pop(); goto next_worklist; } else { - d_termCache[make_pair(top, parentTheory)] = Node::null(); + d_varCache[top] = Node::null(); result.top() << top; worklist.pop(); goto next_worklist; @@ -670,7 +678,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa NodeManager::SKOLEM_EXACT_NAME); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; top.setAttribute(BooleanTermAttr(), n); - d_termCache[make_pair(top, parentTheory)] = n; + d_varCache[top] = n; result.top() << n; worklist.pop(); goto next_worklist; diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index 904d47b5f..89611f5ea 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -35,6 +35,9 @@ namespace attr { typedef expr::Attribute BooleanTermAttr; class BooleanTermConverter { + /** The type of the Boolean term conversion variable cache */ + typedef std::hash_map BooleanTermVarCache; + /** The type of the Boolean term conversion cache */ typedef std::hash_map< std::pair, Node, PairHashFunction< Node, bool, @@ -58,6 +61,8 @@ class BooleanTermConverter { /** The conversion for "true" when in datatypes contexts. */ Node d_ttDt; + /** The cache used during Boolean term variable conversion */ + BooleanTermVarCache d_varCache; /** The cache used during Boolean term conversion */ BooleanTermCache d_termCache; /** The cache used during Boolean term type conversion */ 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 d_BVDivByZero; hash_map d_BVRemByZero; - /** * Function symbol used to implement uninterpreted * int-division-by-zero semantics. Needed to deal with partial @@ -559,6 +558,11 @@ public: Node expandDefinitions(TNode n, hash_map& cache) 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_mapd_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 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 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 v; if((*i).getKind() == kind::APPLY) { Assert((*i).getNumChildren() == 0); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1daa0d1e8..5c591d39c 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -152,7 +152,8 @@ BUG_TESTS = \ bug521.minimized.smt2 \ bug522.smt2 \ bug528a.smt2 \ - bug541.smt2 + bug541.smt2 \ + bug544.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug544.smt2 b/test/regress/regress0/bug544.smt2 new file mode 100644 index 000000000..ec2ef0075 --- /dev/null +++ b/test/regress/regress0/bug544.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +; EXPECT: (((not (select a x)) false)) +(set-option :produce-models true) +(set-logic QF_AUFLIA) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun a () (Array U Bool)) +(assert (select a x)) +(check-sat) +(get-value ((not (select a x)))) -- 2.30.2