diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-21 03:20:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-21 03:20:09 -0500 |
commit | 69d511da599dc18fbf3d42571e0f23b8e1d39032 (patch) | |
tree | b44d1007c3b0a82565494bc112b61ba245a9e001 /test/regress/regress0 | |
parent | 75ccf2b4ad3dbcb1a0edfc336db35b45719a09f5 (diff) |
Sygus inv templ refactor (#1110)
* Decouple single invocation techniques from deep embedding techniques. Embed templates for invariant synthesis into grammar instead of as a global substitution. Add regression.
* Update comment on class
* Cleanup
* Comments for sygus type construction.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sygus/cegar1.sy | 23 |
2 files changed, 25 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index c22f64b93..01f3be1a1 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -62,7 +62,8 @@ TESTS = commutative.sy \ General_plus10.sy \ qe.sy \ cggmp.sy \ - parse-bv-let.sy + parse-bv-let.sy \ + cegar1.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy new file mode 100644 index 000000000..dd7f73e27 --- /dev/null +++ b/test/regress/regress0/sygus/cegar1.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth +(set-logic LIA) + +(synth-inv inv-f ((x Int) (y Int))) + +(declare-primed-var x Int) +(declare-primed-var y Int) + +(define-fun pre-f ((x Int) (y Int)) Bool +(and (and (>= x 0) +(and (<= x 2) +(<= y 2))) (>= y 0))) + +(define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool +(and (= x! (+ x 2)) (= y! (+ y 2)))) + +(define-fun post-f ((x Int) (y Int)) Bool +(not (and (= x 4) (= y 0)))) + +(inv-constraint inv-f pre-f trans-f post-f) + +(check-synth) |