diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/smt/boolean_terms.cpp | |
parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r-- | src/smt/boolean_terms.cpp | 399 |
1 files changed, 293 insertions, 106 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 35184e42e..09d8fcbd4 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -21,6 +21,8 @@ #include "smt/smt_engine.h" #include "theory/theory_engine.h" #include "theory/model.h" +#include "theory/booleans/boolean_term_conversion_mode.h" +#include "theory/booleans/options.h" #include "expr/kind.h" #include "util/hash.h" #include "util/bool.h" @@ -31,10 +33,56 @@ using namespace std; using namespace CVC4::theory; +using namespace CVC4::theory::booleans; namespace CVC4 { namespace smt { +BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : + d_smt(smt), + d_ff(), + d_tt(), + d_ffDt(), + d_ttDt(), + d_termCache(), + d_typeCache() { + + // set up our "false" and "true" conversions based on command-line option + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || + options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) { + d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u)); + d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + } + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) { + d_ffDt = d_ff; + d_ttDt = d_tt; + } else { + Datatype spec("BooleanTerm"); + // don't change the order; false is assumed to come first by the model postprocessor + spec.addConstructor(DatatypeConstructor("BT_False")); + spec.addConstructor(DatatypeConstructor("BT_True")); + const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype(); + d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor())); + d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor())); + // mark this datatype type as being special for Boolean term conversion + TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null()); + if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) { + Assert(d_ff.isNull() && d_tt.isNull()); + d_ff = d_ffDt; + d_tt = d_ttDt; + } + } + + // assert that we set it up correctly + Assert(!d_ff.isNull() && !d_tt.isNull()); + Assert(!d_ffDt.isNull() && !d_ttDt.isNull()); + Assert(d_ff != d_tt); + Assert(d_ff.getType() == d_tt.getType()); + Assert(d_ffDt != d_ttDt); + Assert(d_ffDt.getType() == d_ttDt.getType()); + +}/* BooleanTermConverter::BooleanTermConverter() */ + static inline bool isBoolean(TNode top, unsigned i) { switch(top.getKind()) { case kind::NOT: @@ -63,27 +111,51 @@ static inline bool isBoolean(TNode top, unsigned i) { } } -const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() { - return dt; - // boolean terms not supported in datatypes, yet +const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { + const Datatype*& out = d_datatypeCache[&dt]; + if(out != NULL) { + return *out; + } - Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl; + Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl; for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) { TypeNode t = TypeNode::fromType((*c).getConstructor().getType()); for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) { - if((*a).isBoolean()) { - Datatype newDt(dt.getName() + "'"); + TypeNode converted = convertType(*a, true); + Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl; + if(*a != converted) { + SortConstructorType mySelfType; + set<Type> unresolvedTypes; + if(dt.isParametric()) { + mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters()); + unresolvedTypes.insert(mySelfType); + } + vector<Datatype> newDtVector; + if(dt.isParametric()) { + newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters())); + } else { + newDtVector.push_back(Datatype(dt.getName() + "'")); + } + Datatype& newDt = newDtVector.front(); Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; for(c = dt.begin(); c != dt.end(); ++c) { DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'"); t = TypeNode::fromType((*c).getConstructor().getType()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - if((*a).getType().getRangeType().isBoolean()) { - ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType()); - } else { - Type argType = (*a).getType().getRangeType(); - if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) { + Type argType = (*a).getType().getRangeType(); + if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) { + Debug("boolean-terms") << "argtype " << argType << " is self" << endl; + if(dt.isParametric()) { + Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl; + ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters())); + } else { ctor.addArg((*a).getName() + "'", DatatypeSelfType()); + } + } else { + Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl; + converted = convertType(TypeNode::fromType(argType), true); + if(TypeNode::fromType(argType) != converted) { + ctor.addArg((*a).getName() + "'", converted.toType()); } else { ctor.addArg((*a).getName() + "'", argType); } @@ -91,22 +163,107 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype } newDt.addConstructor(ctor); } - DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt); + vector<DatatypeType> newDttVector = + NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes); + DatatypeType& newDtt = newDttVector.front(); const Datatype& newD = newDtt.getDatatype(); for(c = dt.begin(); c != dt.end(); ++c) { Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl; - d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); - d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); + 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()); for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); + d_termCache[make_pair(Node::fromExpr((*a).getSelector()), theory::THEORY_BUILTIN)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); } } + out = &newD; return newD; } } } + + out = &dt; return dt; -}/* BooleanTermConverter::booleanTermsConvertDatatype() */ + +}/* BooleanTermConverter::convertDatatype() */ + +TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) { + Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl; + // This function recursively converts the type. + if(type.isBoolean()) { + return datatypesContext ? d_ttDt.getType() : d_tt.getType(); + } + const pair<TypeNode, bool> cacheKey(type, datatypesContext); + if(d_typeCache.find(cacheKey) != d_typeCache.end()) { + TypeNode out = d_typeCache[cacheKey]; + return out.isNull() ? type : out; + } + TypeNode& outNode = d_typeCache[cacheKey]; + if(type.getKind() == kind::DATATYPE_TYPE || + type.getKind() == kind::PARAMETRIC_DATATYPE) { + bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE); + const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>(); + TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType()); + Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl; + if(parametric) { + // re-parameterize the translation + vector<TypeNode> params = type.getParamTypes(); + for(size_t i = 0; i < params.size(); ++i) { + Debug("boolean-terms") << "in loop, got "<< params[i] << endl; + params[i] = convertType(params[i], true); + Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl; + } + params.insert(params.begin(), out[0]); + out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params); + Debug("boolean-terms") << "got OUT: " << out << endl; + } + if(out != type) { + outNode = out;// cache it + Debug("boolean-terms") << "OUT is same as TYPE" << endl; + } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl; + return out; + } + if(type.isRecord()) { + const Record& rec = type.getConst<Record>(); + vector< pair<string, Type> > flds; + for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) { + TypeNode converted = convertType(TypeNode::fromType((*i).second), true); + if(TypeNode::fromType((*i).second) != converted) { + flds.push_back(make_pair((*i).first, converted.toType())); + } else { + flds.push_back(*i); + } + } + TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds)); + Debug("tuprec") << "converted " << type << " to " << newRec << endl; + if(newRec != type) { + outNode = newRec;// cache it + } + return newRec; + } + if(type.getNumChildren() > 0) { + Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl; + // This should handle tuples and arrays ok. + // Might handle function types too, but they can't go + // in other types, so it doesn't matter. + NodeBuilder<> b(type.getKind()); + if(type.getMetaKind() == kind::metakind::PARAMETERIZED) { + b << type.getOperator(); + } + for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) { + b << convertType(*i, false); + } + TypeNode out = b; + if(out != type) { + outNode = out;// cache it + } + Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl; + return out; + } + // leave the cache at Null + return type; +}/* BooleanTermConverter::convertType() */ // look for vars from "vars" that occur in a term-context in n; transfer them to output. static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) { @@ -134,11 +291,21 @@ static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TN } } -Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw() { - Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl; +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_booleanTermCache.find(make_pair<Node, bool>(top, boolParent)); - if(i != d_booleanTermCache.end()) { + BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory)); + if(i != d_termCache.end()) { return (*i).second.isNull() ? Node(top) : (*i).second; } @@ -147,22 +314,24 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(BitVector(1u, 1u)); - Node zero = nm->mkConst(BitVector(1u, 0u)); - if(quantBoolVars.find(top) != quantBoolVars.end()) { // this Bool variable is quantified over and we're changing it to a BitVector var - if(boolParent) { - return quantBoolVars[top].eqNode(one); + if(parentTheory == theory::THEORY_BOOL) { + return quantBoolVars[top].eqNode(d_tt); } else { return quantBoolVars[top]; } } - if(!boolParent && top.getType().isBoolean()) { + if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) { // still need to rewrite e.g. function applications over boolean - Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars); - Node n = nm->mkNode(kind::ITE, topRewritten, one, zero); + 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; return n; } @@ -176,19 +345,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st if(constituentType.isBoolean()) { // we have store_all(true) or store_all(false) // just turn it into store_all(1) or store_all(0) - Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst<bool>() ? 1u : 0u)); if(indexType.isBoolean()) { // change index type to BV(1) also - indexType = nm->mkBitVectorType(1); + indexType = d_tt.getType(); } - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr()); + 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; } if(indexType.isBoolean()) { // must change index type to BV(1) - indexType = nm->mkBitVectorType(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; @@ -200,9 +369,10 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st TypeNode t = top.getType(); if(t.isFunction()) { for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) { - if(t[i].isBoolean()) { + TypeNode newType = convertType(t[i], false); + if(newType != t[i]) { vector<TypeNode> argTypes = t.getArgTypes(); - replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1)); + 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", @@ -216,7 +386,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st Node var = nm->mkBoundVar(t[j]); boundVarsBuilder << var; if(t[j].isBoolean()) { - bodyBuilder << nm->mkNode(kind::ITE, var, one, zero); + bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff); } else { bodyBuilder << var; } @@ -226,105 +396,112 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); - d_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } } } else if(t.isArray()) { - TypeNode indexType = t.getArrayIndexType(); - TypeNode constituentType = t.getArrayConstituentType(); - bool rewrite = false; - if(indexType.isBoolean()) { - indexType = nm->mkBitVectorType(1); - rewrite = true; - } - if(constituentType.isBoolean()) { - constituentType = nm->mkBitVectorType(1); - rewrite = true; - } - if(rewrite) { + 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()), + 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_zero = nm->mkNode(kind::SELECT, n, zero); - Node n_one = nm->mkNode(kind::SELECT, n, one); + 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_zero, one)), nm->mkConst(true), - nm->mkNode(kind::EQUAL, n_one, one)); + 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_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; - } else if(t.isTuple()) { - return top; - } else if(t.isRecord()) { + } 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()) { - return top;// no support for datatypes at present - const Datatype& dt = t.getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); - if(dt != dt2) { - Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(), + } 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()); - Assert(top.isVar()); - TypeNode newType = TypeNode::fromType(dt2.getDatatypeType()); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), - newType, "an array variable introduced by Boolean-term conversion", + 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); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - d_booleanTermCache[make_pair(top, boolParent)] = 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_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + d_termCache[make_pair(top, parentTheory)] = Node::null(); return top; } } else if(t.isConstructor()) { - return top;// no support for datatypes at present - Assert(!boolParent); - const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); + 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_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(), + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), "constructor `%s' not in cache", top.toString().c_str()); - return d_booleanTermCache[make_pair(top, boolParent)]; - } else { - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); - return top; + return d_termCache[make_pair(top, parentTheory)]; } + d_termCache[make_pair(top, parentTheory)] = Node::null(); + return top; } else if(t.isTester() || t.isSelector()) { - return top;// no support for datatypes at present - Assert(!boolParent); - const Datatype& dt = t[0].getConst<Datatype>(); - const Datatype& dt2 = booleanTermsConvertDatatype(dt); + 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_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(), + Assert(d_termCache.find(make_pair(top, parentTheory)) != d_termCache.end(), "tester or selector `%s' not in cache", top.toString().c_str()); - return d_booleanTermCache[make_pair(top, boolParent)]; + return d_termCache[make_pair(top, parentTheory)]; } else { - d_booleanTermCache[make_pair(top, boolParent)] = Node::null(); + 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, nm->mkBitVectorType(1)); + 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_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } } @@ -385,11 +562,12 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } } Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); - Node body = rewriteBooleanTermsRec(top[1], true, quantBoolVars); + 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_booleanTermCache[make_pair(top, true)] = quant; - d_booleanTermCache[make_pair(top, false)] = quant.iteNode(one, zero); + 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; } } @@ -400,15 +578,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st NodeBuilder<> b(k); Debug("bt") << "looking at: " << top << endl; if(mk == kind::metakind::PARAMETERIZED) { - if(kindToTheoryId(k) != THEORY_BV && - k != kind::APPLY_TYPE_ASCRIPTION && - k != kind::TUPLE_SELECT && - k != kind::TUPLE_UPDATE && - k != kind::RECORD_SELECT && - k != kind::RECORD_UPDATE && - k != kind::RECORD) { + 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(), false, quantBoolVars); + b << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); Debug("bt") << "got: " << b.getOperator() << endl; } else { b << top.getOperator(); @@ -416,17 +599,21 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, bool boolParent, st } for(unsigned i = 0; i < top.getNumChildren(); ++i) { Debug("bt") << "rewriting: " << top[i] << endl; - b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), quantBoolVars); + 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(boolParent && - n.getType().isBitVector() && - n.getType().getBitVectorSize() == 1) { - n = nm->mkNode(kind::EQUAL, n, one); + 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_booleanTermCache[make_pair(top, boolParent)] = n; + d_termCache[make_pair(top, parentTheory)] = n; return n; } }/* BooleanTermConverter::rewriteBooleanTermsRec() */ |