# HG changeset patch # User blanchet # Date 1387126898 -3600 # Node ID 2eb43ddde491e8d5cc3e576bcd5dab57719aaac1 # Parent 6b0ca7f79e9369af1ce793ef294cda8e6307e7d2 use 'arith' when appropriate in Z3 proofs diff -r 6b0ca7f79e93 -r 2eb43ddde491 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Sun Dec 15 18:01:38 2013 +0100 @@ -17,14 +17,14 @@ structure Atom_Graph : GRAPH - type ref_sequent = atom list * atom + type refute_sequent = atom list * atom type refute_graph = unit Atom_Graph.T type clause = atom list - type direct_sequent = atom list * clause + type direct_sequent = atom * (atom list * clause) type direct_graph = unit Atom_Graph.T - type rich_sequent = clause list * clause + type rich_sequent = atom * (clause list * clause) datatype direct_inference = Have of rich_sequent | @@ -35,9 +35,9 @@ val make_refute_graph : atom -> (atom list * atom) list -> refute_graph val axioms_of_refute_graph : refute_graph -> atom list -> atom list val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list - val sequents_of_refute_graph : refute_graph -> ref_sequent list + val sequents_of_refute_graph : refute_graph -> refute_sequent list val string_of_refute_graph : refute_graph -> string - val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent + val redirect_sequent : atom list -> atom -> refute_sequent -> direct_sequent val direct_graph : direct_sequent list -> direct_graph val redirect_graph : atom list -> atom list -> atom -> refute_graph -> direct_proof val succedent_of_cases : (clause * direct_inference list) list -> clause @@ -51,14 +51,14 @@ structure Atom_Graph = Graph(Atom) -type ref_sequent = atom list * atom +type refute_sequent = atom list * atom type refute_graph = unit Atom_Graph.T type clause = atom list -type direct_sequent = atom list * clause +type direct_sequent = atom * (atom list * clause) type direct_graph = unit Atom_Graph.T -type rich_sequent = clause list * clause +type rich_sequent = atom * (clause list * clause) datatype direct_inference = Have of rich_sequent | @@ -69,7 +69,7 @@ val atom_eq = is_equal o Atom.ord val clause_ord = dict_ord Atom.ord val clause_eq = is_equal o clause_ord -val direct_sequent_ord = prod_ord clause_ord clause_ord +val direct_sequent_ord = prod_ord clause_ord clause_ord o pairself snd val direct_sequent_eq = is_equal o direct_sequent_ord fun make_refute_graph bot infers = @@ -106,11 +106,12 @@ refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines fun redirect_sequent tainted bot (gamma, c) = - if member atom_eq tainted c then - gamma |> List.partition (not o member atom_eq tainted) - |>> not (atom_eq (c, bot)) ? cons c - else - (gamma, [c]) + (c, + if member atom_eq tainted c then + gamma |> List.partition (not o member atom_eq tainted) + |>> not (atom_eq (c, bot)) ? cons c + else + (gamma, [c])) fun direct_graph seqs = let @@ -118,26 +119,19 @@ Atom_Graph.default_node (from, ()) #> Atom_Graph.default_node (to, ()) #> Atom_Graph.add_edge_acyclic (from, to) - fun add_seq (gamma, c) = fold (fn l => fold (add_edge l) c) gamma + fun add_seq (_, (gamma, c)) = fold (fn l => fold (add_edge l) c) gamma in fold add_seq seqs Atom_Graph.empty end fun disj cs = fold (union atom_eq) cs [] |> sort Atom.ord -fun succedent_of_inference (Have (_, c)) = c +fun succedent_of_inference (Have (_, (_, c))) = c | succedent_of_inference (Cases cases) = succedent_of_cases cases and succedent_of_case (c, []) = c | succedent_of_case (_, infs) = succedent_of_inference (List.last infs) and succedent_of_cases cases = disj (map succedent_of_case cases) -fun dest_Have (Have z) = z - | dest_Have _ = raise Fail "non-Have" - -fun enrich_Have nontrivs trivs (cs, c) = - Have (cs |> map (fn c => if member clause_eq nontrivs c then disj (c :: trivs) else c), - disj (c :: trivs)) - fun s_cases cases = [Cases (filter_out (null o snd) cases)] fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single @@ -156,20 +150,20 @@ else if length c < 2 then let val proved = c @ proved - val provable = filter (fn (gamma, _) => subset atom_eq (gamma, proved)) seqs - val horn_provable = filter (fn (_, [_]) => true | _ => false) provable - val seq as (gamma, c) = + val provable = filter (fn (_, (gamma, _)) => subset atom_eq (gamma, proved)) seqs + val horn_provable = filter (fn (_, (_, [_])) => true | _ => false) provable + val seq as (id, (gamma, c)) = (case horn_provable @ provable of [] => raise Fail "ill-formed refutation graph" | next :: _ => next) in - Have (map single gamma, c) :: + Have (id, (map single gamma, c)) :: redirect c proved (filter (curry (not o direct_sequent_eq) seq) seqs) end else let fun subsequents seqs zone = - filter (fn (gamma, _) => subset atom_eq (gamma, zone @ proved)) seqs + filter (fn (_, (gamma, _)) => subset atom_eq (gamma, zone @ proved)) seqs val zones = zones_of (length c) (map (descendants direct_graph) c) val subseqss = map (subsequents seqs) zones val seqs = fold (subtract direct_sequent_eq) subseqss seqs @@ -187,9 +181,9 @@ fun string_of_clause [] = "\" | string_of_clause ls = space_implode " \ " (map Atom.string_of ls) -fun string_of_rich_sequent ch ([], c) = ch ^ " " ^ string_of_clause c - | string_of_rich_sequent ch (cs, c) = - commas (map string_of_clause cs) ^ " " ^ ch ^ " " ^ string_of_clause c +fun string_of_rich_sequent ch (id, (cs, c)) = + (if null cs then "" else commas (map string_of_clause cs) ^ " ") ^ ch ^ " " ^ string_of_clause c ^ + " (* " ^ Atom.string_of id ^ "*)" fun string_of_case depth (c, proof) = indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]" diff -r 6b0ca7f79e93 -r 2eb43ddde491 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:01:38 2013 +0100 @@ -63,6 +63,8 @@ val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] +val is_arith_rule = String.isPrefix z3_th_lemma_rule + fun raw_label_of_num num = (num, 0) fun label_of_clause [(num, _)] = raw_label_of_num num @@ -122,38 +124,38 @@ (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) -fun add_line (line as (name as (_, ss), role, t, rule, [])) lines = +fun add_line_pass1 (line as (name as (_, ss), role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse - role = Hypothesis then + role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then (* Facts are not proof lines. *) lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, [])) else map (replace_dependencies_in_line (name, [])) lines - | add_line line lines = line :: lines + | add_line_pass1 line lines = line :: lines (* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (line as (name, _, t, _, [])) lines = +fun add_line_pass2 (line as (name, _, t, _, [])) lines = if is_only_type_information t then delete_dependency name lines else line :: lines - | add_nontrivial_line line lines = line :: lines + | add_line_pass2 line lines = line :: lines and delete_dependency name lines = - fold_rev add_nontrivial_line (map (replace_dependencies_in_line (name, [])) lines) [] + fold_rev add_line_pass2 (map (replace_dependencies_in_line (name, [])) lines) [] -fun add_desired_lines res [] = rev res - | add_desired_lines res ((name as (_, ss), role, t, rule, deps) :: lines) = - if role <> Plain orelse is_skolemize_rule rule orelse +fun add_line_pass3 res [] = rev res + | add_line_pass3 res ((line as (name as (_, ss), role, t, rule, deps)) :: lines) = + if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse (* the last line must be kept *) null lines orelse (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso length deps >= 2 andalso (* don't keep next to last line, which usually results in a trivial step *) not (can the_single lines)) then - add_desired_lines ((name, role, t, rule, deps) :: res) lines + add_line_pass3 (line :: res) lines else - add_desired_lines res (map (replace_dependencies_in_line (name, deps)) lines) + add_line_pass3 res (map (replace_dependencies_in_line (name, deps)) lines) val add_labels_of_proof = steps_of_proof @@ -266,9 +268,9 @@ atp_proof |> inline_z3_defs [] |> inline_z3_hypotheses [] [] - |> rpair [] |-> fold_rev add_line - |> rpair [] |-> fold_rev add_nontrivial_line - |> add_desired_lines [] + |> rpair [] |-> fold_rev add_line_pass1 + |> rpair [] |-> fold_rev add_line_pass2 + |> add_line_pass3 [] val conjs = map_filter (fn (name, role, _, _, _) => @@ -281,8 +283,8 @@ let val (skos, meth) = if is_skolemize_rule rule then (skolems_of t, MetisM) - else if rule = z3_th_lemma_rule then ([], ArithM) - else ([], SimpM) + else if is_arith_rule rule then ([], ArithM) + else ([], AutoM) in Prove ([], skos, l, maybe_mk_Trueprop t, [], (([], []), meth)) end) @@ -310,9 +312,7 @@ I)))) atp_proof - fun is_clause_skolemize_rule [(s, _)] = - Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true - | is_clause_skolemize_rule _ = false + val rule_of_clause_id = fst o the o Symtab.lookup steps o fst (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or "prop"s (for Z3). TODO: Always use "prop". *) @@ -337,22 +337,28 @@ accum |> (if tainted = [] then cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], - (([the predecessor], []), MetisM))) + ((the_list predecessor, []), MetisM))) else I) |> rev - | isar_steps outer _ accum (Have (gamma, c) :: infs) = + | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = let val l = label_of_clause c val t = prop_of_clause c - val by = (fold add_fact_of_dependencies gamma no_facts, MetisM) + val rule = rule_of_clause_id id + val skolem = is_skolemize_rule rule + fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by) fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs + + val deps = fold add_fact_of_dependencies gamma no_facts + val meth = if is_arith_rule rule then ArithM else MetisM + val by = (deps, meth) in if is_clause_tainted c then (case gamma of [g] => - if is_clause_skolemize_rule g andalso is_clause_tainted g then + if skolem andalso is_clause_tainted g then let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in isar_steps outer (SOME l) [prove [subproof] (no_facts, MetisM)] [] end @@ -360,7 +366,7 @@ do_rest l (prove [] by) | _ => do_rest l (prove [] by)) else - (if is_clause_skolemize_rule c then Prove ([], skolems_of t, l, t, [], by) + (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) |> do_rest l end