diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-20 14:23:04 +0100 |
commit | a50f977b02c5653e03d4f3d9d8c7df1f9e2be48e (patch) | |
tree | 9e8c569a9250c6c8c7eb7826539e63ae414133d9 /test | |
parent | 9e5b1fd1083c1c82d5bbc61a4a316211db629c43 (diff) |
Mark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus regressions.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/sygus/commutative.sy | 22 | ||||
-rw-r--r-- | test/regress/regress0/sygus/constant.sy | 23 | ||||
-rw-r--r-- | test/regress/regress0/sygus/hd-01-d1-prog.sy | 22 | ||||
-rw-r--r-- | test/regress/regress0/sygus/icfp_28_10.sy | 40 | ||||
-rw-r--r-- | test/regress/regress0/sygus/max.sl | 1 | ||||
-rw-r--r-- | test/regress/regress0/sygus/multi-fun-polynomial2.sy | 35 | ||||
-rw-r--r-- | test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy | 36 |
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) |