diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-10 09:11:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-10 09:11:02 -0600 |
commit | e9408ca21267616bb799ef5f7fda85a1fee9c07c (patch) | |
tree | c1abfe14a791ed162e91e31e595a19d818294079 /test/regress/regress1 | |
parent | 261886a6ddc7fb93afcb7492a7e22884d6f75c96 (diff) |
Simplify method for inferring proxy lemmas in strings (#5789)
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.
Diffstat (limited to 'test/regress/regress1')
3 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue5610-2-infer-proxy.smt2 b/test/regress/regress1/strings/issue5610-2-infer-proxy.smt2 new file mode 100644 index 000000000..810498e03 --- /dev/null +++ b/test/regress/regress1/strings/issue5610-2-infer-proxy.smt2 @@ -0,0 +1,11 @@ +; 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) diff --git a/test/regress/regress1/strings/issue5610-infer-proxy.smt2 b/test/regress/regress1/strings/issue5610-infer-proxy.smt2 new file mode 100644 index 000000000..5f4ca326f --- /dev/null +++ b/test/regress/regress1/strings/issue5610-infer-proxy.smt2 @@ -0,0 +1,10 @@ +; 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) diff --git a/test/regress/regress1/strings/issue5692-infer-proxy.smt2 b/test/regress/regress1/strings/issue5692-infer-proxy.smt2 new file mode 100644 index 000000000..54a77ec82 --- /dev/null +++ b/test/regress/regress1/strings/issue5692-infer-proxy.smt2 @@ -0,0 +1,10 @@ +; 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) |