simplified counterexample handling
authorblanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158f028d93798e6
parent 57157 87b4d54b1fbe
child 57159 24cbdebba35a
simplified counterexample handling
src/HOL/Tools/SMT2/smt2_failure.ML
src/HOL/Tools/SMT2/smt2_solver.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/SMT2/smt2_failure.ML	Mon Jun 02 17:34:26 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_failure.ML	Mon Jun 02 17:34:26 2014 +0200
     1.3 @@ -6,55 +6,34 @@
     1.4  
     1.5  signature SMT2_FAILURE =
     1.6  sig
     1.7 -  type counterexample = {
     1.8 -    is_real_cex: bool,
     1.9 -    free_constraints: term list,
    1.10 -    const_defs: term list}
    1.11    datatype failure =
    1.12 -    Counterexample of counterexample |
    1.13 +    Counterexample of bool |
    1.14      Time_Out |
    1.15      Out_Of_Memory |
    1.16      Abnormal_Termination of int |
    1.17      Other_Failure of string
    1.18 -  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
    1.19 -  val string_of_failure: Proof.context -> failure -> string
    1.20 +  val string_of_failure: failure -> string
    1.21    exception SMT of failure
    1.22  end
    1.23  
    1.24  structure SMT2_Failure: SMT2_FAILURE =
    1.25  struct
    1.26  
    1.27 -type counterexample = {
    1.28 -  is_real_cex: bool,
    1.29 -  free_constraints: term list,
    1.30 -  const_defs: term list}
    1.31 -
    1.32  datatype failure =
    1.33 -  Counterexample of counterexample |
    1.34 +  Counterexample of bool |
    1.35    Time_Out |
    1.36    Out_Of_Memory |
    1.37    Abnormal_Termination of int |
    1.38    Other_Failure of string
    1.39  
    1.40 -fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
    1.41 -  let
    1.42 -    val msg =
    1.43 -      if is_real_cex then "Counterexample found (possibly spurious)"
    1.44 +fun string_of_failure (Counterexample genuine) =
    1.45 +      if genuine then "Counterexample found (possibly spurious)"
    1.46        else "Potential counterexample found"
    1.47 -  in
    1.48 -    if null free_constraints andalso null const_defs then Pretty.str msg
    1.49 -    else
    1.50 -      Pretty.big_list (msg ^ ":")
    1.51 -        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
    1.52 -  end
    1.53 -
    1.54 -fun string_of_failure ctxt (Counterexample cex) =
    1.55 -      Pretty.string_of (pretty_counterexample ctxt cex)
    1.56 -  | string_of_failure _ Time_Out = "Timed out"
    1.57 -  | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    1.58 -  | string_of_failure _ (Abnormal_Termination err) =
    1.59 +  | string_of_failure Time_Out = "Timed out"
    1.60 +  | string_of_failure Out_Of_Memory = "Ran out of memory"
    1.61 +  | string_of_failure (Abnormal_Termination err) =
    1.62        "Solver terminated abnormally with error code " ^ string_of_int err
    1.63 -  | string_of_failure _ (Other_Failure msg) = msg
    1.64 +  | string_of_failure (Other_Failure msg) = msg
    1.65  
    1.66  exception SMT of failure
    1.67  
     2.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 17:34:26 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 17:34:26 2014 +0200
     2.3 @@ -183,9 +183,7 @@
     2.4      (case outcome output of
     2.5        (Unsat, ls) =>
     2.6          (case parse_proof0 of SOME pp => pp outer_ctxt replay_data ls | NONE => ([], []))
     2.7 -    | (result, _) =>
     2.8 -        raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
     2.9 -          is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
    2.10 +    | (result, _) => raise SMT2_Failure.SMT (SMT2_Failure.Counterexample (result = Sat)))
    2.11  
    2.12    fun replay outcome replay0 oracle outer_ctxt
    2.13        (replay_data as {context = ctxt, ...} : SMT2_Translate.replay_data) output =
    2.14 @@ -194,9 +192,7 @@
    2.15          if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay0
    2.16          then the replay0 outer_ctxt replay_data ls
    2.17          else oracle ()
    2.18 -    | (result, _) =>
    2.19 -        raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
    2.20 -          is_real_cex = (result = Sat), free_constraints = [], const_defs = []}))
    2.21 +    | (result, _) => raise SMT2_Failure.SMT (SMT2_Failure.Counterexample (result = Sat)))
    2.22  
    2.23    val cfalse = Thm.cterm_of @{theory} @{prop False}
    2.24  in
    2.25 @@ -297,7 +293,7 @@
    2.26  
    2.27  local
    2.28    fun str_of ctxt fail =
    2.29 -    "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure ctxt fail
    2.30 +    "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure fail
    2.31  
    2.32    fun safe_solve ctxt wfacts = SOME (apply_solver_and_replay ctxt wfacts)
    2.33      handle
    2.34 @@ -305,7 +301,7 @@
    2.35          (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
    2.36      | SMT2_Failure.SMT (fail as SMT2_Failure.Time_Out) =>
    2.37          error ("SMT: Solver " ^ quote (SMT2_Config.solver_of ctxt) ^ ": " ^
    2.38 -          SMT2_Failure.string_of_failure ctxt fail ^ " (setting the " ^
    2.39 +          SMT2_Failure.string_of_failure fail ^ " (setting the " ^
    2.40            "configuration option " ^ quote (Config.name_of SMT2_Config.timeout) ^ " might help)")
    2.41      | SMT2_Failure.SMT fail => error (str_of ctxt fail)
    2.42  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Mon Jun 02 17:34:26 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Mon Jun 02 17:34:26 2014 +0200
     3.3 @@ -85,8 +85,8 @@
     3.4     (139, Crashed)]
     3.5  val smt2_failures = z3_failures @ unix_failures
     3.6  
     3.7 -fun failure_of_smt2_failure (SMT2_Failure.Counterexample {is_real_cex, ...}) =
     3.8 -    if is_real_cex then Unprovable else GaveUp
     3.9 +fun failure_of_smt2_failure (SMT2_Failure.Counterexample genuine) =
    3.10 +    if genuine then Unprovable else GaveUp
    3.11    | failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut
    3.12    | failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) =
    3.13      (case AList.lookup (op =) smt2_failures code of