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 | |
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')
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/fmf/sat-logic.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sygus/ccp16.lus.sy | 72 |
4 files changed, 82 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b2ed657d0..122f9219b 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -78,7 +78,8 @@ TESTS = \ cruanes-no-minimal-unk.smt2 \ no-minimal-sat.smt2 \ issue916-fmf-or.smt2 \ - pow2-bool.smt2 + pow2-bool.smt2 \ + sat-logic.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/sat-logic.smt2 b/test/regress/regress0/fmf/sat-logic.smt2 new file mode 100644 index 000000000..678ea3079 --- /dev/null +++ b/test/regress/regress0/fmf/sat-logic.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic SAT) +(set-info :status sat) +(assert (forall ((x Bool) (y Bool)) (exists ((z Bool)) (= z (and x y))))) +(check-sat) 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) |