src/HOL/Library/Old_SMT/old_smt_failure.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 58058 1a0b18176548
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_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
blanchet@58058
     7
signature OLD_SMT_FAILURE =
boehmes@40424
     8
sig
boehmes@40828
     9
  type counterexample = {
boehmes@40828
    10
    is_real_cex: bool,
boehmes@40828
    11
    free_constraints: term list,
boehmes@40828
    12
    const_defs: term list}
boehmes@40424
    13
  datatype failure =
boehmes@40828
    14
    Counterexample of counterexample |
boehmes@40424
    15
    Time_Out |
boehmes@40424
    16
    Out_Of_Memory |
boehmes@40561
    17
    Abnormal_Termination of int |
boehmes@40424
    18
    Other_Failure of string
boehmes@40828
    19
  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
boehmes@40424
    20
  val string_of_failure: Proof.context -> failure -> string
boehmes@40424
    21
  exception SMT of failure
boehmes@40424
    22
end
boehmes@40424
    23
blanchet@58058
    24
structure Old_SMT_Failure: OLD_SMT_FAILURE =
boehmes@40424
    25
struct
boehmes@40424
    26
boehmes@40828
    27
type counterexample = {
boehmes@40828
    28
  is_real_cex: bool,
boehmes@40828
    29
  free_constraints: term list,
boehmes@40828
    30
  const_defs: term list}
boehmes@40828
    31
boehmes@40424
    32
datatype failure =
boehmes@40828
    33
  Counterexample of counterexample |
boehmes@40424
    34
  Time_Out |
boehmes@40424
    35
  Out_Of_Memory |
boehmes@40561
    36
  Abnormal_Termination of int |
boehmes@40424
    37
  Other_Failure of string
boehmes@40424
    38
boehmes@40828
    39
fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
boehmes@40828
    40
  let
boehmes@40828
    41
    val msg =
boehmes@40828
    42
      if is_real_cex then "Counterexample found (possibly spurious)"
boehmes@40828
    43
      else "Potential counterexample found"
boehmes@40828
    44
  in
boehmes@40828
    45
    if null free_constraints andalso null const_defs then Pretty.str msg
boehmes@40828
    46
    else
boehmes@40828
    47
      Pretty.big_list (msg ^ ":")
boehmes@40828
    48
        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
boehmes@40828
    49
  end
boehmes@40828
    50
boehmes@40828
    51
fun string_of_failure ctxt (Counterexample cex) =
boehmes@40828
    52
      Pretty.string_of (pretty_counterexample ctxt cex)
boehmes@40424
    53
  | string_of_failure _ Time_Out = "Timed out"
boehmes@40424
    54
  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
boehmes@40561
    55
  | string_of_failure _ (Abnormal_Termination err) =
boehmes@40561
    56
      "Solver terminated abnormally with error code " ^ string_of_int err
boehmes@40424
    57
  | string_of_failure _ (Other_Failure msg) = msg
boehmes@40424
    58
boehmes@40424
    59
exception SMT of failure
boehmes@40424
    60
boehmes@40424
    61
end