Convert the last few Sygus benchmarks to V2. (#4172)

diff --git a/test/regress/regress0/sygus/c100.sy b/test/regress/regress0/sygus/c100.sy
index ef124c953ed2643123aa9071371b05c61b2cc765..994fb6de37098cf4fca6ce3e8817dfea512f2109 100644 (file)
--- a/test/regress/regress0/sygus/c100.sy
+++ b/test/regress/regress0/sygus/c100.sy
@@ -1,9 +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 constant ((x Int)) Int
+    ((Start Int))
     ((Start Int (0
                  2
                  3
@@ -15,4 +16,3 @@
 (declare-var x Int)
 (constraint (= (constant x) 100))
 (check-synth)
-

diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy
index e169e1a5ccb00e4ae83b0199d59b2b6e36c0f06a..d593a7d9e661a1e1ed59404bf2f2122db259ffd5 100644 (file)
--- a/test/regress/regress0/sygus/check-generic-red.sy
+++ b/test/regress/regress0/sygus/check-generic-red.sy
@@ -1,8 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
 (set-logic LIA)
 
 (synth-fun P ((x Int) (y Int)) Bool
+  ((Start Bool) (StartIntC Int) (StartInt Int))
   ((Start Bool ((and Start Start)
                 (not Start)
                 (<= StartInt StartIntC)

diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 305f5783a5a0f499436fdcb5a58452cec9527f50..31e88f523e95d5045374941988834680b28568c8 100644 (file)
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,9 +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 max2 ((x Int) (y Int)) Int
+    ((Start Int) (StartBool Bool))
     ((Start Int ((Variable Int)
                  (Constant Int)
                  (+ Start Start)
@@ -21,6 +22,4 @@
 
 (constraint (= (max2 x y) (+ x y 500)))
 
-
 (check-synth)
-

diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
index d506dd5b21ffd8e126f918c13ee3416451a1cdea..b08aa892936ce29afb6cae218b4dc588aaf68212 100644 (file)
--- a/test/regress/regress0/sygus/sygus-uf.sy
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -1,10 +1,11 @@
-; COMMAND-LINE: --sygus-out=status --uf-ho
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic ALL)
 
-(declare-fun uf (Int) Int)
+(declare-var uf (-> Int Int))
 
 (synth-fun f ((x Int) (y Int)) Bool
+  ((Start Bool) (IntExpr Int))
   ((Start Bool (true false
                 (<= IntExpr IntExpr)
                 (= IntExpr IntExpr)

diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy
index 6c6da3dd241cd813c4d927b03a94f0878ab38305..2d911e56a4886bc4d04deea162846c3567930945 100644 (file)
--- a/test/regress/regress1/rr-verify/regex.sy
+++ b/test/regress/regress1/rr-verify/regex.sy
@@ -1,17 +1,18 @@
-; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
 
 (set-logic SLIA)
 
-(synth-fun f ((x String) (y String)) Bool (
+(synth-fun f ((x String) (y String)) Bool
+((Start Bool) (StartRe RegLan) (StartStr String)) (
 
 (Start Bool (
   true
   false
   (= StartStr StartStr)
-  (str.in.re StartStr StartRe)
+  (str.in_re StartStr StartRe)
 ))
 
 (StartRe RegLan (
@@ -19,7 +20,7 @@
   (re.++ StartRe StartRe)
   (re.union StartRe StartRe)
   (re.* StartRe)
-  (str.to.re StartStr)
+  (str.to_re StartStr)
 ))
 
 (StartStr String (

diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
index abcfc2217701320395fd30c8c659b662c52b4e25..089a8f11f1684e76cf4793df5b0cc2209a609e38 100644 (file)
--- a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
+++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
@@ -1,14 +1,15 @@
 ; 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 hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) 
-  (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m))))
+(define-fun hd19 ((x (_ BitVec 32)) (m (_ BitVec 32)) (k (_ BitVec 32))) (_ BitVec 32)
+       (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m))))
 
 ; bvand is a duplicate
-(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32)
-                  ((Start (BitVec 32) ((bvand Start Start)
+(synth-fun f ((x (_ BitVec 32)) (m (_ BitVec 32)) (k (_ BitVec 32))) (_ BitVec 32)
+                       ((Start (_ BitVec 32)))
+                       ((Start (_ BitVec 32) ((bvand Start Start)
                                                                (bvsub Start Start)
                                                                (bvxor Start Start)
                                                                (bvor Start Start)
@@ -23,10 +24,9 @@
                                                                k))))
 
 
-(declare-var x (BitVec 32))
-(declare-var m (BitVec 32))
-(declare-var k (BitVec 32))
+(declare-var x (_ BitVec 32))
+(declare-var m (_ BitVec 32))
+(declare-var k (_ BitVec 32))
 
 (constraint (= (hd19 x m k) (f x m k)))
 (check-synth)
-

diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy
index 1f839c229e5678fbaf25e99152cfb7f477f0c7fd..08b5738c15d43cab0bab96906946778410095574 100644 (file)
--- a/test/regress/regress1/sygus/issue3461.sy
+++ b/test/regress/regress1/sygus/issue3461.sy
@@ -1,15 +1,16 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic ALL_SUPPORTED)
 
 (declare-datatype Doc ((D (owner Int) (body Int))))
 
-(declare-datatype Policy 
-  ((p (principal Int)) 
+(declare-datatype Policy
+  ((p (principal Int))
    (por (left Policy) (right Policy))))
 
 (synth-fun mkPolicy ((d Doc)) Policy
+  ((Start Policy) (Q Policy))
   ((Start Policy (Q))
    (Q Policy ((p 0) (p 1) (por Q Q))))
 )

diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy
index 37ed848efbf93ddb886622840b8daa5b4a06ac01..f191d784f7d958e7b5fb71be426d7a66a031a298 100644 (file)
--- a/test/regress/regress1/sygus/max.sy
+++ b/test/regress/regress1/sygus/max.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)
 
 (synth-fun max ((x Int) (y Int)) Int
+  ((Start Int) (StartBool Bool))
   ((Start Int (0 1 x y
                (+ Start Start)
                (- Start Start)
@@ -12,6 +13,7 @@
                     (<= Start Start)))))
 
 ;(synth-fun min ((x Int) (y Int)) Int
+;  ((Start Int) (StartBool Bool))
 ;  ((Start Int ((Constant Int) (Variable Int)
 ;               (+ Start Start)
 ;               (- Start Start)

diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy
index a836c9726acf2bac9d7ab4aa759eecd24c14d811..850cc6610e1fc886d6150898f9deaacf29ea0c62 100644 (file)
--- a/test/regress/regress1/sygus/parity-si-rcons.sy
+++ b/test/regress/regress1/sygus/parity-si-rcons.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
 
 (set-logic BV)
 
@@ -7,6 +7,7 @@
   (xor (not (xor a b)) (not (xor c d))))
 
 (synth-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+ ((Start Bool) (StartAnd Bool) (Vars Bool) (Constants Bool))
  ((Start Bool ((not StartAnd) Vars Constants))
   (StartAnd Bool ((and Start Start)))
   (Vars Bool (a b c d))

diff --git a/test/regress/regress1/sygus/re-concat.sy b/test/regress/regress1/sygus/re-concat.sy
index 3449ed505033c50671dca2eff7f0bccf5b9e6cb7..ac1172e330c541bf080bd92b78e609b04e64260d 100644 (file)
--- a/test/regress/regress1/sygus/re-concat.sy
+++ b/test/regress/regress1/sygus/re-concat.sy
@@ -1,13 +1,13 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
-(synth-fun f () RegLan (
+(synth-fun f () RegLan ((Start RegLan) (Tokens String)) (
                          (Start RegLan (
-                                         (str.to.re Tokens)
+                                         (str.to_re Tokens)
                                          (re.++ Start Start)))
                          (Tokens String ("A" "B"))
                          ))
 
-(constraint (str.in.re "AB" f))
+(constraint (str.in_re "AB" f))
 
 (check-synth)

diff --git a/test/regress/regress1/sygus/simple-regexp.sy b/test/regress/regress1/sygus/simple-regexp.sy
index b4c248de9ee4e3dac0fe00481416a683b12813fc..b7646725dcbf96d956945fc7ab77c92581e46762 100644 (file)
--- a/test/regress/regress1/sygus/simple-regexp.sy
+++ b/test/regress/regress1/sygus/simple-regexp.sy
@@ -1,30 +1,32 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
-(synth-fun P ((x String)) Bool (
-(Start Bool (
-  (str.in.re StartStr StartRL)
+(synth-fun P ((x String)) Bool
+  ((Start Bool) (StartStr String) (StartStrC String) (StartRL RegLan) (StartRLi RegLan)) (
+  (Start Bool (
+    (str.in_re StartStr StartRL)
   ))
-(StartStr String (
-  x
-  (str.++ StartStr StartStr)
+  (StartStr String (
+    x
+    (str.++ StartStr StartStr)
+  ))
+  (StartStrC String (
+    "A" "B" ""
+    (str.++ StartStrC StartStrC)
+  ))
+  (StartRL RegLan (
+    (re.++ StartRLi StartRLi)
+    (re.inter StartRL StartRL)
+    (re.union StartRL StartRL)
+    (re.* StartRLi)
+  ))
+  (StartRLi RegLan (
+    (str.to_re StartStrC)
+    (re.inter StartRLi StartRLi)
+    (re.union StartRLi StartRLi)
+    (re.++ StartRLi StartRLi)
+    (re.* StartRLi)
   ))
-(StartStrC String (
-  "A" "B" ""
-  (str.++ StartStrC StartStrC)))
-(StartRL RegLan (
-(re.++ StartRLi StartRLi)
-(re.inter StartRL StartRL)
-(re.union StartRL StartRL)
-(re.* StartRLi)
-))
-(StartRLi RegLan (
-(str.to.re StartStrC)
-(re.inter StartRLi StartRLi)
-(re.union StartRLi StartRLi)
-(re.++ StartRLi StartRLi)
-(re.* StartRLi)
-))
 ))
 
 (constraint (P "AAAAA"))
@@ -33,5 +35,5 @@
 (constraint (not (P "AB")))
 (constraint (not (P "B")))
 
-; (str.in.re x (re.* (str.to.re "A"))) is a solution
+; (str.in_re x (re.* (str.to_re "A"))) is a solution
 (check-synth)

diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
index 66880eafa17d8315eeef29723621f3552a9dcf5e..7e1cd80b30b901a8d3077b5d22c158a1efe2bdcb 100644 (file)
--- a/test/regress/regress1/sygus/sygus-uf-ex.sy
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -1,18 +1,24 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --uf-ho
-(set-logic UFLIA)
-(declare-fun uf ( Int ) Int)
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
+(set-logic ALL)
+
+(declare-var uf (-> Int Int))
+
 (synth-fun f ((x Int) (y Int)) Bool
-((Start Bool (true false
-  (<= IntExpr IntExpr )
-  (= IntExpr IntExpr )
-  (and Start Start )
-  (or Start Start )
-  (not Start )))
-(IntExpr Int (0 1 x y
-  (+ IntExpr IntExpr )
-  (- IntExpr IntExpr )))))
+  ((Start Bool) (IntExpr Int))
+  ((Start Bool (true false
+    (<= IntExpr IntExpr)
+    (= IntExpr IntExpr)
+    (and Start Start)
+    (or Start Start)
+    (not Start )))
+   (IntExpr Int (0 1 x y
+    (+ IntExpr IntExpr)
+    (- IntExpr IntExpr)))))
+
 (declare-var x Int)
+
 (constraint (f (uf x) (uf x)))
 (constraint (not (f 3 4)))
+
 (check-synth)