| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/Tools/SMT/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1022 B |
|
Quelle smt_failure.ML Sprache: SML |
|||||||||
|
(* 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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28