162 Commits (master)
 

Author SHA1 Message Date
Patrick Lühne a81da75306
Add graph coloring example 1 year ago
Patrick Lühne 57e4a9f145
Version bump for release v0.4.0-beta.3 1 year ago
Patrick Lühne 6fa4645683
Add final lemmas as used in the paper 1 year ago
Patrick Lühne 3812d1302e
Rework example 2 1 year ago
Patrick Lühne 6ca579735b
Add simplification rule 1 year ago
Patrick Lühne b29422cfbf
Format exact cover example like in paper 1 year ago
Patrick Lühne f9dbe54918
Improve wording in status output 1 year ago
Patrick Lühne 8c801426a5
Allow U, V, and W for program variables 1 year ago
Patrick Lühne 789cb4f8f8
Example 2 as proven with Vladimir 1 year ago
Patrick Lühne bd108886dd
Version bump for release 0.4.0-beta.2 1 year ago
Patrick Lühne 12688a7bbe
Make bidirectional proof the default 1 year ago
Patrick Lühne 68dba77156
Clean up example 1 year ago
Patrick Lühne 5d931ab7e6
Split lemmas from specifications 1 year ago
Patrick Lühne f169931eac
Accept more than one specification file 1 year ago
Patrick Lühne 27fff47c91
Minor refactoring 1 year ago
Patrick Lühne fc34aadf90
Show all predicates used in specification by default 1 year ago
Patrick Lühne 4ec8bb56b9
Improve error message 1 year ago
Patrick Lühne 9b6632cc94
Check that only input predicates are used in assumptions 1 year ago
Patrick Lühne 93db8d02b5
Implement tightness check 1 year ago
Patrick Lühne b94ee5134a
Improve examples after meeting 1 year ago
Patrick Lühne dab121c684
Use 4 cores by default (to be improved) 1 year ago
Patrick Lühne 7895bf83c4
Clean-up in example 2 1 year ago
Patrick Lühne c05eb11855
Improve example 2 1 year ago
Patrick Lühne e686575ebf
Only forbid private predicates in spec statements 1 year ago
Patrick Lühne e57a1859d2
Fix supertightness check 1 year ago
Patrick Lühne b52ca236e2
Handle private predicates in specification 1 year ago
Patrick Lühne bd9e0bd709
Simplify examples 1 year ago
Patrick Lühne c3b149a473
Remove incorrect check 1 year ago
Patrick Lühne b80b3bf6d6
Assume private predicates always 1 year ago
Patrick Lühne d72e2af49a
Fix proof direction check 1 year ago
Patrick Lühne 870fdd048c
Handle input predicates correctly 1 year ago
Patrick Lühne 1e55f733d0
Minor clean-up 1 year ago
Patrick Lühne fe277b6773
Minor refactoring 1 year ago
Patrick Lühne 1b827edd45
Clean-up 1 year ago
Patrick Lühne 491a255811
Require supertight programs for backward proof 1 year ago
Patrick Lühne 9b7895a032
Don’t append variable ID if there is only one 1 year ago
Patrick Lühne 499fa0c667
Add option to specify output color choice 1 year ago
Patrick Lühne 739cae1f7c
Rename “assert” statement to “spec” 1 year ago
Patrick Lühne 116f74f63e
Minor clean-up 1 year ago
Patrick Lühne 0578e99dc2
Finish basic simplifications 1 year ago
Patrick Lühne 3b3f9017ba
Determine variable IDs correctly 1 year ago
Patrick Lühne 81ddfd450a
Use custom foliage flavor 1 year ago
Patrick Lühne b62c379b97
Properly handle input/output errors 1 year ago
Patrick Lühne efe354faad
Clean up unused struct 1 year ago
Patrick Lühne efa5656e39
Clean up unused struct 1 year ago
Patrick Lühne d88ac89b01
Add prime number example 1 year ago
Patrick Lühne 86d2857494
Start implementation of simplifications 1 year ago
Patrick Lühne d77c7648b3
Ensure that statements are proven in right order 1 year ago
Patrick Lühne 34b8dce9be
Ignore built-in predicates in completion 1 year ago
Patrick Lühne 7020bc0bf0
Address unused variable 1 year ago