src/HOL/Tools/SMT/verit_proof.ML
author fleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Nov 10 17:49:54 2015 +0100 (2015-11-10)
changeset 61611 a9c0572109af
parent 59014 cc5e34575354
child 69205 8050734eee3e
permissions -rw-r--r--
fixing premises in veriT proof reconstruction
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/verit_proof.ML
fleury@57704
     2
    Author:     Mathias Fleury, ENS Rennes
fleury@57704
     3
    Author:     Sascha Boehme, TU Muenchen
fleury@57704
     4
fleury@57704
     5
VeriT proofs: parsing and abstract syntax tree.
fleury@57704
     6
*)
fleury@57704
     7
fleury@57704
     8
signature VERIT_PROOF =
fleury@57704
     9
sig
fleury@57704
    10
  (*proofs*)
fleury@57704
    11
  datatype veriT_step = VeriT_Step of {
fleury@57712
    12
    id: string,
fleury@57704
    13
    rule: string,
fleury@57704
    14
    prems: string list,
fleury@57704
    15
    concl: term,
fleury@57704
    16
    fixes: string list}
fleury@57704
    17
fleury@57704
    18
  (*proof parser*)
fleury@57704
    19
  val parse: typ Symtab.table -> term Symtab.table -> string list ->
fleury@57704
    20
    Proof.context -> veriT_step list * Proof.context
fleury@57704
    21
fleury@57705
    22
  val veriT_step_prefix : string
fleury@57705
    23
  val veriT_input_rule: string
blanchet@57762
    24
  val veriT_la_generic_rule : string
fleury@57705
    25
  val veriT_rewrite_rule : string
blanchet@57762
    26
  val veriT_simp_arith_rule : string
blanchet@57762
    27
  val veriT_tmp_ite_elim_rule : string
fleury@57714
    28
  val veriT_tmp_skolemize_rule : string
fleury@57704
    29
end;
fleury@57704
    30
fleury@57704
    31
structure VeriT_Proof: VERIT_PROOF =
fleury@57704
    32
struct
fleury@57704
    33
blanchet@58061
    34
open SMTLIB_Proof
fleury@57704
    35
fleury@57704
    36
datatype veriT_node = VeriT_Node of {
fleury@57712
    37
  id: string,
fleury@57704
    38
  rule: string,
fleury@57704
    39
  prems: string list,
fleury@57704
    40
  concl: term,
fleury@57704
    41
  bounds: string list}
fleury@57704
    42
fleury@57704
    43
fun mk_node id rule prems concl bounds =
fleury@57704
    44
  VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
fleury@57704
    45
fleury@57704
    46
datatype veriT_step = VeriT_Step of {
fleury@57712
    47
  id: string,
fleury@57704
    48
  rule: string,
fleury@57704
    49
  prems: string list,
fleury@57704
    50
  concl: term,
fleury@57704
    51
  fixes: string list}
fleury@57704
    52
fleury@57704
    53
fun mk_step id rule prems concl fixes =
fleury@57704
    54
  VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
fleury@57704
    55
fleury@57705
    56
val veriT_step_prefix = ".c"
fleury@57705
    57
val veriT_input_rule = "input"
blanchet@57762
    58
val veriT_la_generic_rule = "la_generic"
blanchet@57762
    59
val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
blanchet@57762
    60
val veriT_simp_arith_rule = "simp_arith"
blanchet@59014
    61
val veriT_tmp_alphaconv_rule = "tmp_alphaconv"
fleury@57708
    62
val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
fleury@57713
    63
val veriT_tmp_skolemize_rule = "tmp_skolemize"
fleury@57708
    64
fleury@57704
    65
(* proof parser *)
fleury@57704
    66
fleury@57704
    67
fun node_of p cx =
fleury@57704
    68
  ([], cx)
blanchet@57747
    69
  ||>> `(with_fresh_names (term_of p))
fleury@57716
    70
  |>> snd
fleury@57704
    71
fleury@57704
    72
(*in order to get Z3-style quantification*)
blanchet@58061
    73
fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) =
blanchet@57762
    74
    let val (quantified_vars, t) = split_last (map repair_quantification l)
fleury@57704
    75
    in
blanchet@58061
    76
      SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: [])
fleury@57704
    77
    end
blanchet@58061
    78
  | repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) =
blanchet@57762
    79
    let val (quantified_vars, t) = split_last (map repair_quantification l)
fleury@57704
    80
    in
blanchet@58061
    81
      SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: [])
fleury@57704
    82
    end
blanchet@58061
    83
  | repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l)
blanchet@57762
    84
  | repair_quantification x = x
fleury@57704
    85
fleury@57708
    86
fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var =
fleury@57705
    87
    (case List.find (fn v => String.isPrefix v var) free_var of
fleury@57708
    88
      NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var)
fleury@57708
    89
    | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var)
fleury@57708
    90
  | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $
fleury@57708
    91
     replace_bound_var_by_free_var v free_vars
fleury@57708
    92
  | replace_bound_var_by_free_var u _ = u
fleury@57705
    93
blanchet@58490
    94
fun find_type_in_formula (Abs (v, T, u)) var_name =
blanchet@58490
    95
    if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
fleury@57705
    96
  | find_type_in_formula (u $ v) var_name =
fleury@57705
    97
    (case find_type_in_formula u var_name of
fleury@57705
    98
      NONE => find_type_in_formula v var_name
blanchet@58490
    99
    | some_T => some_T)
fleury@57705
   100
  | find_type_in_formula _ _ = NONE
fleury@57705
   101
blanchet@58490
   102
fun add_bound_variables_to_ctxt concl =
blanchet@58490
   103
  fold (update_binding o
blanchet@58490
   104
    (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
fleury@57705
   105
blanchet@58490
   106
fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx =
fleury@57708
   107
  if rule = veriT_tmp_ite_elim_rule then
blanchet@58490
   108
    (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx)
fleury@57713
   109
  else if rule = veriT_tmp_skolemize_rule then
blanchet@58490
   110
    let val concl' = replace_bound_var_by_free_var concl bounds in
blanchet@58490
   111
      (mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx)
fleury@57705
   112
    end
fleury@57705
   113
  else
blanchet@58490
   114
    (node, cx)
fleury@57705
   115
fleury@57712
   116
fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
fleury@57705
   117
    cx)) =
fleury@57705
   118
  let
blanchet@58490
   119
    fun mk_prop_of_term concl =
blanchet@58490
   120
      concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
Mathias@61611
   121
    fun update_prems assumption_id prems =
Mathias@61611
   122
      map (fn prem => id_of_father_step ^ prem)
Mathias@61611
   123
          (filter_out (curry (op =) assumption_id) prems)
blanchet@58490
   124
    fun inline_assumption assumption assumption_id
Mathias@61611
   125
        (VeriT_Node {id, rule, prems, concl, bounds}) =
Mathias@61611
   126
      mk_node id rule (update_prems assumption_id prems)
fleury@58493
   127
        (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
fleury@57712
   128
    fun find_input_steps_and_inline [] last_step = ([], last_step)
fleury@57716
   129
      | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
fleury@57712
   130
          last_step =
fleury@57705
   131
        if rule = veriT_input_rule then
fleury@57712
   132
          find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
fleury@57705
   133
        else
fleury@57712
   134
          apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
fleury@57712
   135
            (find_input_steps_and_inline steps (id_of_father_step ^ id'))
fleury@57716
   136
    val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
fleury@57708
   137
    val prems' =
blanchet@58490
   138
      if last_step_id = "" then
blanchet@58490
   139
        prems
fleury@57708
   140
      else
fleury@57708
   141
        (case prems of
fleury@57712
   142
          NONE => SOME [last_step_id]
fleury@57712
   143
        | SOME l => SOME (last_step_id :: l))
fleury@57705
   144
  in
fleury@57712
   145
    (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx))
fleury@57705
   146
  end
fleury@57705
   147
fleury@57705
   148
(*
fleury@57705
   149
(set id rule :clauses(...) :args(..) :conclusion (...)).
fleury@57705
   150
or
fleury@57705
   151
(set id subproof (set ...) :conclusion (...)).
fleury@57705
   152
*)
fleury@57705
   153
fleury@57712
   154
fun parse_proof_step cx =
fleury@57704
   155
  let
fleury@57704
   156
    fun rotate_pair (a, (b, c)) = ((a, b), c)
blanchet@58061
   157
    fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
blanchet@58078
   158
      | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
blanchet@58061
   159
    fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
blanchet@58061
   160
    fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
blanchet@58061
   161
        (SOME (map (fn (SMTLIB.Sym id) => id) source), l)
fleury@57704
   162
      | parse_source l = (NONE, l)
blanchet@58061
   163
    fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
fleury@57712
   164
        let val (subproof_steps, cx') = parse_proof_step cx subproof_step in
fleury@57712
   165
          apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l)
fleury@57705
   166
        end
fleury@57712
   167
      | parse_subproof cx _ l = (([], cx), l)
blanchet@58061
   168
    fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l
fleury@57704
   169
      | skip_args l = l
blanchet@58061
   170
    fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl
fleury@57704
   171
    fun make_or_from_clausification l =
fleury@57708
   172
      foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
fleury@57708
   173
        (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
blanchet@58490
   174
         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
blanchet@58490
   175
    fun to_node (((((id, rule), prems), concl), bounds), cx) =
blanchet@58490
   176
      (mk_node id rule (the_default [] prems) concl bounds, cx)
fleury@57704
   177
  in
fleury@57704
   178
    get_id
fleury@57704
   179
    ##> parse_rule
fleury@57704
   180
    #> rotate_pair
fleury@57704
   181
    ##> parse_source
fleury@57704
   182
    #> rotate_pair
fleury@57704
   183
    ##> skip_args
fleury@57712
   184
    #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
fleury@57705
   185
    #> rotate_pair
fleury@57704
   186
    ##> parse_conclusion
blanchet@57762
   187
    ##> map repair_quantification
fleury@57705
   188
    #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
fleury@57705
   189
         (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
blanchet@57762
   190
    ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
fleury@57712
   191
    #> fix_subproof_steps
fleury@57705
   192
    ##> to_node
fleury@57705
   193
    #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
blanchet@57762
   194
    #-> fold_map update_step_and_cx
fleury@57705
   195
  end
fleury@57705
   196
fleury@57708
   197
(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
fleury@57708
   198
unbalanced on each line*)
fleury@57708
   199
fun seperate_into_steps lines =
fleury@57705
   200
  let
blanchet@58490
   201
    fun count ("(" :: l) n = count l (n + 1)
blanchet@58490
   202
      | count (")" :: l) n = count l (n - 1)
fleury@57705
   203
      | count (_ :: l) n = count l n
fleury@57705
   204
      | count [] n = n
fleury@57705
   205
    fun seperate (line :: l) actual_lines m =
fleury@57705
   206
        let val n = count (raw_explode line) 0 in
fleury@57705
   207
          if m + n = 0 then
fleury@57705
   208
            [actual_lines ^ line] :: seperate l "" 0
blanchet@58490
   209
          else
blanchet@58490
   210
            seperate l (actual_lines ^ line) (m + n)
fleury@57713
   211
        end
fleury@57705
   212
      | seperate [] _ 0 = []
fleury@57705
   213
  in
fleury@57705
   214
    seperate lines "" 0
fleury@57704
   215
  end
fleury@57704
   216
blanchet@58490
   217
(* VeriT adds "@" before every variable. *)
blanchet@58490
   218
fun remove_all_at (SMTLIB.Sym v :: l) =
blanchet@58490
   219
    SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
blanchet@58061
   220
  | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
blanchet@58061
   221
  | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
fleury@57705
   222
  | remove_all_at (v :: l) = v :: remove_all_at l
fleury@57705
   223
  | remove_all_at [] = []
fleury@57705
   224
fleury@57708
   225
fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) =
fleury@57705
   226
    (case List.find (fn v => String.isPrefix v var) bounds of
fleury@57708
   227
      NONE => find_in_which_step_defined var l
fleury@57708
   228
    | SOME _ => id)
fleury@57708
   229
  | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
fleury@57708
   230
fleury@57708
   231
(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
blanchet@58490
   232
fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   233
      (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $
blanchet@58490
   234
      (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) =
fleury@57708
   235
    let
fleury@57708
   236
      fun get_number_of_ite_transformed_var var =
fleury@57708
   237
        perhaps (try (unprefix "ite")) var
fleury@57708
   238
        |> Int.fromString
fleury@57708
   239
      fun is_equal_and_has_correct_substring var var' var'' =
fleury@57708
   240
        if var = var' andalso String.isPrefix "ite" var then SOME var'
fleury@57708
   241
        else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE
fleury@57708
   242
      val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4
fleury@57708
   243
      val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2
fleury@57708
   244
    in
fleury@57708
   245
      (case (var1_introduced_var, var2_introduced_var) of
fleury@57708
   246
        (SOME a, SOME b) =>
fleury@57708
   247
          (*ill-generated case, might be possible when applying the rule to max a a. Only if the
fleury@57708
   248
          variable have been introduced before. Probably an impossible edge case*)
fleury@57708
   249
          (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of
fleury@57708
   250
            (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var
fleury@57708
   251
            (*Otherwise, it is a name clase between a parameter name and the introduced variable.
fleury@57708
   252
             Or the name convention has been changed.*)
fleury@57708
   253
          | (NONE, SOME _) => var2_introduced_var
fleury@57708
   254
          | (SOME _, NONE) => var2_introduced_var)
fleury@57708
   255
      | (_, SOME _) => var2_introduced_var
fleury@57708
   256
      | (SOME _, _) => var1_introduced_var)
fleury@57708
   257
    end
blanchet@58490
   258
  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   259
      (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $
blanchet@58490
   260
      (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) =
fleury@57708
   261
    if var = var' then SOME var else NONE
blanchet@58490
   262
  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   263
      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $
blanchet@58490
   264
      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) =
fleury@57708
   265
    if var = var' then SOME var else NONE
fleury@57708
   266
  | find_ite_var_in_term (p $ q) =
fleury@57708
   267
    (case find_ite_var_in_term p of
fleury@57708
   268
      NONE => find_ite_var_in_term q
fleury@57708
   269
    | x => x)
fleury@57708
   270
  | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
fleury@57708
   271
  | find_ite_var_in_term _ = NONE
fleury@57705
   272
blanchet@58490
   273
fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) =
fleury@57714
   274
  if rule = veriT_tmp_ite_elim_rule then
fleury@57708
   275
    if bounds = [] then
blanchet@57762
   276
      (*if the introduced var has already been defined, adding the definition as a dependency*)
fleury@57708
   277
      let
blanchet@58490
   278
        val new_prems = prems
blanchet@58490
   279
          |> (case find_ite_var_in_term concl of
blanchet@58490
   280
               NONE => I
blanchet@58490
   281
             | SOME var => cons (find_in_which_step_defined var steps))
fleury@57708
   282
      in
fleury@57716
   283
        VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
fleury@57708
   284
      end
fleury@57708
   285
    else
fleury@57708
   286
      (*some new variables are created*)
blanchet@58490
   287
      let val concl' = replace_bound_var_by_free_var concl bounds in
fleury@57715
   288
        mk_node id rule prems concl' []
fleury@57708
   289
      end
fleury@57708
   290
  else
blanchet@58490
   291
    node
fleury@57708
   292
fleury@57708
   293
fun remove_alpha_conversion _ [] = []
fleury@57708
   294
  | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
fleury@57705
   295
    let
blanchet@58490
   296
      val correct_dependency = map (perhaps (Symtab.lookup replace_table))
blanchet@58490
   297
      val find_predecessor = perhaps (Symtab.lookup replace_table)
fleury@57705
   298
    in
blanchet@59014
   299
      if rule = veriT_tmp_alphaconv_rule then
fleury@57712
   300
        remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
fleury@57708
   301
          replace_table) steps
fleury@57708
   302
      else
fleury@57708
   303
        VeriT_Node {id = id, rule = rule, prems = correct_dependency prems,
fleury@57708
   304
          concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps
fleury@57705
   305
    end
fleury@57705
   306
fleury@57708
   307
fun correct_veriT_steps steps =
fleury@57708
   308
  steps
fleury@57712
   309
  |> map (correct_veriT_step steps)
fleury@57708
   310
  |> remove_alpha_conversion Symtab.empty
fleury@57704
   311
fleury@57704
   312
fun parse typs funs lines ctxt =
fleury@57704
   313
  let
blanchet@58061
   314
    val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines))
fleury@57712
   315
    val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
blanchet@58061
   316
      smtlib_lines_without_at (empty_context ctxt typs funs))
fleury@57708
   317
    val t = correct_veriT_steps u
fleury@57708
   318
    fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
fleury@57705
   319
      mk_step id rule prems concl bounds
blanchet@58490
   320
  in
fleury@57705
   321
    (map node_to_step t, ctxt_of env)
fleury@57704
   322
  end
fleury@57704
   323
fleury@57704
   324
end;