Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet tuning file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system file | diff | annotate
Mon, 02 May 2011 17:43:42 +0200 wenzelm merged file | diff | annotate
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; file | diff | annotate
Mon, 02 May 2011 15:01:36 +0200 blanchet make "debug" more verbose and "verbose" less verbose file | diff | annotate
Mon, 02 May 2011 14:40:57 +0200 blanchet use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used file | diff | annotate
Mon, 02 May 2011 14:10:09 +0200 blanchet fixed random number invocation file | diff | annotate
Sun, 01 May 2011 22:36:58 +0200 blanchet use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow... file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet take "partial_types" option with a grain of salt file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet define type system in ATP module so that ATPs can suggest a type system file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet no needless "fequal" proxies if "explicit_apply" is set + always have readable names file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet make sure the minimizer monomorphizes when it should file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet reimplemented the hAPP introduction code so that it's done earlier, when the types are still available file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet move type declarations to the front, for TFF-compliance file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added (without implementation yet) new type encodings for Sledgehammer/ATP file | diff | annotate
Sun, 01 May 2011 18:37:23 +0200 blanchet get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables file | diff | annotate
Fri, 22 Apr 2011 00:57:59 +0200 blanchet iterate the unsound-fact-set removal process to recover even more unsound proofs file | diff | annotate
Fri, 22 Apr 2011 00:00:05 +0200 blanchet automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option file | diff | annotate
Thu, 21 Apr 2011 22:32:00 +0200 blanchet automatically retry with full-types upon unsound proof file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
Thu, 21 Apr 2011 21:14:06 +0200 blanchet tuning -- local semicolon consistency file | diff | annotate
Thu, 21 Apr 2011 18:51:22 +0200 blanchet tuning file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet fixed interaction between monomorphization and slicing for ATPs file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet cleanup: get rid of "may_slice" arguments without changing semantics file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet implemented general slicing for ATPs, especially E 1.2w and above file | diff | annotate
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Fri, 01 Apr 2011 13:21:21 +0200 blanchet remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428 file | diff | annotate
Fri, 01 Apr 2011 11:54:51 +0200 boehmes make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option file | diff | annotate
Thu, 31 Mar 2011 14:02:03 +0200 boehmes provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer) file | diff | annotate
Thu, 31 Mar 2011 11:16:54 +0200 blanchet start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode) file | diff | annotate
Thu, 31 Mar 2011 11:16:53 +0200 blanchet temporary workaround: filter out spurious monomorphic instances file | diff | annotate
Thu, 31 Mar 2011 11:16:52 +0200 blanchet added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default file | diff | annotate
Thu, 24 Mar 2011 17:49:27 +0100 blanchet more precise failure reporting in Sledgehammer/SMT file | diff | annotate
Tue, 22 Mar 2011 17:20:54 +0100 blanchet let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now file | diff | annotate
Tue, 22 Mar 2011 17:20:53 +0100 blanchet make Minimizer honor "verbose" and "debug" options better file | diff | annotate
Thu, 17 Mar 2011 11:18:31 +0100 blanchet add option to function to keep trivial ATP formulas, needed for some experiments file | diff | annotate
Sun, 13 Mar 2011 16:01:00 +0100 wenzelm Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype; file | diff | annotate
Mon, 21 Feb 2011 13:59:44 +0100 blanchet exit code 127 can mean many things -- not just (and probably not) Perl missing file | diff | annotate
Mon, 21 Feb 2011 10:31:48 +0100 blanchet give more weight to Frees than to Consts in relevance filter file | diff | annotate
Thu, 10 Feb 2011 10:09:38 +0100 blanchet make minimizer verbose file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices) file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet renamed field file | diff | annotate
Tue, 08 Feb 2011 16:10:10 +0100 blanchet available_provers ~> supported_provers (for clarity) file | diff | annotate
Tue, 08 Feb 2011 16:10:06 +0100 blanchet enable SMT weights and triggers, since they lead to slight improvements according to the Judgment Day suite file | diff | annotate
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); file | diff | annotate
Tue, 21 Dec 2010 04:33:17 +0100 blanchet proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; file | diff | annotate
Tue, 21 Dec 2010 03:56:51 +0100 blanchet added "smt_triggers" option to experiment with triggers in Sledgehammer; file | diff | annotate
Mon, 20 Dec 2010 14:55:24 +0100 blanchet run SPASS and Vampire in SOS mode only if >= 50 facts are passed -- otherwise we are probably minimizing and then it's better if the prover is run only once with a full strategy file | diff | annotate
Mon, 20 Dec 2010 14:09:45 +0100 blanchet remove spurious line file | diff | annotate
Mon, 20 Dec 2010 12:12:35 +0100 blanchet optionally supply constant weights to E -- turned off by default until properly parameterized file | diff | annotate
Fri, 17 Dec 2010 22:15:08 +0100 blanchet more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle file | diff | annotate
Fri, 17 Dec 2010 21:31:19 +0100 blanchet put the SMT weights back where they belong, so that they're also used by Mirabelle file | diff | annotate
Fri, 17 Dec 2010 15:30:43 +0100 blanchet run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers file | diff | annotate
Fri, 17 Dec 2010 12:10:08 +0100 blanchet make timeout part of the SMT filter's tail file | diff | annotate
less more (0) -60 tip
isabelle