--- 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
--- 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 =
--- 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
--- 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"
--- 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 \<Rightarrow> pattern"
where "pat _ = Pattern"
-definition nopat :: "bool \<Rightarrow> pattern"
+definition nopat :: "'a \<Rightarrow> pattern"
where "nopat _ = Pattern"
definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
--- 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
--- 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 *)