From d16b689f85e4962dfc77e8e9a1b7de23ab11ac7d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Dec 2020 07:04:17 -0600 Subject: [PATCH] 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. --- src/theory/strings/term_registry.cpp | 2 +- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/seq/issue5547-seq-len-unit.smt2 | 8 ++++++++ .../regress0/seq/issue5547-small-seq-len-unit.smt2 | 7 +++++++ 4 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/seq/issue5547-seq-len-unit.smt2 create mode 100644 test/regress/regress0/seq/issue5547-small-seq-len-unit.smt2 diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 8274b7dc0..cce2b117f 100644 --- 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 e2851e37a..a5adf4d9c 100644 --- 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 index 000000000..40b43d318 --- /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 index 000000000..848975c96 --- /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) -- 2.30.2