src/HOL/Tools/SMT/smt_failure.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 58061 3d060f43accb
permissions -rw-r--r--
more symbols;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smt_failure.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Failures and exception of SMT.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature SMT_FAILURE =
blanchet@56078
     8
sig
blanchet@56078
     9
  datatype failure =
blanchet@57158
    10
    Counterexample of bool |
blanchet@56078
    11
    Time_Out |
blanchet@56078
    12
    Out_Of_Memory |
blanchet@56078
    13
    Abnormal_Termination of int |
blanchet@56078
    14
    Other_Failure of string
blanchet@57158
    15
  val string_of_failure: failure -> string
blanchet@56078
    16
  exception SMT of failure
blanchet@57229
    17
end;
blanchet@56078
    18
blanchet@58061
    19
structure SMT_Failure: SMT_FAILURE =
blanchet@56078
    20
struct
blanchet@56078
    21
blanchet@56078
    22
datatype failure =
blanchet@57158
    23
  Counterexample of bool |
blanchet@56078
    24
  Time_Out |
blanchet@56078
    25
  Out_Of_Memory |
blanchet@56078
    26
  Abnormal_Termination of int |
blanchet@56078
    27
  Other_Failure of string
blanchet@56078
    28
blanchet@57158
    29
fun string_of_failure (Counterexample genuine) =
blanchet@57158
    30
      if genuine then "Counterexample found (possibly spurious)"
blanchet@56078
    31
      else "Potential counterexample found"
blanchet@57158
    32
  | string_of_failure Time_Out = "Timed out"
blanchet@57158
    33
  | string_of_failure Out_Of_Memory = "Ran out of memory"
blanchet@57158
    34
  | string_of_failure (Abnormal_Termination err) =
blanchet@56078
    35
      "Solver terminated abnormally with error code " ^ string_of_int err
blanchet@57158
    36
  | string_of_failure (Other_Failure msg) = msg
blanchet@56078
    37
blanchet@56078
    38
exception SMT of failure
blanchet@56078
    39
blanchet@57229
    40
end;