diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /test | |
parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/sygus/enum-test.sy | 8 | ||||
-rw-r--r-- | test/regress/regress0/sygus/inv-example.sy | 12 | ||||
-rw-r--r-- | test/regress/regress0/sygus/nflat-fwd-3.sy | 11 | ||||
-rw-r--r-- | test/regress/regress0/sygus/no-syntax-test-bool.sy | 15 | ||||
-rw-r--r-- | test/regress/regress0/sygus/uminus_one.sy | 7 |
6 files changed, 59 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index dbef0494a..9d7155f78 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -38,7 +38,12 @@ TESTS = commutative.sy \ let-simp.sy \ tl-type.sy \ dup-op.sy \ - nflat-fwd.sy + nflat-fwd.sy \ + nflat-fwd-3.sy \ + enum-test.sy \ + no-syntax-test-bool.sy \ + inv-example.sy \ + uminus_one.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy new file mode 100644 index 000000000..52a72c07d --- /dev/null +++ b/test/regress/regress0/sygus/enum-test.sy @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(define-sort D (Enum (a b))) +(define-fun f ((x D)) Int (ite (= x D::a) 3 7)) +(synth-fun g () D ((Start D (D::a D::b)))) +(constraint (= (f g) 7)) +(check-synth)
\ No newline at end of file diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy new file mode 100644 index 000000000..dda8e0ed5 --- /dev/null +++ b/test/regress/regress0/sygus/inv-example.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3)))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth)
\ No newline at end of file diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy new file mode 100644 index 000000000..bd7c79e3e --- /dev/null +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ (+ Con Con) Con) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) 2)) +(check-synth) + diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy new file mode 100644 index 000000000..cc3855ad1 --- /dev/null +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Bool) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (>= (+ x y) 500))) + + +(check-synth) + diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy new file mode 100644 index 000000000..b020c0bee --- /dev/null +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -0,0 +1,7 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi +(set-logic LIA) +(synth-fun f ((x Int)) Int ((Start Int ((- 1))))) +(declare-var x Int) +(constraint (= (f x) (- 1))) +(check-synth)
\ No newline at end of file |