From ce6d5ca3fac179c2b5846df5c2661c4f26384425 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 16 Dec 2013 07:30:06 -0500 Subject: Fix for bug 544. --- src/smt/boolean_terms.cpp | 54 +++++++++++++++++++++++++++-------------------- 1 file changed, 31 insertions(+), 23 deletions(-) (limited to 'src/smt/boolean_terms.cpp') 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; -- cgit v1.2.3