#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;
}
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 */
projects / cvc5.git / commitdiff