# HG changeset patch # User bulwahn # Date 1256666639 -3600 # Node ID b8d3b7196fe748724f5123c38e6a9f2458395464 # Parent cb3908614f7e516501a3fb6c73761f31320792eb# Parent 2b65e9ed2e6e69799c013fb709e84e90b6905b80 merged diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 27 16:47:27 2009 +0100 +++ b/src/HOL/IsaMakefile Tue Oct 27 19:03:59 2009 +0100 @@ -1195,12 +1195,11 @@ $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy \ SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \ - SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \ - SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \ - SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \ - SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \ - SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML \ - SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML + SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \ + SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \ + SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \ + SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \ + SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 27 16:47:27 2009 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 27 19:03:59 2009 +0100 @@ -302,8 +302,11 @@ fun run_sh prover hard_timeout timeout dir st = let val (ctxt, goal) = Proof.get_goal st - val ctxt' = if is_none dir then ctxt - else Config.put ATP_Wrapper.destdir (the dir) ctxt + val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I) + val ctxt' = + ctxt + |> change_dir dir + |> Config.put ATP_Wrapper.measure_runtime true val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal); val time_limit = diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/Mirabelle/doc/options.txt --- a/src/HOL/Mirabelle/doc/options.txt Tue Oct 27 16:47:27 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -Options for sledgehammer: - - * prover=NAME: name of the external prover to call - * prover_timeout=TIME: timeout for invoked ATP (seconds of process time) - * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time) - * keep=PATH: path where to keep temporary files created by sledgehammer - * full_types: enable full-typed encoding - * minimize: enable minimization of theorem set found by sledgehammer - * minimize_timeout=TIME: timeout for each minimization step (seconds of - process time) - * metis: apply metis with the theorems found by sledgehammer diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Oct 27 16:47:27 2009 +0100 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Oct 27 19:03:59 2009 +0100 @@ -35,8 +35,17 @@ echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" print_action_names echo - echo " A list of available OPTIONs can be found here:" - echo " $MIRABELLE_HOME/doc/options.txt" + echo " Available OPTIONs for the ACTION sledgehammer:" + echo " * prover=NAME: name of the external prover to call" + echo " * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)" + echo " * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed" + echo " time)" + echo " * keep=PATH: path where to keep temporary files created by sledgehammer" + echo " * full_types: enable fully-typed encoding" + echo " * minimize: enable minimization of theorem set found by sledgehammer" + echo " * minimize_timeout=TIME: timeout for each minimization step (seconds of" + echo " process time)" + echo " * metis: apply metis to the theorems found by sledgehammer" echo echo " FILES is a list of theory files, where each file is either NAME.thy" echo " or NAME.thy[START:END] and START and END are numbers indicating the" diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/SMT/SMT_Base.thy --- a/src/HOL/SMT/SMT_Base.thy Tue Oct 27 16:47:27 2009 +0100 +++ b/src/HOL/SMT/SMT_Base.thy Tue Oct 27 19:03:59 2009 +0100 @@ -29,7 +29,7 @@ definition pat :: "'a \ pattern" where "pat _ = Pattern" -definition nopat :: "bool \ pattern" +definition nopat :: "'a \ pattern" where "nopat _ = Pattern" definition andpat :: "pattern \ 'a \ pattern" (infixl "andpat" 60) diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/SMT/Tools/smt_builtin.ML --- a/src/HOL/SMT/Tools/smt_builtin.ML Tue Oct 27 16:47:27 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -(* Title: HOL/SMT/Tools/smt_builtin.ML - Author: Sascha Boehme, TU Muenchen - -Tables for built-in symbols. -*) - -signature SMT_BUILTIN = -sig - type sterm = (SMT_Translate.sym, typ) sterm - type builtin_fun = typ -> sterm list -> (string * sterm list) option - type table = (typ * builtin_fun) list Symtab.table - - val make: (term * string) list -> table - val add: term * builtin_fun -> table -> table - val lookup: table -> theory -> string * typ -> sterm list -> - (string * sterm list) option - - val bv_rotate: (int -> string) -> builtin_fun - val bv_extend: (int -> string) -> builtin_fun - val bv_extract: (int -> int -> string) -> builtin_fun -end - -structure SMT_Builtin: SMT_BUILTIN = -struct - -structure T = SMT_Translate - -type sterm = (SMT_Translate.sym, typ) sterm -type builtin_fun = typ -> sterm list -> (string * sterm list) option -type table = (typ * builtin_fun) list Symtab.table - -fun make entries = - let - fun dest (t, bn) = - let val (n, T) = Term.dest_Const t - in (n, (Logic.varifyT T, K (pair bn))) end - in Symtab.make (AList.group (op =) (map dest entries)) end - -fun add (t, f) tab = - let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t) - in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end - -fun lookup tab thy (n, T) = - AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T - - -fun dest_binT T = - (case T of - Type (@{type_name "Numeral_Type.num0"}, _) => 0 - | Type (@{type_name "Numeral_Type.num1"}, _) => 1 - | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T - | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T - | _ => raise TYPE ("dest_binT", [T], [])) - -fun dest_wordT T = - (case T of - Type (@{type_name "word"}, [T]) => dest_binT T - | _ => raise TYPE ("dest_wordT", [T], [])) - - -val dest_nat = (fn - SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i - | _ => NONE) - -fun bv_rotate mk_name T ts = - dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts)) - -fun bv_extend mk_name T ts = - (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of - (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE - | _ => NONE) - -fun bv_extract mk_name T ts = - (case (try dest_wordT (body_type T), dest_nat (hd ts)) of - (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts) - | _ => NONE) - -end diff -r cb3908614f7e -r b8d3b7196fe7 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Oct 27 16:47:27 2009 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Oct 27 19:03:59 2009 +0100 @@ -9,6 +9,7 @@ (*hooks for problem files*) val destdir: string Config.T val problem_prefix: string Config.T + val measure_runtime: bool Config.T val setup: theory -> theory (*prover configuration, problem format, and prover result*) @@ -61,7 +62,10 @@ val (problem_prefix, problem_prefix_setup) = Attrib.config_string "atp_problem_prefix" "prob"; -val setup = destdir_setup #> problem_prefix_setup; +val (measure_runtime, measure_runtime_setup) = + Attrib.config_bool "atp_measure_runtime" false; + +val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup; (* prover configuration, problem format, and prover result *) @@ -140,9 +144,14 @@ end; (* write out problem file and call prover *) - fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " " - [File.shell_path cmd, args, File.shell_path probfile] ^ " 2> /dev/null" ^ - " ; } 2>&1" + fun cmd_line probfile = + if Config.get ctxt measure_runtime + then (* Warning: suppresses error messages of ATPs *) + "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, + args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1" + else + space_implode " " ["exec", File.shell_path cmd, args, + File.shell_path probfile]; fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -154,10 +163,12 @@ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (proof, as_time t) end; + fun split_time' s = + if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists cmd then write probfile clauses - |> pair (apfst split_time (system_out (cmd_line probfile))) + |> pair (apfst split_time' (system_out (cmd_line probfile))) else error ("Bad executable: " ^ Path.implode cmd); (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)