merged
authorbulwahn
Tue Oct 27 19:03:59 2009 +0100 (2009-10-27)
changeset 33262b8d3b7196fe7
parent 33261 cb3908614f7e
parent 33249 2b65e9ed2e6e
child 33263 03c08ce703bf
merged
src/HOL/IsaMakefile
src/HOL/Mirabelle/doc/options.txt
src/HOL/SMT/Tools/smt_builtin.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Oct 27 16:47:27 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 19:03:59 2009 +0100
     1.3 @@ -1195,12 +1195,11 @@
     1.4  
     1.5  $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy		\
     1.6    SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML	\
     1.7 -  SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML			\
     1.8 -  SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML			\
     1.9 -  SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML			\
    1.10 -  SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML		\
    1.11 -  SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML				\
    1.12 -  SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
    1.13 +  SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML              \
    1.14 +  SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
    1.15 +  SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
    1.16 +  SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
    1.17 +  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
    1.18  	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
    1.19  
    1.20  
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 27 16:47:27 2009 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 27 19:03:59 2009 +0100
     2.3 @@ -302,8 +302,11 @@
     2.4  fun run_sh prover hard_timeout timeout dir st =
     2.5    let
     2.6      val (ctxt, goal) = Proof.get_goal st
     2.7 -    val ctxt' = if is_none dir then ctxt
     2.8 -      else Config.put ATP_Wrapper.destdir (the dir) ctxt
     2.9 +    val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
    2.10 +    val ctxt' =
    2.11 +      ctxt
    2.12 +      |> change_dir dir
    2.13 +      |> Config.put ATP_Wrapper.measure_runtime true
    2.14      val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal);
    2.15  
    2.16      val time_limit =
     3.1 --- a/src/HOL/Mirabelle/doc/options.txt	Tue Oct 27 16:47:27 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,11 +0,0 @@
     3.4 -Options for sledgehammer:
     3.5 -
     3.6 -  * prover=NAME: name of the external prover to call
     3.7 -  * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)
     3.8 -  * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed time)
     3.9 -  * keep=PATH: path where to keep temporary files created by sledgehammer 
    3.10 -  * full_types: enable full-typed encoding
    3.11 -  * minimize: enable minimization of theorem set found by sledgehammer
    3.12 -  * minimize_timeout=TIME: timeout for each minimization step (seconds of
    3.13 -    process time)
    3.14 -  * metis: apply metis with the theorems found by sledgehammer
     4.1 --- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Oct 27 16:47:27 2009 +0100
     4.2 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Oct 27 19:03:59 2009 +0100
     4.3 @@ -35,8 +35,17 @@
     4.4    echo "  either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
     4.5    print_action_names
     4.6    echo
     4.7 -  echo "  A list of available OPTIONs can be found here:"
     4.8 -  echo "    $MIRABELLE_HOME/doc/options.txt"
     4.9 +  echo "  Available OPTIONs for the ACTION sledgehammer:"
    4.10 +  echo "    * prover=NAME: name of the external prover to call"
    4.11 +  echo "    * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)"
    4.12 +  echo "    * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed"
    4.13 +  echo "      time)"
    4.14 +  echo "    * keep=PATH: path where to keep temporary files created by sledgehammer"
    4.15 +  echo "    * full_types: enable fully-typed encoding"
    4.16 +  echo "    * minimize: enable minimization of theorem set found by sledgehammer"
    4.17 +  echo "    * minimize_timeout=TIME: timeout for each minimization step (seconds of"
    4.18 +  echo "      process time)"
    4.19 +  echo "    * metis: apply metis to the theorems found by sledgehammer"
    4.20    echo
    4.21    echo "  FILES is a list of theory files, where each file is either NAME.thy"
    4.22    echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
     5.1 --- a/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 16:47:27 2009 +0100
     5.2 +++ b/src/HOL/SMT/SMT_Base.thy	Tue Oct 27 19:03:59 2009 +0100
     5.3 @@ -29,7 +29,7 @@
     5.4  definition pat :: "'a \<Rightarrow> pattern"
     5.5  where "pat _ = Pattern"
     5.6  
     5.7 -definition nopat :: "bool \<Rightarrow> pattern"
     5.8 +definition nopat :: "'a \<Rightarrow> pattern"
     5.9  where "nopat _ = Pattern"
    5.10  
    5.11  definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
     6.1 --- a/src/HOL/SMT/Tools/smt_builtin.ML	Tue Oct 27 16:47:27 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,78 +0,0 @@
     6.4 -(*  Title:      HOL/SMT/Tools/smt_builtin.ML
     6.5 -    Author:     Sascha Boehme, TU Muenchen
     6.6 -
     6.7 -Tables for built-in symbols.
     6.8 -*)
     6.9 -
    6.10 -signature SMT_BUILTIN =
    6.11 -sig
    6.12 -  type sterm = (SMT_Translate.sym, typ) sterm
    6.13 -  type builtin_fun = typ -> sterm list -> (string * sterm list) option
    6.14 -  type table = (typ * builtin_fun) list Symtab.table
    6.15 -
    6.16 -  val make: (term * string) list -> table
    6.17 -  val add: term * builtin_fun -> table -> table
    6.18 -  val lookup: table -> theory -> string * typ -> sterm list ->
    6.19 -    (string * sterm list) option
    6.20 -
    6.21 -  val bv_rotate: (int -> string) -> builtin_fun
    6.22 -  val bv_extend: (int -> string) -> builtin_fun
    6.23 -  val bv_extract: (int -> int -> string) -> builtin_fun
    6.24 -end
    6.25 -
    6.26 -structure SMT_Builtin: SMT_BUILTIN =
    6.27 -struct
    6.28 -
    6.29 -structure T = SMT_Translate
    6.30 -
    6.31 -type sterm = (SMT_Translate.sym, typ) sterm
    6.32 -type builtin_fun = typ -> sterm list -> (string * sterm list) option
    6.33 -type table = (typ * builtin_fun) list Symtab.table
    6.34 -
    6.35 -fun make entries =
    6.36 -  let
    6.37 -    fun dest (t, bn) =
    6.38 -      let val (n, T) = Term.dest_Const t
    6.39 -      in (n, (Logic.varifyT T, K (pair bn))) end
    6.40 -  in Symtab.make (AList.group (op =) (map dest entries)) end
    6.41 -
    6.42 -fun add (t, f) tab =
    6.43 -  let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
    6.44 -  in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
    6.45 -
    6.46 -fun lookup tab thy (n, T) =
    6.47 -  AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
    6.48 -
    6.49 -
    6.50 -fun dest_binT T =
    6.51 -  (case T of
    6.52 -    Type (@{type_name "Numeral_Type.num0"}, _) => 0
    6.53 -  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    6.54 -  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
    6.55 -  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
    6.56 -  | _ => raise TYPE ("dest_binT", [T], []))
    6.57 -
    6.58 -fun dest_wordT T =
    6.59 -  (case T of
    6.60 -    Type (@{type_name "word"}, [T]) => dest_binT T
    6.61 -  | _ => raise TYPE ("dest_wordT", [T], []))
    6.62 -
    6.63 -
    6.64 -val dest_nat = (fn
    6.65 -    SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
    6.66 -  | _ => NONE)
    6.67 -
    6.68 -fun bv_rotate mk_name T ts =
    6.69 -  dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
    6.70 -
    6.71 -fun bv_extend mk_name T ts =
    6.72 -  (case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
    6.73 -    (SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
    6.74 -  | _ => NONE)
    6.75 -
    6.76 -fun bv_extract mk_name T ts =
    6.77 -  (case (try dest_wordT (body_type T), dest_nat (hd ts)) of
    6.78 -    (SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
    6.79 -  | _ => NONE)
    6.80 -
    6.81 -end
     7.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Oct 27 16:47:27 2009 +0100
     7.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Oct 27 19:03:59 2009 +0100
     7.3 @@ -9,6 +9,7 @@
     7.4    (*hooks for problem files*)
     7.5    val destdir: string Config.T
     7.6    val problem_prefix: string Config.T
     7.7 +  val measure_runtime: bool Config.T
     7.8    val setup: theory -> theory
     7.9  
    7.10    (*prover configuration, problem format, and prover result*)
    7.11 @@ -61,7 +62,10 @@
    7.12  val (problem_prefix, problem_prefix_setup) =
    7.13    Attrib.config_string "atp_problem_prefix" "prob";
    7.14  
    7.15 -val setup = destdir_setup #> problem_prefix_setup;
    7.16 +val (measure_runtime, measure_runtime_setup) =
    7.17 +  Attrib.config_bool "atp_measure_runtime" false;
    7.18 +
    7.19 +val setup = destdir_setup #> problem_prefix_setup #> measure_runtime_setup;
    7.20  
    7.21  
    7.22  (* prover configuration, problem format, and prover result *)
    7.23 @@ -140,9 +144,14 @@
    7.24        end;
    7.25  
    7.26      (* write out problem file and call prover *)
    7.27 -    fun cmd_line probfile = "TIMEFORMAT='%3U'; { time " ^ space_implode " "
    7.28 -      [File.shell_path cmd, args, File.shell_path probfile] ^ " 2> /dev/null" ^
    7.29 -      " ; } 2>&1"
    7.30 +    fun cmd_line probfile =
    7.31 +      if Config.get ctxt measure_runtime
    7.32 +      then (* Warning: suppresses error messages of ATPs *)
    7.33 +        "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
    7.34 +        args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1"
    7.35 +      else
    7.36 +        space_implode " " ["exec", File.shell_path cmd, args,
    7.37 +        File.shell_path probfile];
    7.38      fun split_time s =
    7.39        let
    7.40          val split = String.tokens (fn c => str c = "\n");
    7.41 @@ -154,10 +163,12 @@
    7.42          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
    7.43          val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
    7.44        in (proof, as_time t) end;
    7.45 +    fun split_time' s =
    7.46 +      if Config.get ctxt measure_runtime then split_time s else (s, 0)
    7.47      fun run_on probfile =
    7.48        if File.exists cmd then
    7.49          write probfile clauses
    7.50 -        |> pair (apfst split_time (system_out (cmd_line probfile)))
    7.51 +        |> pair (apfst split_time' (system_out (cmd_line probfile)))
    7.52        else error ("Bad executable: " ^ Path.implode cmd);
    7.53  
    7.54      (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)