Patrick Lühne
4ec8bb56b9
Improve error message
2020-05-29 17:43:02 +02:00
Patrick Lühne
9b6632cc94
Check that only input predicates are used in assumptions
2020-05-29 17:42:05 +02:00
Patrick Lühne
93db8d02b5
Implement tightness check
2020-05-29 14:57:00 +02:00
Patrick Lühne
b52ca236e2
Handle private predicates in specification
2020-05-28 07:27:29 +02:00
Patrick Lühne
c3b149a473
Remove incorrect check
2020-05-28 07:06:01 +02:00
Patrick Lühne
1b827edd45
Clean-up
2020-05-28 05:03:56 +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
116f74f63e
Minor clean-up
2020-05-22 18:17:00 +02:00
Patrick Lühne
81ddfd450a
Use custom foliage flavor
...
With this patch, properties specific to variable, function, and
predicate declarations are directly stored within those objects rather
than external maps that need to be queried via traits. This greatly
simplifies many parts of the logic.
This is made possible by implementing a custom foliage flavor, which
makes it possible to swap the built-in declaration types for extended
versions of those types that fulfill certain requirements.
2020-05-22 02:25:00 +02:00
Patrick Lühne
b62c379b97
Properly handle input/output errors
2020-05-19 13:10:31 +02:00
Patrick Lühne
c1038b398c
Improve warning when using private predicates in specification
2020-05-19 12:47:24 +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
58d89b4d07
Detect cyclic dependencies when hiding predicates
2020-05-18 01:19:59 +02:00
Patrick Lühne
82422cc28f
Support hiding auxiliary predicates
2020-05-13 08:02:04 +02:00
Patrick Lühne
e42fd92d4b
Add parser support for output statements
2020-05-12 05:27:51 +02:00
Patrick Lühne
32b18e2b63
Refactor parsing formulas
2020-05-12 05:20:48 +02:00
Patrick Lühne
91765a7a15
Remove duplicate match arm
2020-05-11 02:45:44 +02:00
Patrick Lühne
70bef152a4
Improve proof output
2020-05-06 21:38:48 +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
Patrick Lühne
b6ecf37211
Add option for input constants
2020-02-05 19:40:21 +01:00
Patrick Lühne
caab0a618e
Add option for input predicates
2020-02-05 01:10:33 +01:00
Patrick Lühne
5ad14f8deb
Add option for specifying input files
2020-02-02 19:20:16 +01:00
Patrick Lühne
e122532fcb
Implement completion
2020-02-02 17:57:27 +01:00
Patrick Lühne
6145c2cf1a
Translate body of rules for verifying properties
2020-01-31 17:19:44 +01:00