Commit Graph

17 Commits

Author SHA1 Message Date
Patrick Lühne f169931eac
Accept more than one specification file 2020-05-29 18:54:47 +02:00
Patrick Lühne fc34aadf90
Show all predicates used in specification by default 2020-05-29 18:41:16 +02:00
Patrick Lühne b52ca236e2
Handle private predicates in specification 2020-05-28 07:27:29 +02:00
Patrick Lühne 1e55f733d0
Minor clean-up 2020-05-28 05:03:57 +02:00
Patrick Lühne fe277b6773
Minor refactoring 2020-05-28 05:03:57 +02:00
Patrick Lühne 491a255811
Require supertight programs for backward proof 2020-05-28 05:03:56 +02:00
Patrick Lühne 499fa0c667
Add option to specify output color choice 2020-05-22 19:33:06 +02:00
Patrick Lühne 0578e99dc2
Finish basic simplifications 2020-05-22 18:14:56 +02:00
Patrick Lühne 3bf981236a
Only warn if private predicates are used in specification 2020-05-19 12:18:11 +02:00
Patrick Lühne 80d39c8c0a
Check that only input/output predicates are used in specification 2020-05-18 02:17:30 +02:00
Patrick Lühne 82422cc28f
Support hiding auxiliary predicates 2020-05-13 08:02:04 +02:00
Patrick Lühne e0b8b1c854
Minor formatting 2020-05-11 03:46:20 +02:00
Patrick Lühne 0d51053b88
Move ProofDirection type to separate module 2020-05-11 03:46:11 +02:00
Patrick Lühne b55bc82b1d
Add option for proof direction 2020-05-07 02:53:48 +02:00
Patrick Lühne 15769d58b3 Add missing file 2020-05-06 21:30:27 +02:00
Patrick Lühne b14f620235
Implement proof mechanism 2020-05-06 00:13:43 +02:00
Patrick Lühne e118442e16
Work in progress 2020-05-05 19:40:57 +02:00