src/HOL/Tools/SMT/smt_failure.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40561 0125cbb5d3c7
child 40828 47ff261431c4
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
     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 * term list |
    11     Time_Out |
    12     Out_Of_Memory |
    13     Abnormal_Termination of int |
    14     Other_Failure of string
    15   val string_of_failure: Proof.context -> 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 * term list |
    24   Time_Out |
    25   Out_Of_Memory |
    26   Abnormal_Termination of int |
    27   Other_Failure of string
    28 
    29 fun string_of_failure ctxt (Counterexample (real, ex)) =
    30       let
    31         val msg =
    32           if real then "Counterexample found (possibly spurious)"
    33           else "Potential counterexample found"
    34       in
    35         if null ex then msg
    36         else Pretty.string_of (Pretty.big_list (msg ^ ":")
    37           (map (Syntax.pretty_term ctxt) ex))
    38       end
    39   | string_of_failure _ Time_Out = "Timed out"
    40   | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    41   | string_of_failure _ (Abnormal_Termination err) =
    42       "Solver terminated abnormally with error code " ^ string_of_int err
    43   | string_of_failure _ (Other_Failure msg) = msg
    44 
    45 exception SMT of failure
    46 
    47 end