Convert V1 Sygus files to V2. (#4136)

25 files changed, 60 insertions, 65 deletions

diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index aec265f2b..02879cb8d 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --no-sygus-repair-const
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index 1792749e2..69bcd0f08 100755
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,11 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
-(synth-fun fb () Int ((Start Int ((Constant Int)))))
-(synth-fun fc () Int ((Start Int ((Constant Int)))))
+(synth-fun fb () Int ((Start Int)) ((Start Int ((Constant Int)))))
+(synth-fun fc () Int ((Start Int)) ((Start Int ((Constant Int)))))
 
-(constraint (= fc (+ fb 10))) 
+(constraint (= fc (+ fb 10)))
 
 (check-synth)
-
diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy
index ef12e3c0e..9330546d8 100644
--- a/test/regress/regress0/sygus/aig-si.sy
+++ b/test/regress/regress0/sygus/aig-si.sy
@@ -1,11 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
   (xor (not (xor a b)) (not (xor c d))))
 
 (synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool))
            ((Start Bool ((and Start Start) (not Start) a b c d))))
 
 (declare-var a Bool)
diff --git a/test/regress/regress0/sygus/array-grammar-select.sy b/test/regress/regress0/sygus/array-grammar-select.sy
index d216bbb24..2c0b4cf9a 100644
--- a/test/regress/regress0/sygus/array-grammar-select.sy
+++ b/test/regress/regress0/sygus/array-grammar-select.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALIA)
 
 (synth-fun f
diff --git a/test/regress/regress0/sygus/array-grammar-store.sy b/test/regress/regress0/sygus/array-grammar-store.sy
index 70525e83b..025a17b15 100644
--- a/test/regress/regress0/sygus/array-grammar-store.sy
+++ b/test/regress/regress0/sygus/array-grammar-store.sy
@@ -1,13 +1,13 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ABV)
 
 (synth-fun f
-  ((s (Array (BitVec 4) (BitVec 4))) (t (BitVec 4)))
-  (Array (BitVec 4) (BitVec 4))
+  ((s (Array (_ BitVec 4) (_ BitVec 4))) (t (_ BitVec 4)))
+  (Array (_ BitVec 4) (_ BitVec 4))
   )
 
-(declare-var x (Array (BitVec 4) (BitVec 4)))
+(declare-var x (Array (_ BitVec 4) (_ BitVec 4)))
 
 (constraint (= (= (store x #b0000 #b0000) (store x #b0001 #b0000)) (= (f x #b0000) (f x #b0001))))
 
diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy
index 662069105..91fe27b0b 100644
--- a/test/regress/regress0/sygus/ccp16.lus.sy
+++ b/test/regress/regress0/sygus/ccp16.lus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SAT)
 
 (define-fun
@@ -30,9 +30,6 @@
 ))
 
 
-(declare-primed-var top.usr.OK Bool)
-(declare-primed-var top.res.init_flag Bool)
-
 (define-fun
   init (
     (top.usr.OK Bool)
diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy
index fc8864f55..8fe64697b 100644
--- a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy
+++ b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 
 (synth-fun f ((x String) (y String)) String)
diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv.sy b/test/regress/regress0/sygus/cegqi-si-string-triv.sy
index 86a68574f..f5ce07ec6 100644
--- a/test/regress/regress0/sygus/cegqi-si-string-triv.sy
+++ b/test/regress/regress0/sygus/cegqi-si-string-triv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 
 (synth-fun f ((x String) (y String)) String)
diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index f4de9b055..e33edf36c 100644
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dt-sel-parse1.sy b/test/regress/regress0/sygus/dt-sel-parse1.sy
index 52edb3278..52f068055 100644
--- a/test/regress/regress0/sygus/dt-sel-parse1.sy
+++ b/test/regress/regress0/sygus/dt-sel-parse1.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 
@@ -27,6 +27,7 @@
 
 ; provide synthesis template 
 (synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange
+((Start ShipRange) (B Bool) (SR ShipRange) (IR IntRange) (LR LocRange) (I Int))
 (
      (Start ShipRange ((ite B SR SR)))
      (B Bool (response))
diff --git a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
index 71af1e916..b410e5d23 100644
--- a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
+++ b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
 ; EXPECT: unsat
 
 (set-logic BV)
 
-(synth-fun f ((x (BitVec 32))) (BitVec 32))
+(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32))
 
-(declare-var x (BitVec 32))
+(declare-var x (_ BitVec 32))
 (constraint (= (bvor x #x00000001) (f x)))
 (check-synth)
diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy
index c3f43fc07..7b7d50e22 100644
--- a/test/regress/regress0/sygus/inv-different-var-order.sy
+++ b/test/regress/regress0/sygus/inv-different-var-order.sy
@@ -1,10 +1,7 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 ;EXPECT: unsat
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
-(declare-primed-var b Bool)
-(declare-primed-var x Int)
-(declare-primed-var y Int)
 (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool
 (and
 (and (>= x 5) (<= x 9))
@@ -19,4 +16,4 @@
 )
 (define-fun post-f ((x Int) (y Int) (b Bool)) Bool true)
 (inv-constraint inv-f pre-f trans-f post-f)
-(check-synth)
\ No newline at end of file
+(check-synth)
diff --git a/test/regress/regress0/sygus/issue3624.sy b/test/regress/regress0/sygus/issue3624.sy
index cc677bb9c..992965432 100644
--- a/test/regress/regress0/sygus/issue3624.sy
+++ b/test/regress/regress0/sygus/issue3624.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 (declare-var A Bool)
 (declare-var B (Array Int Bool))
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 1bb85bed9..9f9eea2a8 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,11 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
-; COMMAND-LINE: --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
 
 (synth-fun f ((x Int)) Int
+    ((Start Int))
     ((Start Int (x
                  0
                  1
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index 7e191e312..91a865035 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,8 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun letf ((z Int)) Int (+ z z))
 (synth-fun f ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
                  0
@@ -13,4 +14,3 @@
 (declare-var y Int)
 (constraint (= (f x y) (* 3 x)))
 (check-synth)
-
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index c6c9383bb..4978b7a57 100644
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
@@ -12,4 +12,3 @@
 
 
 (check-synth)
-
diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index f27a07ee7..696d413ad 100644
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
@@ -12,4 +12,3 @@
 
 
 (check-synth)
-
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 50c7d39a0..09fae5410 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,11 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
   (xor (not (xor a b)) (not (xor c d))))
 
 (synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool))
            ((Start Bool ((and Start Start) (not Start) a b c d))))
 
 (declare-var a Bool)
diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy
index 1329918fc..60bb804b6 100644
--- a/test/regress/regress0/sygus/parse-bv-let.sy
+++ b/test/regress/regress0/sygus/parse-bv-let.sy
@@ -1,20 +1,21 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
-  (let ((modulo-shift (BitVec 32) (bvand bit #x0000001f)))
-	 (bvand modulo-shift x)))
+(define-fun bit-reset ((x (_ BitVec 32)) (bit (_ BitVec 32))) (_ BitVec 32)
+  (let ((modulo-shift (bvand bit #x0000001f)))
+   (bvand modulo-shift x)))
 
-(synth-fun btr ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
-    ((Start (BitVec 32) (
-                         (Constant (BitVec 32))
-                         (Variable (BitVec 32))
-			 (bvneg  Start) (bvnot  Start) (bvadd  Start Start) (bvand  Start Start) (bvlshr Start Start) (bvmul  Start Start) (bvor   Start Start) (bvshl  Start Start)
+(synth-fun btr ((x (_ BitVec 32)) (bit (_ BitVec 32))) (_ BitVec 32)
+    ((Start (_ BitVec 32)))
+    ((Start (_ BitVec 32) (
+                         (Constant (_ BitVec 32))
+                         (Variable (_ BitVec 32))
+       (bvneg  Start) (bvnot  Start) (bvadd  Start Start) (bvand  Start Start) (bvlshr Start Start) (bvmul  Start Start) (bvor   Start Start) (bvshl  Start Start)
                          ))))
 
-(declare-var x   (BitVec 32))
-(declare-var bit (BitVec 32))
+(declare-var x   (_ BitVec 32))
+(declare-var bit (_ BitVec 32))
 (constraint (= (btr x bit) #b00000000000000000000000000000000))
 
 (check-synth)
diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 5fbe91e2e..99c308173 100644
--- a/test/regress/regress0/sygus/pbe-pred-contra.sy
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 ; EXPECT: unknown
 (set-logic LIA)
 (synth-fun P ((x Int)) Bool)
diff --git a/test/regress/regress0/sygus/real-si-all.sy b/test/regress/regress0/sygus/real-si-all.sy
index 81f0ad22f..26524cdf6 100644
--- a/test/regress/regress0/sygus/real-si-all.sy
+++ b/test/regress/regress0/sygus/real-si-all.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LRA)
 
diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy
index 39c392487..49272165d 100644
--- a/test/regress/regress0/sygus/strings-unconstrained.sy
+++ b/test/regress/regress0/sygus/strings-unconstrained.sy
@@ -1,10 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
-((Start String (ntString))
-
-(ntString String (
+((ntString String))
+((ntString String (
 firstname 
 lastname 
 " "
@@ -12,4 +11,3 @@ lastname
 ))
 
 (check-synth)
-
diff --git a/test/regress/regress0/sygus/sygus-no-wf.sy b/test/regress/regress0/sygus/sygus-no-wf.sy
index 40a3d5547..e89d07fd9 100644
--- a/test/regress/regress0/sygus/sygus-no-wf.sy
+++ b/test/regress/regress0/sygus/sygus-no-wf.sy
@@ -1,7 +1,8 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 ; EXPECT: unsat
 (set-logic ALL)
 (synth-fun f ((x0 Bool)) Bool
+	((B Bool) (I Int))
 	(
 		(B Bool ((Variable Bool) (Constant Bool) (= I I) )) 
 		(I Int ((Constant Int) (+ I I)))
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index 94040bf45..9024ac3b6 100644
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
-(synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
+(synth-fun f ((x Int)) Int ((Start Int)) ((Start Int ((- 1)))))
 (declare-var x Int)
 (constraint (= (f x) (- 1)))
 (check-synth)
diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
index c2ed642be..b9bd8e815 100644
--- a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
+++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
@@ -1,21 +1,21 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (synth-fun f ((col1 String) (col2 String)) String
-    ((Start String (ntString))
-     (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
+    ((ntString String) (ntInt Int) (ntBool Bool))
+    ((ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"
                        (str.++ ntString ntString)
                        (str.replace ntString ntString ntString)
                        (str.at ntString ntInt)
-                       (int.to.str ntInt)
+                       (str.from_int ntInt)
                        (ite ntBool ntString ntString)
                        (str.substr ntString ntInt ntInt)))
       (ntInt Int (0 1 2
                   (+ ntInt ntInt)
                   (- ntInt ntInt)
                   (str.len ntString)
-                  (str.to.int ntString)
+                  (str.to_int ntString)
                   (str.indexof ntString ntString ntInt)))
       (ntBool Bool (true false
                     (str.prefixof ntString ntString)