SyGuS language 2.0 support

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_doub_access_init_const.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (n Int) (i Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (n Int) (i Int)) Bool
+    (and (>= n 0) (= i 0)))
+(define-fun trans_fun ((a (Array Int Int)) (n Int) (i Int) (a! (Array Int Int)) (n! Int) (i! Int)) Bool
+    (and (<= i n) (= i! (+ i 1)) (= n! n) (= a! (store (store a (* 2 i) 0) (+ 1 (* 2 i)) 0))))
+(define-fun post_fun ((a (Array Int Int)) (n Int) (i Int)) Bool
+    (or (<= i n) (forall ((j Int)) (=> (and (>= j 0) (<= j (* 2 n))) (>= 0 (select a j))))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_both_ends_multiple_sum.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (b (Array Int Int)) (n Int) (i Int) (i1 Int) (sum Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (b (Array Int Int)) (n Int) (i Int) (i1 Int) (sum Int)) Bool
+    (and (>= n 0) (= i 0) (= sum 0) (= i1 0)))
+(define-fun trans_fun ((a (Array Int Int)) (b (Array Int Int)) (n Int) (i Int) (i1 Int) (sum Int) (a! (Array Int Int)) (b! (Array Int Int)) (n! Int) (i! Int) (i1! Int) (sum! Int)) Bool
+    (and (< i1 (* 2 n)) (= i1! (+ i1! 1)) (= n! n) (ite (< i1 n) (and (< i n) (= i! (+ i 1)) (= a! (store a i i)) (= b! (store b (+ n (- i) (- 1)) i))) (= sum! (+ sum (- (select a (- i1 n)) (select b (+ n (- (- i1 n)) (- 1)))))))))
+(define-fun post_fun ((a (Array Int Int)) (b (Array Int Int)) (n Int) (i Int) (i1 Int) (sum Int)) Bool
+    (or (< i1 (* 2 n)) (= sum 0)))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_nondet_vars.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (n Int) (i Int) (j Int) (k Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (n Int) (i Int) (j Int) (k Int)) Bool
+    (and (< n 100000) (> j 0) (< j 10000) (= i 1)))
+(define-fun trans_fun ((a (Array Int Int)) (n Int) (i Int) (j Int) (k Int) (a! (Array Int Int)) (n! Int) (i! Int) (j! Int) (k! Int)) Bool
+    (and (< i n) (= i! (+ i 1)) (= n! n) (> k! 0) (< k! 10000) (= a! (store a i (+ i j k!)))))
+(define-fun post_fun ((a (Array Int Int)) (n Int) (i Int) (j Int) (k Int)) Bool
+    (or (< i n) (forall ((m Int)) (=> (and (> m 0) (< m n)) (>= (select a m) (+ m 2))))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_pair_sum_const--simplified.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (n Int) (i Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (n Int) (i Int)) Bool
+    (and (>= n 0) (= i 0)))
+(define-fun trans_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (n Int) (i Int) (a! (Array Int Int)) (b! (Array Int Int)) (c! (Array Int Int)) (n! Int) (i! Int)) Bool
+    (and (< i n) (= i! (+ i 1)) (= n! n) (= a! (store a i 1)) (= b! (store b i 2)) (= c! (store c i (+ (select a i) (select b i))))))
+(define-fun post_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (n Int) (i Int)) Bool
+    (or (< i n) (forall ((j Int)) (=> (and (>= j 1) (< j n)) (>= (select c j) 3)))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/sv-benchmarks/2019.array-cav/array_init_pair_symmetr--simplified.sl → benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_pair_symmetr--simplified.sl

@@ -2,36 +2,14 @@
 
 (synth-inv inv_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (n Int) (i Int)))
 
-(declare-primed-var a (Array Int Int))
-(declare-primed-var b (Array Int Int))
-(declare-primed-var c (Array Int Int))
-(declare-primed-var x Int)
-(declare-primed-var i Int)
-(declare-primed-var n Int)
-
-
 (define-fun pre_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (n Int) (i Int)) Bool
-  (and (>= n 0) (= i 0) ))
-
+    (and (>= n 0) (= i 0)))
 (define-fun trans_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (n Int) (i Int) (a! (Array Int Int)) (b! (Array Int Int)) (c! (Array Int Int)) (x! Int) (n! Int) (i! Int)) Bool
-  (and (< i n)
-       (= i! (+ i 1))
-       (= n! n)
-       (> x! -100000)
-       (< x! 100000)
-       (= a! (store a i x!))
-       (= b! (store b i (- x!)))
-       (= c! (store c i (+ (select a i) (select b i))))
-  )
-)
-
+    (and (< i n) (= i! (+ i 1)) (= n! n) (> x! (- 100000)) (< x! 100000) (= a! (store a i x!)) (= b! (store b i (- x!))) (= c! (store c i (+ (select a i) (select b i))))))
 (define-fun post_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (n Int) (i Int)) Bool
-  (or (< i n)
-      (forall ((j Int)) (=> (and (>= j 0) (< j n))
-                            (= (select c j) 0)))
-  )
-)
+    (or (< i n) (forall ((j Int)) (=> (and (>= j 0) (< j n)) (= (select c j) 0)))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
-(check-synth)
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_pair_symmetr2.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (y Int) (n Int) (i Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (y Int) (n Int) (i Int)) Bool
+    (and (>= n 0) (= i 0)))
+(define-fun trans_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (y Int) (n Int) (i Int) (a! (Array Int Int)) (b! (Array Int Int)) (c! (Array Int Int)) (x! Int) (y! Int) (n! Int) (i! Int)) Bool
+    (and (< i n) (= i! (+ i 1)) (= n! n) (> x! (- 100000)) (< x! 100000) (> y! (- 100000)) (< y! 100000) (> x! y!) (= a! (store a i x!)) (= b! (store b i y!)) (= c! (store c i (- (select a i) (select b i))))))
+(define-fun post_fun ((a (Array Int Int)) (b (Array Int Int)) (c (Array Int Int)) (x Int) (y Int) (n Int) (i Int)) Bool
+    (or (< i n) (forall ((j Int)) (=> (and (>= j 0) (=> (< j n))) (> (select c j) 0)))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/sv-benchmarks/2019.array-cav/array_init_var_plus_ind.sl → benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_var_plus_ind.sl

@@ -2,31 +2,14 @@
 
 (synth-inv inv_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)))
 
-(declare-primed-var a (Array Int Int))
-(declare-primed-var j Int)
-(declare-primed-var i Int)
-(declare-primed-var n Int)
-(declare-primed-var x Int)
-
-
 (define-fun pre_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)) Bool
-  (and (>= n 0) (= i 0) (= j 0)))
-
+    (and (>= n 0) (= i 0) (= j 0)))
 (define-fun trans_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (a! (Array Int Int)) (n! Int) (j! Int) (i! Int) (x! Int)) Bool
-  (and (and (< i n) (= x 0))
-       (= n! n)
-       (= j! (+ j i))
-       (= a! (store a i j))
-  )
-)
-
+    (and (and (< i n) (= x 0)) (= n! n) (= j! (+ j i)) (= a! (store a i j))))
 (define-fun post_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)) Bool
-  (or (and (< i n) (= x 0))
-      (forall ((k Int)) (=> (and (> k 0) (< k i))
-                            (>= (select a k) 0)))
-  )
-)
+    (or (and (< i n) (= x 0)) (forall ((k Int)) (=> (and (> k 0) (< k i)) (>= (select a k) 0)))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
-(check-synth)
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_var_plus_ind2.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (k Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (k Int)) Bool
+    (and (>= n 0) (= i 0) (= j 0) (= k 0)))
+(define-fun trans_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (k Int) (a! (Array Int Int)) (n! Int) (j! Int) (i! Int) (x! Int) (k! Int)) Bool
+    (and (and (< i n) (= x 0)) (= n! n) (= k! (- k i)) (= j! (+ j i)) (= a! (store a i j))))
+(define-fun post_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (k Int)) Bool
+    (or (and (< i n) (= x 0)) (forall ((l Int)) (=> (and (> l 0) (< l i)) (>= (select a l) k)))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/sv-benchmarks/2019.array-cav/array_init_var_plus_ind3.sl → benchmarks/ALIA/2019.SV-Comp/array-cav19/array_init_var_plus_ind3.sl

@@ -2,31 +2,14 @@
 
 (synth-inv inv_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)))
 
-(declare-primed-var a (Array Int Int))
-(declare-primed-var j Int)
-(declare-primed-var i Int)
-(declare-primed-var n Int)
-(declare-primed-var x Int)
-
-
 (define-fun pre_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)) Bool
-  (and (>= n 0) (= i 0) (= j 0)))
-
+    (and (>= n 0) (= i 0) (= j 0)))
 (define-fun trans_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int) (a! (Array Int Int)) (n! Int) (j! Int) (i! Int) (x! Int)) Bool
-  (and (and (< i n) (= x 0))
-       (= n! n)
-       (= a! (store a i j))
-       (= j! (- j i))
-  )
-)
-
+    (and (and (< i n) (= x 0)) (= n! n) (= a! (store a i j)) (= j! (- j i))))
 (define-fun post_fun ((a (Array Int Int)) (n Int) (j Int) (i Int) (x Int)) Bool
-  (or (and (< i n) (= x 0))
-      (forall ((l Int)) (=> (and (>= l 4) (< l i))
-                            (<= (select a l) 0)))
-  )
-)
+    (or (and (< i n) (= x 0)) (forall ((l Int)) (=> (and (>= l 4) (< l i)) (<= (select a l) 0)))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
-(check-synth)
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_tiling_poly6.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (i Int) (s Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (i Int) (s Int)) Bool
+    (and (= i 0) (> s 1)))
+(define-fun trans_fun ((a (Array Int Int)) (i Int) (s Int) (a! (Array Int Int)) (i! Int) (s! Int)) Bool
+    (and (< i (* 2 s)) (= i! (+ i! 1)) (= s! s) (ite (< i s) (= a! (store a i (* (- i 1) (+ i 1)))) (= a! (store a (- i s) (- (select a (- i s)) (* (- i s) (- i s))))))))
+(define-fun post_fun ((a (Array Int Int)) (i Int) (s Int)) Bool
+    (or (< i (* 2 s)) (forall ((j Int)) (=> (and (>= j 0) (< j s)) (= (- 1) (select a j))))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/sv-benchmarks/2019.array-cav/array_tiling_tcpy.sl → benchmarks/ALIA/2019.SV-Comp/array-cav19/array_tiling_tcpy.sl

@@ -2,29 +2,14 @@
 
 (synth-inv inv_fun ((a (Array Int Int)) (acopy (Array Int Int)) (s Int) (i Int)))
 
-(declare-primed-var a (Array Int Int))
-(declare-primed-var acopy (Array Int Int))
-(declare-primed-var i Int)
-(declare-primed-var s Int)
-
 (define-fun pre_fun ((a (Array Int Int)) (acopy (Array Int Int)) (s Int) (i Int)) Bool
-  (and (> s 1) (= i 0)))
-
+    (and (> s 1) (= i 0)))
 (define-fun trans_fun ((a (Array Int Int)) (acopy (Array Int Int)) (s Int) (i Int) (a! (Array Int Int)) (acopy! (Array Int Int)) (s! Int) (i! Int)) Bool
-  (and (< i s)
-       (= i! (+ i 1))
-       (= s! s)
-       (= acopy! (store (store acopy i (select a i)) (- (* 2 s) (+ i 1)) (select a (- (* 2 s) (+ i 1))) ))
-  )
-)
-
+    (and (< i s) (= i! (+ i 1)) (= s! s) (= acopy! (store (store acopy i (select a i)) (- (* 2 s) (+ i 1)) (select a (- (* 2 s) (+ i 1)))))))
 (define-fun post_fun ((a (Array Int Int)) (acopy (Array Int Int)) (s Int) (i Int)) Bool
-  (or (< i s)
-      (forall ((j Int)) (=> (and (>= j 0) (< j (* 2 s)))
-                            (= (select acopy j) (select a j))))
-  )
-)
+    (or (< i s) (forall ((j Int)) (=> (and (>= j 0) (< j (* 2 s))) (= (select acopy j) (select a j))))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
-(check-synth)
+(check-synth)
+

benchmarks/ALIA/2019.SV-Comp/array-cav19/array_tripl_access_init_const.sl

@@ -0,0 +1,15 @@
+(set-logic ALIA)
+
+(synth-inv inv_fun ((a (Array Int Int)) (n Int) (i Int)))
+
+(define-fun pre_fun ((a (Array Int Int)) (n Int) (i Int)) Bool
+    (and (>= n 0) (= i 0)))
+(define-fun trans_fun ((a (Array Int Int)) (n Int) (i Int) (a! (Array Int Int)) (n! Int) (i! Int)) Bool
+    (and (<= i n) (= i! (+ i 1)) (= n! n) (= a! (store (store (store a (* 3 i) 0) (+ 1 (* 3 i)) 0) (+ 2 (* 3 i)) 0))))
+(define-fun post_fun ((a (Array Int Int)) (n Int) (i Int)) Bool
+    (or (<= i n) (forall ((j Int)) (=> (and (>= j 0) (<= j (* 3 n))) (>= 0 (select a j))))))
+
+(inv-constraint inv_fun pre_fun trans_fun post_fun)
+
+(check-synth)
+

benchmarks/ALIA/others/add-array.sl

@@ -2,31 +2,14 @@
 
 (synth-inv inv_fun ((x (Array Int Int)) (y Int) (n Int)))
 
-(declare-primed-var x (Array Int Int))
-(declare-primed-var y Int)
-(declare-primed-var n Int)
-
 (define-fun pre_fun ((x (Array Int Int)) (y Int) (n Int)) Bool
-(and
-    (>= n 0)
-    (and (= n (select x 0))
-    (= y 0))
-))
-
+    (and (>= n 0) (and (= n (select x 0)) (= y 0))))
 (define-fun trans_fun ((x (Array Int Int)) (y Int) (n Int) (x! (Array Int Int)) (y! Int) (n! Int)) Bool
-(and
-    (> (select x 0) 0)
-    (and (= n! n)
-    (and (= y! (+ y 1))
-    (= x! (store x 0 (- (select x 0) 1)))))
-))
-
+    (and (> (select x 0) 0) (and (= n! n) (and (= y! (+ y 1)) (= x! (store x 0 (- (select x 0) 1)))))))
 (define-fun post_fun ((x (Array Int Int)) (y Int) (n Int)) Bool
-(or
-  (> (select x 0) 0)
-  (= n (+ (select x 0) y))
-))
+    (or (> (select x 0) 0) (= n (+ (select x 0) y))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
 (check-synth)
+

benchmarks/ALIA/others/array-copyall-bool.sl

@@ -2,36 +2,14 @@
 
 (synth-inv inv_fun ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (n Int) (i Int)))
 
-(declare-primed-var a1 (Array Int Bool))
-(declare-primed-var a2 (Array Int Bool))
-(declare-primed-var i Int)
-(declare-primed-var n Int)
-
 (define-fun pre_fun ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (n Int) (i Int)) Bool
-(and
-    (>= n 0)
-    (and (= i 0)
-    (< i n))
-))
-
+    (and (>= n 0) (and (= i 0) (< i n))))
 (define-fun trans_fun ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (n Int) (i Int) (a1! (Array Int Bool)) (a2! (Array Int Bool)) (n! Int) (i! Int)) Bool
-(and
-    (< i n)
-    (= i! (+ i 1))
-    (and (= n! n)
-    (and (= a2! a2)
-    (= a1! (store a1 i (select a2 i)))))
-))
-
+    (and (< i n) (= i! (+ i 1)) (and (= n! n) (and (= a2! a2) (= a1! (store a1 i (select a2 i)))))))
 (define-fun post_fun ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (n Int) (i Int)) Bool
-(or
-  (< i n)
-  (forall ((j Int))
-          (=> (and (<= 0 j) (< j n))
-              (= (select a1 j)
-                 (select a2 j))))
-))
+    (or (< i n) (forall ((j Int)) (=> (and (<= 0 j) (< j n)) (= (select a1 j) (select a2 j))))))
 
 (inv-constraint inv_fun pre_fun trans_fun post_fun)
 
-(check-synth)
+(check-synth)
+