diff --git a/src/HOL/Tools/SMT/cvc4_proof_parse.ML b/src/HOL/Tools/SMT/cvc4_proof_parse.ML --- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML +++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML @@ -1,47 +1,47 @@ (* Title: HOL/Tools/SMT/cvc4_proof_parse.ML Author: Jasmin Blanchette, TU Muenchen CVC4 proof (actually, unsat core) parsing. *) signature CVC4_PROOF_PARSE = sig val parse_proof: SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> SMT_Solver.parsed_proof end; structure CVC4_Proof_Parse: CVC4_PROOF_PARSE = struct fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output = if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then {outcome = NONE, fact_ids = NONE, atp_proof = K []} else let val num_ll_defs = length ll_defs val id_of_index = Integer.add num_ll_defs val index_of_id = Integer.add (~ num_ll_defs) val used_assert_ids = map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output val used_assm_js = map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) used_assert_ids val conjecture_i = 0 val prems_i = conjecture_i + 1 val num_prems = length prems val facts_i = prems_i + num_prems val fact_ids' = map_filter (fn j => - let val (i, _) = nth assms j in + let val ((i, _), _) = nth assms j in try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) end) used_assm_js in {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []} end end; diff --git a/src/HOL/Tools/SMT/lethe_proof_parse.ML b/src/HOL/Tools/SMT/lethe_proof_parse.ML --- a/src/HOL/Tools/SMT/lethe_proof_parse.ML +++ b/src/HOL/Tools/SMT/lethe_proof_parse.ML @@ -1,76 +1,80 @@ (* Title: HOL/Tools/SMT/verit_proof_parse.ML Author: Mathias Fleury, TU Muenchen Author: Jasmin Blanchette, TU Muenchen VeriT proof parsing. *) signature LETHE_PROOF_PARSE = sig type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step val parse_proof: SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> SMT_Solver.parsed_proof end; structure Lethe_Proof_Parse: LETHE_PROOF_PARSE = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Proof_Reconstruct open Lethe_Isar open Lethe_Proof fun parse_proof ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) xfacts prems concl output = let val num_ll_defs = length ll_defs val id_of_index = Integer.add num_ll_defs val index_of_id = Integer.add (~ num_ll_defs) - fun step_of_assume j (_, th) = - Lethe_Proof.Lethe_Step {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), + fun step_of_assume j ((_, role), th) = + Lethe_Proof.Lethe_Step + {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j), rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} val (actual_steps, _) = Lethe_Proof.parse typs terms output ctxt val used_assert_ids = - map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output + actual_steps + |> map_filter (fn (Lethe_Step { id, ...}) => + try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id) val used_assm_js = map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) used_assert_ids val used_assms = map (nth assms) used_assm_js val assm_steps = map2 step_of_assume used_assm_js used_assms val steps = assm_steps @ actual_steps val conjecture_i = 0 val prems_i = conjecture_i + 1 val num_prems = length prems val facts_i = prems_i + num_prems val num_facts = length xfacts val helpers_i = facts_i + num_facts val conjecture_id = id_of_index conjecture_i val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) val fact_ids' = map_filter (fn j => - let val (i, _) = nth assms j in + let val ((i, _), _) = nth assms j in try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) end) used_assm_js - val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms + val helper_ids' = + map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms val fact_helper_ts = map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ map (fn (_, ((s, _), th)) => (s, Thm.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 = SOME 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 --git a/src/HOL/Tools/SMT/smt_translate.ML b/src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML +++ b/src/HOL/Tools/SMT/smt_translate.ML @@ -1,540 +1,540 @@ (* Title: HOL/Tools/SMT/smt_translate.ML Author: Sascha Boehme, TU Muenchen Translate theorems into an SMT intermediate format and serialize them. *) signature SMT_TRANSLATE = sig (*intermediate term structure*) datatype squant = SForall | SExists datatype 'a spattern = SPat of 'a list | SNoPat of 'a list datatype sterm = SVar of int * sterm list | SConst of string * sterm list | SQua of squant * string list * sterm spattern list * sterm (*translation configuration*) type sign = { logic: string, sorts: string list, dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, funcs: (string * (string list * string)) list } type config = { order: SMT_Util.order, logic: string -> term list -> string, fp_kinds: BNF_Util.fp_kind list, serialize: (string * string) list -> string list -> sign -> (SMT_Util.role * sterm) list -> string } type replay_data = { context: Proof.context, typs: typ Symtab.table, terms: term Symtab.table, ll_defs: term list, rewrite_rules: thm list, - assms: (int * thm) list } + assms: ((int * SMT_Util.role) * thm) list } (*translation*) val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic val translate: Proof.context -> string -> (string * string) list -> string list -> ((int * SMT_Util.role) * thm) list -> string * replay_data end; structure SMT_Translate: SMT_TRANSLATE = struct (* intermediate term structure *) datatype squant = SForall | SExists datatype 'a spattern = SPat of 'a list | SNoPat of 'a list datatype sterm = SVar of int * sterm list | SConst of string * sterm list | SQua of squant * string list * sterm spattern list * sterm (* translation configuration *) type sign = { logic: string, sorts: string list, dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list, funcs: (string * (string list * string)) list } type config = { order: SMT_Util.order, logic: string -> term list -> string, fp_kinds: BNF_Util.fp_kind list, serialize: (string * string) list -> string list -> sign -> (SMT_Util.role * sterm) list -> string } type replay_data = { context: Proof.context, typs: typ Symtab.table, terms: term Symtab.table, ll_defs: term list, rewrite_rules: thm list, - assms: (int * thm) list } + assms: ((int * SMT_Util.role) * thm) list } (* translation context *) fun add_components_of_typ (Type (s, Ts)) = cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts | add_components_of_typ (TFree (s, _)) = cons (perhaps (try (unprefix "'")) s) | add_components_of_typ _ = I; fun suggested_name_of_typ T = space_implode "_" (add_components_of_typ T []); fun suggested_name_of_term (Const (s, _)) = Long_Name.base_name s | suggested_name_of_term (Free (s, _)) = s | suggested_name_of_term _ = Name.uu val empty_tr_context = (Name.context, Typtab.empty, Termtab.empty) val safe_suffix = "$" fun add_typ T proper (cx as (names, typs, terms)) = (case Typtab.lookup typs T of SOME (name, _) => (name, cx) | NONE => let val sugg = Name.desymbolize (SOME true) (suggested_name_of_typ T) ^ safe_suffix val (name, names') = Name.variant sugg names val typs' = Typtab.update (T, (name, proper)) typs in (name, (names', typs', terms)) end) fun add_fun t sort (cx as (names, typs, terms)) = (case Termtab.lookup terms t of SOME (name, _) => (name, cx) | NONE => let val sugg = Name.desymbolize (SOME false) (suggested_name_of_term t) ^ safe_suffix val (name, names') = Name.variant sugg names val terms' = Termtab.update (t, (name, sort)) terms in (name, (names', typs, terms')) end) fun sign_of logic dtyps (_, typs, terms) = { logic = logic, sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], dtyps = dtyps, funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) = let fun add_typ (T, (n, _)) = Symtab.update (n, T) val typs' = Typtab.fold add_typ typs Symtab.empty fun add_fun (t, (n, _)) = Symtab.update (n, t) val terms' = Termtab.fold add_fun terms Symtab.empty in {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules, - assms = map (apfst fst) assms} + assms = assms} end (* preprocessing *) (** (co)datatype declarations **) fun collect_co_datatypes fp_kinds (tr_context, ctxt) ts = let val (fp_decls, ctxt') = ([], ctxt) |> fold (Term.fold_types (SMT_Datatypes.add_decls fp_kinds) o snd) ts |>> flat fun is_decl_typ T = exists (equal T o fst o snd) fp_decls fun add_typ' T proper = (case SMT_Builtin.dest_builtin_typ ctxt' T of SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *) | NONE => add_typ T proper) fun tr_select sel = let val T = Term.range_type (Term.fastype_of sel) in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end fun tr_constr (constr, selects) = add_fun constr NONE ##>> fold_map tr_select selects fun tr_typ (fp, (T, cases)) = add_typ' T false ##>> fold_map tr_constr cases #>> pair fp val (fp_decls', tr_context') = fold_map tr_typ fp_decls tr_context fun add (constr, selects) = Termtab.update (constr, length selects) #> fold (Termtab.update o rpair 1) selects val funcs = fold (fold add o snd o snd) fp_decls Termtab.empty in ((funcs, fp_decls', tr_context', ctxt'), ts) end (* FIXME: also return necessary (co)datatype theorems *) (** eta-expand quantifiers, let expressions and built-ins *) local fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0)) fun exp f T = eta f (Term.domain_type (Term.domain_type T)) fun exp2 T q = let val U = Term.domain_type T in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end fun expf k i T t = let val Ts = drop i (fst (SMT_Util.dest_funT k T)) in Term.incr_boundvars (length Ts) t |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1) |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts end in fun eta_expand ctxt funcs = let fun exp_func t T ts = (case Termtab.lookup funcs t of SOME k => Term.list_comb (t, ts) |> k <> length ts ? expf k (length ts) T | NONE => Term.list_comb (t, ts)) fun expand ((q as Const (\<^const_name>\All\, _)) $ Abs a) = q $ abs_expand a | expand ((q as Const (\<^const_name>\All\, T)) $ t) = q $ exp expand T t | expand (q as Const (\<^const_name>\All\, T)) = exp2 T q | expand ((q as Const (\<^const_name>\Ex\, _)) $ Abs a) = q $ abs_expand a | expand ((q as Const (\<^const_name>\Ex\, T)) $ t) = q $ exp expand T t | expand (q as Const (\<^const_name>\Ex\, T)) = exp2 T q | expand (Const (\<^const_name>\Let\, T) $ t) = let val U = Term.domain_type (Term.range_type T) in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end | expand (Const (\<^const_name>\Let\, T)) = let val U = Term.domain_type (Term.range_type T) in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end | expand t = (case Term.strip_comb t of (Const (\<^const_name>\Let\, _), t1 :: t2 :: ts) => Term.betapplys (Term.betapply (expand t2, expand t1), map expand ts) | (u as Const (c as (_, T)), ts) => (case SMT_Builtin.dest_builtin ctxt c ts of SOME (_, k, us, mk) => if k = length us then mk (map expand us) else if k < length us then chop k (map expand us) |>> mk |> Term.list_comb else expf k (length ts) T (mk (map expand us)) | NONE => exp_func u T (map expand ts)) | (u as Free (_, T), ts) => exp_func u T (map expand ts) | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) | (u, ts) => Term.list_comb (u, map expand ts)) and abs_expand (n, T, t) = Abs (n, T, expand t) in map (apsnd expand) end end (** introduce explicit applications **) local (* Make application explicit for functions with varying number of arguments. *) fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) fun add_type T = apsnd (Typtab.update (T, ())) fun min_arities t = (case Term.strip_comb t of (u as Const _, ts) => add u (length ts) #> fold min_arities ts | (u as Free _, ts) => add u (length ts) #> fold min_arities ts | (Abs (_, T, u), ts) => (can dest_funT T ? add_type T) #> min_arities u #> fold min_arities ts | (_, ts) => fold min_arities ts) fun take_vars_into_account types t i = let fun find_min j (T as Type (\<^type_name>\fun\, [_, T'])) = if j = i orelse Typtab.defined types T then j else find_min (j + 1) T' | find_min j _ = j in find_min 0 (Term.type_of t) end fun app u (t, T) = (Const (\<^const_name>\fun_app\, T --> T) $ t $ u, Term.range_type T) fun apply i t T ts = let val (ts1, ts2) = chop i ts val (_, U) = SMT_Util.dest_funT i T in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end in fun intro_explicit_application ctxt funcs ts = let val explicit_application = Config.get ctxt SMT_Config.explicit_application val get_arities = (case explicit_application of 0 => min_arities | 1 => min_arities | 2 => K I | n => error ("Illegal value for " ^ quote (Config.name_of SMT_Config.explicit_application) ^ ": " ^ string_of_int n)) val (arities, types) = fold (get_arities o snd) ts (Termtab.empty, Typtab.empty) val arities' = arities |> explicit_application = 1 ? Termtab.map (take_vars_into_account types) fun app_func t T ts = if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) else apply (the_default 0 (Termtab.lookup arities' t)) t T ts fun in_list T f t = SMT_Util.mk_symb_list T (map f (SMT_Util.dest_symb_list t)) fun traverse Ts t = (case Term.strip_comb t of (q as Const (\<^const_name>\All\, _), [Abs (x, T, u)]) => q $ Abs (x, T, in_trigger (T :: Ts) u) | (q as Const (\<^const_name>\Ex\, _), [Abs (x, T, u)]) => q $ Abs (x, T, in_trigger (T :: Ts) u) | (q as Const (\<^const_name>\Let\, _), [u1, u2 as Abs _]) => q $ traverse Ts u1 $ traverse Ts u2 | (u as Const (c as (_, T)), ts) => (case SMT_Builtin.dest_builtin ctxt c ts of SOME (_, k, us, mk) => let val (ts1, ts2) = chop k (map (traverse Ts) us) val U = Term.strip_type T |>> snd o chop k |> (op --->) in apply 0 (mk ts1) U ts2 end | NONE => app_func u T (map (traverse Ts) ts)) | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts | (u, ts) => traverses Ts u ts) and in_trigger Ts ((c as \<^Const_>\trigger\) $ p $ t) = c $ in_pats Ts p $ traverse Ts t | in_trigger Ts t = traverse Ts t and in_pats Ts ps = in_list \<^typ>\pattern symb_list\ (in_list \<^typ>\pattern\ (in_pat Ts)) ps and in_pat Ts ((p as \<^Const_>\pat _\) $ t) = p $ traverse Ts t | in_pat Ts ((p as \<^Const_>\nopat _\) $ t) = p $ traverse Ts t | in_pat _ t = raise TERM ("bad pattern", [t]) and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) in map (apsnd (traverse [])) ts end val fun_app_eq = mk_meta_eq @{thm fun_app_def} end (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) local val is_quant = member (op =) [\<^const_name>\All\, \<^const_name>\Ex\] val fol_rules = [ Let_def, @{lemma "P = True == P" by (rule eq_reflection) simp}] exception BAD_PATTERN of unit fun is_builtin_conn_or_pred ctxt c ts = is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse is_some (SMT_Builtin.dest_builtin_pred ctxt c ts) in fun folify ctxt = let fun in_list T f t = SMT_Util.mk_symb_list T (map_filter f (SMT_Util.dest_symb_list t)) fun in_term pat t = (case Term.strip_comb t of (\<^Const_>\True\, []) => t | (\<^Const_>\False\, []) => t | (u as \<^Const_>\If _\, [t1, t2, t3]) => if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 | (Const (c as (n, _)), ts) => if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then if pat then raise BAD_PATTERN () else in_form t else Term.list_comb (Const c, map (in_term pat) ts) | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) | _ => t) and in_pat ((p as Const (\<^const_name>\pat\, _)) $ t) = p $ in_term true t | in_pat ((p as Const (\<^const_name>\nopat\, _)) $ t) = p $ in_term true t | in_pat t = raise TERM ("bad pattern", [t]) and in_pats ps = in_list \<^typ>\pattern symb_list\ (SOME o in_list \<^typ>\pattern\ (try in_pat)) ps and in_trigger ((c as \<^Const_>\trigger\) $ p $ t) = c $ in_pats p $ in_form t | in_trigger t = in_form t and in_form t = (case Term.strip_comb t of (q as Const (qn, _), [Abs (n, T, u)]) => if is_quant qn then q $ Abs (n, T, in_trigger u) else in_term false t | (Const c, ts) => (case SMT_Builtin.dest_builtin_conn ctxt c ts of SOME (_, _, us, mk) => mk (map in_form us) | NONE => (case SMT_Builtin.dest_builtin_pred ctxt c ts of SOME (_, _, us, mk) => mk (map (in_term false) us) | NONE => in_term false t)) | _ => in_term false t) in map (apsnd in_form) #> pair (fol_rules, I) end end (* translation into intermediate format *) (** utility functions **) val quantifier = (fn \<^const_name>\All\ => SOME SForall | \<^const_name>\Ex\ => SOME SExists | _ => NONE) fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = if q = qname then group_quant qname (T :: Ts) u else (Ts, t) | group_quant _ Ts t = (Ts, t) fun dest_pat (Const (\<^const_name>\pat\, _) $ t) = (t, true) | dest_pat (Const (\<^const_name>\nopat\, _) $ t) = (t, false) | dest_pat t = raise TERM ("bad pattern", [t]) fun dest_pats [] = I | dest_pats ts = (case map dest_pat ts |> split_list ||> distinct (op =) of (ps, [true]) => cons (SPat ps) | (ps, [false]) => cons (SNoPat ps) | _ => raise TERM ("bad multi-pattern", ts)) fun dest_trigger \<^Const_>\trigger for tl t\ = (rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t) | dest_trigger t = ([], t) fun dest_quant qn T t = quantifier qn |> Option.map (fn q => let val (Ts, u) = group_quant qn [T] t val (ps, p) = dest_trigger u in (q, rev Ts, ps, p) end) fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat (** translation from Isabelle terms into SMT intermediate terms **) fun intermediate logic dtyps builtin ctxt ts trx = let fun transT (T as TFree _) = add_typ T true | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) | transT (T as Type _) = (case SMT_Builtin.dest_builtin_typ ctxt T of SOME (n, []) => pair n | SOME (n, Ts) => fold_map transT Ts #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns))) | NONE => add_typ T true) fun trans t = (case Term.strip_comb t of (Const (qn, _), [Abs (_, T, t1)]) => (case dest_quant qn T t1 of SOME (q, Ts, ps, b) => fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b')) | NONE => raise TERM ("unsupported quantifier", [t])) | (u as Const (c as (_, T)), ts) => (case builtin ctxt c ts of SOME (n, _, us, _) => fold_map trans us #>> curry SConst n | NONE => trans_applied_fun u T ts) | (u as Free (_, T), ts) => trans_applied_fun u T ts | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar | _ => raise TERM ("bad SMT term", [t])) and trans_applied_fun t T ts = let val (Us, U) = SMT_Util.dest_funT (length ts) T in fold_map transT Us ##>> transT U #-> (fn Up => add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst) end val (us, trx') = fold_map (fn (role, t) => apfst (pair role) o trans t) ts trx in ((sign_of (logic ts) dtyps trx', us), trx') end (* translation *) structure Configs = Generic_Data ( type T = (Proof.context -> config) SMT_Util.dict val empty = [] fun merge data = SMT_Util.dict_merge fst data ) fun add_config (cs, cfg) = Configs.map (SMT_Util.dict_update (cs, cfg)) fun get_config ctxt = let val cs = SMT_Config.solver_class_of ctxt in (case SMT_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of SOME cfg => cfg ctxt | NONE => error ("SMT: no translation configuration found " ^ "for solver class " ^ quote (SMT_Util.string_of_class cs))) end fun translate ctxt prover smt_options comments (ithms : ((int * SMT_Util.role) * thm) list) = let val {order, logic, fp_kinds, serialize} = get_config ctxt fun no_dtyps (tr_context, ctxt) ts = ((Termtab.empty, [], tr_context, ctxt), ts) val ts1 = map (SMT_Util.map_prod snd (Envir.beta_eta_contract o SMT_Util.prop_of)) ithms val ((funcs, dtyps, tr_context, ctxt1), ts2) = ((empty_tr_context, ctxt), ts1) |-> (if null fp_kinds then no_dtyps else collect_co_datatypes fp_kinds) fun is_binder (Const (\<^const_name>\Let\, _) $ _) = true | is_binder t = Lambda_Lifting.is_quantifier t fun mk_trigger ((q as Const (\<^const_name>\All\, _)) $ Abs (n, T, t)) = q $ Abs (n, T, mk_trigger t) | mk_trigger (eq as (Const (\<^const_name>\HOL.eq\, T) $ lhs $ _)) = Term.domain_type T --> \<^typ>\pattern\ |> (fn T => Const (\<^const_name>\pat\, T) $ lhs) |> SMT_Util.mk_symb_list \<^typ>\pattern\ o single |> SMT_Util.mk_symb_list \<^typ>\pattern symb_list\ o single |> (fn t => \<^Const>\trigger for t eq\) | mk_trigger t = t val (ctxt2, (ts3, ll_defs)) = ts2 |> eta_expand ctxt1 funcs |> rpair ctxt1 |-> Lambda_Lifting.lift_lambdas' NONE is_binder |-> (fn (ts', ll_defs) => fn ctxt' => let val ts'' = map (pair SMT_Util.Axiom o mk_trigger) ll_defs @ ts' |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs in (ctxt', (ts'', ll_defs)) end) val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq) in (ts4, tr_context) |-> intermediate (logic prover o map snd) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize smt_options comments) ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms end end; diff --git a/src/HOL/Tools/SMT/smtlib_interface.ML b/src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML +++ b/src/HOL/Tools/SMT/smtlib_interface.ML @@ -1,195 +1,195 @@ (* Title: HOL/Tools/SMT/smtlib_interface.ML Author: Sascha Boehme, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Interface to SMT solvers based on the SMT-LIB 2 format. *) signature SMTLIB_INTERFACE = sig val smtlibC: SMT_Util.class val hosmtlibC: SMT_Util.class val bvsmlibC: SMT_Util.class val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config val assert_name_of_role_and_index: SMT_Util.role -> int -> string val role_and_index_of_assert_name: string -> SMT_Util.role * int end; structure SMTLIB_Interface: SMTLIB_INTERFACE = struct val hoC = ["ho"] val smtlibC = ["smtlib"] (* SMT-LIB 2 *) val hosmtlibC = smtlibC @ hoC (* possibly SMT-LIB 3 *) val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *) (* builtins *) local fun int_num _ i = SOME (string_of_int i) fun is_linear [t] = SMT_Util.is_number t | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u | is_linear _ = false fun times _ _ ts = let val mk = Term.list_comb o pair \<^Const>\times \<^Type>\int\\ in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end in val setup_builtins = SMT_Builtin.add_builtin_typ hosmtlibC (\<^typ>\'a => 'b\, fn Type (\<^type_name>\fun\, Ts) => SOME ("->", Ts), K (K NONE)) #> fold (SMT_Builtin.add_builtin_typ smtlibC) [ (\<^typ>\bool\, K (SOME ("Bool", [])), K (K NONE)), (\<^typ>\int\, K (SOME ("Int", [])), int_num)] #> fold (SMT_Builtin.add_builtin_fun' smtlibC) [ (\<^Const>\True\, "true"), (\<^Const>\False\, "false"), (\<^Const>\Not\, "not"), (\<^Const>\conj\, "and"), (\<^Const>\disj\, "or"), (\<^Const>\implies\, "=>"), (\<^Const>\HOL.eq \<^typ>\'a\\, "="), (\<^Const>\If \<^typ>\'a\\, "ite"), (\<^Const>\less \<^Type>\int\\, "<"), (\<^Const>\less_eq \<^Type>\int\\, "<="), (\<^Const>\uminus \<^Type>\int\\, "-"), (\<^Const>\plus \<^Type>\int\\, "+"), (\<^Const>\minus \<^Type>\int\\, "-")] #> SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const \<^Const>\times \<^Type>\int\\, times) end (* serialization *) (** logic **) fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) structure Logics = Generic_Data ( type T = (int * (string -> term list -> string option)) list val empty = [] fun merge data = Ord_List.merge fst_int_ord data ) fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf) fun del_logic pf = Logics.map (Ord_List.remove fst_int_ord pf) fun choose_logic ctxt prover ts = let fun choose [] = "AUFLIA" | choose ((_, f) :: fs) = (case f prover ts of SOME s => s | NONE => choose fs) in (case choose (Logics.get (Context.Proof ctxt)) of "" => "" (* for default Z3 logic, a subset of everything *) | logic => "(set-logic " ^ logic ^ ")\n") end (** serialization **) fun var i = "?v" ^ string_of_int i fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1)) | tree_of_sterm l (SMT_Translate.SVar (i, ts)) = SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts) | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n | tree_of_sterm l (SMT_Translate.SConst (n, ts)) = SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts) | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) = let val l' = l + length ss fun quant_name SMT_Translate.SForall = "forall" | quant_name SMT_Translate.SExists = "exists" fun gen_trees_of_pat keyword ps = [SMTLIB.Key keyword, SMTLIB.S (map (tree_of_sterm l') ps)] fun trees_of_pat (SMT_Translate.SPat ps) = gen_trees_of_pat "pattern" ps | trees_of_pat (SMT_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps fun tree_of_pats [] t = t | tree_of_pats pats t = SMTLIB.S (SMTLIB.Sym "!" :: t :: maps trees_of_pat pats) val vs = map_index (fn (i, ty) => SMTLIB.S [SMTLIB.Sym (var (l + i)), SMTLIB.Sym ty]) ss val body = t |> tree_of_sterm l' |> tree_of_pats pats in SMTLIB.S [SMTLIB.Sym (quant_name q), SMTLIB.S vs, body] end fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")" fun sctr (name, args) = enclose "(" ")" (space_implode " " (name :: map sctrarg args)) fun sdatatype (name, ctrs) = enclose "(" ")" (space_implode " " (name :: map sctr ctrs)) fun string_of_fun (f, (ss, s)) = f ^ " (" ^ space_implode " " ss ^ ") " ^ s fun named_sterm s t = SMTLIB.S [SMTLIB.Sym "!", t, SMTLIB.Key "named", SMTLIB.Sym s] val conjecture_prefix = "conjecture" (* FUDGE *) val hypothesis_prefix = "hypothesis" (* FUDGE *) val axiom_prefix = "axiom" (* FUDGE *) fun assert_prefix_of_role SMT_Util.Conjecture = conjecture_prefix | assert_prefix_of_role SMT_Util.Hypothesis = hypothesis_prefix | assert_prefix_of_role SMT_Util.Axiom = axiom_prefix fun assert_name_of_role_and_index role i = assert_prefix_of_role role ^ string_of_int i fun unprefix_axiom s = try (pair SMT_Util.Conjecture o unprefix conjecture_prefix) s - |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix hypothesis_prefix) s) - |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix axiom_prefix) s) + |> curry merge_options (try (pair SMT_Util.Hypothesis o unprefix hypothesis_prefix) s) + |> curry merge_options (try (pair SMT_Util.Axiom o unprefix axiom_prefix) s) |> the fun role_and_index_of_assert_name s = apsnd (the_default ~1 o Int.fromString) (unprefix_axiom s) fun sdtyp (fp, dtyps) = Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n" (space_implode "\n " (map sdatatype dtyps))) fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts = let val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true") in Buffer.empty |> fold (Buffer.add o enclose "; " "\n") comments |> fold (fn (k, v) => Buffer.add ("(set-option " ^ k ^ " " ^ v ^ ")\n")) smt_options |> Buffer.add logic |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts) |> fold sdtyp (AList.coalesce (op =) dtyps) |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun) (sort (fast_string_ord o apply2 fst) funcs) |> fold (fn (i, (role, t)) => Buffer.add (enclose "(assert " ")\n" (SMTLIB.str_of (named_sterm (assert_name_of_role_and_index role i) (tree_of_sterm 0 t))))) (map_index I ts) |> Buffer.add "(check-sat)\n" |> Buffer.add (if unsat_core then "(get-unsat-core)\n" else "(get-proof)\n") |> Buffer.content end (* interface *) fun translate_config order ctxt = { order = order, logic = choose_logic ctxt, fp_kinds = [], serialize = serialize} val _ = Theory.setup (Context.theory_map (setup_builtins #> SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #> SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order))) end; diff --git a/src/HOL/Tools/SMT/verit_proof_parse.ML b/src/HOL/Tools/SMT/verit_proof_parse.ML --- a/src/HOL/Tools/SMT/verit_proof_parse.ML +++ b/src/HOL/Tools/SMT/verit_proof_parse.ML @@ -1,79 +1,80 @@ (* Title: HOL/Tools/SMT/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: SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> SMT_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 add_used_asserts_in_step (Verit_Proof.VeriT_Step {prems, ...}) = union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems) fun parse_proof ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) xfacts prems concl output = let val num_ll_defs = length ll_defs val id_of_index = Integer.add num_ll_defs val index_of_id = Integer.add (~ num_ll_defs) - fun step_of_assume j (_, th) = + fun step_of_assume j ((_, role), th) = Verit_Proof.VeriT_Step - {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), + {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j), rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []} val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt val used_assert_ids = fold add_used_asserts_in_step actual_steps [] val used_assm_js = map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end) used_assert_ids val used_assms = map (nth assms) used_assm_js val assm_steps = map2 step_of_assume used_assm_js used_assms val steps = assm_steps @ actual_steps val conjecture_i = 0 val prems_i = conjecture_i + 1 val num_prems = length prems val facts_i = prems_i + num_prems val num_facts = length xfacts val helpers_i = facts_i + num_facts val conjecture_id = id_of_index conjecture_i val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1) val fact_ids' = map_filter (fn j => - let val (i, _) = nth assms j in + let val ((i, _), _) = nth assms j in try (apsnd (nth xfacts)) (id_of_index j, i - facts_i) end) used_assm_js - val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms + val helper_ids' = + map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms val fact_helper_ts = map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ map (fn (_, ((s, _), th)) => (s, Thm.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 = SOME 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 --git a/src/HOL/Tools/SMT/verit_replay.ML b/src/HOL/Tools/SMT/verit_replay.ML --- a/src/HOL/Tools/SMT/verit_replay.ML +++ b/src/HOL/Tools/SMT/verit_replay.ML @@ -1,322 +1,322 @@ (* Title: HOL/Tools/SMT/verit_replay.ML Author: Mathias Fleury, MPII VeriT proof parsing and replay. *) signature VERIT_REPLAY = sig val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm end; structure Verit_Replay: VERIT_REPLAY = struct fun subst_only_free pairs = let fun substf u = (case Termtab.lookup pairs u of SOME u' => u' | NONE => (case u of (Abs(a,T,t)) => Abs(a, T, substf t) | (t$u') => substf t $ substf u' | u => u)) in substf end; fun under_fixes f unchanged_prems (prems, nthms) names args insts decls (concl, ctxt) = let val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("names =", names)) val thms2 = map snd nthms val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("prems=", prems)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("nthms=", nthms)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms1=", thms1)) val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms2=", thms2)) in (f ctxt (thms1 @ thms2) args insts decls concl) end (** Replaying **) fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms concl_transformation global_transformation args insts (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, declarations = decls, ...}) = let val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> id) val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs end val rewrite_concl = if Verit_Proof.keep_app_symbols rule then filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules else rewrite_rules val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_concl [] #> Object_Logic.atomize_term ctxt #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs #> SMTLIB_Isar.unskolemize_names ctxt #> HOLogic.mk_Trueprop end val concl = concl |> Term.subst_free concl_transformation |> subst_only_free global_transformation |> post in if rule = Verit_Proof.input_rule then (case Symtab.lookup assumed id of SOME (_, thm) => thm | _ => raise Fail ("assumption " ^ @{make_string} id ^ " not found")) else under_fixes (method_for rule) unchanged_prems (prems, nthms) (map fst bounds) (map rewrite args) (Symtab.map (K rewrite) insts) decls (concl, ctxt) |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules) end fun add_used_asserts_in_step (Verit_Proof.VeriT_Replay_Node {prems, subproof = (_, _, _, subproof), ...}) = union (op =) (map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) prems @ flat (map (fn x => add_used_asserts_in_step x []) subproof)) fun remove_rewrite_rules_from_rules n = (fn (step as Verit_Proof.VeriT_Replay_Node {id, ...}) => (case try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id of NONE => SOME step | SOME a => if a < n then NONE else SOME step)) fun replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems (step as Verit_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args, insts, subproof = (fixes, assms, input, subproof), concl, ...}) state = let val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt |> (fn (names, ctxt) => (names, fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt)) val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt ||> fold Variable.declare_term (map Free fixes) val export_vars = concl_tranformation @ (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes)))) val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy ((if Verit_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) [] #> Object_Logic.atomize_term ctxt #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs #> SMTLIB_Isar.unskolemize_names ctxt #> HOLogic.mk_Trueprop end val assms = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) assms val input = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) input val (all_proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) (assms @ input)) sub_ctxt fun is_refl thm = Thm.concl_of thm |> (fn (_ $ t) => t) |> HOLogic.dest_eq |> (op =) handle TERM _=> false val all_proof_prems' = all_proof_prems' |> filter_out is_refl val proof_prems' = take (length assms) all_proof_prems' val input = drop (length assms) all_proof_prems' val all_proof_prems = proof_prems @ proof_prems' val replay = replay_theorem_step rewrite_rules ll_defs assumed (input @ inputs) all_proof_prems val (proofs', stats, _, _, sub_global_rew) = fold replay subproof (proofs, stats, sub_ctxt2, export_vars, global_transformation) val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt) (*for sko_ex and sko_forall, assumptions are in proofs', but the definition of the skolem function is in proofs *) val nthms = prems |> map (apsnd export_thm) o map_filter (Symtab.lookup (if (null subproof) then proofs else proofs')) val nthms' = (if Verit_Proof.is_skolemization rule then prems else []) |> map_filter (Symtab.lookup proofs) val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts val proof_prems = if Lethe_Replay_Methods.requires_subproof_assms prems rule then proof_prems else [] val local_inputs = if Lethe_Replay_Methods.requires_local_input prems rule then input @ inputs else [] val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs ctxt assumed [] (proof_prems @ local_inputs) (nthms @ nthms') concl_tranformation global_transformation args insts) val ({elapsed, ...}, thm) = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out val stats' = Symtab.cons_list (rule, Time.toNanoseconds elapsed) stats (* val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed) ^ " " ^ @{make_string} (proof_prems @ local_inputs)) val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) ( (proof_prems @ local_inputs)) val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print}) thm val _ = ((Time.toMilliseconds elapsed > 40) ? @{print}) ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed)) *) val proofs = Symtab.update (id, (map fst bounds, thm)) proofs in (proofs, stats', ctxt, concl_tranformation, sub_global_rew) end fun replay_definition_step rewrite_rules ll_defs _ _ _ (Verit_Proof.VeriT_Replay_Node {id, declarations = raw_declarations, subproof = (_, _, _, subproof), ...}) state = let val _ = if null subproof then () else raise (Fail ("unrecognized veriT proof, definition has a subproof")) val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state val global_transformer = subst_only_free global_transformation val rewrite = let val thy = Proof_Context.theory_of ctxt in Raw_Simplifier.rewrite_term thy (rewrite_rules) [] #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs end val start0 = Timing.start () val declaration = map (apsnd (rewrite o global_transformer)) raw_declarations val (names, ctxt) = Variable.variant_fixes (map fst declaration) ctxt ||> fold Variable.declare_term (map Free (map (apsnd fastype_of) declaration)) val old_names = map Free (map (fn (a, b) => (a, fastype_of b)) declaration) val new_names = map Free (ListPair.zip (names, map (fastype_of o snd) declaration)) fun update_mapping (a, b) tab = if a <> b andalso Termtab.lookup tab a = NONE then Termtab.update_new (a, b) tab else tab val global_transformation = global_transformation |> fold update_mapping (ListPair.zip (old_names, new_names)) val global_transformer = subst_only_free global_transformation val generate_definition = (fn (name, term) => (HOLogic.mk_Trueprop (Const(\<^const_name>\HOL.eq\, fastype_of term --> fastype_of term --> @{typ bool}) $ Free (name, fastype_of term) $ term))) #> global_transformer #> Thm.cterm_of ctxt val decls = map generate_definition declaration val (defs, ctxt) = Assumption.add_assumes decls ctxt val thms_with_old_name = ListPair.zip (map fst declaration, defs) val proofs = fold (fn (name, thm) => Symtab.update (id, ([name], @{thm sym} OF [thm]))) thms_with_old_name proofs val total = Time.toNanoseconds (#elapsed (Timing.result start0)) val stats = Symtab.cons_list ("choice", total) stats in (proofs, stats, ctxt, concl_tranformation, global_transformation) end fun replay_assumed assms ll_defs rewrite_rules stats ctxt term = let val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs end val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term)) val ({elapsed, ...}, thm) = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt) handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out val stats' = Symtab.cons_list (Verit_Proof.input_rule, Time.toNanoseconds elapsed) stats in (thm, stats') end fun replay_step rewrite_rules ll_defs assumed inputs proof_prems (step as Verit_Proof.VeriT_Replay_Node {rule, ...}) state = if rule = Verit_Proof.veriT_def then replay_definition_step rewrite_rules ll_defs assumed inputs proof_prems step state else replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems step state fun replay outer_ctxt ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data) output = let val rewrite_rules = filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify}, Thm.prop_of thm)) rewrite_rules val num_ll_defs = length ll_defs val index_of_id = Integer.add (~ num_ll_defs) val id_of_index = Integer.add num_ll_defs val start0 = Timing.start () val (actual_steps, ctxt2) = Verit_Proof.parse_replay typs terms output ctxt val parsing_time = Time.toNanoseconds (#elapsed (Timing.result start0)) fun step_of_assume (j, (_, th)) = Verit_Proof.VeriT_Replay_Node { id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j), rule = Verit_Proof.input_rule, args = [], prems = [], proof_ctxt = [], concl = Thm.prop_of th |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [], bounds = [], insts = Symtab.empty, declarations = [], subproof = ([], [], [], [])} val used_assert_ids = fold add_used_asserts_in_step actual_steps [] fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in Raw_Simplifier.rewrite_term thy rewrite_rules [] end val used_assm_js = map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i) else NONE end) used_assert_ids val assm_steps = map step_of_assume used_assm_js fun extract (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) = (id, rule, concl, map fst bounds) fun cond rule = rule = Verit_Proof.input_rule val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond val ((_, _), (ctxt3, assumed)) = - add_asssert outer_ctxt rewrite_rules assms + add_asssert outer_ctxt rewrite_rules (map (apfst fst) assms) (map_filter (remove_rewrite_rules_from_rules num_ll_defs) assm_steps) ctxt2 val used_rew_js = map_filter (fn id => let val i = index_of_id id in if i < 0 then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end) used_assert_ids val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) => let val (thm, stats) = replay_assumed assms ll_defs rewrite_rules stats ctxt thm val name = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom id in (Symtab.update (name, ([], thm)) assumed, stats) end) used_rew_js (assumed, Symtab.cons_list ("parsing", parsing_time) Symtab.empty) val ctxt4 = ctxt3 |> put_simpset (SMT_Replay.make_simpset ctxt3 []) |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver) val len = Verit_Proof.number_of_steps actual_steps fun steps_with_depth _ [] = [] | steps_with_depth i (p :: ps) = (i + Verit_Proof.number_of_steps [p], p) :: steps_with_depth (i + Verit_Proof.number_of_steps [p]) ps val actual_steps = steps_with_depth 0 actual_steps val start = Timing.start () val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len fun blockwise f (i, x) (next, y) = (if i > next then print_runtime_statistics i else (); (if i > next then i + 10 else next, f x y)) val global_transformation : term Termtab.table = Termtab.empty val (_, (proofs, stats, ctxt5, _, _)) = fold (blockwise (replay_step rewrite_rules ll_defs assumed [] [])) actual_steps (1, (assumed, stats, ctxt4, [], global_transformation)) val total = Time.toMilliseconds (#elapsed (Timing.result start)) val (_, (_, Verit_Proof.VeriT_Replay_Node {id, ...})) = split_last actual_steps val _ = print_runtime_statistics len val thm_with_defs = Symtab.lookup proofs id |> the |> snd |> singleton (Proof_Context.export ctxt5 outer_ctxt) val _ = SMT_Config.statistics_msg ctxt5 (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats val _ = SMT_Replay.spying (SMT_Config.spy_verit ctxt) ctxt (fn () => SMT_Replay.print_stats (Symtab.dest stats)) "spy_verit" in Verit_Replay_Methods.discharge ctxt [thm_with_defs] @{term False} end end diff --git a/src/HOL/Tools/SMT/z3_replay.ML b/src/HOL/Tools/SMT/z3_replay.ML --- a/src/HOL/Tools/SMT/z3_replay.ML +++ b/src/HOL/Tools/SMT/z3_replay.ML @@ -1,176 +1,176 @@ (* Title: HOL/Tools/SMT/z3_replay.ML Author: Sascha Boehme, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Z3 proof parsing and replay. *) signature Z3_REPLAY = sig val parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> SMT_Solver.parsed_proof val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm end; structure Z3_Replay: Z3_REPLAY = struct local fun extract (Z3_Proof.Z3_Step {id, rule, concl, fixes, ...}) = (id, rule, concl, fixes) fun cond rule = Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis in val add_asserted = SMT_Replay.add_asserted Inttab.update Inttab.empty extract cond end fun add_paramTs names t = fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (SMT_Replay.params_of t) fun new_fixes ctxt nTs = let val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt fun mk (n, T) n' = (n, Thm.cterm_of ctxt' (Free (n', T))) in (ctxt', Symtab.make (map2 mk nTs ns)) end fun forall_elim_term ct (Const (\<^const_name>\Pure.all\, _) $ (a as Abs _)) = Term.betapply (a, Thm.term_of ct) | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt]) fun apply_fixes elim env = fold (elim o the o Symtab.lookup env) val apply_fixes_prem = uncurry o apply_fixes Thm.forall_elim val apply_fixes_concl = apply_fixes forall_elim_term fun export_fixes env names = Drule.forall_intr_list (map (the o Symtab.lookup env) names) fun under_fixes f ctxt (prems, nthms) names concl = let val thms1 = map (SMT_Replay.varify ctxt) prems val (ctxt', env) = add_paramTs names concl [] |> fold (uncurry add_paramTs o apsnd Thm.prop_of) nthms |> new_fixes ctxt val thms2 = map (apply_fixes_prem env) nthms val t = apply_fixes_concl env names concl in export_fixes env names (f ctxt' (thms1 @ thms2) t) end fun replay_thm ctxt assumed nthms (Z3_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) = if Z3_Proof.is_assumption rule then (case Inttab.lookup assumed id of SOME (_, thm) => thm | NONE => Thm.assume (Thm.cterm_of ctxt concl)) else under_fixes (Z3_Replay_Methods.method_for rule) ctxt (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl fun replay_step ctxt assumed (step as Z3_Proof.Z3_Step {id, rule, prems, fixes, ...}) state = let val (proofs, stats) = state val nthms = map (the o Inttab.lookup proofs) prems val replay = Timing.timing (replay_thm ctxt assumed nthms) val ({elapsed, ...}, thm) = SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats in (Inttab.update (id, (fixes, thm)) proofs, stats') end (* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *) local val sk_rules = @{lemma "c = (SOME x. P x) \ (\x. P x) = P c" "c = (SOME x. \ P x) \ (\ (\x. P x)) = (\ P c)" by (metis someI_ex)+} in fun discharge_sk_tac ctxt i st = (resolve_tac ctxt @{thms trans} i THEN resolve_tac ctxt sk_rules i THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1) THEN resolve_tac ctxt @{thms refl} i) st end val true_thm = @{lemma "\False" by simp} fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, @{thm reflexive}, true_thm] val intro_def_rules = @{lemma "(\ P \ P) \ (P \ \ P)" "(P \ \ P) \ (\ P \ P)" by fast+} fun discharge_assms_tac ctxt rules = REPEAT (HEADGOAL (resolve_tac ctxt (intro_def_rules @ rules) ORELSE' SOLVED' (discharge_sk_tac ctxt))) fun discharge_assms ctxt rules thm = (if Thm.nprems_of thm = 0 then thm else (case Seq.pull (discharge_assms_tac ctxt rules thm) of SOME (thm', _) => thm' | NONE => raise THM ("failed to discharge premise", 1, [thm]))) |> Goal.norm_result ctxt fun discharge rules outer_ctxt inner_ctxt = singleton (Proof_Context.export inner_ctxt outer_ctxt) #> discharge_assms outer_ctxt (make_discharge_rules rules) fun parse_proof outer_ctxt ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data) xfacts prems concl output = let val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt - val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 + val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2 fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i)) val conjecture_i = 0 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 fact_ids' = map_filter (fn (i, (id, _)) => try (apsnd (nth xfacts)) (id, i - facts_i)) iidths val helper_ids' = map_filter (try (fn (~1, idth) => idth)) iidths val fact_helper_ts = map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @ map (fn (_, ((s, _), th)) => (s, Thm.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 = SOME fact_ids', atp_proof = fn () => Z3_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps} end fun replay outer_ctxt ({context = ctxt, typs, terms, rewrite_rules, assms, ...} : SMT_Translate.replay_data) output = let val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt val ((_, rules), (ctxt3, assumed)) = - add_asserted outer_ctxt rewrite_rules assms steps ctxt2 + add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2 val ctxt4 = ctxt3 |> put_simpset (SMT_Replay.make_simpset ctxt3 []) |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver) val len = length steps val start = Timing.start () val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len fun blockwise f (i, x) y = (if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y) val (proofs, stats) = fold_index (blockwise (replay_step ctxt4 assumed)) steps (assumed, Symtab.empty) val _ = print_runtime_statistics len val total = Time.toMilliseconds (#elapsed (Timing.result start)) val (_, Z3_Proof.Z3_Step {id, ...}) = split_last steps val _ = SMT_Config.statistics_msg ctxt4 (Pretty.string_of o SMT_Replay.pretty_statistics "Z3" total) stats in Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4 end end;