src/HOL/Tools/SMT/verit_proof.ML
author fleury
Tue Sep 30 14:01:33 2014 +0200 (2014-09-30)
changeset 58493 308f3c7dfb67
parent 58490 f6d99c69dae9
child 59014 cc5e34575354
permissions -rw-r--r--
correct inlining in veriT's subproofs.
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"
blanchet@57762
    57
val veriT_alpha_conv_rule = "tmp_alphaconv"
fleury@57705
    58
val veriT_input_rule = "input"
blanchet@57762
    59
val veriT_la_generic_rule = "la_generic"
blanchet@57762
    60
val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
blanchet@57762
    61
val veriT_simp_arith_rule = "simp_arith"
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}
blanchet@58490
   121
    fun inline_assumption assumption assumption_id
blanchet@58490
   122
        (node as VeriT_Node {id, rule, prems, concl, bounds}) =
fleury@58493
   123
      mk_node id rule (filter_out (curry (op =) assumption_id) prems)
fleury@58493
   124
        (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
fleury@57712
   125
    fun find_input_steps_and_inline [] last_step = ([], last_step)
fleury@57716
   126
      | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
fleury@57712
   127
          last_step =
fleury@57705
   128
        if rule = veriT_input_rule then
fleury@57712
   129
          find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
fleury@57705
   130
        else
fleury@57712
   131
          apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
fleury@57712
   132
            (find_input_steps_and_inline steps (id_of_father_step ^ id'))
fleury@57716
   133
    val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
fleury@57708
   134
    val prems' =
blanchet@58490
   135
      if last_step_id = "" then
blanchet@58490
   136
        prems
fleury@57708
   137
      else
fleury@57708
   138
        (case prems of
fleury@57712
   139
          NONE => SOME [last_step_id]
fleury@57712
   140
        | SOME l => SOME (last_step_id :: l))
fleury@57705
   141
  in
fleury@57712
   142
    (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx))
fleury@57705
   143
  end
fleury@57705
   144
fleury@57705
   145
(*
fleury@57705
   146
(set id rule :clauses(...) :args(..) :conclusion (...)).
fleury@57705
   147
or
fleury@57705
   148
(set id subproof (set ...) :conclusion (...)).
fleury@57705
   149
*)
fleury@57705
   150
fleury@57712
   151
fun parse_proof_step cx =
fleury@57704
   152
  let
fleury@57704
   153
    fun rotate_pair (a, (b, c)) = ((a, b), c)
blanchet@58061
   154
    fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
blanchet@58078
   155
      | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
blanchet@58061
   156
    fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
blanchet@58061
   157
    fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
blanchet@58061
   158
        (SOME (map (fn (SMTLIB.Sym id) => id) source), l)
fleury@57704
   159
      | parse_source l = (NONE, l)
blanchet@58061
   160
    fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
fleury@57712
   161
        let val (subproof_steps, cx') = parse_proof_step cx subproof_step in
fleury@57712
   162
          apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l)
fleury@57705
   163
        end
fleury@57712
   164
      | parse_subproof cx _ l = (([], cx), l)
blanchet@58061
   165
    fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l
fleury@57704
   166
      | skip_args l = l
blanchet@58061
   167
    fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl
fleury@57704
   168
    fun make_or_from_clausification l =
fleury@57708
   169
      foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
fleury@57708
   170
        (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
blanchet@58490
   171
         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
blanchet@58490
   172
    fun to_node (((((id, rule), prems), concl), bounds), cx) =
blanchet@58490
   173
      (mk_node id rule (the_default [] prems) concl bounds, cx)
fleury@57704
   174
  in
fleury@57704
   175
    get_id
fleury@57704
   176
    ##> parse_rule
fleury@57704
   177
    #> rotate_pair
fleury@57704
   178
    ##> parse_source
fleury@57704
   179
    #> rotate_pair
fleury@57704
   180
    ##> skip_args
fleury@57712
   181
    #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
fleury@57705
   182
    #> rotate_pair
fleury@57704
   183
    ##> parse_conclusion
blanchet@57762
   184
    ##> map repair_quantification
fleury@57705
   185
    #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
fleury@57705
   186
         (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
blanchet@57762
   187
    ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
fleury@57712
   188
    #> fix_subproof_steps
fleury@57705
   189
    ##> to_node
fleury@57705
   190
    #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
blanchet@57762
   191
    #-> fold_map update_step_and_cx
fleury@57705
   192
  end
fleury@57705
   193
fleury@57708
   194
(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
fleury@57708
   195
unbalanced on each line*)
fleury@57708
   196
fun seperate_into_steps lines =
fleury@57705
   197
  let
blanchet@58490
   198
    fun count ("(" :: l) n = count l (n + 1)
blanchet@58490
   199
      | count (")" :: l) n = count l (n - 1)
fleury@57705
   200
      | count (_ :: l) n = count l n
fleury@57705
   201
      | count [] n = n
fleury@57705
   202
    fun seperate (line :: l) actual_lines m =
fleury@57705
   203
        let val n = count (raw_explode line) 0 in
fleury@57705
   204
          if m + n = 0 then
fleury@57705
   205
            [actual_lines ^ line] :: seperate l "" 0
blanchet@58490
   206
          else
blanchet@58490
   207
            seperate l (actual_lines ^ line) (m + n)
fleury@57713
   208
        end
fleury@57705
   209
      | seperate [] _ 0 = []
fleury@57705
   210
  in
fleury@57705
   211
    seperate lines "" 0
fleury@57704
   212
  end
fleury@57704
   213
blanchet@58490
   214
(* VeriT adds "@" before every variable. *)
blanchet@58490
   215
fun remove_all_at (SMTLIB.Sym v :: l) =
blanchet@58490
   216
    SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
blanchet@58061
   217
  | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
blanchet@58061
   218
  | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
fleury@57705
   219
  | remove_all_at (v :: l) = v :: remove_all_at l
fleury@57705
   220
  | remove_all_at [] = []
fleury@57705
   221
fleury@57708
   222
fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) =
fleury@57705
   223
    (case List.find (fn v => String.isPrefix v var) bounds of
fleury@57708
   224
      NONE => find_in_which_step_defined var l
fleury@57708
   225
    | SOME _ => id)
fleury@57708
   226
  | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
fleury@57708
   227
fleury@57708
   228
(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
blanchet@58490
   229
fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   230
      (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $
blanchet@58490
   231
      (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) =
fleury@57708
   232
    let
fleury@57708
   233
      fun get_number_of_ite_transformed_var var =
fleury@57708
   234
        perhaps (try (unprefix "ite")) var
fleury@57708
   235
        |> Int.fromString
fleury@57708
   236
      fun is_equal_and_has_correct_substring var var' var'' =
fleury@57708
   237
        if var = var' andalso String.isPrefix "ite" var then SOME var'
fleury@57708
   238
        else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE
fleury@57708
   239
      val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4
fleury@57708
   240
      val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2
fleury@57708
   241
    in
fleury@57708
   242
      (case (var1_introduced_var, var2_introduced_var) of
fleury@57708
   243
        (SOME a, SOME b) =>
fleury@57708
   244
          (*ill-generated case, might be possible when applying the rule to max a a. Only if the
fleury@57708
   245
          variable have been introduced before. Probably an impossible edge case*)
fleury@57708
   246
          (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of
fleury@57708
   247
            (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var
fleury@57708
   248
            (*Otherwise, it is a name clase between a parameter name and the introduced variable.
fleury@57708
   249
             Or the name convention has been changed.*)
fleury@57708
   250
          | (NONE, SOME _) => var2_introduced_var
fleury@57708
   251
          | (SOME _, NONE) => var2_introduced_var)
fleury@57708
   252
      | (_, SOME _) => var2_introduced_var
fleury@57708
   253
      | (SOME _, _) => var1_introduced_var)
fleury@57708
   254
    end
blanchet@58490
   255
  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   256
      (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $
blanchet@58490
   257
      (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) =
fleury@57708
   258
    if var = var' then SOME var else NONE
blanchet@58490
   259
  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
blanchet@58490
   260
      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $
blanchet@58490
   261
      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) =
fleury@57708
   262
    if var = var' then SOME var else NONE
fleury@57708
   263
  | find_ite_var_in_term (p $ q) =
fleury@57708
   264
    (case find_ite_var_in_term p of
fleury@57708
   265
      NONE => find_ite_var_in_term q
fleury@57708
   266
    | x => x)
fleury@57708
   267
  | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
fleury@57708
   268
  | find_ite_var_in_term _ = NONE
fleury@57705
   269
blanchet@58490
   270
fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) =
fleury@57714
   271
  if rule = veriT_tmp_ite_elim_rule then
fleury@57708
   272
    if bounds = [] then
blanchet@57762
   273
      (*if the introduced var has already been defined, adding the definition as a dependency*)
fleury@57708
   274
      let
blanchet@58490
   275
        val new_prems = prems
blanchet@58490
   276
          |> (case find_ite_var_in_term concl of
blanchet@58490
   277
               NONE => I
blanchet@58490
   278
             | SOME var => cons (find_in_which_step_defined var steps))
fleury@57708
   279
      in
fleury@57716
   280
        VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
fleury@57708
   281
      end
fleury@57708
   282
    else
fleury@57708
   283
      (*some new variables are created*)
blanchet@58490
   284
      let val concl' = replace_bound_var_by_free_var concl bounds in
fleury@57715
   285
        mk_node id rule prems concl' []
fleury@57708
   286
      end
fleury@57708
   287
  else
blanchet@58490
   288
    node
fleury@57708
   289
fleury@57708
   290
fun remove_alpha_conversion _ [] = []
fleury@57708
   291
  | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
fleury@57705
   292
    let
blanchet@58490
   293
      val correct_dependency = map (perhaps (Symtab.lookup replace_table))
blanchet@58490
   294
      val find_predecessor = perhaps (Symtab.lookup replace_table)
fleury@57705
   295
    in
fleury@57713
   296
      if rule = veriT_alpha_conv_rule then
fleury@57712
   297
        remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
fleury@57708
   298
          replace_table) steps
fleury@57708
   299
      else
fleury@57708
   300
        VeriT_Node {id = id, rule = rule, prems = correct_dependency prems,
fleury@57708
   301
          concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps
fleury@57705
   302
    end
fleury@57705
   303
fleury@57708
   304
fun correct_veriT_steps steps =
fleury@57708
   305
  steps
fleury@57712
   306
  |> map (correct_veriT_step steps)
fleury@57708
   307
  |> remove_alpha_conversion Symtab.empty
fleury@57704
   308
fleury@57704
   309
fun parse typs funs lines ctxt =
fleury@57704
   310
  let
blanchet@58061
   311
    val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines))
fleury@57712
   312
    val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
blanchet@58061
   313
      smtlib_lines_without_at (empty_context ctxt typs funs))
fleury@57708
   314
    val t = correct_veriT_steps u
fleury@57708
   315
    fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
fleury@57705
   316
      mk_step id rule prems concl bounds
blanchet@58490
   317
  in
fleury@57705
   318
    (map node_to_step t, ctxt_of env)
fleury@57704
   319
  end
fleury@57704
   320
fleury@57704
   321
end;