#
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
#
9a9c6320 |
|
17-Jul-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: various crunch improvements The main one is that crunch now uses wpsimp when determining whether a goal can already be solved, instead of just wp. Crunch can also now use wps when proving a goal and will now always ignore a constant if told to, even if it is the top-level constant being crunched.
|
#
95ddba3d |
|
14-Apr-2019 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improve the parser for crunch. The main benefit of this is that everything in crunch is now ctrl clickable. As an added benefit, supplied rules can now be modified by attributes when needed.
|
#
d77d31a7 |
|
03-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
#
55d20591 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: improved crunch The main aim of this is for crunch to make consistent decisions about whether to prove new rules. If any rules in the wp set can be used to directly solve the goal crunch is working on, then crunch will just use it. Other changes include: - crunch_ignore works properly inside locales again. - if a rule already exists with the specific name crunch is going to use, but that rule does not solve the goal crunch is working on then crunch will now error. - if crunch fails to prove a goal it will now output a warning if adding crunch_simps or crunch_wps would allow it to make more progess.
|
#
d2f38a0a |
|
31-Jan-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: Add multi-crunch command 'crunches'. It's just a parser tweak for crunch, and runs multiple crunch commands with the same sections (wps, ignores, etc). Also update the comments a little, and move them closer to the anchor of command clicks (the @{command_keyword} antiquotation).
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
9a1ec71a |
|
23-Aug-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
Refactor of crunch. Substantial adjustments to crunch. Main user changes are: - 'lift' and 'unfold' mechanisms replaced by more general 'rule'. - some more 'ignores' standardised. - crunch has a more principled overall design: + discover crunch rule * provided or by definition extraction + recurse according to rule + prove goal based on rule, recursive discoveries, standard tactic * wp/simp adjustments tweak tactic
|
#
a2cc6ab3 |
|
11-Nov-2015 |
Corey Lewis <corey.lewis@nicta.com.au> |
Added wp_del and simp_del arguments to crunch.
|
#
17826f9b |
|
18-Apr-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
more Isabelle2015 update; AInvs up to (excluding) Syscall_AI also includes some global replacements
|
#
e8d1ed6d |
|
09-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
ported lib/* theories to Isabelle2014-RC0
|
#
50dda770 |
|
22-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
comment cleanup
|
#
84595f42 |
|
17-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
release cleanup
|
#
2a03e81d |
|
14-Jul-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Import release snapshot.
|