proper error handling for SMT solvers in Sledgehammer

NEWS

merge

integrated "smt" proof method with Sledgehammer

fixed confusion introduced in 008dc2d2c395

merged

reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers

merged

tuned

merged

use partial_function instead of MREC combinator; curried rev'

added Heap monad instance of partial_function package

added Spec_Rule declaration to partial_function

basic documentation for command partial_function

remove outdated "(otherwise)" syntax from manual

declare recursive equation as ".simps", in accordance with other packages

merged

dropped accidental doubled computation

optionally force the remote version of an SMT solver to be executed

tuned

added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)

changed SMT configuration options; updated SMT certificates

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

keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs

merged

merge

clearer error messages

renaming

back again to non-Apple font rendering (cf. 4977324373f2);

dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible;

disable broken popups for now;

tuned;

do not handle arbitrary exceptions;

merged

Code_Runtime.trace

proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};

merged

improved English

whitespace tuning

no need to encode theorem number twice in skolem names

tuning

make SML/NJ happy

relaxing the filtering condition for getting specifications from Spec_Rules

adding new predicate compiler files to the IsaMakefile

using mode_eq instead of op = for lookup in the predicate compiler

renaming split_modeT' to split_modeT

options as first argument to check functions

changing test parameters in examples to get to a result within the global timelimit

adding a global fixed timeout to quickcheck

adding a global time limit to the values command

explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; eliminated auto_flush threads -- use plain line buffering for stdout/stderr; tuned;

more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

explicitly qualify type Output.output, which is a slightly odd internal feature;

export main ML entry by default; observe elisp format for preferences; clarified command setup;

observe Isabelle/ML coding standards;

merged

significantly improved Isabelle/Isar implementation manual;

misc tuning;

removed some remains of Output.debug (follow-up to fce2202892c4);

recovered some odd two-dimensional layout;

merged

dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps

moved sledgehammer to Plain; tuned dependencies

CONTRIBUTORS

merge

merged

updated keywords

introduced manual version of "Auto Solve" as "solve_direct"

make "sledgehammer_params" work on single-threaded platforms

tuning

handle timeouts (to prevent failure from other threads); removed needless functions; added "metis" to the mix

update keywords

some partial_function examples

added ML antiquotation @{assert};

updated keywords;

integrated partial_function into HOL-Plain

first version of partial_function package

Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem

merged

splitting Hotel Key card example into specification and the two tests for counter example generation

adding generator quickcheck

restructuring values command and adding generator compilation

moving general functions from core_data to predicate_compile_aux

updating to new notation in commented examples

merged

use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum

remove legacy comp_dbind option from domain package

change fixrec parser to not accept theorem names with (unchecked) option

tuned

rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd

add lemma strict3

do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas

make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun

direct instantiation unit :: discrete_cpo

remove finite_po class

simplify proofs about flift; remove unneeded lemmas

simplify proof

minimize imports

add type annotation to avoid warning

simplify some proofs, convert to Isar style

rename lemma spair_lemma to spair_Sprod

pcpodef (open) 'a lift

remove intro! attribute from {sinl,sinr}_defined

simplify proofs of ssumE, sprodE

merged

renamed nat_number

nat_number -> eval_nat_numeral

some cleanup in Function_Lib

merged

compile

added SMT solver to Sledgehammer docs

more robust handling of "remote_" vs. non-"remote_" provers

generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)

replaced references with proper record that's threaded through

fixed signature of "is_smt_solver_installed"; renaming

renamed modules

renamed files

took out "smt"/"remote_smt" from default ATPs until they are properly implemented

remove more needless code ("run_smt_solvers"); tuning