diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 12 | ||||
-rw-r--r-- | src/theory/strings/term_registry.cpp | 74 | ||||
-rw-r--r-- | src/theory/strings/term_registry.h | 38 |
3 files changed, 29 insertions, 95 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index cf90c8fbe..0c55d26e8 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -186,17 +186,14 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma) } if (options::stringInferSym()) { - std::vector<Node> vars; - std::vector<Node> subs; std::vector<Node> unproc; for (const Node& ac : ii.d_premises) { - d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc); + d_termReg.removeProxyEqs(ac, unproc); } if (unproc.empty()) { - Node eqs = ii.d_conc.substitute( - vars.begin(), vars.end(), subs.begin(), subs.end()); + Node eqs = ii.d_conc; InferInfo iiSubsLem; iiSubsLem.d_sim = this; // keep the same id for now, since we are transforming the form of the @@ -209,11 +206,6 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma) << "Strings::Infer " << iiSubsLem << std::endl; Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl; - for (unsigned i = 0, nvars = vars.size(); i < nvars; i++) - { - Trace("strings-lemma-debug") - << " " << vars[i] << " -> " << subs[i] << std::endl; - } } Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl; addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem))); diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index cce2b117f..160bc7d73 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -575,83 +575,39 @@ Node TermRegistry::ensureProxyVariableFor(Node n) return proxy; } -void TermRegistry::inferSubstitutionProxyVars(Node n, - std::vector<Node>& vars, - std::vector<Node>& subs, - std::vector<Node>& unproc) const +void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const { if (n.getKind() == AND) { for (const Node& nc : n) { - inferSubstitutionProxyVars(nc, vars, subs, unproc); + removeProxyEqs(nc, unproc); } return; } - if (n.getKind() == EQUAL) + Trace("strings-subs-proxy") << "Input : " << n << std::endl; + Node ns = Rewriter::rewrite(n); + if (ns.getKind() == EQUAL) { - Node ns = n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - ns = Rewriter::rewrite(ns); - if (ns.getKind() == EQUAL) + for (size_t i = 0; i < 2; i++) { - Node s; - Node v; - for (unsigned i = 0; i < 2; i++) + // determine whether this side has a proxy variable + if (ns[i].getAttribute(StringsProxyVarAttribute())) { - Node ss; - // determine whether this side has a proxy variable - if (ns[i].getAttribute(StringsProxyVarAttribute())) + if (getProxyVariableFor(ns[1 - i]) == ns[i]) { - // it is a proxy variable - ss = ns[i]; - } - else if (ns[i].isConst()) - { - ss = getProxyVariableFor(ns[i]); - } - if (!ss.isNull()) - { - v = ns[1 - i]; - // if the other side is a constant or variable - if (v.getNumChildren() == 0) - { - if (s.isNull()) - { - s = ss; - } - else - { - // both sides of the equality correspond to a proxy variable - if (ss == s) - { - // it is a trivial equality, e.g. between a proxy variable - // and its definition - return; - } - else - { - // equality between proxy variables, non-trivial - s = Node::null(); - } - } - } + Trace("strings-subs-proxy") + << "...trivial definition via " << ns[i] << std::endl; + // it is a trivial equality, e.g. between a proxy variable + // and its definition + return; } } - if (!s.isNull()) - { - // the equality can be turned into a substitution - subs.push_back(s); - vars.push_back(v); - return; - } - } - else - { - n = ns; } } if (!n.isConst() || !n.getConst<bool>()) { + Trace("strings-subs-proxy") << "...unprocessed" << std::endl; unproc.push_back(n); } } diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index a713cc60f..ddff32242 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -176,39 +176,25 @@ class TermRegistry */ Node ensureProxyVariableFor(Node n); - /** infer substitution proxy vars - * - * This method attempts to (partially) convert the formula n into a - * substitution of the form: - * v1 -> s1, ..., vn -> sn - * where s1 ... sn are proxy variables and v1 ... vn are either variables - * or constants. - * - * This method ensures that P ^ v1 = s1 ^ ... ^ vn = sn ^ unproc is equivalent - * to P ^ n, where P is the conjunction of equalities corresponding to the - * definition of all proxy variables introduced by the theory of strings. + /** + * This method attempts to (partially) remove trivial parts of an explanation + * n. It adds conjuncts of n that must be included in the explanation into + * unproc and drops the rest. * - * For example, say that v1 was introduced as a proxy variable for "ABC", and - * v2 was introduced as a proxy variable for "AA". + * For example, say that v1 was introduced as a proxy variable for "ABC". * - * Given the input n := v1 = "ABC" ^ v2 = x ^ x = "AA", this method sets: - * vars = { x }, - * subs = { v2 }, - * unproc = {}. + * Given the input n := v1 = "ABC" ^ x = "AA", this method sets: + * unproc = { x = "AA" }. * In particular, this says that the information content of n is essentially - * x = v2. The first and third conjunctions can be dropped from the - * explanation since these equalities simply correspond to definitions - * of proxy variables. + * x = "AA". The first conjunct can be dropped from the explanation since + * that equality simply corresponds to definition of a proxy variable. * * This method is used as a performance heuristic. It can infer when the - * explanation of a fact depends only trivially on equalities corresponding - * to definitions of proxy variables, which can be omitted since they are + * explanation of a fact depends only on equalities corresponding to + * definitions of proxy variables, which can be omitted since they are * assumed to hold globally. */ - void inferSubstitutionProxyVars(Node n, - std::vector<Node>& vars, - std::vector<Node>& subs, - std::vector<Node>& unproc) const; + void removeProxyEqs(Node n, std::vector<Node>& unproc) const; //---------------------------- end proxy variables private: /** Common constants */ |