summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/sygus/Makefile.am7
-rw-r--r--test/regress/regress0/sygus/commutative.sy22
-rw-r--r--test/regress/regress0/sygus/constant.sy23
-rw-r--r--test/regress/regress0/sygus/hd-01-d1-prog.sy22
-rw-r--r--test/regress/regress0/sygus/icfp_28_10.sy40
-rw-r--r--test/regress/regress0/sygus/max.sl1
-rw-r--r--test/regress/regress0/sygus/multi-fun-polynomial2.sy35
-rw-r--r--test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy36
8 files changed, 185 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index ad1296af0..b5ea8b476 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -18,7 +18,12 @@ MAKEFLAGS = -k
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
# put it below in "TESTS +="
-TESTS =
+TESTS = hd-01-d1-prog.sy \
+ icfp_28_10.sy \
+ commutative.sy \
+ constant.sy \
+ multi-fun-polynomial2.sy \
+ unbdd_inv_gen_winf1.sy
# sygus tests currently taking too long for make regress
EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
new file mode 100644
index 000000000..15567b0a8
--- /dev/null
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun comm ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (comm x y) (comm y x)))
+
+
+(check-synth)
+
+; (+ x y) is a valid solution \ No newline at end of file
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
new file mode 100644
index 000000000..ddc12a6a9
--- /dev/null
+++ b/test/regress/regress0/sygus/constant.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun constant ((x Int)) Int
+ ((Start Int (x
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (constant x) (constant y)))
+
+
+(check-synth)
+
+; 0, 1, (- x x) are valid solutions \ No newline at end of file
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
new file mode 100644
index 000000000..a58bc2f64
--- /dev/null
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001)))
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32)
+ ((Start (BitVec 32) ((bvand Start Start)
+ (bvsub Start Start)
+ (bvor Start Start)
+ (bvadd Start Start)
+ (bvxor Start Start)
+ x
+ #x00000000
+ #xFFFFFFFF
+ #x00000001))))
+
+(declare-var x (BitVec 32))
+(constraint (= (hd01 x) (f x)))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
new file mode 100644
index 000000000..6e1610337
--- /dev/null
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic BV)
+
+(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(
+
+(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)
+ ))
+)
+)
+
+
+(constraint (= (f #xd74594057974e439) #x0000d74594057974))
+(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92))
+(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec))
+(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee))
+(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42))
+(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b))
+(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0))
+(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970))
+(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d))
+(constraint (= (f #x12430014ed058b24) #x000012430014ed05))
+(check-synth)
diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl
index aea8e8186..fdd925196 100644
--- a/test/regress/regress0/sygus/max.sl
+++ b/test/regress/regress0/sygus/max.sl
@@ -1,4 +1,5 @@
; EXPECT: unsat
+; COMMAND-LINE: --cegqi
(set-logic LIA)
(synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
new file mode 100644
index 000000000..24d49ee4e
--- /dev/null
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -0,0 +1,35 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+
+(synth-fun addExpr1 ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+(synth-fun addExpr2 ((x Int) (y Int)) Int
+ ((Start Int (x
+ y
+ 0
+ 1
+ (+ Start Start)
+ (- Start Start)
+ ))
+ ))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x y)))
+
+
+(check-synth)
+
+; (x, y), (x-y, 0) ... are valid solutions \ No newline at end of file
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
new file mode 100644
index 000000000..dc39efd84
--- /dev/null
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -0,0 +1,36 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+
+(set-logic LIA)
+(synth-fun inv ((x Int)) Bool
+ (
+ (Start Bool ((and AtomicFormula AtomicFormula)
+ (or AtomicFormula AtomicFormula)))
+ (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
+ (Sum Int ((+ Term Term)))
+ (Term Int ((* Sign Var)))
+ (Sign Int (0 1 -1))
+ (Var Int (x))
+ (Const Int ((+ Const Const) (- Const Const) 0 1))
+ )
+)
+
+(define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2))
+(define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3))
+(define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4))
+(define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5))
+(define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6))
+(define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3))
+(define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4))
+(define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5))
+
+(declare-var s Int)
+
+(declare-var x Int)
+
+(constraint (implies (= x 0) (inv x)))
+(constraint (implies (inv x) (= x 0)))
+(constraint (implies (inv x) (inv x)))
+(constraint (implies (and (inv x) false) (not (= x 0))))
+
+(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback