diff options
| -rw-r--r-- | src/smt/boolean_terms.cpp | 671 |
1 files changed, 375 insertions, 296 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 2eabdbea3..d3a600bf5 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -26,10 +26,12 @@ #include "expr/kind.h" #include "util/hash.h" #include "util/bool.h" +#include "util/ntuple.h" #include <string> #include <algorithm> #include <set> #include <map> +#include <stack> using namespace std; using namespace CVC4::theory; @@ -292,330 +294,407 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN } Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() { - Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; - - // we only distinguish between datatypes, booleans, and "other", and we - // don't even distinguish datatypes except when in "native" conversion - // mode - if(parentTheory != theory::THEORY_BOOL) { - if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE || - parentTheory != theory::THEORY_DATATYPES) { - parentTheory = theory::THEORY_BUILTIN; - } - } - BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory)); - if(i != d_termCache.end()) { - return (*i).second.isNull() ? Node(top) : (*i).second; - } - - Kind k = top.getKind(); - kind::MetaKind mk = top.getMetaKind(); + stack< triple<TNode, theory::TheoryId, bool> > worklist; + worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false)); + stack< NodeBuilder<> > result; + result.push(NodeBuilder<>(kind::TUPLE)); NodeManager* nm = NodeManager::currentNM(); - if(quantBoolVars.find(top) != quantBoolVars.end()) { - // this Bool variable is quantified over and we're changing it to a BitVector var - if(parentTheory == theory::THEORY_BOOL) { - return quantBoolVars[top].eqNode(d_tt); - } else { - return quantBoolVars[top]; - } - } + while(!worklist.empty()) { + top = worklist.top().first; + parentTheory = worklist.top().second; + bool& childrenPushed = worklist.top().third; - if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) { - // still need to rewrite e.g. function applications over boolean - Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars); - Node n; - if(parentTheory == theory::THEORY_DATATYPES) { - n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt); - } else { - n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff); + Kind k = top.getKind(); + kind::MetaKind mk = top.getMetaKind(); + + // we only distinguish between datatypes, booleans, and "other", and we + // don't even distinguish datatypes except when in "native" conversion + // mode + if(parentTheory != theory::THEORY_BOOL) { + if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE || + parentTheory != theory::THEORY_DATATYPES) { + parentTheory = theory::THEORY_BUILTIN; + } } - Debug("boolean-terms") << "constructed ITE: " << n << endl; - return n; - } - if(mk == kind::metakind::CONSTANT) { - if(k == kind::STORE_ALL) { - const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>(); - ArrayType arrType = asa.getType(); - TypeNode indexType = TypeNode::fromType(arrType.getIndexType()); - Type constituentType = arrType.getConstituentType(); - if(constituentType.isBoolean()) { - // we have store_all(true) or store_all(false) - // just turn it into store_all(1) or store_all(0) - if(indexType.isBoolean()) { - // change index type to BV(1) also - indexType = d_tt.getType(); + if(!childrenPushed) { + Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; + + BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory)); + if(i != d_termCache.end()) { + result.top() << ((*i).second.isNull() ? Node(top) : (*i).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 + if(parentTheory == theory::THEORY_BOOL) { + result.top() << quantBoolVars[top].eqNode(d_tt); + } else { + result.top() << quantBoolVars[top]; } - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(), - (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr()); - Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << endl; - return n; + worklist.pop(); + goto next_worklist; } - if(indexType.isBoolean()) { - // must change index type to BV(1) - indexType = d_tt.getType(); - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); - Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << endl; - return n; + + if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) { + // still need to rewrite e.g. function applications over boolean + Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars); + Node n; + if(parentTheory == theory::THEORY_DATATYPES) { + n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt); + } else { + n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff); + } + Debug("boolean-terms") << "constructed ITE: " << n << endl; + result.top() << n; + worklist.pop(); + goto next_worklist; } - } - return top; - } else if(mk == kind::metakind::VARIABLE) { - TypeNode t = top.getType(); - if(t.isFunction()) { - for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) { - TypeNode newType = convertType(t[i], false); - if(newType != t[i]) { - vector<TypeNode> argTypes = t.getArgTypes(); - replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType()); - TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType()); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__", - newType, "a function introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl; - top.setAttribute(BooleanTermAttr(), n); - NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST); - NodeBuilder<> bodyBuilder(kind::APPLY_UF); - bodyBuilder << n; - for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) { - Node var = nm->mkBoundVar(t[j]); - boundVarsBuilder << var; - if(t[j].isBoolean()) { - bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff); - } else { - bodyBuilder << var; + + if(mk == kind::metakind::CONSTANT) { + if(k == kind::STORE_ALL) { + const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>(); + ArrayType arrType = asa.getType(); + TypeNode indexType = TypeNode::fromType(arrType.getIndexType()); + Type constituentType = arrType.getConstituentType(); + if(constituentType.isBoolean()) { + // we have store_all(true) or store_all(false) + // just turn it into store_all(1) or store_all(0) + if(indexType.isBoolean()) { + // change index type to BV(1) also + indexType = d_tt.getType(); } + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(), + (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << endl; + result.top() << n; + worklist.pop(); + goto next_worklist; + } + if(indexType.isBoolean()) { + // must change index type to BV(1) + indexType = d_tt.getType(); + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << endl; + result.top() << n; + worklist.pop(); + goto next_worklist; } - Node boundVars = boundVarsBuilder; - Node body = bodyBuilder; - 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; - return n; } - } - } else if(t.isArray()) { - TypeNode indexType = convertType(t.getArrayIndexType(), false); - TypeNode constituentType = convertType(t.getArrayConstituentType(), false); - if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) { - TypeNode newType = nm->mkArrayType(indexType, constituentType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "an array variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); - Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); - Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr())); - Node repl = nm->mkNode(kind::STORE, - nm->mkNode(kind::STORE, base, nm->mkConst(false), - nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true), - 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; - return n; - } - d_termCache[make_pair(top, parentTheory)] = Node::null(); - return top; - } else if(t.isTuple() || t.isRecord()) { - TypeNode newType = convertType(t, true); - if(t != newType) { - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "a tuple/record variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - n.setAttribute(BooleanTermAttr(), top); - 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; - return n; - } - d_termCache[make_pair(top, parentTheory)] = Node::null(); - return top; - } else if(t.isDatatype() || t.isParametricDatatype()) { - 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(), - "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", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; - 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; - return n; - } else { - d_termCache[make_pair(top, parentTheory)] = Node::null(); - return top; - } - } else if(t.isConstructor()) { - Assert(parentTheory != theory::THEORY_BOOL); - Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE || - t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE); - const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ? - t[t.getNumChildren() - 1].getConst<Datatype>() : - t[t.getNumChildren() - 1][0].getConst<Datatype>(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); - if(dt != dt2) { - Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), - "constructor `%s' not in cache", top.toString().c_str()); - return d_termCache[make_pair(top, parentTheory)]; - } - d_termCache[make_pair(top, parentTheory)] = Node::null(); - return top; - } else if(t.isTester() || t.isSelector()) { - Assert(parentTheory != theory::THEORY_BOOL); - const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ? - t[0].getConst<Datatype>() : - t[0][0].getConst<Datatype>(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); - if(dt != dt2) { - Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), - "tester or selector `%s' not in cache", top.toString().c_str()); - return d_termCache[make_pair(top, parentTheory)]; - } else { - d_termCache[make_pair(top, parentTheory)] = Node::null(); - return top; - } - } else if(t.getNumChildren() > 0) { - for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { - if((*i).isBoolean()) { - vector<TypeNode> argTypes(t.begin(), t.end()); - replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); - TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), - newType, "a variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - top.setAttribute(BooleanTermAttr(), n); - d_termCache[make_pair(top, parentTheory)] = n; - return n; + result.top() << top; + worklist.pop(); + goto next_worklist; + } else if(mk == kind::metakind::VARIABLE) { + TypeNode t = top.getType(); + if(t.isFunction()) { + for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) { + TypeNode newType = convertType(t[i], false); + if(newType != t[i]) { + vector<TypeNode> argTypes = t.getArgTypes(); + replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType()); + TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType()); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__", + newType, "a function introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl; + top.setAttribute(BooleanTermAttr(), n); + NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST); + NodeBuilder<> bodyBuilder(kind::APPLY_UF); + bodyBuilder << n; + for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) { + Node var = nm->mkBoundVar(t[j]); + boundVarsBuilder << var; + if(t[j].isBoolean()) { + bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff); + } else { + bodyBuilder << var; + } + } + Node boundVars = boundVarsBuilder; + Node body = bodyBuilder; + 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; + result.top() << n; + worklist.pop(); + goto next_worklist; + } + } + } else if(t.isArray()) { + TypeNode indexType = convertType(t.getArrayIndexType(), false); + TypeNode constituentType = convertType(t.getArrayConstituentType(), false); + if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) { + TypeNode newType = nm->mkArrayType(indexType, constituentType); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "an array variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); + Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); + Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr())); + Node repl = nm->mkNode(kind::STORE, + nm->mkNode(kind::STORE, base, nm->mkConst(false), + nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true), + 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; + result.top() << n; + worklist.pop(); + goto next_worklist; + } + d_termCache[make_pair(top, parentTheory)] = Node::null(); + result.top() << top; + worklist.pop(); + goto next_worklist; + } else if(t.isTuple() || t.isRecord()) { + TypeNode newType = convertType(t, true); + if(t != newType) { + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", + newType, "a tuple/record variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + top.setAttribute(BooleanTermAttr(), n); + n.setAttribute(BooleanTermAttr(), top); + 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; + result.top() << n; + worklist.pop(); + goto next_worklist; + } + d_termCache[make_pair(top, parentTheory)] = Node::null(); + result.top() << top; + worklist.pop(); + goto next_worklist; + } else if(t.isDatatype() || t.isParametricDatatype()) { + 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(), + "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", + NodeManager::SKOLEM_EXACT_NAME); + Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; + 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; + result.top() << n; + worklist.pop(); + goto next_worklist; + } else { + d_termCache[make_pair(top, parentTheory)] = Node::null(); + result.top() << top; + worklist.pop(); + goto next_worklist; + } + } else if(t.isConstructor()) { + Assert(parentTheory != theory::THEORY_BOOL); + Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE || + t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE); + const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ? + t[t.getNumChildren() - 1].getConst<Datatype>() : + t[t.getNumChildren() - 1][0].getConst<Datatype>(); + TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); + const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); + if(dt != dt2) { + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), + "constructor `%s' not in cache", top.toString().c_str()); + result.top() << d_termCache[make_pair(top, parentTheory)]; + worklist.pop(); + goto next_worklist; + } + d_termCache[make_pair(top, parentTheory)] = Node::null(); + result.top() << top; + worklist.pop(); + goto next_worklist; + } else if(t.isTester() || t.isSelector()) { + Assert(parentTheory != theory::THEORY_BOOL); + const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ? + t[0].getConst<Datatype>() : + t[0][0].getConst<Datatype>(); + TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); + const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>(); + if(dt != dt2) { + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), + "tester or selector `%s' not in cache", top.toString().c_str()); + result.top() << d_termCache[make_pair(top, parentTheory)]; + worklist.pop(); + goto next_worklist; + } else { + d_termCache[make_pair(top, parentTheory)] = Node::null(); + result.top() << top; + worklist.pop(); + goto next_worklist; + } + } else if(t.getNumChildren() > 0) { + for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { + if((*i).isBoolean()) { + vector<TypeNode> argTypes(t.begin(), t.end()); + replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); + TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); + Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), + newType, "a variable introduced by Boolean-term conversion", + NodeManager::SKOLEM_EXACT_NAME); + Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; + top.setAttribute(BooleanTermAttr(), n); + d_termCache[make_pair(top, parentTheory)] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; + } + } } + result.top() << top; + worklist.pop(); + goto next_worklist; } - } - return top; - } - switch(k) { - case kind::LAMBDA: - Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str()); + switch(k) { + case kind::LAMBDA: + Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str()); - case kind::BOUND_VAR_LIST: - return top; + case kind::BOUND_VAR_LIST: + result.top() << top; + worklist.pop(); + goto next_worklist; - case kind::REWRITE_RULE: - case kind::RR_REWRITE: - case kind::RR_DEDUCTION: - case kind::RR_REDUCTION: - // not yet supported - return top; + case kind::REWRITE_RULE: + case kind::RR_REWRITE: + case kind::RR_DEDUCTION: + case kind::RR_REDUCTION: + // not yet supported + result.top() << top; + worklist.pop(); + goto next_worklist; - case kind::FORALL: - case kind::EXISTS: { - Debug("bt") << "looking at quantifier -> " << top << endl; - set<TNode> ourVars; - for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { - if((*i).getType().isBoolean()) { - ourVars.insert(*i); - } - } - if(ourVars.empty()) { - // Simple case, quantifier doesn't quantify over Boolean vars, - // no special handling needed for quantifier. Fall through. - Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl; - } else { - set<TNode> output; - hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen; - collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen); - if(output.empty()) { - // Simple case, quantifier quantifies over Boolean vars, but they - // don't occur in term context. Fall through. - Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl; - } else { - Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl; - // We have Boolean vars appearing in term context. Convert their - // types in the quantifier. - for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) { - Node newVar = nm->mkBoundVar((*i).toString(), nm->mkBitVectorType(1)); - Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)"); - quantBoolVars[*i] = newVar; - } - vector<TNode> boundVars; + case kind::FORALL: + case kind::EXISTS: { + Debug("bt") << "looking at quantifier -> " << top << endl; + set<TNode> ourVars; for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { - map<TNode, Node>::const_iterator j = quantBoolVars.find(*i); - if(j == quantBoolVars.end()) { - boundVars.push_back(*i); + if((*i).getType().isBoolean()) { + ourVars.insert(*i); + } + } + if(ourVars.empty()) { + // Simple case, quantifier doesn't quantify over Boolean vars, + // no special handling needed for quantifier. Fall through. + Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl; + } else { + set<TNode> output; + hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen; + collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen); + if(output.empty()) { + // Simple case, quantifier quantifies over Boolean vars, but they + // don't occur in term context. Fall through. + Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl; } else { - boundVars.push_back((*j).second); + Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl; + // We have Boolean vars appearing in term context. Convert their + // types in the quantifier. + for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) { + Node newVar = nm->mkBoundVar((*i).toString(), nm->mkBitVectorType(1)); + Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)"); + quantBoolVars[*i] = newVar; + } + vector<TNode> boundVars; + for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { + map<TNode, Node>::const_iterator j = quantBoolVars.find(*i); + if(j == quantBoolVars.end()) { + boundVars.push_back(*i); + } else { + boundVars.push_back((*j).second); + } + } + Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); + Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars); + Node quant = nm->mkNode(top.getKind(), boundVarList, body); + Debug("bt") << "rewrote quantifier to -> " << quant << endl; + d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant; + d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff); + d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff); + result.top() << quant; + worklist.pop(); + goto next_worklist; } } - Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); - Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars); - Node quant = nm->mkNode(top.getKind(), boundVarList, body); - Debug("bt") << "rewrote quantifier to -> " << quant << endl; - d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant; - d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff); - d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff); - return quant; + /* intentional fall-through for some cases above */ } - } - /* intentional fall-through for some cases above */ - } - default: - NodeBuilder<> b(k); - Debug("bt") << "looking at: " << top << endl; - if(mk == kind::metakind::PARAMETERIZED) { - if(k == kind::RECORD) { - b << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES); - } else if(k == kind::APPLY_TYPE_ASCRIPTION) { - Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType())); - b << asc; - Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl; - asc.setAttribute(BooleanTermAttr(), top.getOperator()); - } else if(kindToTheoryId(k) != THEORY_BV && - k != kind::TUPLE_SELECT && - k != kind::TUPLE_UPDATE && - k != kind::RECORD_SELECT && - k != kind::RECORD_UPDATE) { - Debug("bt") << "rewriting: " << top.getOperator() << endl; - b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); - Debug("bt") << "got: " << b.getOperator() << endl; - } else { - b << top.getOperator(); + default: + result.push(NodeBuilder<>(k)); + Debug("bt") << "looking at: " << top << endl; + // rewrite the operator, as necessary + if(mk == kind::metakind::PARAMETERIZED) { + if(k == kind::RECORD) { + result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES); + } else if(k == kind::APPLY_TYPE_ASCRIPTION) { + Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType())); + result.top() << asc; + Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl; + asc.setAttribute(BooleanTermAttr(), top.getOperator()); + } else if(kindToTheoryId(k) != THEORY_BV && + k != kind::TUPLE_SELECT && + k != kind::TUPLE_UPDATE && + k != kind::RECORD_SELECT && + k != kind::RECORD_UPDATE) { + Debug("bt") << "rewriting: " << top.getOperator() << endl; + result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); + Debug("bt") << "got: " << result.top().getOperator() << endl; + } else { + result.top() << top.getOperator(); + } + } + // push children + for(int i = top.getNumChildren() - 1; i >= 0; --i) { + Debug("bt") << "rewriting: " << top[i] << endl; + worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), false)); + //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars); + //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl; + } + childrenPushed = true; } - } - for(unsigned i = 0; i < top.getNumChildren(); ++i) { - Debug("bt") << "rewriting: " << top[i] << endl; - b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars); - Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl; - } - Node n = b; - Debug("boolean-terms") << "constructed: " << n << endl; - if(parentTheory == theory::THEORY_BOOL) { - if(n.getType().isBitVector() && - n.getType().getBitVectorSize() == 1) { - n = nm->mkNode(kind::EQUAL, n, d_tt); - } else if(n.getType().isDatatype() && - n.getType().hasAttribute(BooleanTermAttr())) { - n = nm->mkNode(kind::EQUAL, n, d_ttDt); + } else { + Node n = result.top(); + result.pop(); + Debug("boolean-terms") << "constructed: " << n << endl; + if(parentTheory == theory::THEORY_BOOL) { + if(n.getType().isBitVector() && + n.getType().getBitVectorSize() == 1) { + n = nm->mkNode(kind::EQUAL, n, d_tt); + } else if(n.getType().isDatatype() && + n.getType().hasAttribute(BooleanTermAttr())) { + n = nm->mkNode(kind::EQUAL, n, d_ttDt); + } } + d_termCache[make_pair(top, parentTheory)] = n; + result.top() << n; + worklist.pop(); + goto next_worklist; } - d_termCache[make_pair(top, parentTheory)] = n; - return n; + + next_worklist: + ; } + + Assert(worklist.size() == 0); + Assert(result.size() == 1); + Node retval = result.top()[0]; + result.top().clear(); + result.pop(); + return retval; + }/* BooleanTermConverter::rewriteBooleanTermsRec() */ }/* CVC4::smt namespace */ |