a81da75306
Add graph coloring example
2020-06-12 23:03:58 +02:00
57e4a9f145
Version bump for release v0.4.0-beta.3
2020-06-11 18:58:43 +02:00
6fa4645683
Add final lemmas as used in the paper
2020-06-06 06:50:28 +02:00
3812d1302e
Rework example 2
2020-06-05 19:01:32 +02:00
6ca579735b
Add simplification rule
2020-06-05 18:58:14 +02:00
b29422cfbf
Format exact cover example like in paper
2020-06-05 18:54:17 +02:00
f9dbe54918
Improve wording in status output
2020-06-05 18:50:27 +02:00
8c801426a5
Allow U, V, and W for program variables
2020-06-05 18:50:09 +02:00
789cb4f8f8
Example 2 as proven with Vladimir
2020-06-02 00:57:49 +02:00
bd108886dd
Version bump for release 0.4.0-beta.2
2020-05-29 20:05:30 +02:00
12688a7bbe
Make bidirectional proof the default
2020-05-29 19:52:30 +02:00
68dba77156
Clean up example
2020-05-29 19:00:44 +02:00
5d931ab7e6
Split lemmas from specifications
2020-05-29 19:00:36 +02:00
f169931eac
Accept more than one specification file
2020-05-29 18:54:47 +02:00
27fff47c91
Minor refactoring
2020-05-29 18:42:14 +02:00
fc34aadf90
Show all predicates used in specification by default
2020-05-29 18:41:16 +02:00
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
