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)
boehmes@40424
     1
(*  Title:      HOL/Tools/SMT/smt_failure.ML
boehmes@40424
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@40424
     3
boehmes@40424
     4
Failures and exception of SMT.
boehmes@40424
     5
*)
boehmes@40424
     6
boehmes@40424
     7
signature SMT_FAILURE =
boehmes@40424
     8
sig
boehmes@40424
     9
  datatype failure =
boehmes@40424
    10
    Counterexample of bool * term list |
boehmes@40424
    11
    Time_Out |
boehmes@40424
    12
    Out_Of_Memory |
boehmes@40561
    13
    Abnormal_Termination of int |
boehmes@40424
    14
    Other_Failure of string
boehmes@40424
    15
  val string_of_failure: Proof.context -> failure -> string
boehmes@40424
    16
  exception SMT of failure
boehmes@40424
    17
end
boehmes@40424
    18
boehmes@40424
    19
structure SMT_Failure: SMT_FAILURE =
boehmes@40424
    20
struct
boehmes@40424
    21
boehmes@40424
    22
datatype failure =
boehmes@40424
    23
  Counterexample of bool * term list |
boehmes@40424
    24
  Time_Out |
boehmes@40424
    25
  Out_Of_Memory |
boehmes@40561
    26
  Abnormal_Termination of int |
boehmes@40424
    27
  Other_Failure of string
boehmes@40424
    28
boehmes@40424
    29
fun string_of_failure ctxt (Counterexample (real, ex)) =
boehmes@40424
    30
      let
boehmes@40515
    31
        val msg =
boehmes@40515
    32
          if real then "Counterexample found (possibly spurious)"
boehmes@40515
    33
          else "Potential counterexample found"
boehmes@40424
    34
      in
boehmes@40424
    35
        if null ex then msg
boehmes@40424
    36
        else Pretty.string_of (Pretty.big_list (msg ^ ":")
boehmes@40424
    37
          (map (Syntax.pretty_term ctxt) ex))
boehmes@40424
    38
      end
boehmes@40424
    39
  | string_of_failure _ Time_Out = "Timed out"
boehmes@40424
    40
  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
boehmes@40561
    41
  | string_of_failure _ (Abnormal_Termination err) =
boehmes@40561
    42
      "Solver terminated abnormally with error code " ^ string_of_int err
boehmes@40424
    43
  | string_of_failure _ (Other_Failure msg) = msg
boehmes@40424
    44
boehmes@40424
    45
exception SMT of failure
boehmes@40424
    46
boehmes@40424
    47
end