From 569ec5f0ae1ed35e13cc6f581a2d292f7492387e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 15 Feb 2020 16:38:23 -0600 Subject: [PATCH] Move proxy variables to InferenceManager in strings (#3758) --- src/theory/strings/inference_manager.cpp | 135 ++++++++++++++++++++++- src/theory/strings/inference_manager.h | 48 ++++++++ src/theory/strings/theory_strings.cpp | 116 +------------------ src/theory/strings/theory_strings.h | 34 ------ 4 files changed, 185 insertions(+), 148 deletions(-) diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 2b5338a6a..67ba2d5a3 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -34,8 +34,16 @@ InferenceManager::InferenceManager(TheoryStrings& p, context::Context* c, context::UserContext* u, SolverState& s, + SkolemCache& skc, OutputChannel& out) - : d_parent(p), d_state(s), d_out(out), d_keep(c), d_lengthLemmaTermsCache(u) + : d_parent(p), + d_state(s), + d_skCache(skc), + d_out(out), + d_keep(c), + d_proxyVar(u), + d_proxyVarToLength(u), + d_lengthLemmaTermsCache(u) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -284,6 +292,129 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol) d_pendingReqPhase[lit] = pol; } +Node InferenceManager::getProxyVariableFor(Node n) const +{ + NodeNodeMap::const_iterator it = d_proxyVar.find(n); + if (it != d_proxyVar.end()) + { + return (*it).second; + } + return Node::null(); +} + +Node InferenceManager::getSymbolicDefinition(Node n, + std::vector& exp) const +{ + if (n.getNumChildren() == 0) + { + Node pn = getProxyVariableFor(n); + if (pn.isNull()) + { + return Node::null(); + } + Node eq = n.eqNode(pn); + eq = Rewriter::rewrite(eq); + if (std::find(exp.begin(), exp.end(), eq) == exp.end()) + { + exp.push_back(eq); + } + return pn; + } + std::vector children; + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(n.getOperator()); + } + for (const Node& nc : n) + { + if (n.getType().isRegExp()) + { + children.push_back(nc); + } + else + { + Node ns = getSymbolicDefinition(nc, exp); + if (ns.isNull()) + { + return Node::null(); + } + else + { + children.push_back(ns); + } + } + } + return NodeManager::currentNM()->mkNode(n.getKind(), children); +} + +void InferenceManager::registerLength(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + // register length information: + // for variables, split on empty vs positive length + // for concat/const/replace, introduce proxy var and state length relation + Node lsum; + if (n.getKind() != STRING_CONCAT && n.getKind() != CONST_STRING) + { + Node lsumb = nm->mkNode(STRING_LENGTH, n); + lsum = Rewriter::rewrite(lsumb); + // can register length term if it does not rewrite + if (lsum == lsumb) + { + registerLength(n, LENGTH_SPLIT); + return; + } + } + Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym"); + StringsProxyVarAttribute spva; + sk.setAttribute(spva, true); + Node eq = Rewriter::rewrite(sk.eqNode(n)); + Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl; + d_proxyVar[n] = sk; + // If we are introducing a proxy for a constant or concat term, we do not + // need to send lemmas about its length, since its length is already + // implied. + if (n.isConst() || n.getKind() == STRING_CONCAT) + { + // do not send length lemma for sk. + registerLength(sk, LENGTH_IGNORE); + } + Trace("strings-assert") << "(assert " << eq << ")" << std::endl; + d_out.lemma(eq); + Node skl = nm->mkNode(STRING_LENGTH, sk); + if (n.getKind() == STRING_CONCAT) + { + std::vector nodeVec; + for (const Node& nc : n) + { + if (nc.getAttribute(StringsProxyVarAttribute())) + { + Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end()); + nodeVec.push_back(d_proxyVarToLength[nc]); + } + else + { + Node lni = nm->mkNode(STRING_LENGTH, nc); + nodeVec.push_back(lni); + } + } + lsum = nm->mkNode(PLUS, nodeVec); + lsum = Rewriter::rewrite(lsum); + } + else if (n.getKind() == CONST_STRING) + { + lsum = nm->mkConst(Rational(n.getConst().size())); + } + Assert(!lsum.isNull()); + d_proxyVarToLength[sk] = lsum; + Node ceq = Rewriter::rewrite(skl.eqNode(lsum)); + Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; + Trace("strings-lemma-debug") + << " prerewrite : " << skl.eqNode(lsum) << std::endl; + Trace("strings-assert") << "(assert " << ceq << ")" << std::endl; + d_out.lemma(ceq); +} + void InferenceManager::registerLength(Node n, LengthStatus s) { if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end()) @@ -480,7 +611,7 @@ void InferenceManager::inferSubstitutionProxyVars( } else if (ns[i].isConst()) { - ss = d_parent.getProxyVariableFor(ns[i]); + ss = getProxyVariableFor(ns[i]); } if (!ss.isNull()) { diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 819e4b98f..50cfdb6fb 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" +#include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" #include "theory/uf/equality_engine.h" @@ -67,12 +68,14 @@ class TheoryStrings; class InferenceManager { typedef context::CDHashSet NodeSet; + typedef context::CDHashMap NodeNodeMap; public: InferenceManager(TheoryStrings& p, context::Context* c, context::UserContext* u, SolverState& s, + SkolemCache& skc, OutputChannel& out); ~InferenceManager() {} @@ -164,6 +167,32 @@ class InferenceManager * decided with polarity pol. */ void sendPhaseRequirement(Node lit, bool pol); + + //---------------------------- proxy variables and length elaboration + /** Get symbolic definition + * + * This method returns the "symbolic definition" of n, call it n', and + * populates the vector exp with an explanation such that exp => n = n'. + * + * The symbolic definition of n is the term where (maximal) subterms of n + * are replaced by their proxy variables. For example, if we introduced + * proxy variable v for x ++ y, then given input x ++ y = w, this method + * returns v = w and adds v = x ++ y to exp. + */ + Node getSymbolicDefinition(Node n, std::vector& exp) const; + /** Get proxy variable + * + * If this method returns the proxy variable for (string) term n if one + * exists, otherwise it returns null. + */ + Node getProxyVariableFor(Node n) const; + /** register length + * + * This method is called on non-constant string terms n. It sends a lemma + * on the output channel that ensures that the length n satisfies its assigned + * status (given by argument s). + */ + void registerLength(Node n); /** register length * * This method is called on non-constant string terms n. It sends a lemma @@ -186,6 +215,7 @@ class InferenceManager * channel instead of adding them to pending lists. */ void registerLength(Node n, LengthStatus s); + //---------------------------- end proxy variables and length elaboration //----------------------------constructing antecedants /** @@ -290,6 +320,8 @@ class InferenceManager * This is a reference to the solver state of the theory of strings. */ SolverState& d_state; + /** cache of all skolems */ + SkolemCache& d_skCache; /** the output channel * * This is a reference to the output channel of the theory of strings. @@ -316,6 +348,22 @@ class InferenceManager * SAT-context-dependent. */ NodeSet d_keep; + /** + * Map string terms to their "proxy variables". Proxy variables are used are + * intermediate variables so that length information can be communicated for + * constants. For example, to communicate that "ABC" has length 3, we + * introduce a proxy variable v_{"ABC"} for "ABC", and assert: + * v_{"ABC"} = "ABC" ^ len( v_{"ABC"} ) = 3 + * Notice this is required since we cannot directly write len( "ABC" ) = 3, + * which rewrites to 3 = 3. + * In the above example, we store "ABC" -> v_{"ABC"} in this map. + */ + NodeNodeMap d_proxyVar; + /** + * Map from proxy variables to their normalized length. In the above example, + * we store "ABC" -> 3. + */ + NodeNodeMap d_proxyVarToLength; /** List of terms that we have register length for */ NodeSet d_lengthLemmaTermsCache; /** infer substitution proxy vars diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 197f7ac4c..23a41a0bb 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -71,13 +71,11 @@ TheoryStrings::TheoryStrings(context::Context* c, d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_state(c, d_equalityEngine, d_valuation), - d_im(*this, c, u, d_state, out), + d_im(*this, c, u, d_state, d_sk_cache, out), d_pregistered_terms_cache(u), d_registered_terms_cache(u), d_preproc(&d_sk_cache, u), d_extf_infer_cache(c), - d_proxy_var(u), - d_proxy_var_to_length(u), d_functionsTerms(c), d_has_extf(c, false), d_has_str_code(false), @@ -1231,7 +1229,7 @@ void TheoryStrings::checkExtfEval( int effort ) { // only use symbolic definitions if option is set if (options::stringInferSym()) { - nrs = getSymbolicDefinition(sn, exps); + nrs = d_im.getSymbolicDefinition(sn, exps); } if( !nrs.isNull() ){ Trace("strings-extf-debug") << " rewrite " << nrs << "..." << std::endl; @@ -1531,51 +1529,6 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } } -Node TheoryStrings::getProxyVariableFor(Node n) const -{ - NodeNodeMap::const_iterator it = d_proxy_var.find(n); - if (it != d_proxy_var.end()) - { - return (*it).second; - } - return Node::null(); -} -Node TheoryStrings::getSymbolicDefinition(Node n, std::vector& exp) const -{ - if( n.getNumChildren()==0 ){ - Node pn = getProxyVariableFor(n); - if (pn.isNull()) - { - return Node::null(); - } - Node eq = n.eqNode(pn); - eq = Rewriter::rewrite(eq); - if (std::find(exp.begin(), exp.end(), eq) == exp.end()) - { - exp.push_back(eq); - } - return pn; - }else{ - std::vector< Node > children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back( n.getOperator() ); - } - for( unsigned i=0; imkNode( n.getKind(), children ); - } -} - void TheoryStrings::checkRegisterTermsPreNormalForm() { const std::vector& seqc = d_bsolver.getStringEqc(); @@ -1619,7 +1572,7 @@ void TheoryStrings::checkCodes() Node cc = nm->mkNode(kind::STRING_CODE, c); cc = Rewriter::rewrite(cc); Assert(cc.isConst()); - Node cp = getProxyVariableFor(c); + Node cp = d_im.getProxyVariableFor(c); AlwaysAssert(!cp.isNull()); Node vc = nm->mkNode(STRING_CODE, cp); if (!d_state.areEqual(cc, vc)) @@ -1701,68 +1654,7 @@ void TheoryStrings::registerTerm(Node n, int effort) // register length information: // for variables, split on empty vs positive length // for concat/const/replace, introduce proxy var and state length relation - Node lsum; - if (n.getKind() != STRING_CONCAT && n.getKind() != CONST_STRING) - { - Node lsumb = nm->mkNode(STRING_LENGTH, n); - lsum = Rewriter::rewrite(lsumb); - // can register length term if it does not rewrite - if (lsum == lsumb) - { - d_im.registerLength(n, LENGTH_SPLIT); - return; - } - } - Node sk = d_sk_cache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym"); - StringsProxyVarAttribute spva; - sk.setAttribute(spva, true); - Node eq = Rewriter::rewrite(sk.eqNode(n)); - Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq - << std::endl; - d_proxy_var[n] = sk; - // If we are introducing a proxy for a constant or concat term, we do not - // need to send lemmas about its length, since its length is already - // implied. - if (n.isConst() || n.getKind() == STRING_CONCAT) - { - // do not send length lemma for sk. - d_im.registerLength(sk, LENGTH_IGNORE); - } - Trace("strings-assert") << "(assert " << eq << ")" << std::endl; - d_out->lemma(eq); - Node skl = nm->mkNode(STRING_LENGTH, sk); - if (n.getKind() == STRING_CONCAT) - { - std::vector node_vec; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - if (n[i].getAttribute(StringsProxyVarAttribute())) - { - Assert(d_proxy_var_to_length.find(n[i]) - != d_proxy_var_to_length.end()); - node_vec.push_back(d_proxy_var_to_length[n[i]]); - } - else - { - Node lni = nm->mkNode(STRING_LENGTH, n[i]); - node_vec.push_back(lni); - } - } - lsum = nm->mkNode(PLUS, node_vec); - lsum = Rewriter::rewrite(lsum); - } - else if (n.getKind() == CONST_STRING) - { - lsum = nm->mkConst(Rational(n.getConst().size())); - } - Assert(!lsum.isNull()); - d_proxy_var_to_length[sk] = lsum; - Node ceq = Rewriter::rewrite(skl.eqNode(lsum)); - Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; - Trace("strings-lemma-debug") - << " prerewrite : " << skl.eqNode(lsum) << std::endl; - Trace("strings-assert") << "(assert " << ceq << ")" << std::endl; - d_out->lemma(ceq); + d_im.registerLength(n); } else if (n.getKind() == STRING_CODE) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 960d3ceaa..67b7482ca 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -274,22 +274,6 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b) override; private: - /** - * Map string terms to their "proxy variables". Proxy variables are used are - * intermediate variables so that length information can be communicated for - * constants. For example, to communicate that "ABC" has length 3, we - * introduce a proxy variable v_{"ABC"} for "ABC", and assert: - * v_{"ABC"} = "ABC" ^ len( v_{"ABC"} ) = 3 - * Notice this is required since we cannot directly write len( "ABC" ) = 3, - * which rewrites to 3 = 3. - * In the above example, we store "ABC" -> v_{"ABC"} in this map. - */ - NodeNodeMap d_proxy_var; - /** - * Map from proxy variables to their normalized length. In the above example, - * we store "ABC" -> 3. - */ - NodeNodeMap d_proxy_var_to_length; /** All the function terms that the theory has seen */ context::CDList d_functionsTerms; private: @@ -309,24 +293,6 @@ private: /** cache of all skolems */ SkolemCache d_sk_cache; - /** Get proxy variable - * - * If this method returns the proxy variable for (string) term n if one - * exists, otherwise it returns null. - */ - Node getProxyVariableFor(Node n) const; - /** Get symbolic definition - * - * This method returns the "symbolic definition" of n, call it n', and - * populates the vector exp with an explanation such that exp => n = n'. - * - * The symbolic definition of n is the term where (maximal) subterms of n - * are replaced by their proxy variables. For example, if we introduced - * proxy variable v for x ++ y, then given input x ++ y = w, this method - * returns v = w and adds v = x ++ y to exp. - */ - Node getSymbolicDefinition(Node n, std::vector& exp) const; - //--------------------------for checkExtfEval /** * Non-static information about an extended function t. This information is -- 2.30.2