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.

4 files changed, 34 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1e4f42ffd..d942ef940 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2022,7 +2022,10 @@ set(regress_1_tests
   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
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)