Commit Graph

Select branches

Hide Pull Requests

master

v0.4.0-beta.1

v0.4.0-beta.2

v0.4.0-beta.3

Mono Color

• a81da75306
  
  Add graph coloring example master Patrick Lühne 2020-06-12 23:03:58 +0200
• 57e4a9f145
  
  Version bump for release v0.4.0-beta.3 v0.4.0-beta.3 Patrick Lühne 2020-06-11 18:58:43 +0200
• 6fa4645683
  
  Add final lemmas as used in the paper Patrick Lühne 2020-06-06 06:50:28 +0200
• 3812d1302e
  
  Rework example 2 Patrick Lühne 2020-06-05 19:01:32 +0200
• 6ca579735b
  
  Add simplification rule Patrick Lühne 2020-06-05 18:58:14 +0200
• b29422cfbf
  
  Format exact cover example like in paper Patrick Lühne 2020-06-05 18:54:17 +0200
• f9dbe54918
  
  Improve wording in status output Patrick Lühne 2020-06-05 18:50:27 +0200
• 8c801426a5
  
  Allow U, V, and W for program variables Patrick Lühne 2020-06-05 18:50:09 +0200
• 789cb4f8f8
  
  Example 2 as proven with Vladimir Patrick Lühne 2020-06-02 00:57:49 +0200
• bd108886dd
  
  Version bump for release 0.4.0-beta.2 v0.4.0-beta.2 Patrick Lühne 2020-05-29 20:05:30 +0200
• 12688a7bbe
  
  Make bidirectional proof the default Patrick Lühne 2020-05-29 19:52:30 +0200
• 68dba77156
  
  Clean up example Patrick Lühne 2020-05-29 19:00:44 +0200
• 5d931ab7e6
  
  Split lemmas from specifications Patrick Lühne 2020-05-29 18:59:16 +0200
• f169931eac
  
  Accept more than one specification file Patrick Lühne 2020-05-29 18:53:42 +0200
• 27fff47c91
  
  Minor refactoring Patrick Lühne 2020-05-29 18:42:14 +0200
• fc34aadf90
  
  Show all predicates used in specification by default Patrick Lühne 2020-05-29 18:36:58 +0200
• 4ec8bb56b9
  
  Improve error message Patrick Lühne 2020-05-29 17:43:02 +0200
• 9b6632cc94
  
  Check that only input predicates are used in assumptions Patrick Lühne 2020-05-29 17:42:05 +0200
• 93db8d02b5
  
  Implement tightness check Patrick Lühne 2020-05-29 14:57:00 +0200
• b94ee5134a
  
  Improve examples after meeting Patrick Lühne 2020-05-29 12:09:28 +0200
• dab121c684
  
  Use 4 cores by default (to be improved) Patrick Lühne 2020-05-28 18:41:47 +0200
• 7895bf83c4
  
  Clean-up in example 2 Patrick Lühne 2020-05-28 18:40:33 +0200
• c05eb11855
  
  Improve example 2 Patrick Lühne 2020-05-28 18:40:10 +0200
• e686575ebf
  
  Only forbid private predicates in spec statements Patrick Lühne 2020-05-28 18:37:56 +0200
• e57a1859d2
  
  Fix supertightness check Patrick Lühne 2020-05-28 18:37:34 +0200
• b52ca236e2
  
  Handle private predicates in specification Patrick Lühne 2020-05-28 07:27:29 +0200
• bd9e0bd709
  
  Simplify examples Patrick Lühne 2020-05-28 07:06:19 +0200
• c3b149a473
  
  Remove incorrect check Patrick Lühne 2020-05-28 07:06:01 +0200
• b80b3bf6d6
  
  Assume private predicates always Patrick Lühne 2020-05-28 06:30:35 +0200
• d72e2af49a
  
  Fix proof direction check Patrick Lühne 2020-05-28 06:30:14 +0200
• 870fdd048c
  
  Handle input predicates correctly Patrick Lühne 2020-05-28 06:29:57 +0200
• 1e55f733d0
  
  Minor clean-up Patrick Lühne 2020-05-28 05:01:17 +0200
• fe277b6773
  
  Minor refactoring Patrick Lühne 2020-05-28 05:00:56 +0200
• 1b827edd45
  
  Clean-up Patrick Lühne 2020-05-28 04:58:24 +0200
• 491a255811
  
  Require supertight programs for backward proof Patrick Lühne 2020-05-28 04:54:42 +0200
• 9b7895a032
  
  Don’t append variable ID if there is only one Patrick Lühne 2020-05-22 19:43:41 +0200
• 499fa0c667
  
  Add option to specify output color choice Patrick Lühne 2020-05-22 19:33:06 +0200
• 739cae1f7c
  
  Rename “assert” statement to “spec” Patrick Lühne 2020-05-22 18:34:59 +0200
• 116f74f63e
  
  Minor clean-up Patrick Lühne 2020-05-22 18:17:00 +0200
• 0578e99dc2
  
  Finish basic simplifications Patrick Lühne 2020-05-22 18:14:56 +0200
• 3b3f9017ba
  
  Determine variable IDs correctly Patrick Lühne 2020-05-22 02:42:38 +0200
• 81ddfd450a
  
  Use custom foliage flavor Patrick Lühne 2020-05-22 02:25:00 +0200
• b62c379b97
  
  Properly handle input/output errors Patrick Lühne 2020-05-19 13:10:31 +0200
• efe354faad
  
  Clean up unused struct Patrick Lühne 2020-05-19 13:02:12 +0200
• efa5656e39
  
  Clean up unused struct Patrick Lühne 2020-05-19 13:01:04 +0200
• d88ac89b01
  
  Add prime number example Patrick Lühne 2020-05-19 12:57:09 +0200
• 86d2857494
  
  Start implementation of simplifications Patrick Lühne 2020-05-19 12:56:46 +0200
• d77c7648b3
  
  Ensure that statements are proven in right order Patrick Lühne 2020-05-19 12:56:21 +0200
• 34b8dce9be
  
  Ignore built-in predicates in completion Patrick Lühne 2020-05-19 12:54:51 +0200
• 7020bc0bf0
  
  Address unused variable Patrick Lühne 2020-05-19 12:53:37 +0200
• 0229adef78
  
  Add to-do notes Patrick Lühne 2020-05-19 12:49:57 +0200
• c1038b398c
  
  Improve warning when using private predicates in specification Patrick Lühne 2020-05-19 12:47:24 +0200
• 3bf981236a
  
  Only warn if private predicates are used in specification Patrick Lühne 2020-05-19 12:18:11 +0200
• 4de4cc21da
  
  Fix gross bug in translation of division Patrick Lühne 2020-05-18 05:21:27 +0200
• 80d39c8c0a
  
  Check that only input/output predicates are used in specification Patrick Lühne 2020-05-18 02:17:30 +0200
• e2281042c9
  
  Rename example files for consistency Patrick Lühne 2020-05-18 01:46:16 +0200
• ce51d14a9e
  
  Minor formatting Patrick Lühne 2020-05-18 01:29:30 +0200
• 58d89b4d07
  
  Detect cyclic dependencies when hiding predicates Patrick Lühne 2020-05-18 01:19:59 +0200
• c0bfbc923c
  
  Do not add type declarations for built-ins Patrick Lühne 2020-05-18 01:19:30 +0200
• 0cce3bf54d
  
  Rename status message for clarity Patrick Lühne 2020-05-18 01:19:00 +0200
• 7361084eaf
  
  Rename variable in example for consistency Patrick Lühne 2020-05-18 01:09:15 +0200
• 82422cc28f
  
  Support hiding auxiliary predicates Patrick Lühne 2020-05-13 07:41:01 +0200
• 84031c483b
  
  Revert logic for building completed definitions Patrick Lühne 2020-05-13 03:27:47 +0200
• b308847ebd
  
  Add to-do note Patrick Lühne 2020-05-13 03:17:37 +0200
• d35d0d1d98
  
  Use statement kind over section kind Patrick Lühne 2020-05-13 03:16:51 +0200
• 0dbf30bb1b
  
  Work in progress Patrick Lühne 2020-05-13 02:24:13 +0200
• 4d00fbeb97
  
  Minor formatting Patrick Lühne 2020-05-13 01:40:44 +0200
• 07fc6a7f85
  
  Add to-do note Patrick Lühne 2020-05-13 01:28:25 +0200
• 37f0fff09f
  
  Add comments to exact cover example Patrick Lühne 2020-05-12 06:39:50 +0200
• f39393ebce
  
  Add comments to example 2 Patrick Lühne 2020-05-12 06:10:59 +0200
• 9621cb1e0c
  
  Add to-do note Patrick Lühne 2020-05-12 06:10:52 +0200
• 8153352b66
  
  Support comments in specification file Patrick Lühne 2020-05-12 06:08:50 +0200
• e42fd92d4b
  
  Add parser support for output statements Patrick Lühne 2020-05-12 05:27:51 +0200
• 32b18e2b63
  
  Refactor parsing formulas Patrick Lühne 2020-05-12 05:20:48 +0200
• 2f48e51244
  
  Refactor parsing input statement terminator Patrick Lühne 2020-05-12 05:09:13 +0200
• 0d63a721c7
  
  Refactor parsing input statements Patrick Lühne 2020-05-12 05:05:49 +0200
• e5d8a8a96b
  
  Refactor parsing domain specifiers Patrick Lühne 2020-05-12 04:51:31 +0200
• 222f8b535e
  
  Add specification for example 1 Patrick Lühne 2020-05-12 04:33:52 +0200
• 9ffd987e10
  
  Add specification for example 0 Patrick Lühne 2020-05-12 04:28:11 +0200
• 7d06601c17
  
  Color output Patrick Lühne 2020-05-12 04:25:49 +0200
• 2de8a59b63
  
  New output format Patrick Lühne 2020-05-11 05:03:59 +0200
• eab3520e44
  
  Minor formatting Patrick Lühne 2020-05-11 04:14:17 +0200
• fed095ba5c
  
  Remove obsolete example Patrick Lühne 2020-05-11 04:09:52 +0200
• 78935f7c4a
  
  Remove unnecessary lemma Patrick Lühne 2020-05-11 04:08:38 +0200
• 674cee0e87
  
  Remove obsolete to-do note Patrick Lühne 2020-05-11 04:00:51 +0200
• 2ed1e6d89d
  
  Rename function Patrick Lühne 2020-05-11 04:00:06 +0200
• ab7c6d1828
  
  Rename ScopedFormula to OpenFormula Patrick Lühne 2020-05-11 03:58:30 +0200
• 2dff164d90
  
  Add to-do note Patrick Lühne 2020-05-11 03:54:32 +0200
• b5d049a82a
  
  Move InputConstantDeclarationDomains to problem module Patrick Lühne 2020-05-11 03:48:14 +0200
• e0b8b1c854
  
  Minor formatting Patrick Lühne 2020-05-11 03:46:20 +0200
• 0d51053b88
  
  Move ProofDirection type to separate module Patrick Lühne 2020-05-11 03:46:11 +0200
• 7c36c4b239
  
  Move closure functions to separate module Patrick Lühne 2020-05-11 03:41:33 +0200
• 0011fd9d4c
  
  Add to-do note Patrick Lühne 2020-05-11 03:40:27 +0200
• 2c660ff902
  
  Remove unused code Patrick Lühne 2020-05-11 03:39:09 +0200
• cede63b7e4
  
  Remove unused code Patrick Lühne 2020-05-11 03:37:57 +0200
• 7a6fab59ef
  
  Minor refactoring Patrick Lühne 2020-05-11 03:23:25 +0200
• 6bf01db51a
  
  Minor formatting Patrick Lühne 2020-05-11 03:21:51 +0200
• 7832f18ffd
  
  Minor reformatting Patrick Lühne 2020-05-11 03:18:11 +0200
• ee1539e2ab
  
  Rename variable for consistency Patrick Lühne 2020-05-11 03:12:50 +0200
• 17d2373e0d
  
  Refactor proof output Patrick Lühne 2020-05-11 03:11:10 +0200