SSL mirabelle_presburger.ML Sprache: SML

(*  Title:      HOL/Tools/Mirabelle/mirabelle_presburger.ML
    Author:     Martin Desharnais, MPI-INF Saarbrücken

Mirabelle action: "presburger".
*)

structure Mirabelle_Presburger: MIRABELLE_ACTION =
struct

fun make_action ({timeout, ...} : Mirabelle.action_context) =
  let
    fun run ({pre, ...} : Mirabelle.command) =
      (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
        ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
      | (_, false) => "failed")
  in ("", {run = run, finalize = K ""}) end

val () = Mirabelle.register_action "presburger" make_action

end

quality85%

¤ Dauer der Verarbeitung: 0.12 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.