# HG changeset patch # User fleury # Date 1406721792 -7200 # Node ID 4b52c1b319ced0b3399f4f41cd4b97875c096c61 # Parent 0242e9578828d6ee14e1c305004ce8c720469c57 veriT changes for lifted terms, and ite_elim rules. diff -r 0242e9578828 -r 4b52c1b319ce src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:12 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:12 2014 +0200 @@ -103,7 +103,7 @@ "--disable-banner", "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]), smt_options = [], - default_max_relevant = 350 (* FUDGE *), + default_max_relevant = 250 (* FUDGE *), outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"), parse_proof = SOME VeriT_Proof_Parse.parse_proof, replay = NONE } diff -r 0242e9578828 -r 4b52c1b319ce 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 @@ -13,6 +13,7 @@ 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 + val unskolemize_names: term -> term end; structure SMTLIB2_Isar: SMTLIB2_ISAR = @@ -63,6 +64,11 @@ and un_term t = map_aterms un_free t in un_term end +(* It is not entirely clear if this is necessary for abstractions variables. *) +val unskolemize_names = + Term.map_abs_vars (perhaps (try Name.dest_skolem)) + #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) + fun postprocess_step_conclusion concl thy rewrite_rules ll_defs = concl |> Raw_Simplifier.rewrite_term thy rewrite_rules [] @@ -72,6 +78,7 @@ |> unskolemize_names |> push_skolem_all_under_iff |> HOLogic.mk_Trueprop + |> unskolemize_names fun normalizing_prems ctxt concl0 = SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ diff -r 0242e9578828 -r 4b52c1b319ce 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 @@ -41,7 +41,7 @@ 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 + fact_helper_ts hyp_ts concl_t concl ||> unskolemize_names in [(name0, role0, concl0, rule, []), ((sid, []), Plain, concl', veriT_rewrite_rule, diff -r 0242e9578828 -r 4b52c1b319ce 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 @@ -55,9 +55,11 @@ 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_ite_elim_rule = "tmp_ite_elim" val veriT_tmp_skolemize = "tmp_skolemize" +val veriT_alpha_conv = "tmp_alphaconv" + +fun mk_string_id id = veriT_step_prefix ^ (string_of_int id) (* proof parser *) @@ -81,74 +83,71 @@ | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) | fix_quantification x = x -fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var replaced n = +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 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 + 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, ty, u)) var_name = - if var_name = v then SOME ty else find_type_in_formula u var_name + if String.isPrefix 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 add_bound_variables_to_ctxt cx bounds concl = + fold (fn a => fn b => update_binding a b) + (map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) + bounds) cx -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) +fun update_step_and_cx (st 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 cx bounds concl) else if rule = veriT_tmp_skolemize then let - val concl' = replace_bound_var_by_free_var concl bounds [] 0 + val concl' = replace_bound_var_by_free_var concl bounds in - (mk_node id rule prems concl' [], update_ctxt cx bounds concl) + (mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl) end else (st, cx) +(*FIXME: using a reference would be better to know th numbers of the steps to add*) fun fix_subproof_steps number_of_steps ((((id, rule), prems), subproof), ((step_concl, bounds), cx)) = let + fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ? + curry (op $) @{term "Trueprop"}) concl 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 + mk_node (id + number_of_steps) rule (filter_out (curry (op =) assumption_id) prems) + (Const ("Pure.imp", @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"}) + $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds else st - fun inline_assumption_in_conclusion concl (VeriT_Node {rule, concl = assumption,...} :: l) = + fun find_input_steps_and_inline [] last_step_number = ([], last_step_number) + | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) + last_step_number = if rule = veriT_input_rule then - inline_assumption_in_conclusion - (Const (@{const_name Pure.imp}, @{typ "prop => prop => prop"}) $ assumption $ concl) l + find_input_steps_and_inline (map (inline_assumption concl (mk_string_id id')) steps) + last_step_number 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 [] = [] + apfst (cons (mk_node (id' + id + number_of_steps) rule prems concl bounds)) + (find_input_steps_and_inline steps (id' + id + number_of_steps)) + val (subproof', last_step_number) = find_input_steps_and_inline subproof ~1 + val prems' = + if last_step_number = ~1 then prems + else + (case prems of + NONE => SOME [mk_string_id last_step_number] + | SOME l => SOME (string_of_int last_step_number :: l)) in - (find_assumption_and_inline subproof, - (((((id, rule), prems), inline_assumption_in_conclusion step_concl subproof), bounds), cx)) + (subproof', (((((id, rule), prems'), step_concl), bounds), cx)) end (* @@ -168,21 +167,19 @@ (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) + let val (subproof_steps, cx') = parse_proof_step number_of_steps cx subproof_step in + apfst (apfst (curry (op @) subproof_steps)) (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 make_or_from_clausification l = - foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2), - bounds1 @ bounds2)) 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) + (the_default [] prems) concl bounds, cx) in get_id #>> change_id_to_number @@ -204,10 +201,15 @@ #> fix_subproof_steps number_of_steps ##> to_node #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) - #> (fn (steps, cx) => update_step cx (List.last steps)) + #> (fn (steps, cx) => fold_map update_step_and_cx steps cx) end -fun seperate_into_lines_and_subproof lines = + +(*function related to parsing and general transformation*) + +(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are +unbalanced on each line*) +fun seperate_into_steps lines = let fun count ("(" :: l) n = count l (n+1) | count (")" :: l) n = count l (n-1) @@ -232,44 +234,115 @@ | 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 = +fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = (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 + NONE => find_in_which_step_defined var l + | SOME _ => id) + | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var) + +(*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 ("HOL.If", _) $ _ $ + (Const ("HOL.eq", _) $ Free (var1, _) $ Free (var2, _) ) $ + (Const ("HOL.eq", _) $ Free (var3, _) $ Free (var4, _) )) = + 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_steps num_of_steps (st as VeriT_Node {id = id, rule = rule, prems = prems, - concl = concl, bounds = bounds}) = +fun correct_veriT_step num_of_steps steps (st as VeriT_Node {id, rule, prems, concl, bounds}) = if rule = "tmp_ite_elim" then + if bounds = [] then + (*if the introduced var has already been defined, + adding the definition as a dependency*) + let + val SOME var = find_ite_var_in_term concl + val new_dep = find_in_which_step_defined var steps + in + VeriT_Node {id = id, rule = rule, prems = (mk_string_id new_dep) :: prems, + concl = concl, bounds = bounds} + end + else + (*some new variables are created*) + let + val concl' = replace_bound_var_by_free_var concl bounds + in + (*FIXME: horrible hackish method, but seems somehow to work. The difference is in the way + sledgehammer reconstructs: without an empty dependency, the skolemization is not done at all. + But if there is, a new step is added: + {fix sk ....} + hence "..sk.." + thus "(if ..)" + last step does not work: the step before is buggy. Without the proof work.*) + mk_node id veriT_tmp_skolemize (if null prems then [mk_string_id (~num_of_steps - id)] + else prems) concl' [] + end + else + st + +(*remove alpha conversion step, that just renames the variables*) +fun remove_alpha_conversion _ [] = [] + | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = let - val concl' = replace_bound_var_by_free_var concl bounds [] 0 + fun correct_dependency prems = + map (fn x => perhaps (Symtab.lookup replace_table) x) prems + fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem 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' []] + if rule = veriT_alpha_conv then + remove_alpha_conversion (Symtab.update (mk_string_id 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 - else - [st] - +fun correct_veriT_steps steps = + steps + |> map (correct_veriT_step (1 + length steps) steps) + |> remove_alpha_conversion Symtab.empty (* 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_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, ...}) = + val smtlib2_lines_without_at = + remove_all_at (map SMTLIB2.parse (seperate_into_steps lines)) + val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step (length lines) cx l) + smtlib2_lines_without_at (empty_context ctxt typs funs)) + val t = correct_veriT_steps u + 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) diff -r 0242e9578828 -r 4b52c1b319ce 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 @@ -23,13 +23,14 @@ open VeriT_Isar open VeriT_Proof -fun find_and_add_missing_dependances steps assms conjecture_id = +fun find_and_add_missing_dependances steps assms ll_offset = let fun prems_to_theorem_number [] id repl = (([], []), (id, repl)) | prems_to_theorem_number (x :: ths) id replaced = (case Int.fromString (perhaps (try (unprefix SMTLIB2_Interface.assert_prefix)) x) of NONE => - let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced + 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')) end @@ -37,13 +38,17 @@ (case Option.map snd (List.find (fst #> curry (op =) x) replaced) of NONE => let - val id' = if th = conjecture_id then 0 else id - conjecture_id + val id' = if th = ll_offset then 0 else id - ll_offset (* 0: for the conjecture*) val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths - (if th = 0 then id + 1 else id) + (if th <> ll_offset then id + 1 else id) ((x, string_of_int id') :: replaced) - in ((string_of_int id' :: prems, (th, (id', th)) :: iidths), (id'', replaced')) end + in + ((string_of_int id' :: prems, (th, (id', th - ll_offset)) :: iidths), + (id'', replaced')) + end | SOME x => - let val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced + let + val ((prems, iidths), (id', replaced')) = prems_to_theorem_number ths id replaced in ((x :: prems, iidths), (id', replaced')) end)) fun update_step (VeriT_Proof.VeriT_Step {prems, id = id0, rule = rule0, concl = concl0, fixes = fixes0}) (id, replaced) = @@ -71,16 +76,15 @@ ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data) xfacts prems concl output = let - val conjecture_i = length ll_defs val (steps, _) = VeriT_Proof.parse typs terms output ctxt - val (iidths, steps'') = find_and_add_missing_dependances steps assms conjecture_i + val (iidths, steps'') = find_and_add_missing_dependances steps assms (length ll_defs) val steps' = add_missing_steps iidths @ steps'' fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i)) val prems_i = 1 val facts_i = prems_i + length prems - - val conjecture_id = id_of_index conjecture_i + val conjecture_i = 0 + val ll_offset = id_of_index conjecture_i val prem_ids = map id_of_index (prems_i upto facts_i - 1) val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths @@ -94,7 +98,7 @@ in {outcome = NONE, fact_ids = fact_ids, atp_proof = fn () => atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules prems concl - fact_helper_ts prem_ids conjecture_id fact_helper_ids steps'} + fact_helper_ts prem_ids ll_offset fact_helper_ids steps'} end end; diff -r 0242e9578828 -r 4b52c1b319ce 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,7 +50,10 @@ val leo2_extcnf_combined_rule = "extcnf_combined" val spass_pirate_datatype_rule = "DT" val vampire_skolemisation_rule = "skolemisation" -val veriT_skomelisation_rule = "tmp_skolemize" +val veriT_tmp_skolemize_rule = "tmp_skolemize" +val veriT_simp_arith_rule = "simp_arith" +val veriT_la_generic_rule = "la_generic" +val veriT_arith_rules = [veriT_simp_arith_rule, veriT_la_generic_rule] (* 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" @@ -58,10 +61,10 @@ val skolemize_rules = [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, -zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_skomelisation_rule] +zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule] val is_skolemize_rule = member (op =) skolemize_rules -val is_arith_rule = String.isPrefix z3_th_lemma_rule +val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules) val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule fun raw_label_of_num num = (num, 0) @@ -75,10 +78,15 @@ fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) - if role = Conjecture orelse role = Negated_Conjecture then line :: lines - else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines - else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines - else if role = Axiom then lines (* axioms (facts) need no proof lines *) + if role = Conjecture orelse role = Negated_Conjecture then + line :: lines + else if t aconv @{prop True} then + map (replace_dependencies_in_line (name, [])) lines + else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule + orelse is_skolemize_rule rule then + line :: lines + else if role = Axiom then + lines (* axioms (facts) need no proof lines *) else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines