# HG changeset patch # User fleury # Date 1406721792 -7200 # Node ID c0da3fc313e308425f50b862e0433cfbb720fb11 # Parent fefe3ea752898df73d2abb5be0f909a40ece1f24 Basic support for the SMT prover veriT. diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/SMT2.thy Wed Jul 30 14:03:12 2014 +0200 @@ -108,6 +108,7 @@ ML_file "Tools/SMT2/smtlib2.ML" ML_file "Tools/SMT2/smtlib2_interface.ML" ML_file "Tools/SMT2/smtlib2_proof.ML" +ML_file "Tools/SMT2/smtlib2_isar.ML" ML_file "Tools/SMT2/z3_new_proof.ML" ML_file "Tools/SMT2/z3_new_isar.ML" ML_file "Tools/SMT2/smt2_solver.ML" @@ -117,6 +118,9 @@ ML_file "Tools/SMT2/z3_new_replay_rules.ML" ML_file "Tools/SMT2/z3_new_replay_methods.ML" ML_file "Tools/SMT2/z3_new_replay.ML" +ML_file "Tools/SMT2/verit_proof.ML" +ML_file "Tools/SMT2/verit_isar.ML" +ML_file "Tools/SMT2/verit_proof_parse.ML" ML_file "Tools/SMT2/smt2_systems.ML" method_setup smt2 = {* diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:12 2014 +0200 @@ -37,6 +37,8 @@ val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines)) in (test_outcome solver_name l, ls) end +fun on_first_non_unsupported_line test_outcome solver_name lines = + on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) (* CVC3 *) @@ -85,6 +87,26 @@ end +(* veriT *) + +val veriT: SMT2_Solver.solver_config = { + name = "veriT", + class = K SMTLIB2_Interface.smtlib2C, + avail = make_avail "VERIT", + command = make_command "VERIT", + options = (fn ctxt => [ + "--proof-version=1", + "--proof=-", + "--proof-prune", + "--proof-merge", + "--disable-print-success", + "--disable-banner", + "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]), + smt_options = [], + default_max_relevant = 350 (* 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 } (* Z3 *) @@ -160,6 +182,7 @@ val _ = Theory.setup ( SMT2_Solver.add_solver cvc3 #> SMT2_Solver.add_solver cvc4 #> + SMT2_Solver.add_solver veriT #> SMT2_Solver.add_solver z3) end; diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/smtlib2.ML --- a/src/HOL/Tools/SMT2/smtlib2.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2.ML Wed Jul 30 14:03:12 2014 +0200 @@ -118,7 +118,7 @@ read l cs None ((S (rev ts1) :: ts2) :: tss) | read l ("#" :: "x" :: cs) None (ts :: tss) = token read_hex l cs ts tss - | read l ("#" :: cs) None (ts :: tss) = + | read l ("#" :: "b" :: cs) None (ts :: tss) = token read_bin l cs ts tss | read l (":" :: cs) None (ts :: tss) = token (read_sym Key) l cs ts tss diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/smtlib2_interface.ML --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Wed Jul 30 14:03:12 2014 +0200 @@ -11,6 +11,7 @@ val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic val translate_config: Proof.context -> SMT2_Translate.config val assert_index_of_name: string -> int + val assert_prefix : string end; structure SMTLIB2_Interface: SMTLIB2_INTERFACE = diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/smtlib2_isar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -0,0 +1,99 @@ +(* Title: HOL/Tools/SMT2/smtlib2_isar.ML + Author: Jasmin Blanchette, TU Muenchen + Author: Mathias Fleury, ENS Rennes + +General tools for Isar proof reconstruction. +*) + +signature SMTLIB2_ISAR = +sig + 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 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 = +struct + +open ATP_Problem +open ATP_Util + +fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) = + let val t' = simplify_bool t in + if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t' + end + | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t) + | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u) + | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u) + | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u) + | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u) + | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) = + if u aconv v then @{const True} else t + | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u + | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t) + | simplify_bool t = t + +fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T) + | strip_alls t = ([], t) + +fun push_skolem_all_under_iff t = + (case strip_alls t of + (qs as _ :: _, + (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) => + t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2) + | _ => t) + +(* It is not entirely clear why this should be necessary, especially 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 unlift_term ll_defs = + let + val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs + + fun un_free (t as Free (s, _)) = + (case AList.lookup (op =) lifted s of + SOME t => un_term t + | NONE => t) + | un_free t = t + and un_term t = map_aterms un_free t + in un_term end + +fun postprocess_step_conclusion concl thy rewrite_rules ll_defs = + concl + |> Raw_Simplifier.rewrite_term thy rewrite_rules [] + |> Object_Logic.atomize_term thy + |> simplify_bool + |> not (null ll_defs) ? unlift_term ll_defs + |> unskolemize_names + |> push_skolem_all_under_iff + |> HOLogic.mk_Trueprop + +fun normalize_prems ctxt concl0 = + SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ + SMT2_Normalize.abs_min_max_table + |> map_filter (fn (c, th) => + if exists_Const (curry (op =) c o fst) concl0 then + let val s = short_thm_name ctxt th in SOME (s, [s]) end + else + NONE) + +fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t + t = + (case ss of + [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s)) + | _ => + if id = conjecture_id then + (Conjecture, concl_t) + else + (Hypothesis, + (case find_index (curry (op =) id) prem_ids of + ~1 => t + | i => nth hyp_ts i))) + +end; diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/verit_isar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/verit_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -0,0 +1,58 @@ +(* Title: HOL/Tools/SMT2/verit_isar.ML + Author: Mathias Fleury, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +VeriT proofs as generic ATP proofs for Isar proof reconstruction. +*) + +signature VERIT_ISAR = +sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term -> + (string * term) list -> int list -> int -> (int * string) list -> VeriT_Proof.veriT_step list -> + (term, string) ATP_Proof.atp_step list +end; + +structure VeriT_Isar: VERIT_ISAR = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Proof_Reconstruct +open SMTLIB2_Isar +open VeriT_Proof + +fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids + conjecture_id fact_helper_ids proof = + let + val thy = Proof_Context.theory_of ctxt + + fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) = + let + val sid = string_of_int id + val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs + fun standard_step role = + ((sid, []), role, concl', rule, + map (fn id => (id, [])) prems) + in + if rule = verit_proof_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 + else + [standard_step Plain] + end + in + maps steps_of proof + end + +end; diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/verit_proof.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:12 2014 +0200 @@ -0,0 +1,135 @@ +(* Title: HOL/Tools/SMT2/verit_proof.ML + Author: Mathias Fleury, ENS Rennes + Author: Sascha Boehme, TU Muenchen + +VeriT proofs: parsing and abstract syntax tree. +*) + +signature VERIT_PROOF = +sig + (*proofs*) + datatype veriT_step = VeriT_Step of { + id: int, + rule: string, + prems: string list, + concl: term, + fixes: string list} + + (*proof parser*) + 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 +end; + +structure VeriT_Proof: VERIT_PROOF = +struct + +open SMTLIB2_Proof + +(* proof rules *) + +datatype veriT_node = VeriT_Node of { + id: int, + rule: string, + prems: string 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} + +(*two structures needed*) +datatype veriT_step = VeriT_Step of { + id: int, + rule: string, + prems: string 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} + +val verit_step_prefix = ".c" +val verit_proof_input_rule = "input" +val verit_rewrite = "rewrite" + +(* proof parser *) + +fun node_of p cx = + ([], cx) + ||>> with_fresh_names (term_of p) + ||>> next_id + |>> (fn ((prems, (t, ns)), id) => mk_node id verit_proof_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) + in + SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) + end + | fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) = + let val (quantified_vars, t) = split_last (map fix_quantification l) + in + SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) + end + | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) + | fix_quantification x = x + +fun parse_proof 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 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 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 + (*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 + in + get_id + #>> change_id_to_number + ##> parse_rule + #> rotate_pair + ##> parse_source + #> rotate_pair + ##> skip_args + ##> 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 + end + + +(* overall proof parser *) +fun parse typs funs lines ctxt = + let + 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) + end + +end; diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/verit_proof_parse.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:12 2014 +0200 @@ -0,0 +1,100 @@ +(* Title: HOL/Tools/SMT2/verit_proof_parse.ML + Author: Mathias Fleury, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +VeriT proof parsing. +*) + +signature VERIT_PROOF_PARSE = +sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + val parse_proof: Proof.context -> SMT2_Translate.replay_data -> + ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> + SMT2_Solver.parsed_proof +end; + +structure VeriT_Proof_Parse: VERIT_PROOF_PARSE = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Proof_Reconstruct +open VeriT_Isar +open VeriT_Proof + +fun find_and_add_missing_dependances steps assms conjecture_id = + 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 + in + ((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 + NONE => + let + val id' = if th = conjecture_id then 0 else id - conjecture_id + val ((prems, iidths), (id'', replaced')) = prems_to_theorem_number ths + (if th = 0 then id + 1 else id) + ((x, string_of_int id') :: replaced) + in ((string_of_int id' :: prems, (th, (id', th)) :: iidths), (id'', replaced')) end + | SOME x => + 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) = + let val ((prems', iidths), (id', replaced)) = prems_to_theorem_number prems id replaced + in + ((VeriT_Proof.VeriT_Step {id = id0, rule = rule0, prems = prems', concl = concl0, + fixes = fixes0}, iidths), (id', replaced)) + end + in + fold_map update_step steps (1, []) + |> fst + |> `(map snd) + ||> (map fst) + |>> flat + |>> map (fn (_, (id, tm_id)) => let val (i, tm) = nth assms tm_id in (i, (id, tm)) end) + end + +fun add_missing_steps iidths = + let + fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = id, rule = "input", + prems = [], concl = prop_of th, fixes = []} + in map add_single_step iidths end + +fun parse_proof _ + ({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 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 prem_ids = map id_of_index (prems_i upto facts_i - 1) + val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths + + val fact_ids = map_filter (fn (i, (id, _)) => + (try (apsnd (nth xfacts)) (id, i - facts_i))) iidths + val fact_helper_ts = + map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @ + map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids + val fact_helper_ids = + map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids + 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'} + end + +end; diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -18,6 +18,7 @@ open ATP_Problem open ATP_Proof open ATP_Proof_Reconstruct +open SMTLIB2_Isar val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis @@ -62,69 +63,16 @@ end end -fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) = - let val t' = simplify_bool t in - if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t' - end - | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t) - | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u) - | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u) - | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u) - | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u) - | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) = - if u aconv v then @{const True} else t - | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u - | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t) - | simplify_bool t = t - -(* It is not entirely clear why this should be necessary, especially 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 strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T) - | strip_alls t = ([], t) - -fun push_skolem_all_under_iff t = - (case strip_alls t of - (qs as _ :: _, - (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) => - t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2) - | _ => t) - -fun unlift_term ll_defs = - let - val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs - - fun un_free (t as Free (s, _)) = - (case AList.lookup (op =) lifted s of - SOME t => un_term t - | NONE => t) - | un_free t = t - and un_term t = map_aterms un_free t - in un_term end - fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids proof = let val thy = Proof_Context.theory_of ctxt - val unlift_term = unlift_term ll_defs - fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = let val sid = string_of_int id - val concl' = - concl - |> Raw_Simplifier.rewrite_term thy rewrite_rules [] - |> Object_Logic.atomize_term thy - |> simplify_bool - |> not (null ll_defs) ? unlift_term - |> unskolemize_names - |> push_skolem_all_under_iff - |> HOLogic.mk_Trueprop - + val concl' = postprocess_step_conclusion concl thy rewrite_rules ll_defs fun standard_step role = ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule, map (fn id => (string_of_int id, [])) prems) @@ -136,30 +84,15 @@ val name0 = (sid ^ "a", ss) val (role0, concl0) = - (case ss of - [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s)) - | _ => - if id = conjecture_id then - (Conjecture, concl_t) - else - (Hypothesis, - (case find_index (curry (op =) id) prem_ids of - ~1 => concl - | i => nth hyp_ts i))) + distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts + hyp_ts concl_t concl - val normalize_prems = - SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ - SMT2_Normalize.abs_min_max_table - |> map_filter (fn (c, th) => - if exists_Const (curry (op =) c o fst) concl0 then - let val s = short_thm_name ctxt th in SOME (s, [s]) end - else - NONE) + 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 :: normalize_prems)] + name0 :: normalizing_prems)] end | Z3_New_Proof.Rewrite => [standard_step Lemma] | Z3_New_Proof.Rewrite_Star => [standard_step Lemma] diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200 @@ -57,7 +57,7 @@ val skolemize_rules = [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, -zipperposition_cnf_rule, leo2_extcnf_combined_rule] +zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_skomelisation_rule] val is_skolemize_rule = member (op =) skolemize_rules val is_arith_rule = String.isPrefix z3_th_lemma_rule diff -r fefe3ea75289 -r c0da3fc313e3 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 14:03:11 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Jul 30 14:03:12 2014 +0200 @@ -258,6 +258,7 @@ val canonical_isar_supported_prover = eN val z3N = "z3" +val veriT_newN = "veriT" fun isar_supported_prover_of thy name = if is_atp thy name orelse name = z3N then name