Add regressions for array sequence solver (#7874)

This closes the seqArray branch.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 66098220e1eeaa72d807d624dd0a5f1f4af7bac1..4d9d88c6bc2a880cb3052cbe455bef5ace415c93 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1097,8 +1097,8 @@ set(regress_0_tests
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2
-  regress0/seq/intseq_dt.smt2
   regress0/seq/intseq.smt2
+  regress0/seq/intseq_dt.smt2
   regress0/seq/issue4370-bool-terms.smt2
   regress0/seq/issue5543-unit-cmv.smt2
   regress0/seq/issue5547-seq-len-unit.smt2
@@ -1107,6 +1107,18 @@ set(regress_0_tests
   regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/proj-issue340.smt2
+  regress0/seq/quant_len_trigger.smt2
+  regress0/seq/rev.smt2
+  regress0/seq/seqa-model-unsound-dd.smt2
+  regress0/seq/array/array1.smt2
+  regress0/seq/array/array2.smt2
+  regress0/seq/array/array3.smt2
+  regress0/seq/array/array4.smt2
+  regress0/seq/array/distinct-update.smt2
+  regress0/seq/array/model-dd-1220.smt2
+  regress0/seq/array/nth-concat.smt2
+  regress0/seq/array/update-fallback.smt2
+  regress0/seq/array/update-word-eq.smt2
   regress0/seq/seq-2var.smt2
   regress0/seq/seq-ex1.smt2
   regress0/seq/seq-ex2.smt2
@@ -1122,7 +1134,7 @@ set(regress_0_tests
   regress0/seq/seq-nth.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/seq/seq-types.smt2
-  regress0/seq/quant_len_trigger.smt2
+  regress0/seq/update-eq-unsat.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
   regress0/sets/abt-te-exh2.smt2
@@ -2098,6 +2110,7 @@ set(regress_1_tests
   regress1/quantifiers/seu169+1.smt2
   regress1/quantifiers/seq-solved-enum.smt2
   regress1/quantifiers/seq-unsolved-ematch.smt2
+  regress1/quantifiers/seqa-unsat-unknown-110921.smt2
   regress1/quantifiers/small-pipeline-fixpoint-3.smt2
   regress1/quantifiers/smtcomp-qbv-053118.smt2
   regress1/quantifiers/smtlib384a03.smt2
@@ -2410,6 +2423,7 @@ set(regress_1_tests
   regress1/strings/rew-check1.smt2
   regress1/strings/seq-cardinality.smt2
   regress1/strings/seq-quant-infinite-branch.smt2
+  regress1/strings/seq-skeleton-gap.smt2
   regress1/strings/simple-re-consume.smt2
   regress1/strings/stoi-400million.smt2
   regress1/strings/stoi-solve.smt2

diff --git a/test/regress/regress0/seq/array/array1.smt2 b/test/regress/regress0/seq/array/array1.smt2
new file mode 100644 (file)
index 0000000..c447649
--- /dev/null
+++ b/test/regress/regress0/seq/array/array1.smt2
@@ -0,0 +1,25 @@
+; COMMAND-LINE: --incremental --strings-exp --seq-array=eager
+; EXPECT: unsat
+
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () (Seq Int))
+(declare-fun i () Int)
+(declare-fun e () Int)
+
+(assert (>= i 0))
+(assert (< i (seq.len x)))
+
+(assert (= 1 (seq.len x)))
+(assert (= 1 (seq.len y)))
+
+(assert (= e (seq.nth x i)))
+(assert (= e (seq.nth y i)))
+
+(assert (not (= x y)))
+
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/seq/array/array2.smt2 b/test/regress/regress0/seq/array/array2.smt2
new file mode 100644 (file)
index 0000000..51b98a6
--- /dev/null
+++ b/test/regress/regress0/seq/array/array2.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --incremental --strings-exp --seq-array=eager
+; EXPECT: unsat
+
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-fun a () (Seq Int))
+(declare-fun v () (Seq Int))
+
+(declare-fun i () Int)
+
+(declare-fun e () Int)
+(declare-fun e2 () Int)
+
+(assert (> i 0))
+(assert (< i (seq.len a)))
+
+(assert (= v (seq.update a 0 (seq.unit (seq.nth a 0)))))
+(assert (= e (seq.nth v i)))
+(assert (= e2 (seq.nth a i)))
+(assert (not (= e e2)))
+
+(check-sat)

diff --git a/test/regress/regress0/seq/array/array3.smt2 b/test/regress/regress0/seq/array/array3.smt2
new file mode 100644 (file)
index 0000000..97a16a6
--- /dev/null
+++ b/test/regress/regress0/seq/array/array3.smt2
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --incremental --strings-exp --seq-array=lazy
+; EXPECT: sat
+
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun a () (Seq Int))
+(declare-fun v () (Seq Int))
+
+(declare-fun i () Int)
+
+(declare-fun e () Int)
+(declare-fun e2 () Int)
+
+(assert (> i 0))
+(assert (< i (seq.len a)))
+
+(assert (= v (seq.update a 0 (seq.unit 1))))
+(assert (not (= v a)))
+
+(check-sat)

diff --git a/test/regress/regress0/seq/array/array4.smt2 b/test/regress/regress0/seq/array/array4.smt2
new file mode 100644 (file)
index 0000000..9a94fc1
--- /dev/null
+++ b/test/regress/regress0/seq/array/array4.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --incremental --strings-exp --seq-array=eager
+; EXPECT: unsat
+
+(set-info :smt-lib-version 2.6)
+(set-logic ALL)
+(set-info :status unsat)
+
+(declare-sort Element 0)
+(declare-fun a1 () (Seq Element))
+(declare-fun a2 () (Seq Element))
+(declare-fun i1 () Int)
+(declare-fun i2 () Int)
+(assert (let ((?v_0 (seq.update a2 i1 (seq.unit (seq.nth a1 i1))))
+              (?v_1 (seq.update a1 i1 (seq.unit (seq.nth a2 i1)))))
+             (= (seq.update ?v_1 i2 (seq.unit (seq.nth ?v_0 i2))) 
+                (seq.update ?v_0 i2 (seq.unit (seq.nth ?v_1 i2))))))
+(assert (not (= a1 a2)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress0/seq/array/distinct-update.smt2 b/test/regress/regress0/seq/array/distinct-update.smt2
new file mode 100644 (file)
index 0000000..3abd4de
--- /dev/null
+++ b/test/regress/regress0/seq/array/distinct-update.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --strings-exp --seq-array=eager
+(set-logic QF_SLIA)
+(set-info :status unsat)
+
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () (Seq Int))
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (= y (seq.update x 0 (seq.unit a))))
+
+(assert (= z (seq.update x 0 (seq.unit b))))
+
+(assert (not (= a b)))
+(assert (= y z))
+(assert (> (str.len y) 0))
+
+(check-sat)

diff --git a/test/regress/regress0/seq/array/model-dd-1220.smt2 b/test/regress/regress0/seq/array/model-dd-1220.smt2
new file mode 100644 (file)
index 0000000..411f013
--- /dev/null
+++ b/test/regress/regress0/seq/array/model-dd-1220.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --seq-array=lazy --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun v () (Seq Int))
+(assert (= 1 (seq.len v)))
+(assert (= v (seq.update v 0 (seq.unit 1))))
+(check-sat)

diff --git a/test/regress/regress0/seq/array/nth-concat.smt2 b/test/regress/regress0/seq/array/nth-concat.smt2
new file mode 100644 (file)
index 0000000..039ee44
--- /dev/null
+++ b/test/regress/regress0/seq/array/nth-concat.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --incremental --strings-exp --seq-array=eager
+; EXPECT: unsat
+
+(set-logic QF_SLIA)
+(set-info :status unsat)
+
+(declare-fun A () (Seq Int))
+(declare-fun S1 () (Seq Int))
+(declare-fun i () Int)
+
+(assert (<= 0 i))
+(assert (< i (- (seq.len A) 1)))
+(assert (= S1 (seq.extract A i 1)))
+(assert (distinct (seq.nth S1 0) (seq.nth A i)))
+(check-sat)

diff --git a/test/regress/regress0/seq/array/update-fallback.smt2 b/test/regress/regress0/seq/array/update-fallback.smt2
new file mode 100644 (file)
index 0000000..6715f69
--- /dev/null
+++ b/test/regress/regress0/seq/array/update-fallback.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --strings-exp --seq-array=lazy
+; EXPECT: unsat
+
+(set-logic QF_SLIA)
+
+(declare-fun A () (Seq Int))
+(declare-fun i () Int)
+(declare-fun S () (Seq Int))
+(declare-fun B () (Seq Int))
+
+(assert (<= 0 i))
+(assert (< i (- (seq.len A) 1)))
+(assert (= S (seq.extract A i 1)))
+(assert (= (seq.nth A i) (seq.nth A (+ i 1))))
+
+(assert (= B (seq.update A (+ i 1) S)))
+(assert (distinct (seq.nth B (+ i 1)) (seq.nth S 0)))
+(check-sat)

diff --git a/test/regress/regress0/seq/array/update-word-eq.smt2 b/test/regress/regress0/seq/array/update-word-eq.smt2
new file mode 100644 (file)
index 0000000..f81077c
--- /dev/null
+++ b/test/regress/regress0/seq/array/update-word-eq.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --strings-exp --seq-array=eager
+(set-logic QF_SLIA)
+(set-info :status unsat)
+
+(declare-fun x () (Seq Int))
+(declare-fun y () (Seq Int))
+(declare-fun z () (Seq Int))
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun i () Int)
+
+(assert (= (seq.++ (seq.unit a) z) (seq.update x 0 (seq.unit b))))
+(assert (not (= a b)))
+
+(check-sat)

diff --git a/test/regress/regress0/seq/rev.smt2 b/test/regress/regress0/seq/rev.smt2
new file mode 100644 (file)
index 0000000..071122e
--- /dev/null
+++ b/test/regress/regress0/seq/rev.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --seq-array=eager --no-check-unsat-cores
+(set-logic QF_SLIA)
+(set-info :status unsat)
+
+(declare-fun A () (Seq Int))
+(declare-fun B () (Seq Int))
+(declare-const x Int)
+
+(assert (= B (seq.rev A)))
+(assert (and (<= 0 x) (< x (seq.len A))))
+(assert (not (= (seq.nth A x) (seq.nth B (- (- (seq.len A) 1) x)))))
+
+(check-sat)

diff --git a/test/regress/regress0/seq/seqa-model-unsound-dd.smt2 b/test/regress/regress0/seq/seqa-model-unsound-dd.smt2
new file mode 100644 (file)
index 0000000..0caf470
--- /dev/null
+++ b/test/regress/regress0/seq/seqa-model-unsound-dd.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp --seq-array=eager
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort T 0)
+(declare-fun t () T)
+(declare-fun s (T) (Seq (Seq Int)))
+(declare-fun u () (Seq Int))
+(assert (= (seq.unit u) (s t)))
+(assert (distinct u (seq.nth (s t) (- 1 (seq.len (s t))))))
+(check-sat)

diff --git a/test/regress/regress0/seq/update-eq-unsat.smt2 b/test/regress/regress0/seq/update-eq-unsat.smt2
new file mode 100644 (file)
index 0000000..554041a
--- /dev/null
+++ b/test/regress/regress0/seq/update-eq-unsat.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --seq-array=eager
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () (Seq Int))
+
+(assert (= (str.len x) 1))
+(assert (= (seq.update x 0 (seq.unit 1)) (seq.update x 0 (seq.unit 2))))
+
+(check-sat)

diff --git a/test/regress/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 b/test/regress/regress1/quantifiers/seqa-unsat-unknown-110921.smt2
new file mode 100644 (file)
index 0000000..97af47a
--- /dev/null
+++ b/test/regress/regress1/quantifiers/seqa-unsat-unknown-110921.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --strings-exp --seq-array=eager
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort T 0)
+(declare-sort T@ 0)
+(declare-sort |T@[$| 0)
+(declare-sort |T@[| 0)
+(declare-datatypes ((@ 0)) ((($1 (c (Seq (Seq Int)))))))
+(declare-datatypes ((@$ 0)) ((($1 (p @)))))
+(declare-datatypes ((M 0)) (((M (o |T@[|)))))
+(declare-datatypes ((T@$ 0)) (((T))))
+(declare-datatypes ((@M 0)) (((M (|#| |T@[$|)))))
+(declare-datatypes ((E 0)) (((E (s T@)))))
+(declare-datatypes ((L 0)) (((a))))
+(declare-datatypes (($M 0)) ((($M (l L) (p Int) (|#| @)))))
+(declare-datatypes ((@$M 0)) (((M (l L) (p Int) (v (Seq (Seq Int)))))))
+(declare-fun S (T@ T) @M)
+(declare-fun S (|T@[$| T@$) Int)
+(declare-fun S (|T@[| Int) @$)
+(declare-fun e () E)
+(declare-fun |1| () M)
+(declare-fun _$ () (Seq Int))
+(declare-fun $ () $M)
+(declare-fun i () @$M)
+(assert (not (=> (= (|#| $) (p (S (o |1|) 1))) (= i (M (l i) (p i) (seq.unit _$))) (= $ ($M (l $) (p $) ($1 (v i)))) (and (forall ((h T)) (and (forall ((v T@$)) (= 0 (S (|#| (S (s e) h)) T)))))) (= _$ (seq.nth (c (p (S (o |1|) 1))) (- 1 (seq.len (c (p (S (o |1|) 1))))))))))
+(check-sat)

diff --git a/test/regress/regress1/strings/seq-skeleton-gap.smt2 b/test/regress/regress1/strings/seq-skeleton-gap.smt2
new file mode 100644 (file)
index 0000000..30fd01a
--- /dev/null
+++ b/test/regress/regress1/strings/seq-skeleton-gap.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp --seq-array=lazy
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Seq Int))
+(assert (< 1 (seq.len (seq.update a 0 (seq.unit 1)))))
+(assert (distinct a (seq.update a 0 (seq.unit 1))))
+(check-sat)