src/HOL/Nunchaku/Tools/nunchaku.ML
author blanchet
Mon, 24 Oct 2016 22:42:07 +0200
changeset 64389 6273d4c8325b
child 64407 5c5b9d945625
permissions -rw-r--r--
added Nunchaku integration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64389
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Nunchaku/Tools/nunchaku.ML
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     3
    Copyright   2015, 2016
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     4
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     5
The core of the Nunchaku integration in Isabelle.
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     6
*)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     7
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     8
signature NUNCHAKU =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
     9
sig
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    10
  type isa_model = Nunchaku_Reconstruct.isa_model
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    11
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    12
  datatype mode = Auto_Try | Try | Normal
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    13
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    14
  type mode_of_operation_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    15
    {falsify: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    16
     assms: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    17
     spy: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    18
     overlord: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    19
     expect: string}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    20
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    21
  type scope_of_search_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    22
    {wfs: ((string * typ) option * bool option) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    23
     whacks: (term option * bool) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    24
     cards: (typ option * (int option * int option)) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    25
     monos: (typ option * bool option) list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    26
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    27
  type output_format_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    28
    {verbose: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    29
     debug: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    30
     max_potential: int,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    31
     max_genuine: int,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    32
     evals: term list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    33
     atomss: (typ option * string list) list}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    34
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    35
  type optimization_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    36
    {specialize: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    37
     multithread: bool}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    38
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    39
  type timeout_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    40
    {timeout: Time.time,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    41
     wf_timeout: Time.time}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    42
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    43
  type params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    44
    {mode_of_operation_params: mode_of_operation_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    45
     scope_of_search_params: scope_of_search_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    46
     output_format_params: output_format_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    47
     optimization_params: optimization_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    48
     timeout_params: timeout_params}
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    49
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    50
  val genuineN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    51
  val quasi_genuineN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    52
  val potentialN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    53
  val noneN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    54
  val unknownN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    55
  val no_nunchakuN: string
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    56
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    57
  val run_chaku_on_prop: Proof.state -> params -> mode -> int -> term list -> term ->
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    58
    string * isa_model option
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    59
  val run_chaku_on_subgoal: Proof.state -> params -> mode -> int -> string * isa_model option
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    60
end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    61
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    62
structure Nunchaku : NUNCHAKU =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    63
struct
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    64
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    65
open Nunchaku_Util;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    66
open Nunchaku_Collect;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    67
open Nunchaku_Problem;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    68
open Nunchaku_Translate;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    69
open Nunchaku_Model;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    70
open Nunchaku_Reconstruct;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    71
open Nunchaku_Display;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    72
open Nunchaku_Tool;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    73
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    74
datatype mode = Auto_Try | Try | Normal;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    75
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    76
type mode_of_operation_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    77
  {falsify: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    78
   assms: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    79
   spy: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    80
   overlord: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    81
   expect: string};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    82
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    83
type scope_of_search_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    84
  {wfs: ((string * typ) option * bool option) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    85
   whacks: (term option * bool) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    86
   cards: (typ option * (int option * int option)) list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    87
   monos: (typ option * bool option) list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    88
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    89
type output_format_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    90
  {verbose: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    91
   debug: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    92
   max_potential: int,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    93
   max_genuine: int,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    94
   evals: term list,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    95
   atomss: (typ option * string list) list};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    96
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    97
type optimization_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    98
  {specialize: bool,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
    99
   multithread: bool};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   100
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   101
type timeout_params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   102
  {timeout: Time.time,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   103
   wf_timeout: Time.time};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   104
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   105
type params =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   106
  {mode_of_operation_params: mode_of_operation_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   107
   scope_of_search_params: scope_of_search_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   108
   output_format_params: output_format_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   109
   optimization_params: optimization_params,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   110
   timeout_params: timeout_params};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   111
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   112
val genuineN = "genuine";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   113
val quasi_genuineN = "quasi_genuine";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   114
val potentialN = "potential";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   115
val noneN = "none";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   116
val unknownN = "unknown";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   117
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   118
val no_nunchakuN = "no_nunchaku";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   119
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   120
fun str_of_mode Auto_Try = "Auto_Try"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   121
  | str_of_mode Try = "Try"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   122
  | str_of_mode Normal = "Normal";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   123
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   124
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   125
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   126
fun has_lonely_bool_var (@{const Pure.conjunction} $ (@{const Trueprop} $ Free _) $ _) = true
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   127
  | has_lonely_bool_var _ = false;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   128
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   129
val syntactic_sorts =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   130
  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ @{sort numeral};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   131
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   132
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = subset (op =) (S, syntactic_sorts)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   133
  | has_tfree_syntactic_sort _ = false;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   134
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   135
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   136
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   137
(* Give the soft timeout a chance. *)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   138
val timeout_slack = seconds 1.0;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   139
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   140
fun run_chaku_on_prop state
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   141
    ({mode_of_operation_params = {falsify, assms, spy, overlord, expect},
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   142
      scope_of_search_params = {wfs, whacks, cards, monos},
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   143
      output_format_params = {verbose, debug, evals, atomss, ...},
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   144
      optimization_params = {specialize, ...},
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   145
      timeout_params = {timeout, wf_timeout}})
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   146
    mode i all_assms subgoal =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   147
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   148
    val ctxt = Proof.context_of state;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   149
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   150
    val timer = Timer.startRealTimer ()
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   151
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   152
    val print = writeln;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   153
    val print_n = if mode = Normal then writeln else K ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   154
    fun print_v f = if verbose then writeln (f ()) else ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   155
    fun print_d f = if debug then writeln (f ()) else ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   156
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   157
    val das_wort_Model = if falsify then "Countermodel" else "Model";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   158
    val das_wort_model = if falsify then "countermodel" else "model";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   159
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   160
    val tool_params = {overlord = overlord, debug = debug, specialize = specialize,
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   161
      timeout = timeout};
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   162
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   163
    fun run () =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   164
      let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   165
        val outcome as (outcome_code, _) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   166
          let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   167
            val (poly_axioms, isa_problem as {sound, complete, ...}) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   168
              isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   169
                (if assms then all_assms else []) subgoal;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   170
            val _ = print_d (fn () => "*** Isabelle problem ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   171
              str_of_isa_problem ctxt isa_problem);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   172
            val ugly_nun_problem = nun_problem_of_isa ctxt isa_problem;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   173
            val _ = print_d (fn () => "*** Ugly Nunchaku problem ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   174
              str_of_nun_problem ugly_nun_problem);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   175
            val (nice_nun_problem, pool) = nice_nun_problem ugly_nun_problem;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   176
            val _ = print_d (fn () => "*** Nice Nunchaku problem ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   177
              str_of_nun_problem nice_nun_problem);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   178
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   179
            fun print_any_hints () =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   180
              if has_lonely_bool_var subgoal then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   181
                print "Hint: Maybe you forgot a colon after the lemma's name?"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   182
              else if has_syntactic_sorts subgoal then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   183
                print "Hint: Maybe you forgot a type constraint?"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   184
              else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   185
                ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   186
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   187
            fun get_isa_model_opt output =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   188
              let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   189
                val nice_nun_model = nun_model_of_str output;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   190
                val _ = print_d (fn () => "*** Nice Nunchaku model ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   191
                  str_of_nun_model nice_nun_model);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   192
                val ugly_nun_model = ugly_nun_model pool nice_nun_model;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   193
                val _ = print_d (fn () => "*** Ugly Nunchaku model ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   194
                  str_of_nun_model ugly_nun_model);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   195
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   196
                val pat_completes = pat_completes_of_isa_problem isa_problem;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   197
                val isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   198
                val _ = print_d (fn () => "*** Isabelle model ***\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   199
                  str_of_isa_model ctxt isa_model);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   200
              in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   201
                isa_model
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   202
              end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   203
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   204
            fun isa_model_opt output =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   205
              if debug then SOME (get_isa_model_opt output) else try get_isa_model_opt output;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   206
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   207
            val model_str = isa_model_opt #> pretty_of_isa_model_opt ctxt #> Pretty.string_of;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   208
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   209
            fun unsat_means_theorem () =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   210
              null whacks andalso null cards andalso null monos;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   211
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   212
            fun unknown () =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   213
              (print_n ("No " ^ das_wort_model ^ " can be found \<midarrow> the problem lies \
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   214
                 \outside Nunchaku's fragment");
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   215
               (unknownN, NONE));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   216
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   217
            fun unsat_or_unknown complete =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   218
              if complete then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   219
                (print_n ("No " ^ das_wort_model ^ " exists" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   220
                   (if falsify andalso unsat_means_theorem () then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   221
                      " \<midarrow> the goal is a theorem"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   222
                    else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   223
                      ""));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   224
                 (noneN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   225
              else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   226
                unknown ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   227
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   228
            fun sat_or_maybe_sat sound output =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   229
              let val header = if sound then das_wort_Model else "Potential " ^ das_wort_model in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   230
                (case (null poly_axioms, none_true wfs) of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   231
                  (true, true) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   232
                  (print (header ^ ":\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   233
                     model_str output); print_any_hints ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   234
                   (genuineN, isa_model_opt output))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   235
                | (no_poly, no_wf) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   236
                  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   237
                    val ignorings = []
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   238
                      |> not no_poly ? cons "polymorphic axioms"
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   239
                      |> not no_wf ? cons "unchecked well-foundedness";
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   240
                  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   241
                    (print (header ^ " (ignoring " ^ space_implode " and " ignorings ^ "):\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   242
                       model_str output ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   243
                       (if no_poly then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   244
                          ""
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   245
                        else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   246
                          "\nIgnored axioms:\n" ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   247
                          cat_lines (map (prefix "  " o Syntax.string_of_term ctxt) poly_axioms)));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   248
                     print_any_hints ();
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   249
                     (quasi_genuineN, isa_model_opt output))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   250
                  end)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   251
              end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   252
          in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   253
            (case solve_nun_problem tool_params nice_nun_problem of
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   254
              Unsat => unsat_or_unknown complete
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   255
            | Sat (output, _) => sat_or_maybe_sat sound output
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   256
            | Unknown NONE => unknown ()
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   257
            | Unknown (SOME (output, _)) => sat_or_maybe_sat false output
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   258
            | Timeout => (print_n "Time out"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   259
            | Nunchaku_Var_Not_Set =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   260
              (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   261
            | Nunchaku_Cannot_Execute =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   262
              (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   263
            | Nunchaku_Not_Found =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   264
              (print_n "External tool \"nunchaku\" not found"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   265
            | CVC4_Cannot_Execute =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   266
              (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   267
            | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   268
            | Unknown_Error (code, msg) =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   269
              (print_n ("Unknown error: " ^ msg ^
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   270
                 (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   271
               (unknownN, NONE)))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   272
          end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   273
          handle
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   274
            CYCLIC_DEPS () =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   275
            (print_n "Cyclic dependencies (or bug in Nunchaku)"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   276
          | TOO_DEEP_DEPS () =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   277
            (print_n "Too deep dependencies (or bug in Nunchaku)"; (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   278
          | TOO_META t =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   279
            (print_n ("Formula too meta for Nunchaku:\n" ^ Syntax.string_of_term ctxt t);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   280
             (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   281
          | UNEXPECTED_POLYMORPHISM t =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   282
            (print_n ("Unexpected polymorphism in term\n" ^ Syntax.string_of_term ctxt t);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   283
             (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   284
          | UNEXPECTED_VAR t =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   285
            (print_n ("Unexpected schematic variables in term\n" ^ Syntax.string_of_term ctxt t);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   286
             (unknownN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   287
          | UNSUPPORTED_FUNC t =>
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   288
            (print_n ("Unsupported low-level constant in problem: " ^ Syntax.string_of_term ctxt t);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   289
             (unknownN, NONE));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   290
      in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   291
        if expect = "" orelse outcome_code = expect then outcome
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   292
        else error ("Unexpected outcome: " ^ quote outcome_code)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   293
      end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   294
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   295
    val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode"));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   296
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   297
    val outcome as (outcome_code, _) =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   298
      Timeout.apply (Time.+ (timeout, timeout_slack)) run ()
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   299
      handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   300
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   301
    val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   302
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   303
    val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   304
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   305
    if expect = "" orelse outcome_code = expect then outcome
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   306
    else error ("Unexpected outcome: " ^ quote outcome_code)
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   307
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   308
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   309
fun run_chaku_on_subgoal state params mode i =
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   310
  let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   311
    val ctxt = Proof.context_of state;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   312
    val goal = Thm.prop_of (#goal (Proof.raw_goal state));
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   313
  in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   314
    if Logic.count_prems goal = 0 then
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   315
      (writeln "No subgoal!"; (noneN, NONE))
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   316
    else
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   317
      let
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   318
        val subgoal = fst (Logic.goal_params goal i);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   319
        val all_assms = map Thm.term_of (Assumption.all_assms_of ctxt);
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   320
      in
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   321
        run_chaku_on_prop state params mode i all_assms subgoal
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   322
      end
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   323
  end;
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   324
6273d4c8325b added Nunchaku integration
blanchet
parents:
diff changeset
   325
end;