patrick
/
anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
162 Commits 1 Branch 3 Tags 380 KiB
Commit Graph

162 Commits

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