diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-03 21:18:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-03 21:18:01 -0500 |
commit | 2ef8fe2eefaecdb62653d36c88169fe906512b9d (patch) | |
tree | 09e1c088ba3f9e9f99a4238dd1a3528b131a9c59 /test/regress/regress0/sygus | |
parent | f70af84aa6ad1511963e6cec97c6096fdcc1b37d (diff) |
Suppport SAT logic (#1310)
* Support SAT logic.
* Add lustre example.
* Add to smt1 as well.
* Fix.
* Fix.
* Fix for new option.
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sygus/ccp16.lus.sy | 72 |
2 files changed, 74 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 6dfcb922a..3c118a007 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -66,7 +66,8 @@ TESTS = commutative.sy \ cegar1.sy \ triv-type-mismatch-si.sy \ nia-max-square-ns.sy \ - strings-concat-3-args.sy + strings-concat-3-args.sy \ + ccp16.lus.sy # sygus tests currently taking too long for make regress diff --git a/test/regress/regress0/sygus/ccp16.lus.sy b/test/regress/regress0/sygus/ccp16.lus.sy new file mode 100644 index 000000000..662069105 --- /dev/null +++ b/test/regress/regress0/sygus/ccp16.lus.sy @@ -0,0 +1,72 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SAT) + +(define-fun + __node_init_top_0 ( + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + ) Bool + + (and (= top.usr.OK_a_0 true) top.res.init_flag_a_0) +) + +(define-fun + __node_trans_top_0 ( + (top.usr.OK_a_1 Bool) + (top.res.init_flag_a_1 Bool) + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + ) Bool + + (and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1)) +) + + + +(synth-inv str_invariant( + (top.usr.OK Bool) + (top.res.init_flag Bool) +)) + + +(declare-primed-var top.usr.OK Bool) +(declare-primed-var top.res.init_flag Bool) + +(define-fun + init ( + (top.usr.OK Bool) + (top.res.init_flag Bool) + ) Bool + + (and (= top.usr.OK true) top.res.init_flag) +) + +(define-fun + trans ( + + ;; Current state. + (top.usr.OK Bool) + (top.res.init_flag Bool) + + ;; Next state. + (top.usr.OK! Bool) + (top.res.init_flag! Bool) + + ) Bool + + (and (= top.usr.OK! true) (not top.res.init_flag!)) +) + +(define-fun + prop ( + (top.usr.OK Bool) + (top.res.init_flag Bool) + ) Bool + + top.usr.OK +) + +(inv-constraint str_invariant init trans prop) + +(check-synth) |