Basic support for the SMT prover veriT.
--- 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 = {*
--- 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;
--- 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
--- 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 =
--- /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;
--- /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;
--- /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;
--- /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;
--- 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]
--- 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
--- 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