Commit Graph

146 Commits

Author SHA1 Message Date
4ec8bb56b9
Improve error message 2020-05-29 17:43:02 +02:00
9b6632cc94
Check that only input predicates are used in assumptions 2020-05-29 17:42:05 +02:00
93db8d02b5
Implement tightness check 2020-05-29 14:57:00 +02:00
b94ee5134a
Improve examples after meeting 2020-05-29 12:09:28 +02:00
dab121c684
Use 4 cores by default (to be improved) 2020-05-28 18:41:47 +02:00
7895bf83c4
Clean-up in example 2 2020-05-28 18:40:33 +02:00
c05eb11855
Improve example 2 2020-05-28 18:40:10 +02:00
e686575ebf
Only forbid private predicates in spec statements 2020-05-28 18:37:56 +02:00
e57a1859d2
Fix supertightness check 2020-05-28 18:37:34 +02:00
b52ca236e2
Handle private predicates in specification 2020-05-28 07:27:29 +02:00
bd9e0bd709
Simplify examples 2020-05-28 07:06:19 +02:00
c3b149a473
Remove incorrect check 2020-05-28 07:06:01 +02:00
b80b3bf6d6
Assume private predicates always 2020-05-28 06:30:35 +02:00
d72e2af49a
Fix proof direction check 2020-05-28 06:30:14 +02:00
870fdd048c
Handle input predicates correctly 2020-05-28 06:29:57 +02:00
1e55f733d0
Minor clean-up 2020-05-28 05:03:57 +02:00
fe277b6773
Minor refactoring 2020-05-28 05:03:57 +02:00
1b827edd45
Clean-up 2020-05-28 05:03:56 +02:00
491a255811
Require supertight programs for backward proof 2020-05-28 05:03:56 +02:00
9b7895a032
Don’t append variable ID if there is only one 2020-05-22 19:43:41 +02:00
499fa0c667
Add option to specify output color choice 2020-05-22 19:33:06 +02:00
739cae1f7c
Rename “assert” statement to “spec” 2020-05-22 18:34:59 +02:00
116f74f63e
Minor clean-up 2020-05-22 18:17:00 +02:00
0578e99dc2
Finish basic simplifications 2020-05-22 18:14:56 +02:00
3b3f9017ba
Determine variable IDs correctly 2020-05-22 02:42:38 +02:00
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
b62c379b97
Properly handle input/output errors 2020-05-19 13:10:31 +02:00
efe354faad
Clean up unused struct 2020-05-19 13:02:12 +02:00
efa5656e39
Clean up unused struct 2020-05-19 13:01:04 +02:00
d88ac89b01
Add prime number example 2020-05-19 12:57:09 +02:00
86d2857494
Start implementation of simplifications 2020-05-19 12:56:46 +02:00
d77c7648b3
Ensure that statements are proven in right order 2020-05-19 12:56:21 +02:00
34b8dce9be
Ignore built-in predicates in completion 2020-05-19 12:54:51 +02:00
7020bc0bf0
Address unused variable 2020-05-19 12:53:37 +02:00
0229adef78
Add to-do notes 2020-05-19 12:49:57 +02:00
c1038b398c
Improve warning when using private predicates in specification 2020-05-19 12:47:24 +02:00
3bf981236a
Only warn if private predicates are used in specification 2020-05-19 12:18:11 +02:00
4de4cc21da
Fix gross bug in translation of division 2020-05-18 05:21:27 +02:00
80d39c8c0a
Check that only input/output predicates are used in specification 2020-05-18 02:17:30 +02:00
e2281042c9
Rename example files for consistency 2020-05-18 01:46:16 +02:00
ce51d14a9e
Minor formatting 2020-05-18 01:29:30 +02:00
58d89b4d07
Detect cyclic dependencies when hiding predicates 2020-05-18 01:19:59 +02:00
c0bfbc923c
Do not add type declarations for built-ins 2020-05-18 01:19:46 +02:00
0cce3bf54d
Rename status message for clarity 2020-05-18 01:19:00 +02:00
7361084eaf
Rename variable in example for consistency 2020-05-18 01:09:15 +02:00
82422cc28f
Support hiding auxiliary predicates 2020-05-13 08:02:04 +02:00
84031c483b
Revert logic for building completed definitions 2020-05-13 03:27:47 +02:00
b308847ebd
Add to-do note 2020-05-13 03:17:37 +02:00
d35d0d1d98
Use statement kind over section kind 2020-05-13 03:17:33 +02:00
0dbf30bb1b
Work in progress 2020-05-13 02:24:13 +02:00