src/HOL/Library/Old_SMT/old_smt_failure.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 58058 1a0b18176548
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_failure.ML
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     3
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     4
Failures and exception of SMT.
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     5
*)
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_FAILURE =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
     8
sig
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
     9
  type counterexample = {
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    10
    is_real_cex: bool,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    11
    free_constraints: term list,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    12
    const_defs: term list}
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    13
  datatype failure =
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    14
    Counterexample of counterexample |
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    15
    Time_Out |
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    16
    Out_Of_Memory |
40561
0125cbb5d3c7 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents: 40538
diff changeset
    17
    Abnormal_Termination of int |
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    18
    Other_Failure of string
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    19
  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    20
  val string_of_failure: Proof.context -> failure -> string
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    21
  exception SMT of failure
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    22
end
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    23
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    24
structure Old_SMT_Failure: OLD_SMT_FAILURE =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    25
struct
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    26
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    27
type counterexample = {
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    28
  is_real_cex: bool,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    29
  free_constraints: term list,
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    30
  const_defs: term list}
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    31
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    32
datatype failure =
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    33
  Counterexample of counterexample |
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    34
  Time_Out |
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    35
  Out_Of_Memory |
40561
0125cbb5d3c7 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents: 40538
diff changeset
    36
  Abnormal_Termination of int |
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    37
  Other_Failure of string
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    38
40828
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    39
fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    40
  let
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    41
    val msg =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    42
      if is_real_cex then "Counterexample found (possibly spurious)"
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    43
      else "Potential counterexample found"
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    44
  in
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    45
    if null free_constraints andalso null const_defs then Pretty.str msg
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    46
    else
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    47
      Pretty.big_list (msg ^ ":")
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    48
        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    49
  end
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    50
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    51
fun string_of_failure ctxt (Counterexample cex) =
47ff261431c4 split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents: 40561
diff changeset
    52
      Pretty.string_of (pretty_counterexample ctxt cex)
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    53
  | string_of_failure _ Time_Out = "Timed out"
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    54
  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
40561
0125cbb5d3c7 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents: 40538
diff changeset
    55
  | string_of_failure _ (Abnormal_Termination err) =
0125cbb5d3c7 renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents: 40538
diff changeset
    56
      "Solver terminated abnormally with error code " ^ string_of_int err
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    57
  | string_of_failure _ (Other_Failure msg) = msg
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    58
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    59
exception SMT of failure
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    60
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff changeset
    61
end