This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.
Current results on the eager solver on SMT-LIB shows this change has very little performance impact.
Fixes #5692, fixes #5610.
}
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
<< "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)));
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);
}
}
*/
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 */
regress1/strings/issue5483-pp-leq.smt2
regress1/strings/issue5510-re-consume.smt2
regress1/strings/issue5520-re-consume.smt2
+ regress1/strings/issue5610-infer-proxy.smt2
+ regress1/strings/issue5610-2-infer-proxy.smt2
regress1/strings/issue5611-deq-norm-emp.smt2
+ regress1/strings/issue5692-infer-proxy.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun r () String)
+(declare-fun tr () String)
+(declare-fun t () String)
+(assert (not (= tr r)))
+(assert (= (str.prefixof "b" (str.++ r (str.++ (str.from_int (str.len (str.++
+ tr t))) "b"))) (= tr (str.++ (str.from_int (str.len (str.++ tr t))) (str.++
+ t "b")))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun str5 () String)
+(declare-fun str6 () String)
+(declare-fun str10 () String)
+(declare-fun str11 () String)
+(assert (not (= str6 str5)))
+(assert (xor true true true (distinct "" str6 (str.++ (str.from_int (str.len (str.++ str10 str11))) (str.++ str11 "tCEuUoROixKOUo" "wuPPPbRfGeDdhIafLoGcubFWViLfPaiooaekchLBSfgSaprsJijOvY"))) (str.prefixof (str.++ "tCEuUoROixKOUo" "wuPPPbRfGeDdhIafLoGcubFWViLfPaiooaekchLBSfgSaprsJijOvY") (str.++ str5 (str.++ (str.from_int (str.len (str.++ str10 str11))) (str.++ "tCEuUoROixKOUo" "wuPPPbRfGeDdhIafLoGcubFWViLfPaiooaekchLBSfgSaprsJijOvY"))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun str0 () String)
+(declare-fun str3 () String)
+(declare-fun str8 () String)
+(assert (str.< str8 str3))
+(assert (str.prefixof (str.++ str8 (str.++ str0 (str.++ "K" str8))) (str.++ (str.++ str0 str8) (str.++ str0 str3 "Q"))))
+(check-sat)
projects / cvc5.git / commitdiff