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;
     1 (*  Title:      HOL/Library/Old_SMT/old_smt_failure.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Failures and exception of SMT.
     5 *)
     6 
     7 signature OLD_SMT_FAILURE =
     8 sig
     9   type counterexample = {
    10     is_real_cex: bool,
    11     free_constraints: term list,
    12     const_defs: term list}
    13   datatype failure =
    14     Counterexample of counterexample |
    15     Time_Out |
    16     Out_Of_Memory |
    17     Abnormal_Termination of int |
    18     Other_Failure of string
    19   val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
    20   val string_of_failure: Proof.context -> failure -> string
    21   exception SMT of failure
    22 end
    23 
    24 structure Old_SMT_Failure: OLD_SMT_FAILURE =
    25 struct
    26 
    27 type counterexample = {
    28   is_real_cex: bool,
    29   free_constraints: term list,
    30   const_defs: term list}
    31 
    32 datatype failure =
    33   Counterexample of counterexample |
    34   Time_Out |
    35   Out_Of_Memory |
    36   Abnormal_Termination of int |
    37   Other_Failure of string
    38 
    39 fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
    40   let
    41     val msg =
    42       if is_real_cex then "Counterexample found (possibly spurious)"
    43       else "Potential counterexample found"
    44   in
    45     if null free_constraints andalso null const_defs then Pretty.str msg
    46     else
    47       Pretty.big_list (msg ^ ":")
    48         (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
    49   end
    50 
    51 fun string_of_failure ctxt (Counterexample cex) =
    52       Pretty.string_of (pretty_counterexample ctxt cex)
    53   | string_of_failure _ Time_Out = "Timed out"
    54   | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    55   | string_of_failure _ (Abnormal_Termination err) =
    56       "Solver terminated abnormally with error code " ^ string_of_int err
    57   | string_of_failure _ (Other_Failure msg) = msg
    58 
    59 exception SMT of failure
    60 
    61 end