| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
veriT changes for lifted terms, and ite_elim rules.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Subproofs for the SMT solver veriT.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
Skolemization support for leo-II and Zipperposition.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
refined filter for ATP steps to avoid 'have True' steps in E proofs
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
supports gradual skolemization (cf. Z3) by threading context through correctly
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
given two one-liners, only show the best of the two
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:22 +0200 |
blanchet |
don't generate Isar proof skeleton for what amounts to a one-line proof
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Thu, 22 May 2014 05:23:50 +0200 |
blanchet |
properly reconstruct helpers in Z3 proofs
|
file |
diff |
annotate
|
| Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 16 May 2014 19:14:00 +0200 |
blanchet |
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
|
file |
diff |
annotate
|
| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
use 'simp add:' syntax in Sledgehammer rather than 'using'
|
file |
diff |
annotate
|
| Sun, 04 May 2014 19:01:36 +0200 |
blanchet |
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:44:11 +0100 |
blanchet |
consolidate consecutive steps that prove the same formula
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:15:46 +0100 |
blanchet |
undo rewrite rules (e.g. for 'fun_app') in Isar
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:05:45 +0100 |
blanchet |
debugging stuff
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:05:44 +0100 |
blanchet |
more simplification of trivial steps
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 11:05:37 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
simplified preplaying information
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 10:12:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
more generous Isar proof compression -- try to remove failing steps
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
do a second phase of proof compression after minimization
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 23:59:36 +0100 |
blanchet |
rationalized lists of methods
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 23:49:01 +0100 |
blanchet |
extended method list
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
generate comments in Isar proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
tuned behavior of 'smt' option
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
proper fresh name generation
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 13:37:23 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 11:58:38 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 11:37:48 +0100 |
blanchet |
tuned data structure
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
less aggressive evaluation
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
added a new version of 'metis' to the mix
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
implemented new 'try0_isar' semantics
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
got rid of 'try0' step that is now redundant
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
centralize more preplaying
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
centralize preplaying
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
tuned
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
more data structure rationalization
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
more data structure rationalization
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
rationalized threading of 'metis' arguments
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
refactored data structure (step 3)
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
unform treatment of preplay_timeout = 0 and > 0
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
use Skolem proof methods appropriately
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 19:16:41 +0100 |
blanchet |
generalized preplaying infrastructure to store various results for various methods
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 18:43:16 +0100 |
blanchet |
added a 'trace' option
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 18:43:16 +0100 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 18:43:16 +0100 |
blanchet |
added 'algebra' to the mix
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 18:43:16 +0100 |
blanchet |
more informative trace
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:41:54 +0100 |
blanchet |
better tracing + syntactically correct 'metis' calls
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:26:43 +0100 |
blanchet |
tuned ML function names
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:07:20 +0100 |
blanchet |
moved ML code around
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
| base
|
| Thu, 30 Jan 2014 14:37:53 +0100 |
blanchet |
renamed Sledgehammer options for symmetry between positive and negative versions
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 13:43:21 +0100 |
blanchet |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 12:29:29 +0100 |
blanchet |
fixed spying so that the envirnoment variables are queried at run-time not at build-time
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 01:34:34 +0200 |
blanchet |
added comment
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 15:31:18 +0200 |
blanchet |
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 11:52:10 +0200 |
blanchet |
run fewer provers in "try" mode
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 11:28:28 +0200 |
blanchet |
count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
merged "isar_try0" and "isar_minimize" options
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hardcoded obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hard-coded an obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
use configuration mechanism for low-level tracing
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
tuning (use a blacklist instead of a whitelist)
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 23:03:21 +0200 |
blanchet |
fixed subtle bug with "take" + thread overlord through
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 16:03:13 +0200 |
blanchet |
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 22:45:48 +0200 |
wenzelm |
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 22:15:45 +0200 |
wenzelm |
some protocol to determine provers according to ML;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 19:54:16 +0200 |
wenzelm |
always enable "minimize" to simplify interaction model;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 19:13:28 +0200 |
wenzelm |
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 12:21:25 +0200 |
wenzelm |
eliminated pointless subgoal argument;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 12:13:53 +0200 |
wenzelm |
more direct sledgehammer configuration via mode = Normal_Result and output_result;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:57:51 +0200 |
wenzelm |
clarified Query_Operation.register: avoid hard-wired parallel policy;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 14:24:21 +0200 |
wenzelm |
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 21:02:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 00:50:49 +0200 |
wenzelm |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 23:45:05 +0200 |
wenzelm |
system options for Isabelle/HOL proof tools;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:45:06 +0200 |
smolkas |
completely rewrote SH compress; added two parameters for experimentation/fine grained control
|
file |
diff |
annotate
|
| Tue, 11 Jun 2013 16:13:19 -0400 |
smolkas |
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
added compatibility alias
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 23:00:17 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 22:30:24 +0200 |
wenzelm |
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 20:22:46 +0200 |
wenzelm |
maintain ProofGeneral preferences within ProofGeneral module;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:39:41 +0200 |
wenzelm |
just one ProofGeneral module;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
added preplay tracing
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 17:58:07 +0100 |
wenzelm |
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 14:10:51 +0100 |
blanchet |
minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 09:58:28 +0100 |
blanchet |
fixed typo in option name
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
alias for people like me
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:26 +0100 |
blanchet |
killed legacy alias
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 14:35:28 +0100 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 13:57:51 +0100 |
smolkas |
set show_markup to false in order to avoid problems in jedit
|
file |
diff |
annotate
|