Quelle sledgehammer_prover_tactic.ML Sprache: SML

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
    Author:     Jasmin Blanchette, LMU Muenchen
    Author:     Martin Desharnais, LMU Muenchen

Isabelle tactics as Sledgehammer provers.
*)

signature SLEDGEHAMMER_PROVER_TACTIC =
sig
  type stature = ATP_Problem_Generate.stature
  type mode = Sledgehammer_Prover.mode
  type prover = Sledgehammer_Prover.prover
  type base_slice = Sledgehammer_ATP_Systems.base_slice

  val is_tactic_prover : string -> bool
  val good_slices_of_tactic_prover : string -> base_slice list
  val run_tactic_prover : mode -> string -> prover
end;

structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
struct

open ATP_Proof
open Sledgehammer_Proof_Methods
open Sledgehammer_Prover

val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method

local

val slices_of_max_facts = map (fn max_facts => (1, false, false, max_facts, "mesh"))

in

(* FUDGE *)
fun good_slices_of_tactic_prover "metis" = slices_of_max_facts [0, 64, 32, 8, 16, 4, 2, 1]
  | good_slices_of_tactic_prover "fastforce" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
  | good_slices_of_tactic_prover "simp" = slices_of_max_facts [0, 16, 32, 8, 64, 4, 1, 2]
  | good_slices_of_tactic_prover "auto" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
  | good_slices_of_tactic_prover _ = slices_of_max_facts [0, 2, 8, 16, 32, 64]

end

fun meth_of "algebra" = Algebra_Method
  | meth_of "argo" = Argo_Method
  | meth_of "auto" = Auto_Method
  | meth_of "blast" = Blast_Method
  | meth_of "fastforce" = Fastforce_Method
  | meth_of "force" = Force_Method
  | meth_of "linarith" = Linarith_Method
  | meth_of "meson" = Meson_Method
  | meth_of "metis" = Metis_Method (NONE, NONE, [])
  | meth_of "order" = Order_Method
  | meth_of "presburger" = Presburger_Method
  | meth_of "satx" = SATx_Method
  | meth_of "simp" = Simp_Method
  | meth_of _ = Metis_Method (NONE, NONE, [])

fun run_tactic_prover mode name ({slices, timeout, ...} : params)
    ({state, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
  let
    val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice
    val facts = facts_of_basic_slice basic_slice factss
    val ctxt = Proof.context_of state

    fun run_try0 () : Try0.result option =
      let
        val run_timeout = slice_timeout slice_size slices timeout
        fun is_cartouche str = String.isPrefix "\" str andalso String.isSuffix "\" str
        fun xref_of_fact (((name, _), thm) : Sledgehammer_Fact.fact) =
            let
              val xref =
                if is_cartouche name then
                  Facts.Fact (Pretty.pure_string_of (Thm.pretty_thm ctxt thm))
                else
                  Facts.named name
            in
              (xref, [])
            end
        val xrefs = map xref_of_fact facts
        val facts : Try0.facts = {usings = xrefs, simps = [], intros = [], elims = [], dests = []}
      in
        Try0.get_proof_method_or_noop name (SOME run_timeout) facts state
      end

    val timer = Timer.startRealTimer ()
    val (outcome, command) =
      (case run_try0 () of
        NONE => (SOME GaveUp, "")
      | SOME {command, ...} => (NONE, command))
      handle ERROR _ => (SOME GaveUp, "")
           | Exn.Interrupt_Breakdown => (SOME GaveUp, "")
           | Timeout.TIMEOUT _ => (SOME TimedOut, "")
    val run_time = Timer.checkRealTimer timer

    val used_facts =
      (case outcome of
        NONE => (found_something name; map fst facts)
      | SOME _ => [])

    val message = fn preplay_outcome =>
      (case outcome of
        NONE =>
        let
          val banner = proof_banner mode name
        in
          (case preplay_outcome of
            NONE => try_command_line banner (Played run_time) command
          | SOME preplay_result =>
              one_line_proof_text (preplay_result, banner, subgoal, subgoal_count))
        end
      | SOME failure => string_of_atp_failure failure)
  in
    {outcome = outcome, used_facts = used_facts, used_from = facts,
     preferred_methss = (meth_of name, []), run_time = run_time, message = message}
  end

end;

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.