Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT.thy
Fri, 23 Feb 2024 09:11:31 +0100 blanchet new less ad hoc implementation of the 'moura' tactic for skolemization file | diff | annotate
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
Fri, 19 Jan 2024 13:56:26 +0100 Mathias Fleury fix reconstruction of Alethe's and_pos rule file | diff | annotate
Thu, 09 Nov 2023 15:11:51 +0000 haftmann weakened dependency 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
Fri, 09 Sep 2022 21:28:35 +0200 haftmann less specialized euclidean relation on int file | diff | annotate
Mon, 22 Aug 2022 06:27:28 +0200 Mathias Fleury remove duplicate parsing for alethe; fix skolemization; file | diff | annotate
Sun, 21 Aug 2022 06:18:23 +0000 haftmann simplified computation algorithm construction 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
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
Tue, 09 Nov 2021 19:17:47 +0100 wenzelm tuned text; 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:52:08 +0100 wenzelm more direct unlimited smt_timeout; file | diff | annotate
Wed, 28 Oct 2020 08:41:07 +0100 Mathias Fleury better handling of skolemization for Isar reconstruction in Sledgehammer for veriT file | diff | annotate
Mon, 12 Oct 2020 18:59:44 +0200 Mathias Fleury add reconstruction for the SMT solver veriT file | diff | annotate
Wed, 30 Sep 2020 18:37:22 +0200 desharna Effectively disable timeout for smt method/tactic file | diff | annotate
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches; file | diff | annotate
Tue, 30 Oct 2018 16:24:04 +0100 fleury add reconstruction by veriT in method smt file | diff | annotate
Tue, 30 Oct 2018 16:24:01 +0100 fleury split SMT reconstruction into library file | diff | annotate
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment file | diff | annotate
Wed, 11 Apr 2018 10:59:13 +0200 boehmes avoid adding unnecessary quantified lemmas when embedding natural number terms into integer terms: quantified lemmas can cause Z3 to produce complex proofs that are hard to replay in Isabelle file | diff | annotate
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources file | diff | annotate
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols; file | diff | annotate
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization file | diff | annotate
Wed, 30 Aug 2017 23:36:21 +0200 blanchet added options to make veriT more complete file | diff | annotate
Tue, 29 Aug 2017 18:30:23 +0200 blanchet towards support for HO SMT-LIB file | diff | annotate
Thu, 03 Aug 2017 23:43:17 +0200 blanchet pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better file | diff | annotate
Fri, 28 Jul 2017 15:36:32 +0100 blanchet introduced option for nat-as-int in SMT file | diff | annotate
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t; file | diff | annotate
Tue, 10 Nov 2015 23:41:20 +0100 wenzelm recovered from a9c0572109af; file | diff | annotate
Tue, 10 Nov 2015 17:49:54 +0100 fleury fixing premises in veriT proof reconstruction file | diff | annotate
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches; 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
Fri, 16 Jan 2015 23:23:31 +0100 boehmes more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet added one more CVC4 option that helps Judgment Day (10 theory version) file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet added Z3 reconstruction rule suggested by F. Maric file | diff | annotate
Mon, 24 Nov 2014 12:35:13 +0100 blanchet one more CVC4 option that helps 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
Thu, 20 Nov 2014 17:29:18 +0100 blanchet added CVC4 option that helps on JD file | diff | annotate
Thu, 20 Nov 2014 17:29:18 +0100 blanchet removed explicit '--quant-cf' option to CVC4, now that it's the default file | diff | annotate
Wed, 19 Nov 2014 10:31:15 +0100 blanchet parse CVC4 unsat cores file | diff | annotate
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section; file | diff | annotate
Fri, 24 Oct 2014 15:07:51 +0200 hoelzl use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating file | diff | annotate
Mon, 06 Oct 2014 19:19:16 +0200 blanchet strengthened 'moura' method file | diff | annotate
Mon, 29 Sep 2014 14:32:30 +0200 blanchet made 'moura' tactic more powerful file | diff | annotate
Thu, 25 Sep 2014 13:30:57 +0200 blanchet added useful options to CVC4 file | diff | annotate
Wed, 17 Sep 2014 16:53:39 +0200 blanchet added interface for CVC4 extensions file | diff | annotate
Thu, 28 Aug 2014 16:58:26 +0200 blanchet tuned method description file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate | base
Sat, 16 Aug 2014 18:31:47 +0200 wenzelm updated to named_theorems; file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet reduces Sledgehammer dependencies file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet tuning file | diff | annotate
Thu, 12 Jun 2014 01:00:49 +0200 blanchet use 'ctr_sugar' abstraction in SMT(2) file | diff | annotate
Wed, 11 Jun 2014 11:28:46 +0200 blanchet fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle file | diff | annotate
Tue, 11 Mar 2014 15:34:38 +0100 blanchet full path file | diff | annotate
Sun, 19 Jan 2014 22:38:17 +0100 boehmes removed obsolete remote_cvc3 and remote_z3 file | diff | annotate
Mon, 13 Jan 2014 20:20:44 +0100 wenzelm activation of Z3 via "z3_non_commercial" system option (without requiring restart); file | diff | annotate
less more (0) -100 -60 tip
isabelle