summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/sygus/c100.sy4
-rw-r--r--test/regress/regress0/sygus/check-generic-red.sy3
-rw-r--r--test/regress/regress0/sygus/const-var-test.sy5
-rw-r--r--test/regress/regress0/sygus/sygus-uf.sy7
-rw-r--r--test/regress/regress1/rr-verify/regex.sy9
-rw-r--r--test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy18
-rw-r--r--test/regress/regress1/sygus/issue3461.sy7
-rw-r--r--test/regress/regress1/sygus/max.sy4
-rw-r--r--test/regress/regress1/sygus/parity-si-rcons.sy3
-rw-r--r--test/regress/regress1/sygus/re-concat.sy8
-rw-r--r--test/regress/regress1/sygus/simple-regexp.sy50
-rw-r--r--test/regress/regress1/sygus/sygus-uf-ex.sy30
12 files changed, 81 insertions, 67 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback