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_setup_solvers.ML
Fri, 17 Dec 2010 15:30:00 +0100
boehmes
fixed the command-line syntax for setting Yices' random seed
file
|
diff
|
annotate
Wed, 15 Dec 2010 10:12:48 +0100
boehmes
adapted the Z3 proof parser to recent changes in Z3's proof format;
file
|
diff
|
annotate
Wed, 15 Dec 2010 10:12:44 +0100
boehmes
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
file
|
diff
|
annotate
Wed, 15 Dec 2010 08:39:24 +0100
boehmes
added option to modify the random seed of SMT solvers
file
|
diff
|
annotate
Mon, 06 Dec 2010 11:25:21 +0100
blanchet
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
file
|
diff
|
annotate
Mon, 08 Nov 2010 12:13:44 +0100
boehmes
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
file
|
diff
|
annotate
Fri, 29 Oct 2010 18:17:06 +0200
boehmes
clarified error message
file
|
diff
|
annotate
Wed, 27 Oct 2010 08:58:03 +0200
boehmes
made SML/NJ happy
file
|
diff
|
annotate
Tue, 26 Oct 2010 17:35:51 +0200
boehmes
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
file
|
diff
|
annotate
Tue, 26 Oct 2010 11:45:12 +0200
boehmes
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
file
|
diff
|
annotate
less
more
(0)
tip