src/HOL/Tools/SMT/verit_replay.ML

Added tag Isabelle2019-RC4 for changeset ad2d84c42380

(*  Title:      HOL/Tools/SMT/verit_replay.ML
    Author:     Mathias Fleury, MPII

VeriT proof parsing and replay.
*)

signature VERIT_REPLAY =
sig
  val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm
end;

structure Verit_Replay: VERIT_REPLAY =
struct

fun under_fixes f unchanged_prems (prems, nthms) names args (concl, ctxt) =
  let
    val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems
    val _ =  SMT_Config.veriT_msg ctxt (fn () => \<^print>  ("names =", names))
    val thms2 = map snd nthms
    val _ = SMT_Config.veriT_msg ctxt (fn () => \<^print> ("prems=", prems))
    val _ = SMT_Config.veriT_msg ctxt (fn () => \<^print> ("nthms=", nthms))
    val _ = SMT_Config.veriT_msg ctxt (fn () => \<^print> ("thms1=", thms1))
    val _ = SMT_Config.veriT_msg ctxt (fn () => \<^print> ("thms2=", thms2))
  in (f ctxt (thms1 @ thms2) args concl) end


(** Replaying **)

fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms
    concl_transformation global_transformation args
    (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds,  ...}) =
  let
    val _ = SMT_Config.veriT_msg ctxt (fn () => \<^print> id)
    val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
        Raw_Simplifier.rewrite_term thy rewrite_rules []
        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
      end
    val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
        Raw_Simplifier.rewrite_term thy rewrite_rules []
        #> Object_Logic.atomize_term ctxt
        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
        #> SMTLIB_Isar.unskolemize_names ctxt
        #> HOLogic.mk_Trueprop
      end
    val concl = concl
      |> concl_transformation
      |> global_transformation
      |> post
in
  if rule = VeriT_Proof.veriT_input_rule then
    (case Symtab.lookup assumed id of
      SOME (_, thm) => thm)
  else
    under_fixes (method_for rule) unchanged_prems
      (prems, nthms) (map fst bounds)
      (map rewrite args) (concl, ctxt)
end

fun add_used_asserts_in_step (VeriT_Proof.VeriT_Replay_Node {prems,
    subproof = (_, _, subproof), ...}) =
  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems @
     flat (map (fn x => add_used_asserts_in_step x []) subproof))

fun remove_rewrite_rules_from_rules n =
  (fn (step as VeriT_Proof.VeriT_Replay_Node {id, ...}) =>
    (case try SMTLIB_Interface.assert_index_of_name id of
      NONE => SOME step
    | SOME a => if a < n then NONE else SOME step))

fun replay_step rewrite_rules ll_defs assumed proof_prems
  (step as VeriT_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args,
     subproof = (fixes, assms, subproof), concl, ...}) state =
  let
    val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
    val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt
      |> (fn (names, ctxt) => (names,
        fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt))

    val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt
       ||> fold Variable.declare_term (map Free fixes)
    val export_vars =
      Term.subst_free (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
      o concl_tranformation

    val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
        Raw_Simplifier.rewrite_term thy rewrite_rules []
        #> Object_Logic.atomize_term ctxt
        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
        #> SMTLIB_Isar.unskolemize_names ctxt
        #> HOLogic.mk_Trueprop
      end
    val assms = map (export_vars o global_transformation o post) assms
    val (proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) assms)
      sub_ctxt

    val all_proof_prems = proof_prems @ proof_prems'
    val (proofs', stats, _, _, sub_global_rew) =
       fold (replay_step rewrite_rules ll_defs assumed all_proof_prems) subproof
         (assumed, stats, sub_ctxt2, export_vars, global_transformation)
    val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt)
    val nthms = prems
      |>  map (apsnd export_thm o the o (Symtab.lookup (if null subproof then proofs else proofs')))
    val proof_prems =
       if Verit_Replay_Methods.veriT_step_requires_subproof_assms rule then proof_prems else []
    val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
       ctxt assumed [] (proof_prems) nthms concl_tranformation global_transformation args)
    val ({elapsed, ...}, thm) =
      SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
    val stats' = Symtab.cons_list (rule, Time.toMilliseconds elapsed) stats
  in (Symtab.update (id, (map fst bounds, thm)) proofs, stats', ctxt,
       concl_tranformation, sub_global_rew) end

fun replay_ll_def assms ll_defs rewrite_rules stats ctxt term =
  let
    val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
        Raw_Simplifier.rewrite_term thy rewrite_rules []
        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
      end
   val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
    val ({elapsed, ...}, thm) =
      SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay
         (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt)
        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
    val stats' = Symtab.cons_list ("ll_defs", Time.toMilliseconds elapsed) stats
  in
    (thm, stats')
  end

fun replay outer_ctxt
    ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data)
     output =
  let
    val rewrite_rules =
      filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify},
          Thm.prop_of thm))
        rewrite_rules
    val num_ll_defs = length ll_defs
    val index_of_id = Integer.add (~ num_ll_defs)
    val id_of_index = Integer.add num_ll_defs

    val (actual_steps, ctxt2) =
      VeriT_Proof.parse_replay typs terms output ctxt

    fun step_of_assume (j, (_, th)) =
      VeriT_Proof.VeriT_Replay_Node {
        id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
        rule = VeriT_Proof.veriT_input_rule,
        args = [],
        prems = [],
        proof_ctxt = [],
        concl = Thm.prop_of th
          |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
               (empty_simpset ctxt addsimps rewrite_rules)) [] [],
        bounds = [],
        subproof = ([], [], [])}
    val used_assert_ids = fold add_used_asserts_in_step actual_steps []
    fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
      Raw_Simplifier.rewrite_term thy rewrite_rules [] end
    val used_assm_js =
      map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
          else NONE end)
        used_assert_ids

    val assm_steps = map step_of_assume used_assm_js
    val steps = assm_steps @ actual_steps

    fun extract (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) =
         (id, rule, concl, map fst bounds)
    fun cond rule = rule = VeriT_Proof.veriT_input_rule
    val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
    val ((_, _), (ctxt3, assumed)) =
      add_asssert outer_ctxt rewrite_rules assms
        (map_filter (remove_rewrite_rules_from_rules num_ll_defs) steps) ctxt2

    val used_rew_js =
      map_filter (fn id => let val i = index_of_id id in if i < 0
          then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end)
        used_assert_ids
    val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) =>
           let val (thm, stats) =  replay_ll_def assms ll_defs rewrite_rules stats ctxt thm
           in (Symtab.update (SMTLIB_Interface.assert_name_of_index id, ([], thm)) assumed, stats)
           end)
         used_rew_js (assumed,  Symtab.empty)

    val ctxt4 =
      ctxt3
      |> put_simpset (SMT_Replay.make_simpset ctxt3 [])
      |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
    val len = length steps
    val start = Timing.start ()
    val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len
    fun blockwise f (i, x) y =
      (if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y)
    val (proofs, stats, ctxt5, _, _) =
      fold_index (blockwise (replay_step rewrite_rules ll_defs assumed [])) steps
        (assumed, stats, ctxt4, fn x => x, fn x => x)
    val _ = print_runtime_statistics len
    val total = Time.toMilliseconds (#elapsed (Timing.result start))
    val (_, VeriT_Proof.VeriT_Replay_Node {id, ...}) = split_last steps
    val _ = SMT_Config.statistics_msg ctxt5
      (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats
  in
    Symtab.lookup proofs id |> the |> snd |> singleton (Proof_Context.export ctxt5 outer_ctxt)
  end

end