diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/smt | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/boolean_terms.cpp | 819 | ||||
-rw-r--r-- | src/smt/boolean_terms.h | 79 | ||||
-rw-r--r-- | src/smt/ite_removal.cpp | 103 | ||||
-rw-r--r-- | src/smt/ite_removal.h | 16 | ||||
-rw-r--r-- | src/smt/model_postprocessor.cpp | 203 | ||||
-rw-r--r-- | src/smt/model_postprocessor.h | 22 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 83 |
7 files changed, 97 insertions, 1228 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index bcacd4bd4..442355580 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -38,824 +38,5 @@ 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_varCache(smt.d_userContext), - d_termCache(smt.d_userContext), - d_typeCache(), - d_datatypeCache(), - d_datatypeReverseCache() { - - // 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: - case kind::AND: - case kind::IFF: - case kind::IMPLIES: - case kind::OR: - case kind::XOR: - case kind::FORALL: - case kind::EXISTS: - case kind::REWRITE_RULE: - case kind::RR_REWRITE: - case kind::RR_DEDUCTION: - case kind::RR_REDUCTION: - case kind::INST_PATTERN: - return true; - - case kind::ITE: - if(i == 0) { - return true; - } - return top.getType().isBoolean(); - - default: - return false; - } -} - -// This function rewrites "in" as an "as"---this is actually expected -// to be for model-substitution, so the "in" is a Boolean-term-converted -// node, and "as" is the original. See how it's used in function -// handling, below. -// -// Note this isn't the case any longer, and parts of what's below have -// been repurposed for *forward* conversion, meaning this works in either -// direction. -Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw() { - Debug("boolean-terms2") << "Rewrite as " << in << " " << as << std::endl; - if(in.getType() == as) { - return in; - } - if(in.getType().isBoolean()) { - Assert(d_tt.getType() == as); - return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff); - } - if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in); - } - TypeNode in_t = in.getType(); - if( processing.find( in_t )==processing.end() ){ - processing[in_t] = true; - if(in.getType().isParametricDatatype() && - in.getType().isInstantiatedDatatype()) { - // We have something here like (Pair Bool Bool)---need to dig inside - // and make it (Pair BV1 BV1) - Assert(as.isParametricDatatype() && as.isInstantiatedDatatype()); - const Datatype* dt2 = &as[0].getDatatype(); - std::vector<TypeNode> fromParams, toParams; - for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { - fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); - toParams.push_back(as[i + 1]); - } - const Datatype* dt1; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; - } - Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); - Node out; - for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { - DatatypeConstructor ctor = (*dt1)[i]; - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[i].getConstructor(); - for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); - asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing); - } - Node appctor = appctorb; - if(i == 0) { - out = appctor; - } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; - } - } - processing.erase( in_t ); - return out; - } - if(in.getType().isDatatype()) { - if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { - processing.erase( in_t ); - return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); - } - Assert(as.isDatatype()); - const Datatype* dt2 = &as.getDatatype(); - const Datatype* dt1; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; - } - Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); - Node out; - for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { - DatatypeConstructor ctor = (*dt1)[i]; - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[i].getConstructor(); - for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing); - } - Node appctor = appctorb; - if(i == 0) { - out = appctor; - } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; - } - } - processing.erase( in_t ); - return out; - } - if(in.getType().isArray()) { - // convert in to in' - // e.g. in : (Array Int Bool) - // for in' : (Array Int (_ BitVec 1)) - // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x] - Assert(as.isArray()); - Assert(as.getArrayIndexType() == in.getType().getArrayIndexType()); - Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType()); - Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType()); - Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x); - Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x); - Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing); - Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime); - Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam); - Assert(out.getType() == as); - processing.erase( in_t ); - return out; - } - Unhandled(in); - }else{ - Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl; - exit( 0 ); - } -} - -const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { - const Datatype*& out = d_datatypeCache[&dt]; - if(out != NULL) { - return *out; - } - - 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) { - 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(), false)); - } else { - newDtVector.push_back(Datatype(dt.getName() + "'", false)); - } - 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) { - 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); - } - } - } - newDt.addConstructor(ctor); - } - 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; - const DatatypeConstructor *newC; - Node::fromExpr((*(newC = &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_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) { - Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr? - d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); - } - } - out = &newD; - d_datatypeReverseCache[&newD] = &dt; - return newD; - } - } - } - - // this is identity; don't need the reverse cache - out = &dt; - return dt; - -}/* 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].getDatatype() : type.getDatatype(); - 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.isSort() && 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) { - if(vars.empty()) { - return; - } - const pair<TNode, bool> cacheKey(n, boolParent); - if(alreadySeen.find(cacheKey) != alreadySeen.end()) { - return; - } - alreadySeen.insert(cacheKey); - - if(n.isVar() && vars.find(n) != vars.end() && !boolParent) { - vars.erase(n); - output.insert(n); - if(vars.empty()) { - return; - } - } - for(size_t i = 0; i < n.getNumChildren(); ++i) { - collectVarsInTermContext(n[i], vars, output, isBoolean(n, i), alreadySeen); - if(vars.empty()) { - return; - } - } -} - -Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() { - - stack< triple<TNode, theory::TheoryId, bool> > worklist; - worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false)); - stack< NodeBuilder<> > result; - //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND". - //result.push(NodeBuilder<>(kind::TUPLE)); - result.push(NodeBuilder<>(kind::AND)); - - NodeManager* nm = NodeManager::currentNM(); - - while(!worklist.empty()) { - top = worklist.top().first; - parentTheory = worklist.top().second; - bool& childrenPushed = worklist.top().third; - - 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; - } - } - - if(!childrenPushed) { - Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; - - 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<Node, theory::TheoryId>(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 - if(parentTheory == theory::THEORY_BOOL) { - result.top() << quantBoolVars[top].eqNode(d_tt); - } else { - result.top() << quantBoolVars[top]; - } - worklist.pop(); - goto next_worklist; - } - - if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) { - // 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; - } - - 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; - } - } - 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(); ++i) { - TypeNode newType = convertType(t[i], false); - // is this the return type? (allowed to be Bool) - bool returnType = (i == t.getNumChildren() - 1); - if(newType != t[i] && (!t[i].isBoolean() || !returnType)) { - vector<TypeNode> argTypes = t.getArgTypes(); - for(unsigned j = 0; j < argTypes.size(); ++j) { - argTypes[j] = convertType(argTypes[j], false); - } - TypeNode rangeType = t.getRangeType(); - if(!rangeType.isBoolean()) { - rangeType = convertType(rangeType, false); - } - TypeNode newType = nm->mkFunctionType(argTypes, rangeType); - 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] != argTypes[j]) { - std::map< TypeNode, bool > processing; - bodyBuilder << rewriteAs(var, argTypes[j], processing); - } else { - bodyBuilder << var; - } - } - Node boundVars = boundVarsBuilder; - Node body = bodyBuilder; - if(t.getRangeType() != rangeType) { - std::map< TypeNode, bool > processing; - Node convbody = rewriteAs(body, t.getRangeType(), processing); - body = convbody; - } - Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); - Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); - d_varCache[top] = 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()), (*TypeEnumerator(n_ff.getType())).toExpr())); - Node repl = nm->mkNode(kind::STORE, - nm->mkNode(kind::STORE, base, nm->mkConst(true), - n_tt), - nm->mkConst(false), n_ff); - Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else 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; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else 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_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - d_varCache[top] = 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_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", - 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_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else { - d_varCache[top] = 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].getDatatype() : - t[t.getNumChildren() - 1][0].getDatatype(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype(); - if(dt != dt2) { - Assert(d_varCache.find(top) != d_varCache.end(), - "constructor `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top].get(); - worklist.pop(); - goto next_worklist; - } - d_varCache[top] = 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].getDatatype() : - t[0][0].getDatatype(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype(); - if(dt != dt2) { - Assert(d_varCache.find(top) != d_varCache.end(), - "tester or selector `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top].get(); - worklist.pop(); - goto next_worklist; - } else { - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; - } - } else if(!t.isSort() && t.getNumChildren() > 0) { - if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){ - 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_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - } - } - } - result.top() << top; - worklist.pop(); - goto next_worklist; - } - switch(k) { - //case kind::INST_ATTRIBUTE: - 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: - case kind::SEP_STAR: - case kind::SEP_WAND: - // 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; - set<TNode> output; - for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { - if((*i).getType().isBoolean()) { - ourVars.insert(*i); - } else if(convertType((*i).getType(), false) != (*i).getType()) { - output.insert(*i); - } - } - if(ourVars.empty() && output.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 { - 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(), convertType((*i).getType(), false)); - 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; - if( top.getNumChildren()==3 ){ - Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars); - quant = nm->mkNode(top.getKind(), boundVarList, body, ipl ); - }else{ - 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; - } - } - /* intentional fall-through for some cases above */ - } - - default: - result.push(NodeBuilder<>(k)); - Debug("bt") << "looking at: " << top << endl; - // rewrite the operator, as necessary - if(mk == kind::metakind::PARAMETERIZED) { - 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_UPDATE && - k != kind::RECORD_UPDATE && - k != kind::DIVISIBLE && - // Theory parametric functions go here - k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT && - k != kind::FLOATINGPOINT_TO_FP_REAL && - k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_UBV && - k != kind::FLOATINGPOINT_TO_SBV && - k != kind::FLOATINGPOINT_TO_REAL - ) { - 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], top.getKind() == kind::CHAIN ? parentTheory : ((isBoolean(top, i) || top.getKind()==kind::INST_ATTRIBUTE) ? 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; - } - } else { - Node n = result.top(); - result.pop(); - Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << 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; - } - - 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 */ }/* CVC4 namespace */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index 0a63f7fd8..0fb82aafe 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -28,84 +28,5 @@ namespace CVC4 { namespace smt { -namespace attr { - struct BooleanTermAttrTag { }; -}/* CVC4::smt::attr namespace */ - -typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr; - -class BooleanTermConverter { - /** The type of the Boolean term conversion variable cache */ - typedef context::CDHashMap<Node, Node, NodeHashFunction> BooleanTermVarCache; - - /** The type of the Boolean term conversion cache */ - typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node, - PairHashFunction< Node, bool, - NodeHashFunction, std::hash<size_t> > > BooleanTermCache; - /** The type of the Boolean term conversion type cache */ - typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode, - PairHashFunction< TypeNode, bool, - TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache; - /** The type of the Boolean term conversion datatype cache */ - typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache; - - /** The SmtEngine to which we're associated */ - SmtEngine& d_smt; - - /** The conversion for "false." */ - Node d_ff; - /** The conversion for "true." */ - Node d_tt; - /** The conversion for "false" when in datatypes contexts. */ - Node d_ffDt; - /** The conversion for "true" when in datatypes contexts. */ - Node d_ttDt; - - /** The cache used during Boolean term variable conversion */ - BooleanTermVarCache d_varCache; - /** The cache used during Boolean term conversion */ - BooleanTermCache d_termCache; - /** The cache used during Boolean term type conversion */ - BooleanTermTypeCache d_typeCache; - /** The cache used during Boolean term datatype conversion */ - BooleanTermDatatypeCache d_datatypeCache; - /** A (reverse) cache for Boolean term datatype conversion */ - BooleanTermDatatypeCache d_datatypeReverseCache; - - Node rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw(); - - /** - * Scan a datatype for and convert as necessary. - */ - const Datatype& convertDatatype(const Datatype& dt) throw(); - - /** - * Convert a type. - */ - TypeNode convertType(TypeNode type, bool datatypesContext); - - Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw(); - -public: - - /** - * Construct a Boolean-term converter associated to the given - * SmtEngine. - */ - BooleanTermConverter(SmtEngine& smt); - - /** - * Rewrite Boolean terms under a node. The node itself is not converted - * if boolParent is true, but its Boolean subterms appearing in a - * non-Boolean context will be rewritten. - */ - Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() { - std::map<TNode, Node> quantBoolVars; - Assert(!(boolParent && dtParent)); - return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars); - } - -};/* class BooleanTermConverter */ - }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp index d31d54121..0202a5a2d 100644 --- a/src/smt/ite_removal.cpp +++ b/src/smt/ite_removal.cpp @@ -25,36 +25,36 @@ using namespace std; namespace CVC4 { -RemoveITE::RemoveITE(context::UserContext* u) +RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) : d_iteCache(u) { d_containsVisitor = new theory::ContainsTermITEVisitor(); } -RemoveITE::~RemoveITE(){ +RemoveTermFormulas::~RemoveTermFormulas(){ delete d_containsVisitor; } -void RemoveITE::garbageCollect(){ +void RemoveTermFormulas::garbageCollect(){ d_containsVisitor->garbageCollect(); } -theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { +theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { return d_containsVisitor; } -size_t RemoveITE::collectedCacheSizes() const{ +size_t RemoveTermFormulas::collectedCacheSizes() const{ return d_containsVisitor->cache_size() + d_iteCache.size(); } -void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) { size_t n = output.size(); for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { // Do this in two steps to avoid Node problems(?) // Appears related to bug 512, splitting this into two lines // fixes the bug on clang on Mac OS - Node itesRemoved = run(output[i], output, iteSkolemMap, false); + Node itesRemoved = run(output[i], output, iteSkolemMap, false, false); // In some calling contexts, not necessary to report dependence information. if (reportDeps && (options::unsatCores() || options::fewerPreprocessingHoles())) { @@ -69,22 +69,27 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool } } -bool RemoveITE::containsTermITE(TNode e) const { +bool RemoveTermFormulas::containsTermITE(TNode e) const { return d_containsVisitor->containsTermITE(e); } -Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, bool inQuant) { +Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) { // Current node - Debug("ite") << "removeITEs(" << node << ")" << endl; - - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ + Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; + + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } // The result may be cached already - std::pair<Node, bool> cacheKey(node, inQuant); + int cv = cacheVal( inQuant, inTerm ); + std::pair<Node, int> cacheKey(node, cv); NodeManager *nodeManager = NodeManager::currentNM(); ITECache::const_iterator i = d_iteCache.find(cacheKey); if(i != d_iteCache.end()) { @@ -93,14 +98,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, return cached.isNull() ? Node(node) : cached; } - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - // If an ITE replace it + // If an ITE, replace it + TypeNode nodeType = node.getType(); if(node.getKind() == kind::ITE) { - TypeNode nodeType = node.getType(); if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { Node skolem; // Make the skolem to represent the ITE @@ -116,7 +117,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, d_iteCache.insert(cacheKey, skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); iteSkolemMap[skolem] = output.size(); output.push_back(newAssertion); @@ -125,6 +126,40 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, return skolem; } } + //if a non-variable Boolean term, replace it + if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ + Node skolem; + // Make the skolem to represent the Boolean term + //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); + skolem = nodeManager->mkBooleanTermVariable(); + + // The new assertion + Node newAssertion = skolem.eqNode( node ); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && + node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ + // Remember if we're inside a term + Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; + inTerm = true; + } // If not an ITE, go deep vector<Node> newChildren; @@ -134,7 +169,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // Remove the ITEs from the children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap, inQuant); + Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } @@ -150,24 +185,32 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } } -Node RemoveITE::replace(TNode node, bool inQuant) const { - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ +Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } // Check the cache NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); + int cv = cacheVal( inQuant, inTerm ); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); if(i != d_iteCache.end()) { Node cached = (*i).second; return cached.isNull() ? Node(node) : cached; } - // Remember that we're inside a quantifier if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier inQuant = true; - } + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ + // Remember if we're inside a term + inTerm = true; + } vector<Node> newChildren; bool somethingChanged = false; @@ -176,7 +219,7 @@ Node RemoveITE::replace(TNode node, bool inQuant) const { } // Replace in children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant); + Node newChild = replace(*it, inQuant, inTerm); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h index c0a46c316..e629c93d7 100644 --- a/src/smt/ite_removal.h +++ b/src/smt/ite_removal.h @@ -35,15 +35,15 @@ namespace theory { typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; -class RemoveITE { - typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache; +class RemoveTermFormulas { + typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache; ITECache d_iteCache; - + static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } public: - RemoveITE(context::UserContext* u); - ~RemoveITE(); + RemoveTermFormulas(context::UserContext* u); + ~RemoveTermFormulas(); /** * Removes the ITE nodes by introducing skolem variables. All @@ -65,13 +65,13 @@ public: * ite created in conjunction with that skolem variable. */ Node run(TNode node, std::vector<Node>& additionalAssertions, - IteSkolemMap& iteSkolemMap, bool inQuant); + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm); /** * Substitute under node using pre-existing cache. Do not remove * any ITEs not seen during previous runs. */ - Node replace(TNode node, bool inQuant = false) const; + Node replace(TNode node, bool inQuant = false, bool inTerm = false) const; /** Returns true if e contains a term ite. */ bool containsTermITE(TNode e) const; @@ -82,7 +82,7 @@ public: /** Garbage collects non-context dependent data-structures. */ void garbageCollect(); - /** Return the RemoveITE's containsVisitor. */ + /** Return the RemoveTermFormulas's containsVisitor. */ theory::ContainsTermITEVisitor* getContainsVisitor(); private: diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 5988d81f9..0076b9de9 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -25,209 +25,6 @@ using namespace std; namespace CVC4 { namespace smt { -Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { - if(n.getType().isSubtypeOf(asType)) { - // good to go, we have the right type - return n; - } - if(n.getKind() == kind::LAMBDA) { - Assert(asType.isFunction()); - Node rhs = rewriteAs(n[1], asType[1]); - Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs); - Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl; - Debug("boolean-terms") << "need type " << asType << endl; - // Assert(out.getType() == asType); - return out; - } - if(!n.isConst()) { - // we don't handle non-const right now - return n; - } - if(asType.isBoolean()) { - if(n.getType().isBitVector(1u)) { - // type mismatch: should only happen for Boolean-term conversion under - // datatype constructor applications; rewrite from BV(1) back to Boolean - bool tf = (n.getConst<BitVector>().getValue() == 1); - return NodeManager::currentNM()->mkConst(tf); - } - if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) { - // type mismatch: should only happen for Boolean-term conversion under - // datatype constructor applications; rewrite from datatype back to Boolean - Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); - Assert(n.getNumChildren() == 0); - // we assume (by construction) false is first; see boolean_terms.cpp - bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1); - Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl; - return NodeManager::currentNM()->mkConst(tf); - } - } - if(n.getType().isBoolean()) { - bool tf = n.getConst<bool>(); - if(asType.isBitVector(1u)) { - return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u)); - } - if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) { - const Datatype& asDatatype = asType.getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor()); - } - } - Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; - if(n.getType().isArray()) { - Assert(asType.isArray()); - if(n.getKind() == kind::STORE) { - return NodeManager::currentNM()->mkNode(kind::STORE, - rewriteAs(n[0], asType), - rewriteAs(n[1], asType[0]), - rewriteAs(n[2], asType[1])); - } - Assert(n.getKind() == kind::STORE_ALL); - const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); - Node val = rewriteAs(asa.getExpr(), asType[1]); - return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr())); - } - if( n.getType().isSet() ){ - if( n.getKind()==kind::UNION ){ - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - children.push_back( rewriteAs( n[i], asType ) ); - } - return NodeManager::currentNM()->mkNode(kind::UNION,children); - } - } - if(n.getType().isParametricDatatype() && - n.getType().isInstantiatedDatatype() && - asType.isParametricDatatype() && - asType.isInstantiatedDatatype() && - n.getType()[0] == asType[0]) { - // Here, we're doing something like rewriting a (Pair BV1 BV1) as a - // (Pair Bool Bool). - const Datatype* dt2 = &asType[0].getDatatype(); - std::vector<TypeNode> fromParams, toParams; - for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { - fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); - toParams.push_back(asType[i + 1]); - } - Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr())); - size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr()); - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[ctor_ix].getConstructor(); - for(size_t j = 0; j < n.getNumChildren(); ++j) { - TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType()); - asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(n[j], asType); - } - Node out = appctorb; - return out; - } - if(asType.getNumChildren() != n.getNumChildren() || - n.getMetaKind() == kind::metakind::CONSTANT) { - return n; - } - NodeBuilder<> b(n.getKind()); - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - b << n.getOperator(); - } - TypeNode::iterator t = asType.begin(); - for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { - Assert(t != asType.end()); - b << rewriteAs(*i, *t); - } - Assert(t == asType.end()); - Debug("boolean-terms") << "+++ constructing " << b << endl; - Node out = b; - return out; -} - -void ModelPostprocessor::visit(TNode current, TNode parent) { - Debug("tuprec") << "visiting " << current << endl; - Assert(!alreadyVisited(current, TNode::null())); - bool rewriteChildren = false; - if(current.getKind() == kind::APPLY_CONSTRUCTOR && - ( current.getOperator().hasAttribute(BooleanTermAttr()) || - ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && - current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { - NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); - Node realOp; - if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) { - TNode oldAsc = current.getOperator().getOperator(); - Debug("boolean-terms") << "old asc: " << oldAsc << endl; - Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr()); - Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType())); - Debug("boolean-terms") << "new asc: " << newAsc << endl; - if(newCons.getType().getRangeType().isParametricDatatype()) { - vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes(); - vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes(); - Assert(oldParams.size() == newParams.size() && oldParams.size() > 0); - newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType())); - } - realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons); - } else { - realOp = current.getOperator().getAttribute(BooleanTermAttr()); - } - b << realOp; - Debug("boolean-terms") << "+ op " << b.getOperator() << endl; - TypeNode::iterator j = realOp.getType().begin(); - for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) { - Assert(j != realOp.getType().end()); - Assert(alreadyVisited(*i, TNode::null())); - TNode repl = d_nodes[*i]; - repl = repl.isNull() ? *i : repl; - Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl; - b << rewriteAs(repl, *j); - } - Node n = b; - Debug("boolean-terms") << "model-post: " << current << endl - << "- returning " << n << endl; - d_nodes[current] = n; - return; - //all kinds with children that can occur in nodes in a model go here - } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || - current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) { - rewriteChildren = true; - } - if( rewriteChildren ){ - // rewrite based on children - bool self = true; - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - if(!d_nodes[current[i]].isNull()) { - self = false; - break; - } - } - if(self) { - Debug("tuprec") << "returning self for kind " << current.getKind() << endl; - // rewrite to self - d_nodes[current] = Node::null(); - } else { - // rewrite based on children - NodeBuilder<> nb(current.getKind()); - if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { - TNode op = current.getOperator(); - Node realOp; - if(op.getAttribute(BooleanTermAttr(), realOp)) { - nb << realOp; - } else { - nb << op; - } - } - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - TNode rw = d_nodes[current[i]]; - if(rw.isNull()) { - rw = current[i]; - } - nb << rw; - } - d_nodes[current] = nb; - Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl; - } - } else { - Debug("tuprec") << "returning self for kind " << current.getKind() << endl; - // rewrite to self - d_nodes[current] = Node::null(); - } -}/* ModelPostprocessor::visit() */ } /* namespace smt */ } /* namespace CVC4 */ diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h index d9e749677..a354315ef 100644 --- a/src/smt/model_postprocessor.h +++ b/src/smt/model_postprocessor.h @@ -24,28 +24,6 @@ namespace CVC4 { namespace smt { -class ModelPostprocessor { - std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; - -public: - typedef Node return_type; - - Node rewriteAs(TNode n, TypeNode asType); - - bool alreadyVisited(TNode current, TNode parent) { - return d_nodes.find(current) != d_nodes.end(); - } - - void visit(TNode current, TNode parent); - - void start(TNode n) { } - - Node done(TNode n) { - Assert(alreadyVisited(n, TNode::null())); - TNode retval = d_nodes[n]; - return retval.isNull() ? n : retval; - } -};/* class ModelPostprocessor */ }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e647c45d1..cefef9345 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -185,8 +185,6 @@ public: struct SmtEngineStatistics { /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; - /** time spent in Boolean term rewriting */ - TimerStat d_rewriteBooleanTermsTime; /** time spent in non-clausal simplification */ TimerStat d_nonclausalSimplificationTime; /** time spent in miplib pass */ @@ -233,7 +231,6 @@ struct SmtEngineStatistics { SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), - d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), @@ -258,7 +255,6 @@ struct SmtEngineStatistics { { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime); smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); @@ -284,7 +280,6 @@ struct SmtEngineStatistics { ~SmtEngineStatistics() { smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime); smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); @@ -510,9 +505,6 @@ class SmtEnginePrivate : public NodeManagerListener { /** Size of assertions array when preprocessing starts */ unsigned d_realAssertionsEnd; - /** The converter for Boolean terms -> BITVECTOR(1). */ - BooleanTermConverter* d_booleanTermConverter; - /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; bool d_propagatorNeedsFinish; @@ -567,7 +559,7 @@ public: IteSkolemMap d_iteSkolemMap; /** Instance of the ITE remover */ - RemoveITE d_iteRemover; + RemoveTermFormulas d_iteRemover; private: @@ -676,7 +668,6 @@ public: d_listenerRegistrations(new ListenerRegistrationList()), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), - d_booleanTermConverter(NULL), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), d_assertions(), @@ -756,10 +747,6 @@ public: d_propagator.finish(); d_propagatorNeedsFinish = false; } - if(d_booleanTermConverter != NULL) { - delete d_booleanTermConverter; - d_booleanTermConverter = NULL; - } d_smt.d_nodeManager->unsubscribeEvents(this); } @@ -859,11 +846,6 @@ public: throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** - * Rewrite Boolean terms in a Node. - */ - Node rewriteBooleanTerms(TNode n); - - /** * Simplify node "in" by expanding definitions and applying any * substitutions learned from preprocessing. */ @@ -1447,6 +1429,15 @@ void SmtEngine::setDefaults() { d_logic = log; d_logic.lock(); } + if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) { + if(!d_logic.isTheoryEnabled(THEORY_UF)) { + LogicInfo log(d_logic.getUnlockedCopy()); + Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl; + log.enableTheory(THEORY_UF); + d_logic = log; + d_logic.lock(); + } + } // by default, symmetry breaker is on only for QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { @@ -2918,7 +2909,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for (; pos != newSubstitutions.end(); ++pos) { // Add back this substitution as an assertion TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second); - Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs); + Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs); substitutionsBuilder << n; Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; } @@ -3775,42 +3766,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, return false; } -Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); - - spendResource(options::preprocessStep()); - - if(d_booleanTermConverter == NULL) { - // This needs to be initialized _after_ the whole SMT framework is in place, subscribed - // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype - // definition, and not dump it properly. - d_booleanTermConverter = new BooleanTermConverter(d_smt); - } - Node retval = d_booleanTermConverter->rewriteBooleanTerms(n); - if(retval != n) { - switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { - case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - case booleans::BOOLEAN_TERM_CONVERT_NATIVE: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_BV); - d_smt.d_logic.lock(); - } - break; - case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_DATATYPES); - d_smt.d_logic.lock(); - } - break; - default: - Unhandled(mode); - } - } - return retval; -} - void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(options::preprocessStep()); @@ -3904,15 +3859,6 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-abstraction", d_assertions); } - dumpAssertions("pre-boolean-terms", d_assertions); - { - Chat() << "rewriting Boolean terms..." << endl; - for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { - d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i])); - } - } - dumpAssertions("post-boolean-terms", d_assertions); - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; dumpAssertions("pre-constrain-subtypes", d_assertions); @@ -4523,6 +4469,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec }/* SmtEngine::assertFormula() */ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { +/* ModelPostprocessor mpost; NodeVisitor<ModelPostprocessor> visitor; Node value = visitor.run(mpost, node); @@ -4534,6 +4481,8 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl; } return realValue; + */ + return node; } Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { @@ -4627,8 +4576,9 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // used by the Model classes. It's not clear to me exactly how these // two are different, but they need to be unified. This ugly hack here // is to fix bug 554 until we can revamp boolean-terms and models [MGD] + + //AJR : necessary? if(!n.getType().isFunction()) { - n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); } @@ -4732,7 +4682,6 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptExce // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(*i, cache); - n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; |