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;
     1 (*  Title:      HOL/Tools/SMT/smt_failure.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Failures and exception of SMT.
     5 *)
     6 
     7 signature SMT_FAILURE =
     8 sig
     9   datatype failure =
    10     Counterexample of bool |
    11     Time_Out |
    12     Out_Of_Memory |
    13     Abnormal_Termination of int |
    14     Other_Failure of string
    15   val string_of_failure: failure -> string
    16   exception SMT of failure
    17 end;
    18 
    19 structure SMT_Failure: SMT_FAILURE =
    20 struct
    21 
    22 datatype failure =
    23   Counterexample of bool |
    24   Time_Out |
    25   Out_Of_Memory |
    26   Abnormal_Termination of int |
    27   Other_Failure of string
    28 
    29 fun string_of_failure (Counterexample genuine) =
    30       if genuine then "Counterexample found (possibly spurious)"
    31       else "Potential counterexample found"
    32   | string_of_failure Time_Out = "Timed out"
    33   | string_of_failure Out_Of_Memory = "Ran out of memory"
    34   | string_of_failure (Abnormal_Termination err) =
    35       "Solver terminated abnormally with error code " ^ string_of_int err
    36   | string_of_failure (Other_Failure msg) = msg
    37 
    38 exception SMT of failure
    39 
    40 end;