Fix SAT-context dependent issue in strings preregistration (#5564)

This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.

Fixes #5547.

This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.

It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.

I will do performance testing on this PR.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 8274b7dc0c086b291cd23e7f77b26fa734d5ce14..cce2b117fda82ebe976b9cb30aec145a2eddfcd6 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -46,7 +46,7 @@ TermRegistry::TermRegistry(SolverState& s,
       d_hasStrCode(false),
       d_functionsTerms(s.getSatContext()),
       d_inputVars(s.getUserContext()),
-      d_preregisteredTerms(s.getUserContext()),
+      d_preregisteredTerms(s.getSatContext()),
       d_registeredTerms(s.getUserContext()),
       d_registeredTypes(s.getUserContext()),
       d_lengthLemmaTermsCache(s.getUserContext()),

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e2851e37a7c1b0796f894b2eb490e193e2de4f6e..a5adf4d9cea4dffe29b5ea130c506af5c6131111 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -954,6 +954,8 @@ set(regress_0_tests
   regress0/seq/intseq.smt2
   regress0/seq/issue4370-bool-terms.smt2
   regress0/seq/issue5543-unit-cmv.smt2
+  regress0/seq/issue5547-seq-len-unit.smt2
+  regress0/seq/issue5547-small-seq-len-unit.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2

diff --git a/test/regress/regress0/seq/issue5547-seq-len-unit.smt2 b/test/regress/regress0/seq/issue5547-seq-len-unit.smt2
new file mode 100644 (file)
index 0000000..40b43d3
--- /dev/null
+++ b/test/regress/regress0/seq/issue5547-seq-len-unit.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun seq3 () (Seq Int))
+(declare-fun seq10 () (Seq Int))
+(declare-fun seq12 () (Seq Int))
+(assert (seq.suffixof (seq.++ (seq.unit (seq.len (seq.++ seq12 (seq.rev seq3)))) seq3) seq10))
+(check-sat)

diff --git a/test/regress/regress0/seq/issue5547-small-seq-len-unit.smt2 b/test/regress/regress0/seq/issue5547-small-seq-len-unit.smt2
new file mode 100644 (file)
index 0000000..848975c
--- /dev/null
+++ b/test/regress/regress0/seq/issue5547-small-seq-len-unit.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --simplification=none --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Seq Int))
+(declare-fun b () (Seq Int))
+(assert (= a (seq.++ b (seq.unit (+ (seq.len b) 1)))))
+(check-sat)