summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/inference_manager.cpp12
-rw-r--r--src/theory/strings/term_registry.cpp74
-rw-r--r--src/theory/strings/term_registry.h38
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback