# HG changeset patch # User fleury # Date 1540913044 -3600 # Node ID 8050734eee3ee3b314962bfb02e978f85f3dba17 # Parent d5ab1636660bfbf976d2cd69f8149bf1572e800c add reconstruction by veriT in method smt diff -r d5ab1636660b -r 8050734eee3e CONTRIBUTORS --- a/CONTRIBUTORS Tue Oct 30 16:24:01 2018 +0100 +++ b/CONTRIBUTORS Tue Oct 30 16:24:04 2018 +0100 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* October 2018: Mathias Fleury + Proof reconstruction for the SMT solver veriT in the smt method + Contributions to Isabelle2018 ----------------------------- diff -r d5ab1636660b -r 8050734eee3e NEWS --- a/NEWS Tue Oct 30 16:24:01 2018 +0100 +++ b/NEWS Tue Oct 30 16:24:04 2018 +0100 @@ -55,6 +55,8 @@ * Sledgehammer: The URL for SystemOnTPTP, which is used by remote provers, has been updated. +* SMT: reconstruction is now possible using the SMT solver veriT. + * Session HOL-SPARK: .prv files are no longer written to the file-system, but exported to the session database. Results may be retrieved with the "isabelle export" command-line tool like this: diff -r d5ab1636660b -r 8050734eee3e src/HOL/SMT.thy --- a/src/HOL/SMT.thy Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/SMT.thy Tue Oct 30 16:24:04 2018 +0100 @@ -190,6 +190,100 @@ by (simp add: z3mod_def) +subsection \Extra theorems for veriT reconstruction\ + +lemma verit_sko_forall: \(\x. P x) \ P (SOME x. \P x)\ + using someI[of \\x. \P x\] + by auto + +lemma verit_sko_forall': \P (SOME x. \P x) = A \ (\x. P x) = A\ + by (subst verit_sko_forall) + +lemma verit_sko_forall_indirect: \x = (SOME x. \P x) \ (\x. P x) \ P x\ + using someI[of \\x. \P x\] + by auto + +lemma verit_sko_ex: \(\x. P x) \ P (SOME x. P x)\ + using someI[of \\x. P x\] + by auto + +lemma verit_sko_ex': \P (SOME x. P x) = A \ (\x. P x) = A\ + by (subst verit_sko_ex) + +lemma verit_sko_ex_indirect: \x = (SOME x. P x) \ (\x. P x) \ P x\ + using someI[of \\x. P x\] + by auto + +lemma verit_Pure_trans: + \P \ Q \ Q \ P\ + by auto + +lemma verit_if_cong: + assumes \b \ c\ + and \c \ x \ u\ + and \\ c \ y \ v\ + shows \(if b then x else y) \ (if c then u else v)\ + using assms if_cong[of b c x u] by auto + +lemma verit_if_weak_cong': + \b \ c \ (if b then x else y) \ (if c then x else y)\ + by auto + +lemma verit_ite_intro_simp: + \(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\ + \(if c then R else b = (if c then R' else Q')) = + (if c then R else b = Q')\ + \(if c then a' = a' else b' = b')\ + by (auto split: if_splits) + +lemma verit_or_neg: + \(A \ B) \ B \ \A\ + \(\A \ B) \ B \ A\ + by auto + +lemma verit_subst_bool: \P \ f True \ f P\ + by auto + +lemma verit_and_pos: + \(a \ \b \ A) \ \(a \ b) \ A\ + \(a \ A) \ \a \ A\ + \(\a \ A) \ a \ A\ + by blast+ + +lemma verit_la_generic: + \(a::int) \ x \ a = x \ a \ x\ + by linarith + +lemma verit_tmp_bfun_elim: + \(if b then P True else P False) = P b\ + by (cases b) auto + +lemma verit_eq_true_simplify: + \(P = True) \ P\ + by auto + +lemma verit_and_neg: + \B \ B' \ (A \ B) \ \A \ B'\ + \B \ B' \ (\A \ B) \ A \ B'\ + by auto + +lemma verit_forall_inst: + \A \ B \ \A \ B\ + \\A \ B \ A \ B\ + \A \ B \ \B \ A\ + \A \ \B \ B \ A\ + \A \ B \ \A \ B\ + \\A \ B \ A \ B\ + by blast+ + +lemma verit_eq_transitive: + \A = B \ B = C \ A = C\ + \A = B \ C = B \ A = C\ + \B = A \ B = C \ A = C\ + \B = A \ C = B \ A = C\ + by auto + + subsection \Setup\ ML_file "Tools/SMT/smt_util.ML" @@ -218,6 +312,8 @@ ML_file "Tools/SMT/z3_replay_rules.ML" ML_file "Tools/SMT/z3_replay_methods.ML" ML_file "Tools/SMT/z3_replay.ML" +ML_file "Tools/SMT/verit_replay_methods.ML" +ML_file "Tools/SMT/verit_replay.ML" ML_file "Tools/SMT/smt_systems.ML" method_setup smt = \ @@ -276,7 +372,7 @@ declare [[cvc3_options = ""]] declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] -declare [[verit_options = "--index-sorts --index-fresh-sorts"]] +declare [[verit_options = "--index-fresh-sorts"]] declare [[z3_options = ""]] text \ diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/conj_disj_perm.ML --- a/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Oct 30 16:24:04 2018 +0100 @@ -124,4 +124,4 @@ resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i | _ => no_tac)) -end +end; diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Tue Oct 30 16:24:04 2018 +0100 @@ -47,6 +47,7 @@ val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit + val veriT_msg: Proof.context -> (unit -> 'a) -> unit (*certificates*) val select_certificates: string -> Context.generic -> Context.generic @@ -179,6 +180,7 @@ val read_only_certificates = Attrib.setup_config_bool \<^binding>\smt_read_only_certificates\ (K false) val verbose = Attrib.setup_config_bool \<^binding>\smt_verbose\ (K true) val trace = Attrib.setup_config_bool \<^binding>\smt_trace\ (K false) +val trace_veriT = Attrib.setup_config_bool \<^binding>\smt_debug_verit\ (K false) val statistics = Attrib.setup_config_bool \<^binding>\smt_statistics\ (K false) val monomorph_limit = Attrib.setup_config_int \<^binding>\smt_monomorph_limit\ (K 10) val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (K 500) @@ -198,6 +200,8 @@ fun trace_msg ctxt = cond_trace (Config.get ctxt trace) fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics) +fun veriT_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_veriT) then ignore(x ()) else () + (* tools *) diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/smt_real.ML --- a/src/HOL/Tools/SMT/smt_real.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/smt_real.ML Tue Oct 30 16:24:04 2018 +0100 @@ -110,6 +110,6 @@ SMTLIB_Interface.add_logic (10, smtlib_logic) #> setup_builtins #> Z3_Interface.add_mk_builtins z3_mk_builtins #> - Z3_Replay_Util.add_simproc real_linarith_proc)) + SMT_Replay.add_simproc real_linarith_proc)) end; diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 30 16:24:04 2018 +0100 @@ -90,12 +90,14 @@ val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input - val {redirected_output = res, output = err, return_code} = - SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input + val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) = + Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val output = drop_suffix (equal "") res val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output + val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)] + val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)] val _ = member (op =) normal_return_codes return_code orelse raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Oct 30 16:24:04 2018 +0100 @@ -119,7 +119,7 @@ avail = make_avail "VERIT", command = make_command "VERIT", options = (fn ctxt => [ - "--proof-version=1", + "--proof-version=2", "--proof-prune", "--proof-merge", "--disable-print-success", @@ -129,7 +129,7 @@ default_max_relevant = 200 (* FUDGE *), outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"), parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), - replay = NONE } + replay = SOME Verit_Replay.replay } end diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/smtlib_proof.ML --- a/src/HOL/Tools/SMT/smtlib_proof.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/smtlib_proof.ML Tue Oct 30 16:24:04 2018 +0100 @@ -265,10 +265,13 @@ fun dest_binding (SMTLIB.S [SMTLIB.Sym name, t]) = (name, Tree t) | dest_binding b = raise SMTLIB_PARSE ("bad SMT let binding format", b) +fun mk_choice (x, T, P) = HOLogic.choice_const T $ absfree (x, T) P + fun term_of t cx = (case t of SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx + | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] => with_bindings (map dest_binding bindings) (term_of body) cx | SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/verit_proof.ML --- a/src/HOL/Tools/SMT/verit_proof.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Oct 30 16:24:04 2018 +0100 @@ -12,20 +12,36 @@ id: string, rule: string, prems: string list, + proof_ctxt: term list, concl: term, fixes: string list} + datatype veriT_replay_node = VeriT_Replay_Node of { + id: string, + rule: string, + args: term list, + prems: string list, + proof_ctxt: term list, + concl: term, + bounds: (string * typ) list, + subproof: (string * typ) list * term list * veriT_replay_node list} + (*proof parser*) val parse: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> veriT_step list * Proof.context + val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> + Proof.context -> veriT_replay_node list * Proof.context + val map_replay_prems: (string list -> string list) -> veriT_replay_node -> veriT_replay_node val veriT_step_prefix : string val veriT_input_rule: string + val veriT_normalized_input_rule: string val veriT_la_generic_rule : string val veriT_rewrite_rule : string val veriT_simp_arith_rule : string - val veriT_tmp_ite_elim_rule : string val veriT_tmp_skolemize_rule : string + val veriT_subproof_rule : string + val veriT_local_input_rule : string end; structure VeriT_Proof: VERIT_PROOF = @@ -33,33 +49,66 @@ open SMTLIB_Proof +datatype raw_veriT_node = Raw_VeriT_Node of { + id: string, + rule: string, + args: SMTLIB.tree, + prems: string list, + concl: SMTLIB.tree, + subproof: raw_veriT_node list} + +fun mk_raw_node id rule args prems concl subproof = + Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, concl = concl, + subproof = subproof} + datatype veriT_node = VeriT_Node of { id: string, rule: string, prems: string list, + proof_ctxt: term list, concl: term, bounds: string list} -fun mk_node id rule prems concl bounds = - VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} +fun mk_node id rule prems proof_ctxt concl bounds = + VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, + bounds = bounds} + +datatype veriT_replay_node = VeriT_Replay_Node of { + id: string, + rule: string, + args: term list, + prems: string list, + proof_ctxt: term list, + concl: term, + bounds: (string * typ) list, + subproof: (string * typ) list * term list * veriT_replay_node list} + +fun mk_replay_node id rule args prems proof_ctxt concl bounds subproof = + VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, + concl = concl, bounds = bounds, subproof = subproof} datatype veriT_step = VeriT_Step of { id: string, rule: string, prems: string list, + proof_ctxt: term list, concl: term, fixes: string list} -fun mk_step id rule prems concl fixes = - VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} +fun mk_step id rule prems proof_ctxt concl fixes = + VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, + fixes = fixes} val veriT_step_prefix = ".c" val veriT_input_rule = "input" val veriT_la_generic_rule = "la_generic" +val veriT_normalized_input_rule = "__normalized_input" (* arbitrary *) val veriT_rewrite_rule = "__rewrite" (* arbitrary *) +val veriT_subproof_rule = "subproof" +val veriT_local_input_rule = "__local_input" (* arbitrary *) val veriT_simp_arith_rule = "simp_arith" -val veriT_tmp_alphaconv_rule = "tmp_alphaconv" -val veriT_tmp_ite_elim_rule = "tmp_ite_elim" + +(* Even the veriT developer do not know if the following rule can still appear in proofs: *) val veriT_tmp_skolemize_rule = "tmp_skolemize" (* proof parser *) @@ -69,131 +118,229 @@ ||>> `(with_fresh_names (term_of p)) |>> snd -(*in order to get Z3-style quantification*) -fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) = - let val (quantified_vars, t) = split_last (map repair_quantification l) - in - SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: []) - end - | repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) = - let val (quantified_vars, t) = split_last (map repair_quantification l) - in - SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: []) - end - | repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l) - | repair_quantification x = x - -fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var = - (case List.find (fn v => String.isPrefix v var) free_var of - NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var) - | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var) - | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $ - replace_bound_var_by_free_var v free_vars - | replace_bound_var_by_free_var u _ = u - fun find_type_in_formula (Abs (v, T, u)) var_name = if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name | find_type_in_formula (u $ v) var_name = (case find_type_in_formula u var_name of NONE => find_type_in_formula v var_name | some_T => some_T) + | find_type_in_formula (Free(v, T)) var_name = + if String.isPrefix var_name v then SOME T else NONE | find_type_in_formula _ _ = NONE +fun find_type_of_free_in_formula (Free (v, T) $ u) var_name = + if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name + | find_type_of_free_in_formula (Abs (v, T, u)) var_name = + if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name + | find_type_of_free_in_formula (u $ v) var_name = + (case find_type_in_formula u var_name of + NONE => find_type_in_formula v var_name + | some_T => some_T) + | find_type_of_free_in_formula _ _ = NONE + fun add_bound_variables_to_ctxt concl = fold (update_binding o (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) -fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx = - if rule = veriT_tmp_ite_elim_rule then - (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx) - else if rule = veriT_tmp_skolemize_rule then - let val concl' = replace_bound_var_by_free_var concl bounds in - (mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx) - end - else - (node, cx) + +local + + fun remove_Sym (SMTLIB.Sym y) = y + + fun extract_symbols bds = + bds + |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, SMTLIB.Sym y] => [x, y] + | SMTLIB.S syms => map remove_Sym syms) + |> flat + + fun extract_symbols_map bds = + bds + |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, _] => [x] + | SMTLIB.S syms => map remove_Sym syms) + |> flat +in -fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds), - cx)) = +fun bound_vars_by_rule "bind" (SMTLIB.S bds) = extract_symbols bds + | bound_vars_by_rule "qnt_simplify" (SMTLIB.S bds) = extract_symbols_map bds + | bound_vars_by_rule "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds + | bound_vars_by_rule "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds + | bound_vars_by_rule _ _ = [] + +fun global_bound_vars_by_rule _ _ = [] + +(* VeriT adds "?" before some variable. *) +fun remove_all_qm (SMTLIB.Sym v :: l) = + SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l + | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' + | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l + | remove_all_qm (v :: l) = v :: remove_all_qm l + | remove_all_qm [] = [] + +fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) + | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) + | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v + | remove_all_qm2 v = v + +val parse_rule_and_args = let - fun mk_prop_of_term concl = - concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop} - fun update_prems assumption_id prems = - map (fn prem => id_of_father_step ^ prem) - (filter_out (curry (op =) assumption_id) prems) - fun inline_assumption assumption assumption_id - (VeriT_Node {id, rule, prems, concl, bounds}) = - mk_node id rule (update_prems assumption_id prems) - (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds - fun find_input_steps_and_inline [] last_step = ([], last_step) - | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) - last_step = - if rule = veriT_input_rule then - find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step - else - apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds)) - (find_input_steps_and_inline steps (id_of_father_step ^ id')) - val (subproof', last_step_id) = find_input_steps_and_inline subproof "" - val prems' = - if last_step_id = "" then - prems - else - (case prems of - NONE => SOME [last_step_id] - | SOME l => SOME (last_step_id :: l)) + fun parse_rule_name (SMTLIB.Sym rule :: l) = (rule, l) + | parse_rule_name l = (veriT_subproof_rule, l) + fun parse_args (SMTLIB.Key "args" :: args :: l) = (remove_all_qm2 args, l) + | parse_args l = (SMTLIB.S [], l) in - (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx)) + parse_rule_name + ##> parse_args end -(* -(set id rule :clauses(...) :args(..) :conclusion (...)). -or -(set id subproof (set ...) :conclusion (...)). -*) +end -fun parse_proof_step cx = +fun parse_raw_proof_step (p : SMTLIB.tree) : raw_veriT_node = let fun rotate_pair (a, (b, c)) = ((a, b), c) fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l) | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t) - fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l) fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) = (SOME (map (fn (SMTLIB.Sym id) => id) source), l) | parse_source l = (NONE, l) - fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) = - let val (subproof_steps, cx') = parse_proof_step cx subproof_step in - apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l) + fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) = + let + val subproof_steps = parse_raw_proof_step subproof_step + in + apfst (curry (op ::) subproof_steps) (parse_subproof rule args id_of_father_step l) end - | parse_subproof cx _ l = (([], cx), l) - fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l - | skip_args l = l - fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl - fun make_or_from_clausification l = - foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => - (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, - perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l - fun to_node (((((id, rule), prems), concl), bounds), cx) = - (mk_node id rule (the_default [] prems) concl bounds, cx) + | parse_subproof _ _ _ l = ([], l) + + fun parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S [] :: []) = + SMTLIB.Sym "false" + | parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = + (SMTLIB.S (remove_all_qm (SMTLIB.Sym "or" :: concl))) + + fun to_raw_node ((((((id, rule), args), prems), subproof), concl)) = + (mk_raw_node id rule args (the_default [] prems) concl subproof) in - get_id - ##> parse_rule + (get_id + ##> parse_rule_and_args + #> rotate_pair #> rotate_pair ##> parse_source #> rotate_pair - ##> skip_args - #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub)) + #> (fn ((((id, rule), args), prems), sub) => + ((((id, rule), args), prems), parse_subproof rule args id sub)) #> rotate_pair - ##> parse_conclusion - ##> map repair_quantification - #> (fn ((((id, rule), prems), (subproof, cx)), terms) => - (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) - ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls) - #> fix_subproof_steps - ##> to_node - #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) - #-> fold_map update_step_and_cx + ##> parse_and_clausify_conclusion + #> to_raw_node) + p + end + +fun proof_ctxt_of_rule "bind" t = t + | proof_ctxt_of_rule "sko_forall" t = t + | proof_ctxt_of_rule "sko_ex" t = t + | proof_ctxt_of_rule "let" t = t + | proof_ctxt_of_rule "qnt_simplify" t = t + | proof_ctxt_of_rule _ _ = [] + +fun args_of_rule "forall_inst" t = t + | args_of_rule _ _ = [] + +fun map_replay_prems f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, + subproof = (bound, assms, subproof)}) = + (VeriT_Replay_Node {id = id, rule = rule, args = args, prems = f prems, proof_ctxt = proof_ctxt, + concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_prems f) subproof)}) + +fun map_replay_id f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, + subproof = (bound, assms, subproof)}) = + (VeriT_Replay_Node {id = f id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, + concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_id f) subproof)}) + +fun id_of_last_step prems = + if null prems then [] + else + let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end + +val extract_assumptions_from_subproof = + let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) = + if rule = veriT_local_input_rule then [concl] else [] + in + map extract_assumptions_from_subproof + #> flat end +fun normalized_rule_name id rule = + (case (rule = veriT_input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of + (true, true) => veriT_normalized_input_rule + | (true, _) => veriT_local_input_rule + | _ => rule) + +fun is_assm_repetition id rule = + rule = veriT_input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id + +fun postprocess_proof ctxt step = + let fun postprocess (Raw_VeriT_Node {id = id, rule = rule, args = args, + prems = prems, concl = concl, subproof = subproof}) cx = + let + val ((concl, bounds), cx') = node_of concl cx + + val bound_vars = bound_vars_by_rule rule args + + (* postprocess conclusion *) + val new_global_bounds = global_bound_vars_by_rule rule args + val concl = SMTLIB_Isar.unskolemize_names ctxt concl + + val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) + val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "cx' =", cx', + "bound_vars =", bound_vars)) + val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars + val bound_tvars = + map (fn s => (s, the (find_type_in_formula concl s))) bound_vars + val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx + val (p : veriT_replay_node list list, _) = + fold_map postprocess subproof subproof_cx + + (* postprocess assms *) + val SMTLIB.S stripped_args = args + val sanitized_args = + proof_ctxt_of_rule rule stripped_args + |> map + (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] + | SMTLIB.S syms => + SMTLIB.S (SMTLIB.Sym "and" :: map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) syms) + | x => x) + val (termified_args, _) = fold_map node_of sanitized_args subproof_cx |> apfst (map fst) + val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args + + val subproof_assms = proof_ctxt_of_rule rule normalized_args + + (* postprocess arguments *) + val rule_args = args_of_rule rule stripped_args + val (termified_args, _) = fold_map term_of rule_args subproof_cx + val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args + val rule_args = normalized_args + + (* fix subproof *) + val p = flat p + val p = map (map_replay_prems (map (curry (op ^) id))) p + val p = map (map_replay_id (curry (op ^) id)) p + + val extra_assms2 = + (if rule = veriT_subproof_rule then extract_assumptions_from_subproof p else []) + + (* fix step *) + val bound_t = + bounds + |> map (fn s => (s, the_default dummyT (find_type_of_free_in_formula concl s))) + val fixed_prems = + (if null subproof then prems else map (curry (op ^) id) prems) @ + (if is_assm_repetition id rule then [id] else []) @ + id_of_last_step p + val normalized_rule = normalized_rule_name id rule + val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl + bound_t (bound_tvars, subproof_assms @ extra_assms2, p) + in + ([step], cx') + end + in postprocess step end + + (*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are unbalanced on each line*) fun seperate_into_steps lines = @@ -214,111 +361,72 @@ seperate lines "" 0 end +fun unprefix_all_syms c (SMTLIB.Sym v :: l) = + SMTLIB.Sym (perhaps (try (unprefix c)) v) :: unprefix_all_syms c l + | unprefix_all_syms c (SMTLIB.S l :: l') = SMTLIB.S (unprefix_all_syms c l) :: unprefix_all_syms c l' + | unprefix_all_syms c (SMTLIB.Key v :: l) = SMTLIB.Key v :: unprefix_all_syms c l + | unprefix_all_syms c (v :: l) = v :: unprefix_all_syms c l + | unprefix_all_syms _ [] = [] + (* VeriT adds "@" before every variable. *) -fun remove_all_at (SMTLIB.Sym v :: l) = - SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l - | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l' - | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l - | remove_all_at (v :: l) = v :: remove_all_at l - | remove_all_at [] = [] +val remove_all_ats = unprefix_all_syms "@" -fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = - (case List.find (fn v => String.isPrefix v var) bounds of - NONE => find_in_which_step_defined var l - | SOME _ => id) - | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var) +val linearize_proof = + let + fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems, + proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) = + let + fun mk_prop_of_term concl = + concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop} + fun remove_assumption_id assumption_id prems = + filter_out (curry (op =) assumption_id) prems + fun inline_assumption assumption assumption_id + (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) = + mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt + (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds + fun find_input_steps_and_inline [] = [] + | find_input_steps_and_inline + (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) = + if rule = veriT_input_rule then + find_input_steps_and_inline (map (inline_assumption concl id') steps) + else + mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps -(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) -fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ - (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $ - (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) = + val subproof = flat (map linearize subproof) + val subproof' = find_input_steps_and_inline subproof + in + subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)] + end + in linearize end + +local + fun import_proof_and_post_process typs funs lines ctxt = let - fun get_number_of_ite_transformed_var var = - perhaps (try (unprefix "ite")) var - |> Int.fromString - fun is_equal_and_has_correct_substring var var' var'' = - if var = var' andalso String.isPrefix "ite" var then SOME var' - else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE - val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4 - val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2 - in - (case (var1_introduced_var, var2_introduced_var) of - (SOME a, SOME b) => - (*ill-generated case, might be possible when applying the rule to max a a. Only if the - variable have been introduced before. Probably an impossible edge case*) - (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of - (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var - (*Otherwise, it is a name clase between a parameter name and the introduced variable. - Or the name convention has been changed.*) - | (NONE, SOME _) => var2_introduced_var - | (SOME _, NONE) => var2_introduced_var) - | (_, SOME _) => var2_introduced_var - | (SOME _, _) => var1_introduced_var) - end - | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ - (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $ - (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) = - if var = var' then SOME var else NONE - | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ - (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $ - (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) = - if var = var' then SOME var else NONE - | find_ite_var_in_term (p $ q) = - (case find_ite_var_in_term p of - NONE => find_ite_var_in_term q - | x => x) - | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body - | find_ite_var_in_term _ = NONE - -fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) = - if rule = veriT_tmp_ite_elim_rule then - if bounds = [] then - (*if the introduced var has already been defined, adding the definition as a dependency*) - let - val new_prems = prems - |> (case find_ite_var_in_term concl of - NONE => I - | SOME var => cons (find_in_which_step_defined var steps)) - in - VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds} - end - else - (*some new variables are created*) - let val concl' = replace_bound_var_by_free_var concl bounds in - mk_node id rule prems concl' [] - end - else - node - -fun remove_alpha_conversion _ [] = [] - | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = - let - val correct_dependency = map (perhaps (Symtab.lookup replace_table)) - val find_predecessor = perhaps (Symtab.lookup replace_table) - in - if rule = veriT_tmp_alphaconv_rule then - remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems)) - replace_table) steps - else - VeriT_Node {id = id, rule = rule, prems = correct_dependency prems, - concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps - end - -fun correct_veriT_steps steps = - steps - |> map (correct_veriT_step steps) - |> remove_alpha_conversion Symtab.empty + val smtlib_lines_without_at = + seperate_into_steps lines + |> map SMTLIB.parse + |> remove_all_ats + in apfst flat (fold_map (fn l => postprocess_proof ctxt (parse_raw_proof_step l)) + smtlib_lines_without_at (empty_context ctxt typs funs)) end +in fun parse typs funs lines ctxt = let - val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines)) - val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l) - smtlib_lines_without_at (empty_context ctxt typs funs)) - val t = correct_veriT_steps u + val (u, env) = import_proof_and_post_process typs funs lines ctxt + val t = flat (map linearize_proof u) fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = - mk_step id rule prems concl bounds + mk_step id rule prems [] concl bounds in (map node_to_step t, ctxt_of env) end +fun parse_replay typs funs lines ctxt = + let + val (u, env) = import_proof_and_post_process typs funs lines ctxt + val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} u) + in + (u, ctxt_of env) + end +end + end; diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/verit_proof_parse.ML --- a/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Oct 30 16:24:04 2018 +0100 @@ -37,7 +37,7 @@ fun step_of_assume j (_, th) = VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j), - rule = veriT_input_rule, prems = [], concl = Thm.prop_of th, fixes = []} + rule = veriT_input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt val used_assert_ids = fold add_used_asserts_in_step actual_steps [] diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/verit_replay.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT/verit_replay.ML Tue Oct 30 16:24:04 2018 +0100 @@ -0,0 +1,207 @@ +(* 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 diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/SMT/verit_replay_methods.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Tue Oct 30 16:24:04 2018 +0100 @@ -0,0 +1,843 @@ +(* Title: HOL/Tools/SMT/verit_replay_methods.ML + Author: Mathias Fleury, MPII + +Proof methods for replaying veriT proofs. +*) + +signature VERIT_REPLAY_METHODS = +sig + + val is_skolemisation: string -> bool + val is_skolemisation_step: VeriT_Proof.veriT_replay_node -> bool + + (* methods for veriT proof rules *) + val method_for: string -> Proof.context -> thm list -> term list -> term -> + thm + + val veriT_step_requires_subproof_assms : string -> bool + val eq_congruent_pred: Proof.context -> 'a -> term -> thm +end; + + +structure Verit_Replay_Methods: VERIT_REPLAY_METHODS = +struct + +(*Some general comments on the proof format: + 1. Double negations are not always removed. This means for example that the equivalence rules + cannot assume that the double negations have already been removed. Therefore, we match the + term, instantiate the theorem, then use simp (to remove double negations), and finally use + assumption. + 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule + is doing much more that is supposed to do. Moreover types can make trivial goals (for the + boolean structure) impossible to prove. + 3. Duplicate literals are sometimes removed, mostly by the SAT solver. We currently do not care + about it, since in all cases we have met, a rule like tmp_AC_simp is called to do the + simplification. + + Rules unsupported on purpose: + * Distinct_Elim, XOR, let (we don't need them). + * tmp_skolemize (because it is not clear if veriT still generates using it). +*) + +datatype verit_rule = + False | True | + + (* input: a repeated (normalized) assumption of assumption of in a subproof *) + Normalized_Input | Local_Input | + (* Subproof: *) + Subproof | + (* Conjunction: *) + And | Not_And | And_Pos | And_Neg | + (* Disjunction"" *) + Or | Or_Pos | Not_Or | Or_Neg | + (* Disjunction: *) + Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | + (* Equivalence: *) + Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | + (* If-then-else: *) + ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | + (* Equality: *) + Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | + (* Arithmetics: *) + LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | + NLA_Generic | + (* Quantifiers: *) + Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Qnt_Simplify | Bind | Skolem_Forall | Skolem_Ex | + (* Resolution: *) + Theory_Resolution | Resolution | + (* Various transformation: *) + Connective_Equiv | + (* Temporary rules, that the veriT developpers want to remove: *) + Tmp_AC_Simp | + Tmp_Bfun_Elim | + (* Unsupported rule *) + Unsupported + +val is_skolemisation = member (op =) ["sko_forall", "sko_ex"] +fun is_skolemisation_step (VeriT_Proof.VeriT_Replay_Node {id, ...}) = is_skolemisation id + +fun verit_rule_of "bind" = Bind + | verit_rule_of "cong" = Cong + | verit_rule_of "refl" = Refl + | verit_rule_of "equiv1" = Equiv1 + | verit_rule_of "equiv2" = Equiv2 + | verit_rule_of "equiv_pos1" = Equiv_pos1 + | verit_rule_of "equiv_pos2" = Equiv_pos2 + | verit_rule_of "equiv_neg1" = Equiv_neg1 + | verit_rule_of "equiv_neg2" = Equiv_neg2 + | verit_rule_of "sko_forall" = Skolem_Forall + | verit_rule_of "sko_ex" = Skolem_Ex + | verit_rule_of "eq_reflexive" = Eq_Reflexive + | verit_rule_of "th_resolution" = Theory_Resolution + | verit_rule_of "forall_inst" = Forall_Inst + | verit_rule_of "implies_pos" = Implies_Pos + | verit_rule_of "or" = Or + | verit_rule_of "not_or" = Not_Or + | verit_rule_of "resolution" = Resolution + | verit_rule_of "eq_congruent" = Eq_Congruent + | verit_rule_of "connective_equiv" = Connective_Equiv + | verit_rule_of "trans" = Trans + | verit_rule_of "false" = False + | verit_rule_of "tmp_AC_simp" = Tmp_AC_Simp + | verit_rule_of "and" = And + | verit_rule_of "not_and" = Not_And + | verit_rule_of "and_pos" = And_Pos + | verit_rule_of "and_neg" = And_Neg + | verit_rule_of "or_pos" = Or_Pos + | verit_rule_of "or_neg" = Or_Neg + | verit_rule_of "not_equiv1" = Not_Equiv1 + | verit_rule_of "not_equiv2" = Not_Equiv2 + | verit_rule_of "not_implies1" = Not_Implies1 + | verit_rule_of "not_implies2" = Not_Implies2 + | verit_rule_of "implies_neg1" = Implies_Neg1 + | verit_rule_of "implies_neg2" = Implies_Neg2 + | verit_rule_of "implies" = Implies + | verit_rule_of "tmp_bfun_elim" = Tmp_Bfun_Elim + | verit_rule_of "ite1" = ITE1 + | verit_rule_of "ite2" = ITE2 + | verit_rule_of "not_ite1" = Not_ITE1 + | verit_rule_of "not_ite2" = Not_ITE2 + | verit_rule_of "ite_pos1" = ITE_Pos1 + | verit_rule_of "ite_pos2" = ITE_Pos2 + | verit_rule_of "ite_neg1" = ITE_Neg1 + | verit_rule_of "ite_neg2" = ITE_Neg2 + | verit_rule_of "ite_intro" = ITE_Intro + | verit_rule_of "la_disequality" = LA_Disequality + | verit_rule_of "lia_generic" = LIA_Generic + | verit_rule_of "la_generic" = LA_Generic + | verit_rule_of "la_tautology" = LA_Tautology + | verit_rule_of "la_totality" = LA_Totality + | verit_rule_of "la_rw_eq"= LA_RW_Eq + | verit_rule_of "nla_generic"= NLA_Generic + | verit_rule_of "eq_transitive" = Eq_Transitive + | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused + | verit_rule_of "qnt_simplify" = Qnt_Simplify + | verit_rule_of "qnt_join" = Qnt_Join + | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred + | verit_rule_of "subproof" = Subproof + | verit_rule_of r = + if r = VeriT_Proof.veriT_normalized_input_rule then Normalized_Input + else if r = VeriT_Proof.veriT_local_input_rule then Local_Input + else Unsupported + +fun string_of_verit_rule Bind = "Bind" + | string_of_verit_rule Cong = "Cong" + | string_of_verit_rule Refl = "Refl" + | string_of_verit_rule Equiv1 = "Equiv1" + | string_of_verit_rule Equiv2 = "Equiv2" + | string_of_verit_rule Equiv_pos1 = "Equiv_pos1" + | string_of_verit_rule Equiv_pos2 = "Equiv_pos2" + | string_of_verit_rule Equiv_neg1 = "Equiv_neg1" + | string_of_verit_rule Equiv_neg2 = "Equiv_neg2" + | string_of_verit_rule Skolem_Forall = "Skolem_Forall" + | string_of_verit_rule Skolem_Ex = "Skolem_Ex" + | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive" + | string_of_verit_rule Theory_Resolution = "Theory_Resolution" + | string_of_verit_rule Forall_Inst = "forall_inst" + | string_of_verit_rule Or = "Or" + | string_of_verit_rule Not_Or = "Not_Or" + | string_of_verit_rule Resolution = "Resolution" + | string_of_verit_rule Eq_Congruent = "eq_congruent" + | string_of_verit_rule Connective_Equiv = "connective_equiv" + | string_of_verit_rule Trans = "trans" + | string_of_verit_rule False = "false" + | string_of_verit_rule And = "and" + | string_of_verit_rule And_Pos = "and_pos" + | string_of_verit_rule Not_And = "not_and" + | string_of_verit_rule And_Neg = "and_neg" + | string_of_verit_rule Or_Pos = "or_pos" + | string_of_verit_rule Or_Neg = "or_neg" + | string_of_verit_rule Tmp_AC_Simp = "tmp_AC_simp" + | string_of_verit_rule Not_Equiv1 = "not_equiv1" + | string_of_verit_rule Not_Equiv2 = "not_equiv2" + | string_of_verit_rule Not_Implies1 = "not_implies1" + | string_of_verit_rule Not_Implies2 = "not_implies2" + | string_of_verit_rule Implies_Neg1 = "implies_neg1" + | string_of_verit_rule Implies_Neg2 = "implies_neg2" + | string_of_verit_rule Implies = "implies" + | string_of_verit_rule Tmp_Bfun_Elim = "tmp_bfun_elim" + | string_of_verit_rule ITE1 = "ite1" + | string_of_verit_rule ITE2 = "ite2" + | string_of_verit_rule Not_ITE1 = "not_ite1" + | string_of_verit_rule Not_ITE2 = "not_ite2" + | string_of_verit_rule ITE_Pos1 = "ite_pos1" + | string_of_verit_rule ITE_Pos2 = "ite_pos2" + | string_of_verit_rule ITE_Neg1 = "ite_neg1" + | string_of_verit_rule ITE_Neg2 = "ite_neg2" + | string_of_verit_rule ITE_Intro = "ite_intro" + | string_of_verit_rule LA_Disequality = "la_disequality" + | string_of_verit_rule LA_Generic = "la_generic" + | string_of_verit_rule LIA_Generic = "lia_generic" + | string_of_verit_rule LA_Tautology = "la_tautology" + | string_of_verit_rule LA_RW_Eq = "la_rw_eq" + | string_of_verit_rule LA_Totality = "LA_Totality" + | string_of_verit_rule NLA_Generic = "nla_generic" + | string_of_verit_rule Eq_Transitive = "eq_transitive" + | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused" + | string_of_verit_rule Qnt_Simplify = "qnt_simplify" + | string_of_verit_rule Qnt_Join = "qnt_join" + | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred" + | string_of_verit_rule Normalized_Input = VeriT_Proof.veriT_normalized_input_rule + | string_of_verit_rule Local_Input = VeriT_Proof.veriT_normalized_input_rule + | string_of_verit_rule Subproof = "subproof" + | string_of_verit_rule r = "Unsupported rule: " ^ @{make_string} r + +(*** Methods to Replay Normal steps ***) +(* sko_forall requires the assumptions to be able to SMT_Replay_Methods.prove the equivalence in case of double +skolemization. See comment below. *) +fun veriT_step_requires_subproof_assms t = + member (op =) ["refl", "cong", VeriT_Proof.veriT_local_input_rule, "sko_forall", + "sko_ex"] t + +fun simplify_tac ctxt thms = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms not_not eq_commute} addsimps thms) + |> Simplifier.full_simp_tac + +val bind_thms = + [@{lemma "(\x x'. P x = Q x) \ (\x. P x) = (\y. Q y)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\x. P x) = (\y. Q y)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\x. P x = Q x)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\x. P x = Q x)" + by blast}] + +fun TRY' tac = fn i => TRY (tac i) +fun REPEAT' tac = fn i => REPEAT (tac i) +fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i)) + +fun bind ctxt [prems] t = SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT' (resolve_tac ctxt bind_thms) + THEN' match_tac ctxt [prems] + THEN' simplify_tac ctxt [] + THEN' REPEAT' (match_tac ctxt [@{thm refl}])) + + +fun refl ctxt thm t = + (case find_first (fn thm => t = Thm.full_prop_of thm) thm of + SOME thm => thm + | NONE => + (case try (Z3_Replay_Methods.refl ctxt thm) t of + NONE => + ( Z3_Replay_Methods.cong ctxt thm t) + | SOME thm => thm)) + +local + fun equiv_pos_neg_term ctxt thm (@{term Trueprop} $ + (@{term HOL.disj} $ (_) $ + ((@{term HOL.disj} $ a $ b)))) = + Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm + + fun prove_equiv_pos_neg thm ctxt _ t = + let val thm = equiv_pos_neg_term ctxt thm t + in + SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [thm] + THEN' simplify_tac ctxt []) + end +in + +val equiv_pos1_thm = + @{lemma "\(a \ ~b) \ a \ b" + by blast+} + +val equiv_pos1 = prove_equiv_pos_neg equiv_pos1_thm + +val equiv_pos2_thm = + @{lemma "\a b. ((\a) \ b) \ a \ b" + by blast+} + +val equiv_pos2 = prove_equiv_pos_neg equiv_pos2_thm + +val equiv_neg1_thm = + @{lemma "(~a \ ~b) \ a \ b" + by blast} + +val equiv_neg1 = prove_equiv_pos_neg equiv_neg1_thm + +val equiv_neg2_thm = + @{lemma "(a \ b) \ a \ b" + by blast} + +val equiv_neg2 = prove_equiv_pos_neg equiv_neg2_thm + +end + +(* Most of the code below is due to the proof output of veriT: The description of the rule is wrong +(and according to Pascal Fontaine, it is a bug). Anyway, currently, forall_inst does: + 1. swapping out the forall quantifiers + 2. instantiation + 3. boolean. + +However, types can mess-up things: + lemma \(0 < degree a) = (0 \ degree a) \ 0 = degree a \ 0 < degree a\ + by fast +works unlike + lemma \((0::nat) < degree a) = (0 \ degree a) \ 0 = degree a \ 0 < degree a\ + by fast. +Therefore, we use fast and auto as fall-back. +*) +fun forall_inst ctxt _ args t = + let + val instantiate = + fold (fn inst => fn tac => + let val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inst)] @{thm spec} + in tac THEN' dmatch_tac ctxt [thm]end) + args + (K all_tac) + in + SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]] + THEN' TRY' (Raw_Simplifier.rewrite_goal_tac ctxt @{thms all_simps[symmetric] not_all}) + THEN' TRY' instantiate + THEN' TRY' (simplify_tac ctxt []) + THEN' TRY' (SOLVED' (fn _ => HEADGOAL ( (assume_tac ctxt) + ORELSE' + TRY' (dresolve_tac ctxt @{thms conjE} + THEN_ALL_NEW assume_tac ctxt) + ORELSE' + TRY' (dresolve_tac ctxt @{thms verit_forall_inst} + THEN_ALL_NEW assume_tac ctxt)))) + THEN' (TRY' (Classical.fast_tac ctxt)) + THEN' (TRY' (K (Clasimp.auto_tac ctxt)))) + end + +fun or _ [thm] _ = thm + +val implies_pos_thm = + [@{lemma "\(A \ B) \ \A \ B" + by blast}, + @{lemma "\(\A \ B) \ A \ B" + by blast}] + +fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt implies_pos_thm) + +fun extract_rewrite_rule_assumption thms = + let + fun is_rewrite_rule thm = + (case Thm.prop_of thm of + @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ Free(_, _) $ _) => true + | _ => false) + in + thms + |> filter is_rewrite_rule + |> map (fn thm => thm COMP @{thm eq_reflection}) + end + +(* We need to unfold the assumptions if we are in a subproof: For multiple skolemization, the context +contains a mapping "verit_vrX \ Eps f". The variable "verit_vrX" must be unfolded to "Eps f". +Otherwise, the proof cannot be done. *) +fun skolem_forall ctxt (thms) t = + let + val ts = extract_rewrite_rule_assumption thms + in + SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_forall'}) + THEN' TRY' (simplify_tac ctxt ts) + THEN' TRY'(resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl}) + THEN' TRY' (resolve_tac ctxt @{thms refl})) + end + +fun skolem_ex ctxt (thms) t = + let + val ts = extract_rewrite_rule_assumption thms + in + SMT_Replay_Methods.prove ctxt t (fn _ => + Raw_Simplifier.rewrite_goal_tac ctxt ts + THEN' REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_ex'}) + THEN' REPEAT_CHANGED (resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl}) + THEN' TRY' (resolve_tac ctxt @{thms refl})) + end + +fun eq_reflexive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [@{thm refl}]) + +fun connective_equiv ctxt thms t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt thms + THEN' K (Clasimp.auto_tac ctxt)) + + +fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' TRY' (simplify_tac ctxt []) + THEN' TRY' (K (Clasimp.auto_tac ctxt))) + +val false_rule_thm = @{lemma "\False" by blast} + +fun false_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [false_rule_thm]) + + +(* transitivity *) + +val trans_bool_thm = + @{lemma "P = Q \ Q \ P" by blast} +fun trans _ [thm1, thm2] _ = + (case (Thm.full_prop_of thm1, Thm.full_prop_of thm2) of + (@{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ _ $ t2), + @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ t3 $ _)) => + if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans})) + else thm1 RSN (1, (thm2 RS sym) RSN (2, @{thm trans})) + | _ => trans_bool_thm OF [thm1, thm2]) + | trans ctxt (thm1 :: thm2 :: thms) t = + trans ctxt (trans ctxt [thm1, thm2] t :: thms) t + +fun tmp_AC_rule ctxt _ t = + let + val simplify = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms ac_simps conj_ac}) + |> Simplifier.full_simp_tac + in SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_ALL_NEW (simplify_tac ctxt [] + THEN' TRY' simplify + THEN' TRY' (Classical.fast_tac ctxt))) end + +fun and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1))) + THEN' TRY' (assume_tac ctxt) + THEN' TRY' (simplify_tac ctxt [])) + +fun not_and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems THEN' + Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) + +fun not_or_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems THEN' + Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) + +local + fun simplify_and_pos ctxt = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel} + addsimps @{thms simp_thms de_Morgan_conj}) + |> Simplifier.full_simp_tac +in + +fun and_pos ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos}) + THEN' TRY' (simplify_and_pos ctxt) + THEN' TRY' (assume_tac ctxt) + THEN' TRY' (Classical.fast_tac ctxt)) + +end + +fun and_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_neg}) + THEN' simplify_tac ctxt @{thms de_Morgan_conj[symmetric] excluded_middle + excluded_middle[of \\_\, unfolded not_not]}) + +fun or_pos_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + simplify_tac ctxt @{thms simp_thms}) + +fun or_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt @{thms verit_or_neg} + THEN' (fn i => dresolve_tac ctxt @{thms verit_subst_bool} i + THEN assume_tac ctxt (i+1)) + THEN' simplify_tac ctxt @{thms simp_thms}) + +val not_equiv1_thm = + @{lemma "\(A \ B) \ A \ B" + by blast} + +fun not_equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [not_equiv1_thm OF [thm]] + THEN' simplify_tac ctxt []) + +val not_equiv2_thm = + @{lemma "\(A \ B) \ \A \ \B" + by blast} + +fun not_equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [not_equiv2_thm OF [thm]] + THEN' simplify_tac ctxt []) + +val equiv1_thm = + @{lemma "(A \ B) \ \A \ B" + by blast} + +fun equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [equiv1_thm OF [thm]] + THEN' simplify_tac ctxt []) + +val equiv2_thm = + @{lemma "(A \ B) \ A \ \B" + by blast} + +fun equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [equiv2_thm OF [thm]] + THEN' simplify_tac ctxt []) + + +val not_implies1_thm = + @{lemma "\(A \ B) \ A" + by blast} + +fun not_implies1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [not_implies1_thm OF [thm]] + THEN' simplify_tac ctxt []) + +val not_implies2_thm = + @{lemma "\(A \B) \ \B" + by blast} + +fun not_implies2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [not_implies2_thm OF [thm]] + THEN' simplify_tac ctxt []) + + +local + fun implies_pos_neg_term ctxt thm (@{term Trueprop} $ + (@{term HOL.disj} $ (@{term HOL.implies} $ a $ b) $ _)) = + Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm + + fun prove_implies_pos_neg thm ctxt _ t = + let val thm = implies_pos_neg_term ctxt thm t + in + SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt [thm] + THEN' simplify_tac ctxt []) + end +in + +val implies_neg1_thm = + @{lemma "(a \ b) \ a" + by blast} + +val implies_neg1 = prove_implies_pos_neg implies_neg1_thm + +val implies_neg2_thm = + @{lemma "(a \ b) \ \b" by blast} + +val implies_neg2 = prove_implies_pos_neg implies_neg2_thm + +end + +val implies_thm = + @{lemma "(~a \ b) \ a \ b" + "(a \ b) \ \a \ b" + by blast+} + +fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' resolve_tac ctxt implies_thm + THEN' assume_tac ctxt) + + +(* +Here is a case where force_tac fails, but auto_tac succeeds: + Ex (P x) \ P x c \ + (\v0. if x then P True v0 else P False v0) \ (if x then P True c else P False c) + +(this was before we added the eqsubst_tac). Therefore, to be safe, we add the fast, auto, and force. +*) +fun tmp_bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => + Method.insert_tac ctxt prems + THEN' REPEAT_CHANGED (EqSubst.eqsubst_tac ctxt [0] @{thms verit_tmp_bfun_elim}) + THEN' TRY' (simplify_tac ctxt []) + THEN' (Classical.fast_tac ctxt + ORELSE' K (Clasimp.auto_tac ctxt) + ORELSE' Clasimp.force_tac ctxt)) + +val ite_pos1_thm = + @{lemma "\(if x then P else Q) \ x \ Q" + by auto} + +fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [ite_pos1_thm]) + +val ite_pos2_thms = + @{lemma "\(if x then P else Q) \ \x \ P" "\(if \x then P else Q) \ x \ P" + by auto} + +fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt ite_pos2_thms) + +val ite_neg1_thms = + @{lemma "(if x then P else Q) \ x \ \Q" "(if x then P else \Q) \ x \ Q" + by auto} + +fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt ite_neg1_thms) + +val ite_neg2_thms = + @{lemma "(if x then P else Q) \ \x \ \P" "(if \x then P else Q) \ x \ \P" + "(if x then \P else Q) \ \x \ P" "(if \x then \P else Q) \ x \ P" + by auto} + +fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt ite_neg2_thms) + +val ite1_thm = + @{lemma "(if x then P else Q) \ x \ Q" + by (auto split: if_splits) } + +fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [ite1_thm OF [thm]]) + +val ite2_thm = + @{lemma "(if x then P else Q) \ \x \ P" + by (auto split: if_splits) } + +fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [ite2_thm OF [thm]]) + + +val not_ite1_thm = + @{lemma "\(if x then P else Q) \ x \ \Q" + by (auto split: if_splits) } + +fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [not_ite1_thm OF [thm]]) + +val not_ite2_thm = + @{lemma "\(if x then P else Q) \ \x \ \P" + by (auto split: if_splits) } + +fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [not_ite2_thm OF [thm]]) + + +fun unit_res ctxt thms t = + let + val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms + val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) + val (_, t2) = Logic.dest_equals (Thm.prop_of t') + val thm = Z3_Replay_Methods.unit_res ctxt thms t2 + in + @{thm verit_Pure_trans} OF [t', thm] + end + +fun ite_intro ctxt _ t = + let + fun simplify_ite ctxt = + ctxt + |> empty_simpset + |> put_simpset HOL_basic_ss + |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel} + addsimps @{thms simp_thms}) + |> Simplifier.full_simp_tac + in + SMT_Replay_Methods.prove ctxt t (fn _ => + (simplify_ite ctxt + THEN' TRY' (Blast.blast_tac ctxt + ORELSE' K (Clasimp.auto_tac ctxt) + ORELSE' Clasimp.force_tac ctxt))) + end + + +(* Quantifiers *) + +fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + Classical.fast_tac ctxt) + +fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + Classical.fast_tac ctxt) + +fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + Classical.fast_tac ctxt) + + +(* Equality *) + +fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}]) + THEN' REPEAT' (resolve_tac ctxt @{thms impI}) + THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) + THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1)) + THEN' resolve_tac ctxt @{thms refl}) + +local + + (* Rewrite might apply below choice. As we do not want to change them (it can break other + rewriting steps), we cannot use Term.lambda *) + fun abstract_over_no_choice (v, body) = + let + fun abs lev tm = + if v aconv tm then Bound lev + else + (case tm of + Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) + | t as (Const (\<^const_name>\Hilbert_Choice.Eps\, _) $ _) => t + | t $ u => + (abs lev t $ (abs lev u handle Same.SAME => u) + handle Same.SAME => t $ abs lev u) + | _ => raise Same.SAME); + in abs 0 body handle Same.SAME => body end; + + fun lambda_name (x, v) t = + Abs (if x = "" then Term.term_name v else x, fastype_of v, abstract_over_no_choice (v, t)); + + fun lambda v t = lambda_name ("", v) t; + + fun extract_equal_terms (Const(\<^const_name>\Trueprop\, _) $ t) = + let fun ext (Const(\<^const_name>\HOL.disj\, _) $ (Const(\<^const_name>\HOL.Not\, _) $ + (Const(\<^const_name>\HOL.eq\, _) $ t1 $ t2)) $ t) = + apfst (curry (op ::) (t1, t2)) (ext t) + | ext t = ([], t) + in ext t end + fun eq_congruent_tac ctxt t = + let + val (eqs, g) = extract_equal_terms t + fun replace1 (t1, t2) (g, tac) = + let + val abs_t1 = lambda t2 g + val subst = Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [t1, t2, abs_t1]) + @{thm subst} + in (Term.betapply (abs_t1, t1), + tac THEN' resolve_tac ctxt [subst] + THEN' TRY' (assume_tac ctxt)) end + val (_, tac) = fold replace1 eqs (g, K all_tac) + in + tac + end +in + +fun eq_congruent_pred ctxt _ t = + SMT_Replay_Methods.prove ctxt t (fn _ => + REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \_ = _\]} RSN (1, @{thm iffD2}) OF @{thms impI}]) + THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) + THEN' eq_congruent_tac ctxt t + THEN' resolve_tac ctxt @{thms refl excluded_middle + excluded_middle[of \\_\, unfolded not_not]}) + +end + + +(* subproof *) + +fun subproof ctxt [prem] t = + SMT_Replay_Methods.prove ctxt t (fn _ => + (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}], + @{thm disj_not1[of \\_\, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]] + THEN' resolve_tac ctxt [prem] + THEN_ALL_NEW assume_tac ctxt + THEN' TRY' (assume_tac ctxt)) + ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt)) + + +(* la_rw_eq *) + +val la_rw_eq_thm = @{lemma \(a :: nat) = b \ (a \ b) \ (a \ b)\ + by auto} + +fun la_rw_eq ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => + resolve_tac ctxt [la_rw_eq_thm]) + +(* congruence *) +fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt + (string_of_verit_rule Cong) [ + ("basic", SMT_Replay_Methods.cong_basic ctxt thms), + ("full", SMT_Replay_Methods.cong_full ctxt thms), + ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms)] thms + + +fun unsupported rule ctxt thms _ t = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule" + rule thms t + +fun ignore_args f ctxt thm _ t = f ctxt thm t + +fun choose Bind = ignore_args bind + | choose Refl = ignore_args refl + | choose And_Pos = ignore_args and_pos + | choose And_Neg = ignore_args and_neg_rule + | choose Cong = ignore_args cong + | choose Equiv_pos1 = ignore_args equiv_pos1 + | choose Equiv_pos2 = ignore_args equiv_pos2 + | choose Equiv_neg1 = ignore_args equiv_neg1 + | choose Equiv_neg2 = ignore_args equiv_neg2 + | choose Equiv1 = ignore_args equiv1 + | choose Equiv2 = ignore_args equiv2 + | choose Not_Equiv1 = ignore_args not_equiv1 + | choose Not_Equiv2 = ignore_args not_equiv2 + | choose Not_Implies1 = ignore_args not_implies1 + | choose Not_Implies2 = ignore_args not_implies2 + | choose Implies_Neg1 = ignore_args implies_neg1 + | choose Implies_Neg2 = ignore_args implies_neg2 + | choose Implies_Pos = ignore_args implies_pos + | choose Implies = ignore_args implies_rules + | choose Forall_Inst = forall_inst + | choose Skolem_Forall = ignore_args skolem_forall + | choose Skolem_Ex = ignore_args skolem_ex + | choose Or = ignore_args or + | choose Theory_Resolution = ignore_args unit_res + | choose Resolution = ignore_args unit_res + | choose Eq_Reflexive = ignore_args eq_reflexive + | choose Connective_Equiv = ignore_args connective_equiv + | choose Trans = ignore_args trans + | choose False = ignore_args false_rule + | choose Tmp_AC_Simp = ignore_args tmp_AC_rule + | choose And = ignore_args and_rule + | choose Not_And = ignore_args not_and_rule + | choose Not_Or = ignore_args not_or_rule + | choose Or_Pos = ignore_args or_pos_rule + | choose Or_Neg = ignore_args or_neg_rule + | choose Tmp_Bfun_Elim = ignore_args tmp_bfun_elim + | choose ITE1 = ignore_args ite1 + | choose ITE2 = ignore_args ite2 + | choose Not_ITE1 = ignore_args not_ite1 + | choose Not_ITE2 = ignore_args not_ite2 + | choose ITE_Pos1 = ignore_args ite_pos1 + | choose ITE_Pos2 = ignore_args ite_pos2 + | choose ITE_Neg1 = ignore_args ite_neg1 + | choose ITE_Neg2 = ignore_args ite_neg2 + | choose ITE_Intro = ignore_args ite_intro + | choose LA_Disequality = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose LIA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose LA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose LA_Totality = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose LA_Tautology = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose LA_RW_Eq = ignore_args la_rw_eq + | choose NLA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma + | choose Normalized_Input = ignore_args normalized_input + | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused + | choose Qnt_Simplify = ignore_args qnt_simplify + | choose Qnt_Join = ignore_args qnt_join + | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred + | choose Eq_Congruent = ignore_args eq_congruent_pred + | choose Eq_Transitive = ignore_args eq_transitive + | choose Local_Input = ignore_args refl + | choose Subproof = ignore_args subproof + | choose r = unsupported (string_of_verit_rule r) + +type Verit_method = Proof.context -> thm list -> term -> thm +type abs_context = int * term Termtab.table + +fun with_tracing rule method ctxt thms args t = + let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t + in method ctxt thms args t end + +fun method_for rule = with_tracing rule (choose (verit_rule_of rule)) + +end; diff -r d5ab1636660b -r 8050734eee3e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 16:24:01 2018 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 16:24:04 2018 +0100 @@ -55,7 +55,6 @@ val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" -val veriT_tmp_ite_elim_rule = "tmp_ite_elim" val veriT_tmp_skolemize_rule = "tmp_skolemize" val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") @@ -63,7 +62,7 @@ val skolemize_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, - spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, + spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)