patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
162 Commits 1 Branch 3 Tags
master
Commit Graph
162 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
patrick a81da75306 Add graph coloring example 2020-06-12 23:03:58 +02:00
patrick 57e4a9f145 Version bump for release v0.4.0-beta.3 v0.4.0-beta.3 2020-06-11 18:58:43 +02:00
patrick 6fa4645683 Add final lemmas as used in the paper 2020-06-06 06:50:28 +02:00
patrick 3812d1302e Rework example 2 2020-06-05 19:01:32 +02:00
patrick 6ca579735b Add simplification rule 2020-06-05 18:58:14 +02:00
patrick b29422cfbf Format exact cover example like in paper 2020-06-05 18:54:17 +02:00
patrick f9dbe54918 Improve wording in status output 2020-06-05 18:50:27 +02:00
patrick 8c801426a5 Allow U, V, and W for program variables 2020-06-05 18:50:09 +02:00
patrick 789cb4f8f8 Example 2 as proven with Vladimir 2020-06-02 00:57:49 +02:00
patrick bd108886dd Version bump for release 0.4.0-beta.2 v0.4.0-beta.2 2020-05-29 20:05:30 +02:00
patrick 12688a7bbe Make bidirectional proof the default 2020-05-29 19:52:30 +02:00
patrick 68dba77156 Clean up example 2020-05-29 19:00:44 +02:00
patrick 5d931ab7e6 Split lemmas from specifications 2020-05-29 19:00:36 +02:00
patrick f169931eac Accept more than one specification file 2020-05-29 18:54:47 +02:00
patrick 27fff47c91 Minor refactoring 2020-05-29 18:42:14 +02:00
patrick fc34aadf90 Show all predicates used in specification by default 2020-05-29 18:41:16 +02:00
patrick 4ec8bb56b9 Improve error message 2020-05-29 17:43:02 +02:00
patrick 9b6632cc94 Check that only input predicates are used in assumptions 2020-05-29 17:42:05 +02:00
patrick 93db8d02b5 Implement tightness check 2020-05-29 14:57:00 +02:00
patrick b94ee5134a Improve examples after meeting 2020-05-29 12:09:28 +02:00
patrick dab121c684 Use 4 cores by default (to be improved) 2020-05-28 18:41:47 +02:00
patrick 7895bf83c4 Clean-up in example 2 2020-05-28 18:40:33 +02:00
patrick c05eb11855 Improve example 2 2020-05-28 18:40:10 +02:00
patrick e686575ebf Only forbid private predicates in spec statements 2020-05-28 18:37:56 +02:00
patrick e57a1859d2 Fix supertightness check 2020-05-28 18:37:34 +02:00
patrick b52ca236e2 Handle private predicates in specification 2020-05-28 07:27:29 +02:00
patrick bd9e0bd709 Simplify examples 2020-05-28 07:06:19 +02:00
patrick c3b149a473 Remove incorrect check 2020-05-28 07:06:01 +02:00
patrick b80b3bf6d6 Assume private predicates always 2020-05-28 06:30:35 +02:00
patrick d72e2af49a Fix proof direction check 2020-05-28 06:30:14 +02:00
patrick 870fdd048c Handle input predicates correctly 2020-05-28 06:29:57 +02:00
patrick 1e55f733d0 Minor clean-up 2020-05-28 05:03:57 +02:00
patrick fe277b6773 Minor refactoring 2020-05-28 05:03:57 +02:00
patrick 1b827edd45 Clean-up 2020-05-28 05:03:56 +02:00
patrick 491a255811 Require supertight programs for backward proof 2020-05-28 05:03:56 +02:00
patrick 9b7895a032 Don’t append variable ID if there is only one 2020-05-22 19:43:41 +02:00
patrick 499fa0c667 Add option to specify output color choice 2020-05-22 19:33:06 +02:00
patrick 739cae1f7c Rename “assert” statement to “spec” 2020-05-22 18:34:59 +02:00
patrick 116f74f63e Minor clean-up 2020-05-22 18:17:00 +02:00
patrick 0578e99dc2 Finish basic simplifications 2020-05-22 18:14:56 +02:00
patrick 3b3f9017ba Determine variable IDs correctly 2020-05-22 02:42:38 +02:00
patrick 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 b62c379b97 Properly handle input/output errors 2020-05-19 13:10:31 +02:00
patrick efe354faad Clean up unused struct 2020-05-19 13:02:12 +02:00
patrick efa5656e39 Clean up unused struct 2020-05-19 13:01:04 +02:00
patrick d88ac89b01 Add prime number example 2020-05-19 12:57:09 +02:00
patrick 86d2857494 Start implementation of simplifications 2020-05-19 12:56:46 +02:00
patrick d77c7648b3 Ensure that statements are proven in right order 2020-05-19 12:56:21 +02:00
patrick 34b8dce9be Ignore built-in predicates in completion 2020-05-19 12:54:51 +02:00
patrick 7020bc0bf0 Address unused variable 2020-05-19 12:53:37 +02:00