Patrick Lühne
e686575ebf
Only forbid private predicates in spec statements
2020-05-28 18:37:56 +02:00
Patrick Lühne
e57a1859d2
Fix supertightness check
2020-05-28 18:37:34 +02:00
Patrick Lühne
b52ca236e2
Handle private predicates in specification
2020-05-28 07:27:29 +02:00
Patrick Lühne
bd9e0bd709
Simplify examples
2020-05-28 07:06:19 +02:00
Patrick Lühne
c3b149a473
Remove incorrect check
2020-05-28 07:06:01 +02:00
Patrick Lühne
b80b3bf6d6
Assume private predicates always
2020-05-28 06:30:35 +02:00
Patrick Lühne
d72e2af49a
Fix proof direction check
2020-05-28 06:30:14 +02:00
Patrick Lühne
870fdd048c
Handle input predicates correctly
2020-05-28 06:29:57 +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
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
9b7895a032
Don’t append variable ID if there is only one
2020-05-22 19:43:41 +02:00
Patrick Lühne
499fa0c667
Add option to specify output color choice
2020-05-22 19:33:06 +02:00
Patrick Lühne
739cae1f7c
Rename “assert” statement to “spec”
2020-05-22 18:34:59 +02:00
Patrick Lühne
116f74f63e
Minor clean-up
2020-05-22 18:17:00 +02:00
Patrick Lühne
0578e99dc2
Finish basic simplifications
2020-05-22 18:14:56 +02:00
Patrick Lühne
3b3f9017ba
Determine variable IDs correctly
2020-05-22 02:42:38 +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
efe354faad
Clean up unused struct
2020-05-19 13:02:12 +02:00
Patrick Lühne
efa5656e39
Clean up unused struct
2020-05-19 13:01:04 +02:00
Patrick Lühne
d88ac89b01
Add prime number example
2020-05-19 12:57:09 +02:00
Patrick Lühne
86d2857494
Start implementation of simplifications
2020-05-19 12:56:46 +02:00
Patrick Lühne
d77c7648b3
Ensure that statements are proven in right order
2020-05-19 12:56:21 +02:00
Patrick Lühne
34b8dce9be
Ignore built-in predicates in completion
2020-05-19 12:54:51 +02:00
Patrick Lühne
7020bc0bf0
Address unused variable
2020-05-19 12:53:37 +02:00
Patrick Lühne
0229adef78
Add to-do notes
2020-05-19 12:49:57 +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
3bf981236a
Only warn if private predicates are used in specification
2020-05-19 12:18:11 +02:00
Patrick Lühne
4de4cc21da
Fix gross bug in translation of division
2020-05-18 05:21:27 +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
e2281042c9
Rename example files for consistency
2020-05-18 01:46:16 +02:00
Patrick Lühne
ce51d14a9e
Minor formatting
2020-05-18 01:29:30 +02:00
Patrick Lühne
58d89b4d07
Detect cyclic dependencies when hiding predicates
2020-05-18 01:19:59 +02:00
Patrick Lühne
c0bfbc923c
Do not add type declarations for built-ins
2020-05-18 01:19:46 +02:00
Patrick Lühne
0cce3bf54d
Rename status message for clarity
2020-05-18 01:19:00 +02:00
Patrick Lühne
7361084eaf
Rename variable in example for consistency
2020-05-18 01:09:15 +02:00
Patrick Lühne
82422cc28f
Support hiding auxiliary predicates
2020-05-13 08:02:04 +02:00
Patrick Lühne
84031c483b
Revert logic for building completed definitions
2020-05-13 03:27:47 +02:00
Patrick Lühne
b308847ebd
Add to-do note
2020-05-13 03:17:37 +02:00
Patrick Lühne
d35d0d1d98
Use statement kind over section kind
2020-05-13 03:17:33 +02:00
Patrick Lühne
0dbf30bb1b
Work in progress
2020-05-13 02:24:13 +02:00
Patrick Lühne
4d00fbeb97
Minor formatting
2020-05-13 01:40:44 +02:00
Patrick Lühne
07fc6a7f85
Add to-do note
2020-05-13 01:28:25 +02:00
Patrick Lühne
37f0fff09f
Add comments to exact cover example
2020-05-12 06:39:50 +02:00
Patrick Lühne
f39393ebce
Add comments to example 2
2020-05-12 06:10:59 +02:00
Patrick Lühne
9621cb1e0c
Add to-do note
2020-05-12 06:10:52 +02:00
Patrick Lühne
8153352b66
Support comments in specification file
2020-05-12 06:08:50 +02:00
Patrick Lühne
e42fd92d4b
Add parser support for output statements
2020-05-12 05:27:51 +02:00