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/SMT/smt_systems.ML
Fri, 16 Feb 2024 09:24:45 +0100 blanchet Distinguish two versions of cvc5 -- one used for Sledgehammer, one for proof reconstruction in SMT. provided by Mathias Fleury file | diff | annotate
Mon, 19 Jun 2023 22:28:09 +0200 Mathias Fleury early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals; file | diff | annotate
Wed, 15 Feb 2023 10:56:23 +0100 blanchet added refute mode to Sledgehammer to find 'counterexamples' file | diff | annotate
Mon, 22 Aug 2022 06:27:28 +0200 Mathias Fleury remove duplicate parsing for alethe; fix skolemization; file | diff | annotate
Wed, 17 Aug 2022 15:09:53 +0200 blanchet tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s file | diff | annotate
Fri, 12 Aug 2022 15:35:07 +0200 blanchet added support for cvc5 (whose interface is almost identical to CVC4) file | diff | annotate
Fri, 25 Mar 2022 13:52:23 +0100 blanchet first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size' file | diff | annotate
Mon, 14 Mar 2022 07:12:48 +0100 Mathias Fleury split veriT reconstruction into Lethe and veriT part file | diff | annotate
Mon, 07 Feb 2022 15:26:22 +0100 blanchet added possibility of extra options to SMT slices file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet crude implementation of centralized slicing file | diff | annotate
Wed, 17 Nov 2021 15:09:10 +0100 fleury generate problems with correct logic for veriT file | diff | annotate
Thu, 04 Nov 2021 16:50:03 +0100 Mathias Fleury proper support of verit's return code for timeout file | diff | annotate
Tue, 19 Oct 2021 11:48:31 +0200 desharna proper veriT --max-time option file | diff | annotate
Thu, 07 Oct 2021 10:16:52 +0200 desharna added timeout to veriT file | diff | annotate
Mon, 19 Jul 2021 14:47:52 +0200 blanchet removed setup for outdated CVC3 from Isabelle file | diff | annotate
Fri, 05 Mar 2021 20:38:55 +0100 wenzelm clarified smt: support Timeout.ignored and Timeout.scale_time; file | diff | annotate
Fri, 08 Jan 2021 20:38:46 +0100 Mathias Fleury ignore error messages produced by CVC4 when generating BV file | diff | annotate
Fri, 13 Nov 2020 09:47:59 +0100 desharna Add support for CVC4 1.8 to Sledgehammer file | diff | annotate
Thu, 15 Oct 2020 18:17:57 +0200 Mathias Fleury remove unsupported max-time option from veriT calls file | diff | annotate
Thu, 15 Oct 2020 13:47:55 +0200 wenzelm proper support for Windows exe; file | diff | annotate
Thu, 15 Oct 2020 13:24:16 +0200 wenzelm proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT; file | diff | annotate
Mon, 12 Oct 2020 18:59:44 +0200 Mathias Fleury add reconstruction for the SMT solver veriT file | diff | annotate
Fri, 07 Jun 2019 11:08:29 +0200 blanchet handle timeouts gracefully in 'smt' proof method (patch due to Mathias Fleury) file | diff | annotate
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches; file | diff | annotate
Tue, 30 Oct 2018 16:24:04 +0100 fleury add reconstruction by veriT in method smt file | diff | annotate
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix; file | diff | annotate
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings; file | diff | annotate
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources file | diff | annotate
Tue, 29 Aug 2017 18:30:23 +0200 blanchet towards support for HO SMT-LIB file | diff | annotate
Fri, 04 Nov 2016 15:22:12 +0100 blanchet disable CVC4 statistics, and hence crashes upon user interruptions file | diff | annotate
Fri, 20 May 2016 07:54:54 +0200 fleury better handling of veriT's 'unknown' status file | diff | annotate
Tue, 10 Nov 2015 17:49:54 +0100 fleury fixing premises in veriT proof reconstruction file | diff | annotate
Thu, 05 Nov 2015 11:59:45 +0100 fleury updating options to verit file | diff | annotate
Sat, 25 Apr 2015 09:48:06 +0200 blanchet made CVC4 support work also without unsat cores file | diff | annotate
Wed, 08 Apr 2015 18:47:38 +0200 blanchet updated SMT module and Sledgehammer to fully open source Z3 file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names file | diff | annotate
Wed, 19 Nov 2014 10:31:15 +0100 blanchet parse CVC4 unsat cores file | diff | annotate
Tue, 30 Sep 2014 14:19:25 +0200 blanchet give more facts to veriT -- it seems to be able to cope with them file | diff | annotate
Tue, 30 Sep 2014 11:34:20 +0200 blanchet tuning file | diff | annotate
Wed, 17 Sep 2014 16:53:39 +0200 blanchet added interface for CVC4 extensions file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate | base
less more (0) tip
isabelle