| Wed, 08 Jun 2011 13:43:15 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 08 Jun 2011 11:59:45 +0200 |
boehmes |
only collect substituions neither seen before nor derived in the same refinement step
|
changeset |
files
|
| Wed, 08 Jun 2011 12:13:37 +0200 |
wenzelm |
updated imports (cf. 93b1183e43e5);
|
changeset |
files
|
| Wed, 08 Jun 2011 10:24:07 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
new Metis version
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
exploit new semantics of "max_new_instances"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
minor optimization
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly extensionalize
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
tuned
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed experimental code submitted by mistake
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
removed removed option from documentation
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
changeset |
files
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
slightly faster/cleaner accumulation of polymorphic consts
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
more conventional variable naming
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
dropped outdated/speculative historical comments;
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
less redundant tags
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
removed generation of instantiated pattern set, which is never actually used
|
changeset |
files
|
| Wed, 08 Jun 2011 00:01:20 +0200 |
krauss |
more precise type for obscure "prfx" field
|
changeset |
files
|
| Tue, 07 Jun 2011 21:37:40 +0200 |
boehmes |
clarified (and slightly modified) the semantics of max_new_instances
|
changeset |
files
|
| Tue, 07 Jun 2011 19:22:52 +0200 |
kleing |
use null_heap instead of %_. 0 to avoid printing problems
|
changeset |
files
|
| Tue, 07 Jun 2011 14:38:42 +0200 |
blanchet |
prioritize more relevant facts for monomorphization
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
workaround current "max_new_instances" semantics
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
fixed missing proof handling
|
changeset |
files
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
optimized the relevance filter a little bit
|
changeset |
files
|
| Tue, 07 Jun 2011 14:06:12 +0200 |
bulwahn |
printing environment in mutabelle's log
|
changeset |
files
|
| Tue, 07 Jun 2011 11:24:54 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 07 Jun 2011 11:24:16 +0200 |
bulwahn |
merged; manually merged IsaMakefile
|
changeset |
files
|
| Tue, 07 Jun 2011 11:12:05 +0200 |
bulwahn |
splitting Cset into Cset and List_Cset
|
changeset |
files
|
| Tue, 07 Jun 2011 11:11:01 +0200 |
bulwahn |
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:58 +0200 |
bulwahn |
adding examples with existentials
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:57 +0200 |
bulwahn |
renaming the formalisation of the birthday problem to a proper English name
|
changeset |
files
|
| Tue, 07 Jun 2011 11:10:42 +0200 |
bulwahn |
adding compilation that allows existentials in Quickcheck_Narrowing
|
changeset |
files
|
| Tue, 07 Jun 2011 11:13:52 +0200 |
blanchet |
move away from old SMT monomorphizer
|
changeset |
files
|
| Tue, 07 Jun 2011 11:12:52 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 07 Jun 2011 11:05:09 +0200 |
blanchet |
merged
|
changeset |
files
|
| Tue, 07 Jun 2011 11:04:17 +0200 |
blanchet |
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
|
changeset |
files
|
| Tue, 07 Jun 2011 10:46:09 +0200 |
blanchet |
removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
|
changeset |
files
|
| Tue, 07 Jun 2011 10:43:18 +0200 |
blanchet |
nicely thread monomorphism verbosity in Metis and Sledgehammer
|
changeset |
files
|
| Tue, 07 Jun 2011 10:24:16 +0200 |
boehmes |
clarified meaning of monomorphization configuration option by renaming it
|
changeset |
files
|
| Tue, 07 Jun 2011 08:58:23 +0200 |
blanchet |
documentation tweaks
|
changeset |
files
|
| Tue, 07 Jun 2011 08:52:35 +0200 |
blanchet |
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
|
changeset |
files
|
| Tue, 07 Jun 2011 07:57:24 +0200 |
blanchet |
fixed typo in legacy feature message
|
changeset |
files
|
| Tue, 07 Jun 2011 07:45:12 +0200 |
blanchet |
use new monomorphization code
|
changeset |
files
|
| Tue, 07 Jun 2011 07:44:54 +0200 |
blanchet |
added (currently unused) verbose configuration option
|
changeset |
files
|
| Tue, 07 Jun 2011 07:06:24 +0200 |
blanchet |
renamed ML function
|
changeset |
files
|
| Tue, 07 Jun 2011 07:04:53 +0200 |
blanchet |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
changeset |
files
|
| Tue, 07 Jun 2011 06:58:52 +0200 |
blanchet |
pass props not thms to ATP translator
|
changeset |
files
|
| Mon, 06 Jun 2011 23:46:02 +0200 |
blanchet |
slighly more reasonable Vampire slices (until new monomorphizer is used)
|
changeset |
files
|
| Mon, 06 Jun 2011 23:43:28 +0200 |
blanchet |
removed confusing slicing logic
|
changeset |
files
|
| Mon, 06 Jun 2011 23:26:40 +0200 |
blanchet |
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
|
changeset |
files
|
| Mon, 06 Jun 2011 23:11:14 +0200 |
blanchet |
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
|
changeset |
files
|
| Mon, 06 Jun 2011 22:03:58 +0200 |
blanchet |
minor: curly brackets, not square brackets
|
changeset |
files
|
| Mon, 06 Jun 2011 21:58:29 +0200 |
blanchet |
document metis better in Sledgehammer docs
|
changeset |
files
|
| Mon, 06 Jun 2011 21:02:24 +0200 |
blanchet |
updated Sledgehammer message
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
removed old optimization that isn't one anyone
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
generate less type information in polymorphic case
|
changeset |
files
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
Metis code cleanup
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:36 +0200 |
blanchet |
enable new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
made "explicit_apply"'s smart mode (more) complete
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fall back in case path finder fails -- these errors are sometimes salvageable
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
marked "metisF" as legacy -- nobody uses it or needs it
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more preparations towards hijacking Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't mention "metisX" so much in the docs -- it will go away soon
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
reintroduced metisFT in example
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
imported patch metis_reconstr_give_type_infer_a_chance
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make "metisX"'s default more like old "metis"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
whitespace tuning
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuned Metis examples
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more through tests of new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed type helper indices in new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
improved ATP clausifier so it can deal with "x => (y <=> z)"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
avoid renumbering hypotheses
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed reconstruction of new Skolem constants in new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't translate new Skolemizer assumptions in new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed detection of Skolem constants in type construction detection code
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
reveal Skolems in new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
slacker version of "fastype_of", in case a function has dummy type
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't stumble on Skolem names
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
conceal old Skolems in new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
properly unmangle names in path finder
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
only uncombine combinators in textual Isar proofs, not in Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
properly locate helpers whose constants have several entries in the helper table
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
skip "hBOOL" in new Metis path finder
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't pass "~ " to new Metis
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
temporarily document "metisX"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
use "metisX" as fallback, since it's much faster than "metisFT"
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
temporarily added "MetisX" as reconstructor and minimizer
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
show what failed to play
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
killed odd connectives
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added Metis examples to test the new type encodings
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
tuned CASC method
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
clean up unnecessary machinery -- helpers work also with monomorphic type encodings
|
changeset |
files
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added support for helpers in new Metis, so far only for polymorphic type encodings
|
changeset |
files
|
| Mon, 06 Jun 2011 16:29:38 +0200 |
kleing |
imported rest of new IMP
|
changeset |
files
|
| Mon, 06 Jun 2011 16:29:13 +0200 |
kleing |
atLeastAtMostSuc_conv on int
|
changeset |
files
|
| Mon, 06 Jun 2011 14:11:54 +0200 |
kleing |
fixed typo
|
changeset |
files
|
| Sun, 05 Jun 2011 15:00:52 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Sun, 05 Jun 2011 15:00:17 +0200 |
boehmes |
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
|
changeset |
files
|
| Fri, 03 Jun 2011 19:37:26 +0200 |
bulwahn |
changing the mira setting again for the mutabelle configuration
|
changeset |
files
|
| Fri, 03 Jun 2011 07:25:44 +0200 |
bulwahn |
adding more settings to mira's mutabelle configuration
|
changeset |
files
|
| Thu, 02 Jun 2011 15:17:23 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 02 Jun 2011 10:10:23 +0200 |
nipkow |
Added typed IMP
|
changeset |
files
|
| Thu, 02 Jun 2011 10:13:46 +0200 |
bulwahn |
adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
|
changeset |
files
|
| Thu, 02 Jun 2011 09:51:40 +0200 |
bulwahn |
adding invocation of exhaustive testing without using finite types to mutabelle
|
changeset |
files
|
| Thu, 02 Jun 2011 09:51:40 +0200 |
bulwahn |
moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
|
changeset |
files
|
| Thu, 02 Jun 2011 08:55:08 +0200 |
bulwahn |
splitting Dlist theory in Dlist and Dlist_Cset
|
changeset |
files
|
| Wed, 01 Jun 2011 23:08:04 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 01 Jun 2011 22:47:26 +0200 |
nipkow |
Made comments text
|
changeset |
files
|
| Wed, 01 Jun 2011 22:42:37 +0200 |
nipkow |
Fixed denotational semantics
|
changeset |
files
|
| Wed, 01 Jun 2011 21:50:49 +0200 |
nipkow |
Removed old IMP files
|
changeset |
files
|
| Wed, 01 Jun 2011 21:35:34 +0200 |
nipkow |
Replacing old IMP with new Semantics material
|
changeset |
files
|
| Wed, 01 Jun 2011 15:53:47 +0200 |
nipkow |
tuned lemmas
|
changeset |
files
|
| Wed, 01 Jun 2011 19:50:59 +0200 |
blanchet |
fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
|
changeset |
files
|
| Wed, 01 Jun 2011 13:50:37 +0200 |
bulwahn |
setting up code generation for extended reals
|
changeset |
files
|
| Wed, 01 Jun 2011 11:51:25 +0200 |
nipkow |
new lemmas
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
fixed interaction between type tags and hAPP in reconstruction code
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
implemented missing hAPP and ti cases of new path finder
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
support lightweight tags in new Metis
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
tuned names
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
export one more function
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
clausify "<=>" (needed for some type information)
|
changeset |
files
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
distinguish different kinds of typing informations in the fact name
|
changeset |
files
|
| Wed, 01 Jun 2011 09:10:13 +0200 |
bulwahn |
splitting RBT theory into RBT and RBT_Mapping
|
changeset |
files
|
| Wed, 01 Jun 2011 08:07:28 +0200 |
bulwahn |
creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
|
changeset |
files
|
| Wed, 01 Jun 2011 08:07:27 +0200 |
bulwahn |
code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
|
changeset |
files
|
| Wed, 01 Jun 2011 00:23:16 +0200 |
blanchet |
make SML/NJ happier
|
changeset |
files
|
| Wed, 01 Jun 2011 00:12:38 +0200 |
blanchet |
make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
|
changeset |
files
|
| Tue, 31 May 2011 23:39:27 +0200 |
blanchet |
speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call
|
changeset |
files
|
| Tue, 31 May 2011 19:28:03 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Tue, 31 May 2011 19:27:19 +0200 |
boehmes |
proper nesting of loops in new monomorphizer;
|
changeset |
files
|
| Tue, 31 May 2011 19:21:20 +0200 |
boehmes |
use new monomorphizer for SMT;
|
changeset |
files
|
| Tue, 31 May 2011 18:13:00 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Tue, 31 May 2011 15:45:27 +0200 |
bulwahn |
Quickcheck Narrowing only requires one compilation with GHC now
|
changeset |
files
|
| Tue, 31 May 2011 15:45:26 +0200 |
bulwahn |
splitting test_goal_terms in Quickcheck into smaller basic functions
|
changeset |
files
|
| Tue, 31 May 2011 15:45:24 +0200 |
bulwahn |
adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
|
changeset |
files
|
| Tue, 31 May 2011 17:15:14 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 31 May 2011 17:05:44 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
monomorphize in the new Metis if the type system calls for it
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed comment
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed new path finder for type information tag
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
no need for type arguments with "xxx_tags_heavy" type system
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use ":" for type information (looks good in Metis's output) and handle it in new path finder
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
make "prepare_atp_problem" more robust w.r.t. choice of type system
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
parse optional type system specification
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
proper handling of type variable classes in new Metis
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
fixed recursive call in new path finder and (untested:) handle hAPP
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
don't preprocess twice
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more robust and simpler adjustment computation
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new Metis
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
removed obscure option
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added "metisX" syntax (temporary)
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added new metis mode, with no implementation yet
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
changeset |
files
|
| Tue, 31 May 2011 11:21:47 +0200 |
krauss |
more precise authorship, reflecting my own ignorance and hg annotate
|
changeset |
files
|
| Tue, 31 May 2011 11:16:52 +0200 |
krauss |
generate raw induction rule as instance of generic rule with careful treatment of currying
|
changeset |
files
|
| Tue, 31 May 2011 11:16:34 +0200 |
krauss |
generic fixpoint induction (with explicit curry/uncurry predicates) and instance for option type
|
changeset |
files
|
| Tue, 31 May 2011 11:11:17 +0200 |
krauss |
admissibility on option type
|
changeset |
files
|
| Mon, 23 May 2011 21:34:37 +0200 |
krauss |
also manage induction rule;
|
changeset |
files
|
| Mon, 30 May 2011 17:55:34 +0200 |
bulwahn |
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
|
changeset |
files
|
| Mon, 30 May 2011 16:15:37 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 30 May 2011 16:10:12 +0100 |
paulson |
Workaround for bug involving makeindex, hyperref and the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
parameterize print_theorems over actual search function
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
added experimental yxml_find_theorems web service (but no client yet)
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
generic ScgiServer.simple_handler
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
moved html templates to a separate module, making their awkward signatures explicit
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
attempt to clarify code; removed "handle _" and dead code
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
(de)serialization for search query and result
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
explicit type for search queries
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
moved questionable goal modification out of filter_theorems
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
exported raw query parser; removed inconsistent clone
|
changeset |
files
|
| Mon, 30 May 2011 17:07:48 +0200 |
krauss |
separate query parsing from actual search
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
document new explicit apply
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
made "explicit_apply" smarter -- no need to force explicit applications in minimizer on all constants, better do it more fine granularly
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
don't slice if there are too few facts
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
nicer failure message when one-line proof reconstruction fails
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make SML/NJ happy
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
make all messages urgent in verbose mode
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize automatically even if Metis failed, if the external prover was really fast
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
fixed syntax of min options
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
better merging of similar outputs
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
update minimization documentation
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
imported patch sledge_doc_metis_as_prover
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
changeset |
files
|
| Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
changeset |
files
|
| Mon, 30 May 2011 15:30:05 +0100 |
paulson |
Workaround for hyperref bug affecting index entries involving the | symbol
|
changeset |
files
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
changeset |
files
|
| Mon, 30 May 2011 13:57:59 +0200 |
bulwahn |
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
|
changeset |
files
|
| Mon, 30 May 2011 12:20:04 +0100 |
paulson |
merged multiple heads
|
changeset |
files
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
changeset |
files
|
| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
changeset |
files
|
| Fri, 27 May 2011 21:11:44 +0200 |
krauss |
function tutorial: do not omit termination proof, even when discussing other things
|
changeset |
files
|
| Fri, 27 May 2011 16:45:24 +0200 |
boehmes |
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
|
changeset |
files
|
| Fri, 27 May 2011 10:41:09 +0200 |
blanchet |
document new "try"
|
changeset |
files
|
| Fri, 27 May 2011 10:33:16 +0200 |
blanchet |
tuned comments
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
new timeout section (cf. Nitpick manual)
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more Sledgehammer documentation updates
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
minor update
|
changeset |
files
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
changeset |
files
|