Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
Tue, 22 Feb 2022 15:00:04 +0100 blanchet have Sledgehammer honor 'smt_nat_as_int' option file | diff | annotate
Wed, 09 Feb 2022 14:52:05 +0100 desharna uniformized fact selection for ATP and SMT in Sledgehammer file | diff | annotate
Wed, 09 Feb 2022 13:02:59 +0100 desharna used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer file | diff | annotate
Mon, 07 Feb 2022 15:26:22 +0100 blanchet added possibility of extra options to SMT slices file | diff | annotate
Wed, 02 Feb 2022 13:43:48 +0100 blanchet more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweaked Auto Sledgehammer's behavior and output file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet run all installed provers by default file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet tweaked verbose output file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet rationalize slicing format file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet thread slices through file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet changed logic of 'slice' option to 'slices' file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet rationalized output for forthcoming slicing model file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet disable slicing within SMT (in preparation for factoring it out) file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet generalized the 'slice' option towards more flexible slicing file | diff | annotate
Wed, 17 Nov 2021 19:52:17 +0100 desharna added support for higher-order SMT proof search in Sledgehammer file | diff | annotate
Tue, 01 Dec 2020 15:29:54 +0100 desharna tuned proof preplay to explicitly refer to Z3 backend file | diff | annotate
Thu, 29 Oct 2020 16:07:41 +0100 desharna Added smt (verit) to Sledgehammer's proof preplay. file | diff | annotate
Thu, 08 Oct 2020 17:02:56 +0200 desharna tune filename file | diff | annotate
Wed, 10 Jun 2020 15:55:41 +0200 blanchet simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais) file | diff | annotate
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches; file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends file | diff | annotate
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations; file | diff | annotate
Mon, 28 Mar 2016 12:05:47 +0200 blanchet early warning when Sledgehammer finds a proof file | diff | annotate
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules; file | diff | annotate
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala; file | diff | annotate
Sat, 25 Apr 2015 09:48:06 +0200 blanchet made CVC4 support work also without unsat cores file | diff | annotate
Thu, 20 Nov 2014 17:29:18 +0100 blanchet other way of crashing (with CVC4) file | diff | annotate
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message; file | diff | annotate
Tue, 30 Sep 2014 14:54:14 +0200 blanchet tuned output in case of one-liner failure file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate | base
Thu, 12 Jun 2014 17:02:03 +0200 blanchet reintroduced vital 'Thm.transfer' file | diff | annotate
Fri, 23 May 2014 14:12:22 +0200 blanchet removed noise 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
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer 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
Mon, 03 Feb 2014 23:38:33 +0100 blanchet properly overwrite replay data from one compression iteration to another 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 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:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' 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 12:30:54 +0100 blanchet refactor large ML file file | diff | annotate
less more (0) tip
isabelle