Supporting seq.nth (#4723)

This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.

6 files changed, 68 insertions, 0 deletions

diff --git a/test/regress/regress0/seq/intseq.smt2 b/test/regress/regress0/seq/intseq.smt2
new file mode 100644
index 000000000..e9d07e050
--- /dev/null
+++ b/test/regress/regress0/seq/intseq.smt2
@@ -0,0 +1,14 @@
+;EXPECT: unsat
+(set-logic ALL)
+(declare-fun tickleBool (Bool) Bool)
+(assert (and (tickleBool true) (tickleBool false)))
+(declare-fun ControlFlow (Int Int) Int)
+(declare-fun s@0 () (Seq Int))
+(declare-fun s@1 () (Seq Int))
+(declare-fun s@2 () (Seq Int))
+(assert (not
+ (=> (= (ControlFlow 0 0) 170) (let ((anon0_correct  (=> (= s@0 (seq.++ (as seq.empty (Seq Int)) (seq.unit 0))) (=> (and (= s@1 (seq.++ s@0 (seq.unit 1))) (= s@2 (seq.++ s@1 (seq.unit 2)))) (and (=> (= (ControlFlow 0 135) (- 0 217)) (= (seq.len s@2) 3)) (=> (= (seq.len s@2) 3) (=> (= (ControlFlow 0 135) (- 0 224)) (= (seq.extract s@2 1 2) (seq.++ (seq.unit 1) (seq.unit 2))))))))))
+(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 170) 135) anon0_correct)))
+PreconditionGeneratedEntry_correct)))
+))
+(check-sat)
diff --git a/test/regress/regress0/seq/intseq_dt.smt2 b/test/regress/regress0/seq/intseq_dt.smt2
new file mode 100644
index 000000000..36d2f4842
--- /dev/null
+++ b/test/regress/regress0/seq/intseq_dt.smt2
@@ -0,0 +1,20 @@
+;COMMAND-LINE: --dt-nested-rec
+;EXPECT: unsat
+(set-logic ALL)
+(declare-fun tickleBool (Bool) Bool)
+(assert (and (tickleBool true) (tickleBool false)))
+(declare-datatypes ((T@Value 0)(T@ValueArray 0)) (((Integer (|i#Integer| Int) ) (Vector (|v#Vector| T@ValueArray) ) ) ((ValueArray (|v#ValueArray| (Seq T@Value)) ) ) ))
+(declare-fun ControlFlow (Int Int) Int)
+(declare-fun s@0 () T@ValueArray)
+(declare-fun s@1 () T@ValueArray)
+(declare-fun s@2 () T@ValueArray)
+(declare-fun s@3 () T@ValueArray)
+(declare-fun s@4 () T@ValueArray)
+(declare-fun s@5 () T@ValueArray)
+(set-info :boogie-vc-id test)
+(assert (not
+ (=> (= (ControlFlow 0 0) 427) (let ((anon0_correct  (=> (= s@0 (ValueArray (as seq.empty (Seq T@Value)))) (and (=> (= (ControlFlow 0 331) (- 0 448)) (= (seq.len (|v#ValueArray| s@0)) 0)) (=> (= (seq.len (|v#ValueArray| s@0)) 0) (=> (= s@1 (ValueArray (seq.++ (|v#ValueArray| s@0) (seq.unit (Integer 0))))) (=> (and (= s@2 (ValueArray (seq.++ (|v#ValueArray| s@1) (seq.unit (Integer 1))))) (= s@3 (ValueArray (seq.++ (|v#ValueArray| s@2) (seq.unit (Integer 2)))))) (and (=> (= (ControlFlow 0 331) (- 0 490)) (= (seq.len (|v#ValueArray| s@3)) 3)) (=> (= (seq.len (|v#ValueArray| s@3)) 3) (and (=> (= (ControlFlow 0 331) (- 0 497)) (= (seq.nth (|v#ValueArray| s@3) 1) (Integer 1))) (=> (= (seq.nth (|v#ValueArray| s@3) 1) (Integer 1)) (=> (= s@4 (ValueArray (seq.extract (|v#ValueArray| s@3) 0 (- (seq.len (|v#ValueArray| s@3)) 1)))) (and (=> (= (ControlFlow 0 331) (- 0 517)) (= (seq.len (|v#ValueArray| s@4)) 2)) (=> (= (seq.len (|v#ValueArray| s@4)) 2) (=> (= s@5 (ValueArray (seq.++ (|v#ValueArray| s@4) (|v#ValueArray| s@4)))) (and (=> (= (ControlFlow 0 331) (- 0 534)) (= (seq.len (|v#ValueArray| s@5)) 4)) (=> (= (seq.len (|v#ValueArray| s@5)) 4) (=> (= (ControlFlow 0 331) (- 0 541)) (= (seq.nth (|v#ValueArray| s@5) 3) (Integer 1))))))))))))))))))))
+(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 427) 331) anon0_correct)))
+PreconditionGeneratedEntry_correct)))
+))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-nth-uf-z.smt2 b/test/regress/regress0/seq/seq-nth-uf-z.smt2
new file mode 100644
index 000000000..0ae8a702b
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nth-uf-z.smt2
@@ -0,0 +1,11 @@
+;EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () (Seq Int))
+(declare-fun b () (Seq Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (or (= x z) (= y z)))
+(assert (not (= (seq.nth a x) (seq.nth a z))))
+(assert (not (= (seq.nth b y) (seq.nth b z))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/seq/seq-nth-uf.smt2 b/test/regress/regress0/seq/seq-nth-uf.smt2
new file mode 100644
index 000000000..af0b93170
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nth-uf.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UFSLIA)
+(set-info :status unsat)
+(declare-fun a () (Seq Int))
+(declare-fun b () (Seq Int))
+(declare-fun c () (Seq Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (or (= a b) (= a c)))
+(assert (not (= (seq.nth a x) (seq.nth b x))))
+(assert (not (= (seq.nth a y) (seq.nth c y))))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-nth-undef.smt2 b/test/regress/regress0/seq/seq-nth-undef.smt2
new file mode 100644
index 000000000..765b3e2f6
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nth-undef.smt2
@@ -0,0 +1,6 @@
+;EXPECT: sat
+(set-logic ALL)
+(declare-fun s () (Seq Int))
+(assert (= 5 (seq.nth s 5)))
+(assert (= 2 (seq.len s)))
+(check-sat)
diff --git a/test/regress/regress0/seq/seq-nth.smt2 b/test/regress/regress0/seq/seq-nth.smt2
new file mode 100644
index 000000000..765b3e2f6
--- /dev/null
+++ b/test/regress/regress0/seq/seq-nth.smt2
@@ -0,0 +1,6 @@
+;EXPECT: sat
+(set-logic ALL)
+(declare-fun s () (Seq Int))
+(assert (= 5 (seq.nth s 5)))
+(assert (= 2 (seq.len s)))
+(check-sat)