# HG changeset patch # User fleury # Date 1406721792 -7200 # Node ID 5da48dae7d037b87236d139b475154f5a87eddbd # Parent c0da3fc313e308425f50b862e0433cfbb720fb11 Subproofs for the SMT solver veriT. diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/SMT2/smtlib2_isar.ML --- a/src/HOL/Tools/SMT2/smtlib2_isar.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -10,10 +10,9 @@ val simplify_bool: term -> term val unlift_term: term list -> term -> term val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term - val normalize_prems : Proof.context -> term -> (string * string list) list + val normalizing_prems : Proof.context -> term -> (string * string list) list val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list -> (''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c - end; structure SMTLIB2_Isar: SMTLIB2_ISAR = @@ -74,7 +73,7 @@ |> push_skolem_all_under_iff |> HOLogic.mk_Trueprop -fun normalize_prems ctxt concl0 = +fun normalizing_prems ctxt concl0 = SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ SMT2_Normalize.abs_min_max_table |> map_filter (fn (c, th) => diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/SMT2/verit_isar.ML --- a/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -36,18 +36,16 @@ ((sid, []), role, concl', rule, map (fn id => (id, [])) prems) in - if rule = verit_proof_input_rule then + if rule = veriT_input_rule then let val ss = the_list (AList.lookup (op =) fact_helper_ids id) val name0 = (sid ^ "a", ss) val (role0, concl0) = distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl - - val normalizing_prems = normalize_prems ctxt concl0 in [(name0, role0, concl0, rule, []), - ((sid, []), Plain, concl', verit_rewrite, - name0 :: normalizing_prems)] end + ((sid, []), Plain, concl', veriT_rewrite_rule, + name0 :: normalizing_prems ctxt concl0)] end else [standard_step Plain] end diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/SMT2/verit_proof.ML --- a/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:12 2014 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/SMT2/verit_proof.ML +(* Title: HOL/Tools/SMT2/veriT_proof.ML Author: Mathias Fleury, ENS Rennes Author: Sascha Boehme, TU Muenchen @@ -19,9 +19,9 @@ val parse: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> veriT_step list * Proof.context - val verit_step_prefix : string - val verit_proof_input_rule: string - val verit_rewrite : string + val veriT_step_prefix : string + val veriT_input_rule: string + val veriT_rewrite_rule : string end; structure VeriT_Proof: VERIT_PROOF = @@ -52,9 +52,12 @@ fun mk_step id rule prems concl fixes = VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} -val verit_step_prefix = ".c" -val verit_proof_input_rule = "input" -val verit_rewrite = "rewrite" +val veriT_step_prefix = ".c" +val veriT_input_rule = "input" +val veriT_rewrite_rule = "__rewrite" (*arbitrary*) +val veriT_proof_ite_elim_rule = "tmp_ite_elim" +val veriT_var_suffix = "v" +val veriT_tmp_skolemize = "tmp_skolemize" (* proof parser *) @@ -62,12 +65,11 @@ ([], cx) ||>> with_fresh_names (term_of p) ||>> next_id - |>> (fn ((prems, (t, ns)), id) => mk_node id verit_proof_input_rule prems t ns) + |>> (fn ((prems, (t, ns)), id) => mk_node id veriT_input_rule prems t ns) (*in order to get Z3-style quantification*) fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) = - let - val (quantified_vars, t) = split_last (map fix_quantification l) + let val (quantified_vars, t) = split_last (map fix_quantification l) in SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) end @@ -79,30 +81,108 @@ | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) | fix_quantification x = x -fun parse_proof cx = +fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var replaced n = + (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 replaced (n+1)) + | SOME _ => + replace_bound_var_by_free_var u free_var ((n, Free (var ^ veriT_var_suffix, ty)) :: replaced) + (n+1)) + | replace_bound_var_by_free_var (Bound n) _ replaced_vars _ = + (case List.find (curry (op =) n o fst) replaced_vars of + NONE => Bound n + | SOME (_, var) => var) + | replace_bound_var_by_free_var (u $ v) free_vars replaced n = + replace_bound_var_by_free_var u free_vars replaced n $ + replace_bound_var_by_free_var v free_vars replaced n + | replace_bound_var_by_free_var u _ _ _ = u + +fun find_type_in_formula (Abs(v, ty, u)) var_name = + if var_name = v then SOME ty 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 + | a => a) + | find_type_in_formula _ _ = NONE + + +fun update_ctxt cx bounds concl = + fold_index (fn (_, a) => fn b => update_binding a b) + (map (fn s => ((s, Term (Free (s ^ "__" ^ veriT_var_suffix, + the_default dummyT (find_type_in_formula concl s)))))) bounds) cx + +fun update_step cx (st as VeriT_Node {id, rule, prems, concl, bounds}) = + if rule = veriT_proof_ite_elim_rule then + (mk_node id rule prems concl bounds, update_ctxt cx bounds concl) + else if rule = veriT_tmp_skolemize then + let + val concl' = replace_bound_var_by_free_var concl bounds [] 0 + in + (mk_node id rule prems concl' [], update_ctxt cx bounds concl) + end + else + (st, cx) + +fun fix_subproof_steps number_of_steps ((((id, rule), prems), subproof), ((step_concl, bounds), + cx)) = + let + fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl, + bounds}) = + if List.find (curry (op =) assumption_id) prems <> NONE then + mk_node (id + number_of_steps) rule (filter_out (curry (op =) assumption_id) prems) + ((Const ("Pure.imp", @{typ "prop => prop => prop"}) $ assumption) $ concl) + bounds + else + st + fun inline_assumption_in_conclusion concl (VeriT_Node {rule, concl = assumption,...} :: l) = + if rule = veriT_input_rule then + inline_assumption_in_conclusion + (Const (@{const_name Pure.imp}, @{typ "prop => prop => prop"}) $ assumption $ concl) l + else + inline_assumption_in_conclusion concl l + | inline_assumption_in_conclusion concl [] = concl + fun find_assumption_and_inline (VeriT_Node {id, rule, prems, concl, bounds} :: l) = + if rule = veriT_input_rule then + map (inline_assumption step_concl (veriT_step_prefix ^ string_of_int id)) l + else + (mk_node (id + number_of_steps) rule prems concl bounds) :: find_assumption_and_inline l + | find_assumption_and_inline [] = [] + in + (find_assumption_and_inline subproof, + (((((id, rule), prems), inline_assumption_in_conclusion step_concl subproof), bounds), cx)) + end + +(* +(set id rule :clauses(...) :args(..) :conclusion (...)). +or +(set id subproof (set ...) :conclusion (...)). +*) + +fun parse_proof_step number_of_steps cx = let fun rotate_pair (a, (b, c)) = ((a, b), c) fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) - fun change_id_to_number x = (unprefix verit_step_prefix #> Int.fromString #> the) x + fun change_id_to_number x = (unprefix veriT_step_prefix #> Int.fromString #> the) x fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) | parse_source l = (NONE, l) + fun parse_subproof cx ((subproof_step as SMTLIB2.S (SMTLIB2.Sym "set" :: _)) :: l) = + let val (step, cx') = parse_proof_step number_of_steps cx subproof_step in + apfst (apfst (cons step)) (parse_subproof cx' l) + end + | parse_subproof cx l = (([], cx), l) + fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l | skip_args l = l - fun parse_conclusion [SMTLIB2.Key "conclusion", SMTLIB2.S concl] = concl + fun parse_conclusion (SMTLIB2.Key "conclusion" :: SMTLIB2.S concl :: []) = concl fun make_or_from_clausification l = foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2), bounds1 @ bounds2)) l - (*the conclusion is empty, ie no false*) - fun to_node ((((id, rule), prems), ([], cx))) = (mk_node id rule (the_default [] prems) - @{const False} [], cx) - | to_node ((((id, rule), prems), (concls, cx))) = - let val (concl, bounds) = make_or_from_clausification concls in - (mk_node id rule (the_default [] prems) concl bounds, cx) end + fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule + (the_default [] prems) concl bounds, cx) in get_id #>> change_id_to_number @@ -111,25 +191,88 @@ ##> parse_source #> rotate_pair ##> skip_args + ##> parse_subproof cx + #> rotate_pair ##> parse_conclusion ##> map fix_quantification - ##> (fn terms => fold_map (fn t => fn cx => node_of t cx) terms cx) - ##> apfst (map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds))) - #> to_node + #> (fn ((((id, rule), prems), (subproof, cx)), terms) => + (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) + ##> apfst ((map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds)))) + (*the conclusion is the empty list, ie no false is written, we have to add it.*) + ##> (apfst (fn [] => (@{const False}, []) + | concls => make_or_from_clausification concls)) + #> fix_subproof_steps number_of_steps + ##> to_node + #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) + #> (fn (steps, cx) => update_step cx (List.last steps)) + end + +fun seperate_into_lines_and_subproof lines = + let + fun count ("(" :: l) n = count l (n+1) + | count (")" :: l) n = count l (n-1) + | count (_ :: l) n = count l n + | count [] n = n + fun seperate (line :: l) actual_lines m = + let val n = count (raw_explode line) 0 in + if m + n = 0 then + [actual_lines ^ line] :: seperate l "" 0 + else seperate l (actual_lines ^ line) (m + n) + end + | seperate [] _ 0 = [] + in + seperate lines "" 0 end + (*VeriT adds @ before every variable.*) +fun remove_all_at (SMTLIB2.Sym v :: l) = + SMTLIB2.Sym (if nth_string v 0 = "@" then String.extract (v, 1, NONE) else v) :: remove_all_at l + | remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l' + | remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l + | remove_all_at (v :: l) = v :: remove_all_at l + | remove_all_at [] = [] + +fun replace_all_by_exist (Const (@{const_name Pure.all}, ty) $ Abs (var, ty', u)) bounds = + (case List.find (fn v => String.isPrefix v var) bounds of + NONE => (Const (@{const_name Pure.all}, ty) $ Abs (var, ty', replace_all_by_exist u bounds)) + | SOME _ => Const (@{const_name HOL.Ex}, (ty' --> @{typ bool}) --> @{typ bool}) $ + Abs (var ^ veriT_var_suffix, ty', replace_all_by_exist u bounds)) + | replace_all_by_exist (@{term "Trueprop"} $ g) bounds = replace_all_by_exist g bounds + | replace_all_by_exist (f $ g) bounds = + replace_all_by_exist f bounds $ replace_all_by_exist g bounds + | replace_all_by_exist (Abs (var, ty, u)) bounds = Abs (var, ty, replace_all_by_exist u bounds) + | replace_all_by_exist f _ = f + + +fun correct_veriT_steps num_of_steps (st as VeriT_Node {id = id, rule = rule, prems = prems, + concl = concl, bounds = bounds}) = + if rule = "tmp_ite_elim" then + let + val concl' = replace_bound_var_by_free_var concl bounds [] 0 + in + [mk_node (num_of_steps + id) rule prems (@{term "Trueprop"} $ + replace_all_by_exist concl bounds) [], + mk_node id veriT_tmp_skolemize (veriT_step_prefix ^ (string_of_int (num_of_steps + id)) :: + []) concl' []] + end + else + [st] + + (* overall proof parser *) fun parse typs funs lines ctxt = let + val smtlib2_lines_without_at = + remove_all_at (map SMTLIB2.parse (seperate_into_lines_and_subproof lines)) val (u, env) = - fold_map (fn l => fn cx => parse_proof cx l) (map (fn f => SMTLIB2.parse [f]) lines) - (empty_context ctxt typs funs) - val t = - map (fn (VeriT_Node {id, rule, prems, concl, bounds, ...}) => - mk_step id rule prems concl bounds) u - in - (t, ctxt_of env) + fold_map (fn l => fn cx => parse_proof_step (length lines) cx l) smtlib2_lines_without_at + (empty_context ctxt typs funs) + val t = map (correct_veriT_steps (1 + length u)) u |> flat + fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = + mk_step id rule prems concl bounds + in + (map node_to_step t, ctxt_of env) end end; diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/SMT2/verit_proof_parse.ML --- a/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:12 2014 +0200 @@ -31,7 +31,7 @@ NONE => let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced in - ((perhaps (try (unprefix verit_step_prefix)) x :: prems, iidths), (id', replaced')) + ((perhaps (try (unprefix veriT_step_prefix)) x :: prems, iidths), (id', replaced')) end | SOME th => (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -87,12 +87,11 @@ distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t concl - val normalizing_prems = normalize_prems ctxt concl0 in (if role0 = Axiom then [] else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @ [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite, - name0 :: normalizing_prems)] + name0 :: normalizing_prems ctxt concl0)] end | Z3_New_Proof.Rewrite => [standard_step Lemma] | Z3_New_Proof.Rewrite_Star => [standard_step Lemma] diff -r c0da3fc313e3 -r 5da48dae7d03 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -50,6 +50,7 @@ val leo2_extcnf_combined_rule = "extcnf_combined" val spass_pirate_datatype_rule = "DT" val vampire_skolemisation_rule = "skolemisation" +val veriT_skomelisation_rule = "tmp_skolemize" (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) val z3_skolemize_rule = "sk" val z3_th_lemma_rule = "th-lemma"