From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Sat, 28 Mar 2020 17:39:47 +0000 (-0500)
Subject: Convert the last few Sygus benchmarks to V2. (#4172)
X-Git-Tag: cvc5-1.0.0~3431
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=830c09d3cadc119845aff27684bd68c16e442692;p=cvc5.git

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 ef124c953..994fb6de3 100644
--- 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 e169e1a5c..d593a7d9e 100644
--- 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 305f5783a..31e88f523 100644
--- 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 d506dd5b2..b08aa8929 100644
--- 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 6c6da3dd2..2d911e56a 100644
--- 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 abcfc2217..089a8f11f 100644
--- 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 1f839c229..08b5738c1 100644
--- 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 37ed848ef..f191d784f 100644
--- 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 a836c9726..850cc6610 100644
--- 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 3449ed505..ac1172e33 100644
--- 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 b4c248de9..b7646725d 100644
--- 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 66880eafa..7e1cd80b3 100644
--- 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)