integrated "smt" proof method with Sledgehammer
authorblanchet
Tue Oct 26 13:16:43 2010 +0200 (2010-10-26)
changeset 401813788b7adab36
parent 40179 7ecfa9beef91
child 40182 e4fbe44838dd
integrated "smt" proof method with Sledgehammer
src/HOL/Main.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Main.thy	Tue Oct 26 12:23:39 2010 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Oct 26 13:16:43 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Plain Record Predicate_Compile Nitpick SMT
     1.8 +imports Plain Record Predicate_Compile Nitpick
     1.9  begin
    1.10  
    1.11  text {*
     2.1 --- a/src/HOL/Sledgehammer.thy	Tue Oct 26 12:23:39 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Tue Oct 26 13:16:43 2010 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Sledgehammer: Isabelle--ATP Linkup *}
     2.5  
     2.6  theory Sledgehammer
     2.7 -imports ATP
     2.8 +imports ATP SMT
     2.9  uses "Tools/Sledgehammer/sledgehammer_util.ML"
    2.10       "Tools/Sledgehammer/sledgehammer_filter.ML"
    2.11       "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 12:23:39 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 13:16:43 2010 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  
     3.5  signature SLEDGEHAMMER =
     3.6  sig
     3.7 -  type failure = ATP_Systems.failure
     3.8 +  type failure = ATP_Proof.failure
     3.9    type locality = Sledgehammer_Filter.locality
    3.10    type relevance_fudge = Sledgehammer_Filter.relevance_fudge
    3.11    type relevance_override = Sledgehammer_Filter.relevance_override
    3.12 @@ -99,7 +99,7 @@
    3.13  
    3.14  fun is_prover_installed ctxt name =
    3.15    let val thy = ProofContext.theory_of ctxt in
    3.16 -    if is_smt_prover name then true (* FIXME *)
    3.17 +    if is_smt_prover name then SMT_Solver.is_locally_installed ctxt
    3.18      else is_atp_installed thy name
    3.19    end
    3.20  
    3.21 @@ -406,34 +406,33 @@
    3.22       run_time_in_msecs = msecs}
    3.23    end
    3.24  
    3.25 -(* FIXME: dummy *)
    3.26 -fun saschas_run_smt_solver remote timeout state axioms i =
    3.27 -  (OS.Process.sleep (Time.fromMilliseconds 1500);
    3.28 -   {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
    3.29 -    run_time_in_msecs = NONE})
    3.30 +fun failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
    3.31 +  | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
    3.32 +  | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
    3.33  
    3.34  fun run_smt_solver remote ({timeout, ...} : params) minimize_command
    3.35                     ({state, subgoal, subgoal_count, axioms, ...}
    3.36                      : prover_problem) =
    3.37    let
    3.38 -    val {outcome, used_axioms, run_time_in_msecs} =
    3.39 -      saschas_run_smt_solver remote timeout state
    3.40 -                             (map_filter (try dest_Untranslated) axioms) subgoal
    3.41 +    val {outcome, used_facts, run_time_in_msecs} =
    3.42 +      SMT_Solver.smt_filter remote timeout state
    3.43 +                            (map_filter (try dest_Untranslated) axioms) subgoal
    3.44      val message =
    3.45        if outcome = NONE then
    3.46          try_command_line (proof_banner false)
    3.47                           (apply_on_subgoal subgoal subgoal_count ^
    3.48 -                          command_call smtN (map fst used_axioms)) ^
    3.49 -        minimize_line minimize_command (map fst used_axioms)
    3.50 +                          command_call smtN (map fst used_facts)) ^
    3.51 +        minimize_line minimize_command (map fst used_facts)
    3.52        else
    3.53          ""
    3.54    in
    3.55 -    {outcome = outcome, used_axioms = used_axioms,
    3.56 -     run_time_in_msecs = run_time_in_msecs, message = message}
    3.57 +    {outcome = outcome |> Option.map failure_from_smt_failure,
    3.58 +     used_axioms = used_facts, run_time_in_msecs = SOME run_time_in_msecs,
    3.59 +     message = message}
    3.60    end
    3.61  
    3.62  fun get_prover thy auto name =
    3.63 -  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
    3.64 +  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
    3.65    else run_atp auto name (get_atp thy name)
    3.66  
    3.67  fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 12:23:39 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 13:16:43 2010 +0200
     4.3 @@ -130,9 +130,6 @@
     4.4    val extend = I
     4.5    fun merge p : T = AList.merge (op =) (K true) p)
     4.6  
     4.7 -(* FIXME: dummy *)
     4.8 -fun is_smt_solver_installed ctxt = true
     4.9 -
    4.10  fun remotify_prover_if_available_and_not_already_remote thy name =
    4.11    if String.isPrefix remote_prefix name then
    4.12      SOME name