Compute model values for nested sequences in order (#6631)

Fixes #6337 (the other benchmarks in this issue are either solved
correctly or time out after the changes in #6615) and fixes #5665.

While computing the model for a nested equivalence class containing
seq.unit, we were looking up the representative of the argument in
(seq.unit (seq.unit j)) and the representative was simpliy (seq.unit j). However, we had assigned (seq.unit 0) to (seq.unit j) earlier.
A second equivalence class of type (Seq (Seq Int)) and length 1 was
later assigned (seq.unit (seq.unit 0)) and we didn't detect that
(seq.unit (seq.unit j)) and (seq.unit (seq.unit 0)) have the same
value. This was incorrect because we do not allow assigning the same
value to different equivalence classes. In this case, it led to one of
the assertions being false.

This commit fixes the issues in two ways: it ensures that types are
processed in ascending order of nesting (e.g., (Seq Int) terms are
processed before (Seq (Seq Int)) terms) and it changes the procedure
to look up the representative in the model instead of the theory state
to take into account the model values assigned to the elements of
sequences.

cc @yoni206

3 files changed, 25 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7de2d9789..cff39938c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -997,6 +997,8 @@ set(regress_0_tests
   regress0/seq/issue5543-unit-cmv.smt2
   regress0/seq/issue5547-seq-len-unit.smt2
   regress0/seq/issue5547-small-seq-len-unit.smt2
+  regress0/seq/issue5665-invalid-model.smt2
+  regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
diff --git a/test/regress/regress0/seq/issue5665-invalid-model.smt2 b/test/regress/regress0/seq/issue5665-invalid-model.smt2
new file mode 100644
index 000000000..5a4b1186d
--- /dev/null
+++ b/test/regress/regress0/seq/issue5665-invalid-model.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_SLIA)
+(declare-fun a () (Seq (Seq Int)))
+(declare-fun b () (Seq (Seq Int)))
+(declare-fun c () (Seq (Seq Int)))
+(declare-fun d () (Seq Int))
+(declare-fun e () Int)
+(declare-fun f () Int)
+(assert (= (seq.extract d e 1) (seq.unit f)))
+(assert (distinct a b (seq.++ (seq.unit d) c)))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress0/seq/issue6337-seq.smt2 b/test/regress/regress0/seq/issue6337-seq.smt2
new file mode 100644
index 000000000..f6436f412
--- /dev/null
+++ b/test/regress/regress0/seq/issue6337-seq.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_SLIA)
+(declare-fun x () (Seq (Seq Int)))
+(declare-fun y () (Seq (Seq Int)))
+(declare-fun z () (Seq Int))
+(declare-fun w () (Seq Int))
+(declare-fun j () Int)
+(assert (= w (seq.unit j)))
+(assert (not (= x (seq.unit z))))
+(assert (not (= y (seq.unit w))))
+(assert (not (= x y)))
+(set-info :status sat)
+(check-sat)