Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: smt_failure.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Tools/SMT/smt_failure.ML
    Author:     Sascha Boehme, TU Muenchen

Failures and exception of SMT.
*)

signature SMT_FAILURE =
sig
  datatype failure =
    Counterexample of bool |
    Time_Out |
    Out_Of_Memory |
    Abnormal_Termination of int |
    Other_Failure of string
  val string_of_failure: failure -> string
  exception SMT of failure
end;

structure SMT_Failure: SMT_FAILURE =
struct

datatype failure =
  Counterexample of bool |
  Time_Out |
  Out_Of_Memory |
  Abnormal_Termination of int |
  Other_Failure of string

fun string_of_failure (Counterexample genuine) =
      if genuine then "Counterexample found (possibly spurious)"
      else "Potential counterexample found"
  | string_of_failure Time_Out = "Timed out"
  | string_of_failure Out_Of_Memory = "Ran out of memory"
  | string_of_failure (Abnormal_Termination err) =
      "Solver terminated abnormally with error code " ^ string_of_int err
  | string_of_failure (Other_Failure msg) = msg

exception SMT of failure

end;

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.