From: Morgan Deters Date: Fri, 15 Mar 2013 17:30:05 +0000 (-0400) Subject: Boolean terms rewriting for quantified variables of type Bool, when quantifier body... X-Git-Tag: cvc5-1.0.0~7390 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5617905a03c6810978cc66a18a370f5a95b7c5b4;p=cvc5.git Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context --- diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 262244f42..35184e42e 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -22,8 +22,12 @@ #include "theory/theory_engine.h" #include "theory/model.h" #include "expr/kind.h" +#include "util/hash.h" +#include "util/bool.h" #include #include +#include +#include using namespace std; using namespace CVC4::theory; @@ -104,8 +108,34 @@ const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype return dt; }/* BooleanTermConverter::booleanTermsConvertDatatype() */ -Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw() { - Debug("boolean-terms") << "rewriteBooleanTerms: " << top << " - boolParent=" << boolParent << endl; +// look for vars from "vars" that occur in a term-context in n; transfer them to output. +static void collectVarsInTermContext(TNode n, std::set& vars, std::set& output, bool boolParent, std::hash_set< std::pair, PairHashFunction >& alreadySeen) { + if(vars.empty()) { + return; + } + const pair 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, bool boolParent, std::map& quantBoolVars) throw() { + Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - boolParent=" << boolParent << endl; BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair(top, boolParent)); if(i != d_booleanTermCache.end()) { @@ -117,11 +147,21 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw 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); + } else { + return quantBoolVars[top]; + } + } + if(!boolParent && top.getType().isBoolean()) { - Node one = nm->mkConst(BitVector(1u, 1u)); - Node zero = nm->mkConst(BitVector(1u, 0u)); // still need to rewrite e.g. function applications over boolean - Node topRewritten = rewriteBooleanTerms(top, true); + Node topRewritten = rewriteBooleanTermsRec(top, true, quantBoolVars); Node n = nm->mkNode(kind::ITE, topRewritten, one, zero); Debug("boolean-terms") << "constructed ITE: " << n << endl; return n; @@ -143,7 +183,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw } ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr()); Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + Debug("boolean-terms") << " returning new store_all: " << n << endl; return n; } if(indexType.isBoolean()) { @@ -151,7 +191,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw indexType = nm->mkBitVectorType(1); ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + Debug("boolean-terms") << " returning new store_all: " << n << endl; return n; } } @@ -176,8 +216,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw Node var = nm->mkBoundVar(t[j]); boundVarsBuilder << var; if(t[j].isBoolean()) { - bodyBuilder << nm->mkNode(kind::ITE, var, nm->mkConst(BitVector(1u, 1u)), - nm->mkConst(BitVector(1u, 0u))); + bodyBuilder << nm->mkNode(kind::ITE, var, one, zero); } else { bodyBuilder << var; } @@ -185,7 +224,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw Node boundVars = boundVarsBuilder; Node body = bodyBuilder; Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); - Debug("boolean-terms") << "substituting " << top << " ==> " << lam << std::endl; + Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); d_booleanTermCache[make_pair(top, boolParent)] = n; return n; @@ -210,8 +249,6 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw NodeManager::SKOLEM_EXACT_NAME); top.setAttribute(BooleanTermAttr(), n); Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - Node one = nm->mkConst(BitVector(1u, 1u)); - Node zero = nm->mkConst(BitVector(1u, 0u)); Node n_zero = nm->mkNode(kind::SELECT, n, zero); Node n_one = nm->mkNode(kind::SELECT, n, one); Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr())); @@ -308,9 +345,60 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw // not yet supported return top; + case kind::FORALL: + case kind::EXISTS: { + Debug("bt") << "looking at quantifier -> " << top << endl; + set 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 output; + hash_set< pair, PairHashFunction > 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::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 boundVars; + for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { + map::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], true, 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); + return quant; + } + } + /* intentional fall-through for some cases above */ + } + default: NodeBuilder<> b(k); - Debug("bt") << "looking at: " << top << std::endl; + Debug("bt") << "looking at: " << top << endl; if(mk == kind::metakind::PARAMETERIZED) { if(kindToTheoryId(k) != THEORY_BV && k != kind::APPLY_TYPE_ASCRIPTION && @@ -319,29 +407,29 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw k != kind::RECORD_SELECT && k != kind::RECORD_UPDATE && k != kind::RECORD) { - Debug("bt") << "rewriting: " << top.getOperator() << std::endl; - b << rewriteBooleanTerms(top.getOperator(), false); - Debug("bt") << "got: " << b.getOperator() << std::endl; + Debug("bt") << "rewriting: " << top.getOperator() << endl; + b << rewriteBooleanTermsRec(top.getOperator(), false, quantBoolVars); + Debug("bt") << "got: " << b.getOperator() << endl; } else { b << top.getOperator(); } } for(unsigned i = 0; i < top.getNumChildren(); ++i) { - Debug("bt") << "rewriting: " << top[i] << std::endl; - b << rewriteBooleanTerms(top[i], isBoolean(top, i)); - Debug("bt") << "got: " << b[b.getNumChildren() - 1] << std::endl; + Debug("bt") << "rewriting: " << top[i] << endl; + b << rewriteBooleanTermsRec(top[i], isBoolean(top, i), 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, nm->mkConst(BitVector(1u, 1u))); + n = nm->mkNode(kind::EQUAL, n, one); } d_booleanTermCache[make_pair(top, boolParent)] = n; return n; } -}/* BooleanTermConverter::rewriteBooleanTerms() */ +}/* BooleanTermConverter::rewriteBooleanTermsRec() */ }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index e51a7bbb0..c53eadfa0 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -24,6 +24,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "util/hash.h" +#include #include namespace CVC4 { @@ -52,6 +53,8 @@ class BooleanTermConverter { */ const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw(); + Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map& quantBoolVars) throw(); + public: BooleanTermConverter(SmtEngine& smt) : @@ -61,7 +64,10 @@ public: /** * We rewrite Boolean terms in assertions as bitvectors of length 1. */ - Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw(); + Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() { + std::map quantBoolVars; + return rewriteBooleanTermsRec(n, boolParent, quantBoolVars); + } };/* class BooleanTermConverter */