# HG changeset patch # User blanchet # Date 1394713093 -3600 # Node ID 624faeda77b5679ca7cd77b1287d4b317a2ac720 # Parent d397030fb27e69c3ee927835f74a07cf82334e11 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle diff -r d397030fb27e -r 624faeda77b5 src/HOL/Real.thy --- a/src/HOL/Real.thy Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Real.thy Thu Mar 13 13:18:13 2014 +0100 @@ -2197,7 +2197,20 @@ times_real_inst.times_real uminus_real_inst.uminus_real zero_real_inst.zero_real + +subsection {* Setup for SMT *} + ML_file "Tools/SMT/smt_real.ML" setup SMT_Real.setup +ML_file "Tools/SMT2/smt2_real.ML" +ML_file "Tools/SMT2/z3_new_real.ML" + +lemma [z3_new_rule]: + "0 + (x::real) = x" + "x + 0 = x" + "0 * x = 0" + "1 * x = x" + "x + y = y + x" + by auto end diff -r d397030fb27e -r 624faeda77b5 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/SMT.thy Thu Mar 13 13:18:13 2014 +0100 @@ -31,14 +31,13 @@ quantifier block. *} -datatype pattern = Pattern +typedecl pattern -definition pat :: "'a \ pattern" where "pat _ = Pattern" -definition nopat :: "'a \ pattern" where "nopat _ = Pattern" +consts + pat :: "'a \ pattern" + nopat :: "'a \ pattern" -definition trigger :: "pattern list list \ bool \ bool" -where "trigger _ P = P" - +definition trigger :: "pattern list list \ bool \ bool" where "trigger _ P = P" subsection {* Quantifier weights *} @@ -67,7 +66,6 @@ *} - subsection {* Higher-order encoding *} text {* @@ -88,7 +86,6 @@ fun_upd_upd fun_app_def - subsection {* First-order logic *} text {* @@ -107,7 +104,6 @@ definition term_false where "term_false = False" - subsection {* Integer division and modulo for Z3 *} definition z3div :: "int \ int \ int" where @@ -117,7 +113,6 @@ "z3mod k l = (if 0 \ l then k mod l else k mod (-l))" - subsection {* Setup *} ML_file "Tools/SMT/smt_builtin.ML" @@ -426,7 +421,7 @@ hide_type (open) pattern -hide_const Pattern fun_app term_true term_false z3div z3mod +hide_const fun_app term_true term_false z3div z3mod hide_const (open) trigger pat nopat weight end diff -r d397030fb27e -r 624faeda77b5 src/HOL/SMT2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SMT2.thy Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,398 @@ +(* Title: HOL/SMT2.thy + Author: Sascha Boehme, TU Muenchen +*) + +header {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *} + +theory SMT2 +imports Record +keywords "smt2_status" :: diag +begin + +ML_file "Tools/SMT2/smt2_utils.ML" +ML_file "Tools/SMT2/smt2_failure.ML" +ML_file "Tools/SMT2/smt2_config.ML" + + +subsection {* Triggers for quantifier instantiation *} + +text {* +Some SMT solvers support patterns as a quantifier instantiation +heuristics. Patterns may either be positive terms (tagged by "pat") +triggering quantifier instantiations -- when the solver finds a +term matching a positive pattern, it instantiates the corresponding +quantifier accordingly -- or negative terms (tagged by "nopat") +inhibiting quantifier instantiations. A list of patterns +of the same kind is called a multipattern, and all patterns in a +multipattern are considered conjunctively for quantifier instantiation. +A list of multipatterns is called a trigger, and their multipatterns +act disjunctively during quantifier instantiation. Each multipattern +should mention at least all quantified variables of the preceding +quantifier block. +*} + +typedecl pattern + +consts + pat :: "'a \ pattern" + nopat :: "'a \ pattern" + +definition trigger :: "pattern list list \ bool \ bool" where "trigger _ P = P" + + +subsection {* Quantifier weights *} + +text {* +Weight annotations to quantifiers influence the priority of quantifier +instantiations. They should be handled with care for solvers, which support +them, because incorrect choices of weights might render a problem unsolvable. +*} + +definition weight :: "int \ bool \ bool" where "weight _ P = P" + +text {* +Weights must be non-negative. The value @{text 0} is equivalent to providing +no weight at all. + +Weights should only be used at quantifiers and only inside triggers (if the +quantifier has triggers). Valid usages of weights are as follows: + +\begin{itemize} +\item +@{term "\x. trigger [[pat (P x)]] (weight 2 (P x))"} +\item +@{term "\x. weight 3 (P x)"} +\end{itemize} +*} + + +subsection {* Higher-order encoding *} + +text {* +Application is made explicit for constants occurring with varying +numbers of arguments. This is achieved by the introduction of the +following constant. +*} + +definition fun_app :: "'a \ 'a" where "fun_app f = f" + +text {* +Some solvers support a theory of arrays which can be used to encode +higher-order functions. The following set of lemmas specifies the +properties of such (extensional) arrays. +*} + +lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def + + +subsection {* Integer division and modulo for Z3 *} + +definition z3div :: "int \ int \ int" where + "z3div k l = (if 0 \ l then k div l else -(k div (-l)))" + +definition z3mod :: "int \ int \ int" where + "z3mod k l = (if 0 \ l then k mod l else k mod (-l))" + + +subsection {* Setup *} + +ML_file "Tools/SMT2/smt2_builtin.ML" +ML_file "Tools/SMT2/smt2_datatypes.ML" +ML_file "Tools/SMT2/smt2_normalize.ML" +ML_file "Tools/SMT2/smt2_translate.ML" +ML_file "Tools/SMT2/smt2_solver.ML" +ML_file "Tools/SMT2/smtlib2.ML" +ML_file "Tools/SMT2/smtlib2_interface.ML" +ML_file "Tools/SMT2/z3_new_interface.ML" +ML_file "Tools/SMT2/z3_new_proof.ML" +ML_file "Tools/SMT2/z3_new_proof_tools.ML" +ML_file "Tools/SMT2/z3_new_proof_literals.ML" +ML_file "Tools/SMT2/z3_new_proof_rules.ML" +ML_file "Tools/SMT2/z3_new_proof_methods.ML" +ML_file "Tools/SMT2/z3_new_proof_replay.ML" +ML_file "Tools/SMT2/z3_new_isar.ML" +ML_file "Tools/SMT2/smt2_setup_solvers.ML" + +method_setup smt2 = {* + Scan.optional Attrib.thms [] >> + (fn thms => fn ctxt => + METHOD (fn facts => HEADGOAL (SMT2_Solver.smt2_tac ctxt (thms @ facts)))) +*} "apply an SMT solver to the current goal (based on SMT-LIB 2)" + + +subsection {* Configuration *} + +text {* +The current configuration can be printed by the command +@{text smt2_status}, which shows the values of most options. +*} + + + +subsection {* General configuration options *} + +text {* +The option @{text smt2_solver} can be used to change the target SMT +solver. The possible values can be obtained from the @{text smt2_status} +command. + +Due to licensing restrictions, Yices and Z3 are not installed/enabled +by default. Z3 is free for non-commercial applications and can be enabled +by setting Isabelle system option @{text z3_non_commercial} to @{text yes}. +*} + +declare [[ smt2_solver = z3_new ]] + +text {* +Since SMT solvers are potentially non-terminating, there is a timeout +(given in seconds) to restrict their runtime. A value greater than +120 (seconds) is in most cases not advisable. +*} + +declare [[ smt2_timeout = 20 ]] + +text {* +SMT solvers apply randomized heuristics. In case a problem is not +solvable by an SMT solver, changing the following option might help. +*} + +declare [[ smt2_random_seed = 1 ]] + +text {* +In general, the binding to SMT solvers runs as an oracle, i.e, the SMT +solvers are fully trusted without additional checks. The following +option can cause the SMT solver to run in proof-producing mode, giving +a checkable certificate. This is currently only implemented for Z3. +*} + +declare [[ smt2_oracle = false ]] + +text {* +Each SMT solver provides several commandline options to tweak its +behaviour. They can be passed to the solver by setting the following +options. +*} + +(* declare [[ cvc3_options = "" ]] TODO *) +(* declare [[ yices_options = "" ]] TODO *) +(* declare [[ z3_options = "" ]] TODO *) + +text {* +The SMT method provides an inference mechanism to detect simple triggers +in quantified formulas, which might increase the number of problems +solvable by SMT solvers (note: triggers guide quantifier instantiations +in the SMT solver). To turn it on, set the following option. +*} + +declare [[ smt2_infer_triggers = false ]] + +text {* +Enable the following option to use built-in support for div/mod, datatypes, +and records in Z3. Currently, this is implemented only in oracle mode. +*} + +declare [[ z3_new_extensions = false ]] + +text {* +The SMT method monomorphizes the given facts, that is, it tries to +instantiate all schematic type variables with fixed types occurring +in the problem. This is a (possibly nonterminating) fixed-point +construction whose cycles are limited by the following option. +*} + +declare [[ monomorph_max_rounds = 5 ]] + +text {* +In addition, the number of generated monomorphic instances is limited +by the following option. +*} + +declare [[ monomorph_max_new_instances = 500 ]] + + + +subsection {* Certificates *} + +text {* +By setting the option @{text smt2_certificates} to the name of a file, +all following applications of an SMT solver a cached in that file. +Any further application of the same SMT solver (using the very same +configuration) re-uses the cached certificate instead of invoking the +solver. An empty string disables caching certificates. + +The filename should be given as an explicit path. It is good +practice to use the name of the current theory (with ending +@{text ".certs"} instead of @{text ".thy"}) as the certificates file. +Certificate files should be used at most once in a certain theory context, +to avoid race conditions with other concurrent accesses. +*} + +declare [[ smt2_certificates = "" ]] + +text {* +The option @{text smt2_read_only_certificates} controls whether only +stored certificates are should be used or invocation of an SMT solver +is allowed. When set to @{text true}, no SMT solver will ever be +invoked and only the existing certificates found in the configured +cache are used; when set to @{text false} and there is no cached +certificate for some proposition, then the configured SMT solver is +invoked. +*} + +declare [[ smt2_read_only_certificates = false ]] + + + +subsection {* Tracing *} + +text {* +The SMT method, when applied, traces important information. To +make it entirely silent, set the following option to @{text false}. +*} + +declare [[ smt2_verbose = true ]] + +text {* +For tracing the generated problem file given to the SMT solver as +well as the returned result of the solver, the option +@{text smt2_trace} should be set to @{text true}. +*} + +declare [[ smt2_trace = false ]] + +text {* +From the set of assumptions given to the SMT solver, those assumptions +used in the proof are traced when the following option is set to +@{term true}. This only works for Z3 when it runs in non-oracle mode +(see options @{text smt2_solver} and @{text smt2_oracle} above). +*} + +declare [[ smt2_trace_used_facts = false ]] + + +subsection {* Schematic rules for Z3 proof reconstruction *} + +text {* +Several prof rules of Z3 are not very well documented. There are two +lemma groups which can turn failing Z3 proof reconstruction attempts +into succeeding ones: the facts in @{text z3_rule} are tried prior to +any implemented reconstruction procedure for all uncertain Z3 proof +rules; the facts in @{text z3_simp} are only fed to invocations of +the simplifier when reconstructing theory-specific proof steps. +*} + +lemmas [z3_new_rule] = + refl eq_commute conj_commute disj_commute simp_thms nnf_simps + ring_distribs field_simps times_divide_eq_right times_divide_eq_left + if_True if_False not_not + +lemma [z3_new_rule]: + "(P \ Q) = (\(\P \ \Q))" + "(P \ Q) = (\(\Q \ \P))" + "(\P \ Q) = (\(P \ \Q))" + "(\P \ Q) = (\(\Q \ P))" + "(P \ \Q) = (\(\P \ Q))" + "(P \ \Q) = (\(Q \ \P))" + "(\P \ \Q) = (\(P \ Q))" + "(\P \ \Q) = (\(Q \ P))" + by auto + +lemma [z3_new_rule]: + "(P \ Q) = (Q \ \P)" + "(\P \ Q) = (P \ Q)" + "(\P \ Q) = (Q \ P)" + "(True \ P) = P" + "(P \ True) = True" + "(False \ P) = True" + "(P \ P) = True" + by auto + +lemma [z3_new_rule]: + "((P = Q) \ R) = (R | (Q = (\P)))" + by auto + +lemma [z3_new_rule]: + "(\True) = False" + "(\False) = True" + "(x = x) = True" + "(P = True) = P" + "(True = P) = P" + "(P = False) = (\P)" + "(False = P) = (\P)" + "((\P) = P) = False" + "(P = (\P)) = False" + "((\P) = (\Q)) = (P = Q)" + "\(P = (\Q)) = (P = Q)" + "\((\P) = Q) = (P = Q)" + "(P \ Q) = (Q = (\P))" + "(P = Q) = ((\P \ Q) \ (P \ \Q))" + "(P \ Q) = ((\P \ \Q) \ (P \ Q))" + by auto + +lemma [z3_new_rule]: + "(if P then P else \P) = True" + "(if \P then \P else P) = True" + "(if P then True else False) = P" + "(if P then False else True) = (\P)" + "(if P then Q else True) = ((\P) \ Q)" + "(if P then Q else True) = (Q \ (\P))" + "(if P then Q else \Q) = (P = Q)" + "(if P then Q else \Q) = (Q = P)" + "(if P then \Q else Q) = (P = (\Q))" + "(if P then \Q else Q) = ((\Q) = P)" + "(if \P then x else y) = (if P then y else x)" + "(if P then (if Q then x else y) else x) = (if P \ (\Q) then y else x)" + "(if P then (if Q then x else y) else x) = (if (\Q) \ P then y else x)" + "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" + "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" + "(if P then x else if P then y else z) = (if P then x else z)" + "(if P then x else if Q then x else y) = (if P \ Q then x else y)" + "(if P then x else if Q then x else y) = (if Q \ P then x else y)" + "(if P then x = y else x = z) = (x = (if P then y else z))" + "(if P then x = y else y = z) = (y = (if P then x else z))" + "(if P then x = y else z = y) = (y = (if P then x else z))" + by auto + +lemma [z3_new_rule]: + "0 + (x::int) = x" + "x + 0 = x" + "x + x = 2 * x" + "0 * x = 0" + "1 * x = x" + "x + y = y + x" + by auto + +lemma [z3_new_rule]: (* for def-axiom *) + "P = Q \ P \ Q" + "P = Q \ \P \ \Q" + "(\P) = Q \ \P \ Q" + "(\P) = Q \ P \ \Q" + "P = (\Q) \ \P \ Q" + "P = (\Q) \ P \ \Q" + "P \ Q \ P \ \Q" + "P \ Q \ \P \ Q" + "P \ (\Q) \ P \ Q" + "(\P) \ Q \ P \ Q" + "P \ Q \ P \ (\Q)" + "P \ Q \ (\P) \ Q" + "P \ \Q \ P \ Q" + "\P \ Q \ P \ Q" + "P \ y = (if P then x else y)" + "P \ (if P then x else y) = y" + "\P \ x = (if P then x else y)" + "\P \ (if P then x else y) = x" + "P \ R \ \(if P then Q else R)" + "\P \ Q \ \(if P then Q else R)" + "\(if P then Q else R) \ \P \ Q" + "\(if P then Q else R) \ P \ R" + "(if P then Q else R) \ \P \ \Q" + "(if P then Q else R) \ P \ \R" + "(if P then \Q else R) \ \P \ Q" + "(if P then Q else \R) \ P \ R" + by auto + +hide_type (open) pattern +hide_const fun_app z3div z3mod +hide_const (open) trigger pat nopat weight + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Mar 13 13:18:13 2014 +0100 @@ -7,7 +7,7 @@ header {* Sledgehammer: Isabelle--ATP Linkup *} theory Sledgehammer -imports ATP SMT +imports ATP SMT SMT2 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl begin diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_builtin.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_builtin.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,231 @@ +(* Title: HOL/Tools/SMT2/smt2_builtin.ML + Author: Sascha Boehme, TU Muenchen + +Tables of types and terms directly supported by SMT solvers. +*) + +signature SMT2_BUILTIN = +sig + (*for experiments*) + val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context + + (*built-in types*) + val add_builtin_typ: SMT2_Utils.class -> + typ * (typ -> string option) * (typ -> int -> string option) -> + Context.generic -> Context.generic + val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic -> + Context.generic + val dest_builtin_typ: Proof.context -> typ -> string option + val is_builtin_typ_ext: Proof.context -> typ -> bool + + (*built-in numbers*) + val dest_builtin_num: Proof.context -> term -> (string * typ) option + val is_builtin_num: Proof.context -> term -> bool + val is_builtin_num_ext: Proof.context -> term -> bool + + (*built-in functions*) + type 'a bfun = Proof.context -> typ -> term list -> 'a + type bfunr = string * int * term list * (term list -> term) + val add_builtin_fun: SMT2_Utils.class -> + (string * typ) * bfunr option bfun -> Context.generic -> Context.generic + val add_builtin_fun': SMT2_Utils.class -> term * string -> Context.generic -> + Context.generic + val add_builtin_fun_ext: (string * typ) * term list bfun -> + Context.generic -> Context.generic + val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic + val add_builtin_fun_ext'': string -> Context.generic -> Context.generic + val dest_builtin_fun: Proof.context -> string * typ -> term list -> + bfunr option + val dest_builtin_eq: Proof.context -> term -> term -> bfunr option + val dest_builtin_pred: Proof.context -> string * typ -> term list -> + bfunr option + val dest_builtin_conn: Proof.context -> string * typ -> term list -> + bfunr option + val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option + val dest_builtin_ext: Proof.context -> string * typ -> term list -> + term list option + val is_builtin_fun: Proof.context -> string * typ -> term list -> bool + val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool +end + +structure SMT2_Builtin: SMT2_BUILTIN = +struct + + +(* built-in tables *) + +datatype ('a, 'b) kind = Ext of 'a | Int of 'b + +type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Utils.dict + +fun typ_ord ((T, _), (U, _)) = + let + fun tord (TVar _, Type _) = GREATER + | tord (Type _, TVar _) = LESS + | tord (Type (n, Ts), Type (m, Us)) = + if n = m then list_ord tord (Ts, Us) + else Term_Ord.typ_ord (T, U) + | tord TU = Term_Ord.typ_ord TU + in tord (T, U) end + +fun insert_ttab cs T f = + SMT2_Utils.dict_map_default (cs, []) + (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) + +fun merge_ttab ttabp = + SMT2_Utils.dict_merge (Ord_List.merge typ_ord) ttabp + +fun lookup_ttab ctxt ttab T = + let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U) + in + get_first (find_first match) + (SMT2_Utils.dict_lookup ttab (SMT2_Config.solver_class_of ctxt)) + end + +type ('a, 'b) btab = ('a, 'b) ttab Symtab.table + +fun insert_btab cs n T f = + Symtab.map_default (n, []) (insert_ttab cs T f) + +fun merge_btab btabp = Symtab.join (K merge_ttab) btabp + +fun lookup_btab ctxt btab (n, T) = + (case Symtab.lookup btab n of + NONE => NONE + | SOME ttab => lookup_ttab ctxt ttab T) + +type 'a bfun = Proof.context -> typ -> term list -> 'a + +type bfunr = string * int * term list * (term list -> term) + +structure Builtins = Generic_Data +( + type T = + (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab * + (term list bfun, bfunr option bfun) btab + val empty = ([], Symtab.empty) + val extend = I + fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2)) +) + +fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst))) + +fun filter_builtins keep_T = + Context.proof_map (Builtins.map (fn (ttab, btab) => + (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab))) + + +(* built-in types *) + +fun add_builtin_typ cs (T, f, g) = + Builtins.map (apfst (insert_ttab cs T (Int (f, g)))) + +fun add_builtin_typ_ext (T, f) = + Builtins.map (apfst (insert_ttab SMT2_Utils.basicC T (Ext f))) + +fun lookup_builtin_typ ctxt = + lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt))) + +fun dest_builtin_typ ctxt T = + (case lookup_builtin_typ ctxt T of + SOME (_, Int (f, _)) => f T + | _ => NONE) + +fun is_builtin_typ_ext ctxt T = + (case lookup_builtin_typ ctxt T of + SOME (_, Int (f, _)) => is_some (f T) + | SOME (_, Ext f) => f T + | NONE => false) + + +(* built-in numbers *) + +fun dest_builtin_num ctxt t = + (case try HOLogic.dest_number t of + NONE => NONE + | SOME (T, i) => + if i < 0 then NONE else + (case lookup_builtin_typ ctxt T of + SOME (_, Int (_, g)) => g T i |> Option.map (rpair T) + | _ => NONE)) + +val is_builtin_num = is_some oo dest_builtin_num + +fun is_builtin_num_ext ctxt t = + (case try HOLogic.dest_number t of + NONE => false + | SOME (T, _) => is_builtin_typ_ext ctxt T) + + +(* built-in functions *) + +fun add_builtin_fun cs ((n, T), f) = + Builtins.map (apsnd (insert_btab cs n T (Int f))) + +fun add_builtin_fun' cs (t, n) = + let + val c as (m, T) = Term.dest_Const t + fun app U ts = Term.list_comb (Const (m, U), ts) + fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U) + in add_builtin_fun cs (c, bfun) end + +fun add_builtin_fun_ext ((n, T), f) = + Builtins.map (apsnd (insert_btab SMT2_Utils.basicC n T (Ext f))) + +fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I) + +fun add_builtin_fun_ext'' n context = + let val thy = Context.theory_of context + in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end + +fun lookup_builtin_fun ctxt = + lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt))) + +fun dest_builtin_fun ctxt (c as (_, T)) ts = + (case lookup_builtin_fun ctxt c of + SOME (_, Int f) => f ctxt T ts + | _ => NONE) + +fun dest_builtin_eq ctxt t u = + let + val aT = TFree (Name.aT, @{sort type}) + val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool}) + fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts) + in + dest_builtin_fun ctxt c [] + |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk)) + end + +fun special_builtin_fun pred ctxt (c as (_, T)) ts = + if pred (Term.body_type T, Term.binder_types T) then + dest_builtin_fun ctxt c ts + else NONE + +fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt + +fun dest_builtin_conn ctxt = + special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt + +fun dest_builtin ctxt c ts = + let val t = Term.list_comb (Const c, ts) + in + (case dest_builtin_num ctxt t of + SOME (n, _) => SOME (n, 0, [], K t) + | NONE => dest_builtin_fun ctxt c ts) + end + +fun dest_builtin_fun_ext ctxt (c as (_, T)) ts = + (case lookup_builtin_fun ctxt c of + SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us) + | SOME (_, Ext f) => SOME (f ctxt T ts) + | NONE => NONE) + +fun dest_builtin_ext ctxt c ts = + if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME [] + else dest_builtin_fun_ext ctxt c ts + +fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts) + +fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_config.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_config.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,250 @@ +(* Title: HOL/Tools/SMT2/smt2_config.ML + Author: Sascha Boehme, TU Muenchen + +Configuration options and diagnostic tools for SMT. +*) + +signature SMT2_CONFIG = +sig + (*solver*) + type solver_info = { + name: string, + class: Proof.context -> SMT2_Utils.class, + avail: unit -> bool, + options: Proof.context -> string list } + val add_solver: solver_info -> Context.generic -> Context.generic + val set_solver_options: string * string -> Context.generic -> Context.generic + val is_available: Proof.context -> string -> bool + val available_solvers_of: Proof.context -> string list + val select_solver: string -> Context.generic -> Context.generic + val solver_of: Proof.context -> string + val solver_class_of: Proof.context -> SMT2_Utils.class + val solver_options_of: Proof.context -> string list + + (*options*) + val oracle: bool Config.T + val timeout: real Config.T + val random_seed: int Config.T + val read_only_certificates: bool Config.T + val verbose: bool Config.T + val trace: bool Config.T + val trace_used_facts: bool Config.T + val monomorph_limit: int Config.T + val monomorph_instances: int Config.T + val infer_triggers: bool Config.T + val filter_only_facts: bool Config.T + val debug_files: string Config.T + + (*tools*) + val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b + + (*diagnostics*) + val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit + val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit + + (*certificates*) + val select_certificates: string -> Context.generic -> Context.generic + val certificates_of: Proof.context -> Cache_IO.cache option + + (*setup*) + val print_setup: Proof.context -> unit +end + +structure SMT2_Config: SMT2_CONFIG = +struct + +(* solver *) + +type solver_info = { + name: string, + class: Proof.context -> SMT2_Utils.class, + avail: unit -> bool, + options: Proof.context -> string list } + +(* FIXME just one data slot (record) per program unit *) +structure Solvers = Generic_Data +( + type T = (solver_info * string list) Symtab.table * string option + val empty = (Symtab.empty, NONE) + val extend = I + fun merge ((ss1, s1), (ss2, s2)) = + (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2)) +) + +fun set_solver_options (name, options) = + let val opts = String.tokens (Symbol.is_ascii_blank o str) options + in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end + +fun add_solver (info as {name, ...} : solver_info) context = + if Symtab.defined (fst (Solvers.get context)) name then + error ("Solver already registered: " ^ quote name) + else + context + |> Solvers.map (apfst (Symtab.update (name, (info, [])))) + |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options")) + (Scan.lift (@{keyword "="} |-- Args.name) >> + (Thm.declaration_attribute o K o set_solver_options o pair name)) + ("Additional command line options for SMT solver " ^ quote name)) + +fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt))) + +fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt)) + +fun is_available ctxt name = + (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of + SOME ({avail, ...}, _) => avail () + | NONE => false) + +fun available_solvers_of ctxt = + filter (is_available ctxt) (all_solvers_of ctxt) + +fun warn_solver (Context.Proof ctxt) name = + Context_Position.if_visible ctxt + warning ("The SMT solver " ^ quote name ^ " is not installed.") + | warn_solver _ _ = (); + +fun select_solver name context = + let + val ctxt = Context.proof_of context + val upd = Solvers.map (apsnd (K (SOME name))) + in + if not (member (op =) (all_solvers_of ctxt) name) then + error ("Trying to select unknown solver: " ^ quote name) + else if not (is_available ctxt name) then + (warn_solver context name; upd context) + else upd context + end + +fun no_solver_err () = error "No SMT solver selected" + +fun solver_of ctxt = + (case solver_name_of ctxt of + SOME name => name + | NONE => no_solver_err ()) + +fun solver_info_of default select ctxt = + (case Solvers.get (Context.Proof ctxt) of + (solvers, SOME name) => select (Symtab.lookup solvers name) + | (_, NONE) => default ()) + +fun solver_class_of ctxt = + let fun class_of ({class, ...}: solver_info, _) = class ctxt + in solver_info_of no_solver_err (class_of o the) ctxt end + +fun solver_options_of ctxt = + let + fun all_options NONE = [] + | all_options (SOME ({options, ...} : solver_info, opts)) = + opts @ options ctxt + in solver_info_of (K []) all_options ctxt end + +val setup_solver = + Attrib.setup @{binding smt2_solver} + (Scan.lift (@{keyword "="} |-- Args.name) >> + (Thm.declaration_attribute o K o select_solver)) + "SMT solver configuration" + + +(* options *) + +val oracle = Attrib.setup_config_bool @{binding smt2_oracle} (K true) +val timeout = Attrib.setup_config_real @{binding smt2_timeout} (K 30.0) +val random_seed = Attrib.setup_config_int @{binding smt2_random_seed} (K 1) +val read_only_certificates = Attrib.setup_config_bool @{binding smt2_read_only_certificates} (K false) +val verbose = Attrib.setup_config_bool @{binding smt2_verbose} (K true) +val trace = Attrib.setup_config_bool @{binding smt2_trace} (K false) +val trace_used_facts = Attrib.setup_config_bool @{binding smt2_trace_used_facts} (K false) +val monomorph_limit = Attrib.setup_config_int @{binding smt2_monomorph_limit} (K 10) +val monomorph_instances = Attrib.setup_config_int @{binding smt2_monomorph_instances} (K 500) +val infer_triggers = Attrib.setup_config_bool @{binding smt2_infer_triggers} (K false) +val filter_only_facts = Attrib.setup_config_bool @{binding smt2_filter_only_facts} (K false) +val debug_files = Attrib.setup_config_string @{binding smt2_debug_files} (K "") + + +(* diagnostics *) + +fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else () + +fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) + +fun trace_msg ctxt = cond_trace (Config.get ctxt trace) + + +(* tools *) + +fun with_timeout ctxt f x = + TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x + handle TimeLimit.TimeOut => raise SMT2_Failure.SMT SMT2_Failure.Time_Out + + +(* certificates *) + +(* FIXME just one data slot (record) per program unit *) +structure Certificates = Generic_Data +( + type T = Cache_IO.cache option + val empty = NONE + val extend = I + fun merge (s, _) = s (* FIXME merge options!? *) +) + +val get_certificates_path = + Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof + +fun select_certificates name context = context |> Certificates.put ( + if name = "" then NONE + else + Path.explode name + |> Path.append (Thy_Load.master_directory (Context.theory_of context)) + |> SOME o Cache_IO.unsynchronized_init) + +val certificates_of = Certificates.get o Context.Proof + +val setup_certificates = + Attrib.setup @{binding smt2_certificates} + (Scan.lift (@{keyword "="} |-- Args.name) >> + (Thm.declaration_attribute o K o select_certificates)) + "SMT certificates configuration" + + +(* setup *) + +val _ = Theory.setup ( + setup_solver #> + setup_certificates) + +fun print_setup ctxt = + let + fun string_of_bool b = if b then "true" else "false" + + val names = available_solvers_of ctxt + val ns = if null names then ["(none)"] else sort_strings names + val n = the_default "(none)" (solver_name_of ctxt) + val opts = solver_options_of ctxt + + val t = string_of_real (Config.get ctxt timeout) + + val certs_filename = + (case get_certificates_path ctxt of + SOME path => Path.print path + | NONE => "(disabled)") + in + Pretty.writeln (Pretty.big_list "SMT setup:" [ + Pretty.str ("Current SMT solver: " ^ n), + Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), + Pretty.str_list "Available SMT solvers: " "" ns, + Pretty.str ("Current timeout: " ^ t ^ " seconds"), + Pretty.str ("With proofs: " ^ + string_of_bool (not (Config.get ctxt oracle))), + Pretty.str ("Certificates cache: " ^ certs_filename), + Pretty.str ("Fixed certificates: " ^ + string_of_bool (Config.get ctxt read_only_certificates))]) + end + +val _ = + Outer_Syntax.improper_command @{command_spec "smt2_status"} + "show the available SMT solvers, the currently selected SMT solver, \ + \and the values of SMT configuration options" + (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_datatypes.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,133 @@ +(* Title: HOL/Tools/SMT2/smt2_datatypes.ML + Author: Sascha Boehme, TU Muenchen + +Collector functions for common type declarations and their representation +as algebraic datatypes. +*) + +signature SMT2_DATATYPES = +sig + val add_decls: typ -> + (typ * (term * term list) list) list list * Proof.context -> + (typ * (term * term list) list) list list * Proof.context +end + +structure SMT2_Datatypes: SMT2_DATATYPES = +struct + +val lhs_head_of = Term.head_of o fst o Logic.dest_equals o Thm.prop_of + +fun mk_selectors T Ts ctxt = + let + val (sels, ctxt') = + Variable.variant_fixes (replicate (length Ts) "select") ctxt + in (map2 (fn n => fn U => Free (n, T --> U)) sels Ts, ctxt') end + + +(* datatype declarations *) + +fun get_datatype_decl ({descr, ...} : Datatype.info) n Ts ctxt = + let + fun get_vars (_, (m, vs, _)) = if m = n then SOME vs else NONE + val vars = the (get_first get_vars descr) ~~ Ts + val lookup_var = the o AList.lookup (op =) vars + + fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt + | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts) + | typ_of (Datatype.DtRec i) = + the (AList.lookup (op =) descr i) + |> (fn (m, dts, _) => Type (m, map typ_of dts)) + + fun mk_constr T (m, dts) ctxt = + let + val Ts = map typ_of dts + val constr = Const (m, Ts ---> T) + val (selects, ctxt') = mk_selectors T Ts ctxt + in ((constr, selects), ctxt') end + + fun mk_decl (i, (_, _, constrs)) ctxt = + let + val T = typ_of (Datatype.DtRec i) + val (css, ctxt') = fold_map (mk_constr T) constrs ctxt + in ((T, css), ctxt') end + + in fold_map mk_decl descr ctxt end + + +(* record declarations *) + +val record_name_of = Long_Name.implode o fst o split_last o Long_Name.explode + +fun get_record_decl ({ext_def, ...} : Record.info) T ctxt = + let + val (con, _) = Term.dest_Const (lhs_head_of ext_def) + val (fields, more) = Record.get_extT_fields (Proof_Context.theory_of ctxt) T + val fieldTs = map snd fields @ [snd more] + + val constr = Const (con, fieldTs ---> T) + val (selects, ctxt') = mk_selectors T fieldTs ctxt + in ((T, [(constr, selects)]), ctxt') end + + +(* typedef declarations *) + +fun get_typedef_decl (info : Typedef.info) T Ts = + let + val ({Abs_name, Rep_name, abs_type, rep_type, ...}, _) = info + + val env = snd (Term.dest_Type abs_type) ~~ Ts + val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) + + val constr = Const (Abs_name, instT (rep_type --> abs_type)) + val select = Const (Rep_name, instT (abs_type --> rep_type)) + in (T, [(constr, [select])]) end + + +(* collection of declarations *) + +fun declared declss T = exists (exists (equal T o fst)) declss +fun declared' dss T = exists (exists (equal T o fst) o snd) dss + +fun get_decls T n Ts ctxt = + let val thy = Proof_Context.theory_of ctxt + in + (case Datatype.get_info thy n of + SOME info => get_datatype_decl info n Ts ctxt + | NONE => + (case Record.get_info thy (record_name_of n) of + SOME info => get_record_decl info T ctxt |>> single + | NONE => + (case Typedef.get_info ctxt n of + [] => ([], ctxt) + | info :: _ => ([get_typedef_decl info T Ts], ctxt)))) + end + +fun add_decls T (declss, ctxt) = + let + fun depends Ts ds = exists (member (op =) (map fst ds)) Ts + + fun add (TFree _) = I + | add (TVar _) = I + | add (T as Type (@{type_name fun}, _)) = + fold add (Term.body_type T :: Term.binder_types T) + | add @{typ bool} = I + | add (T as Type (n, Ts)) = (fn (dss, ctxt1) => + if declared declss T orelse declared' dss T then (dss, ctxt1) + else if SMT2_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1) + else + (case get_decls T n Ts ctxt1 of + ([], _) => (dss, ctxt1) + | (ds, ctxt2) => + let + val constrTs = + maps (map (snd o Term.dest_Const o fst) o snd) ds + val Us = fold (union (op =) o Term.binder_types) constrTs [] + + fun ins [] = [(Us, ds)] + | ins ((Uds as (Us', _)) :: Udss) = + if depends Us' ds then (Us, ds) :: Uds :: Udss + else Uds :: ins Udss + in fold add Us (ins dss, ctxt2) end)) + in add T ([], ctxt) |>> append declss o map snd end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_failure.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_failure.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,61 @@ +(* Title: HOL/Tools/SMT2/smt2_failure.ML + Author: Sascha Boehme, TU Muenchen + +Failures and exception of SMT. +*) + +signature SMT2_FAILURE = +sig + type counterexample = { + is_real_cex: bool, + free_constraints: term list, + const_defs: term list} + datatype failure = + Counterexample of counterexample | + Time_Out | + Out_Of_Memory | + Abnormal_Termination of int | + Other_Failure of string + val pretty_counterexample: Proof.context -> counterexample -> Pretty.T + val string_of_failure: Proof.context -> failure -> string + exception SMT of failure +end + +structure SMT2_Failure: SMT2_FAILURE = +struct + +type counterexample = { + is_real_cex: bool, + free_constraints: term list, + const_defs: term list} + +datatype failure = + Counterexample of counterexample | + Time_Out | + Out_Of_Memory | + Abnormal_Termination of int | + Other_Failure of string + +fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} = + let + val msg = + if is_real_cex then "Counterexample found (possibly spurious)" + else "Potential counterexample found" + in + if null free_constraints andalso null const_defs then Pretty.str msg + else + Pretty.big_list (msg ^ ":") + (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs)) + end + +fun string_of_failure ctxt (Counterexample cex) = + Pretty.string_of (pretty_counterexample ctxt cex) + | string_of_failure _ Time_Out = "Timed out" + | string_of_failure _ Out_Of_Memory = "Ran out of memory" + | string_of_failure _ (Abnormal_Termination err) = + "Solver terminated abnormally with error code " ^ string_of_int err + | string_of_failure _ (Other_Failure msg) = msg + +exception SMT of failure + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_normalize.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,652 @@ +(* Title: HOL/Tools/SMT2/smt2_normalize.ML + Author: Sascha Boehme, TU Muenchen + +Normalization steps on theorems required by SMT solvers. +*) + +signature SMT2_NORMALIZE = +sig + val drop_fact_warning: Proof.context -> thm -> unit + val atomize_conv: Proof.context -> conv + type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list + val add_extra_norm: SMT2_Utils.class * extra_norm -> Context.generic -> + Context.generic + val normalize: (int * (int option * thm)) list -> Proof.context -> + (int * thm) list * Proof.context +end + +structure SMT2_Normalize: SMT2_NORMALIZE = +struct + +fun drop_fact_warning ctxt = + SMT2_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o + Display.string_of_thm ctxt) + + +(* general theorem normalizations *) + +(** instantiate elimination rules **) + +local + val (cpfalse, cfalse) = + `SMT2_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False}) + + fun inst f ct thm = + let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) + in Thm.instantiate ([], [(cv, ct)]) thm end +in + +fun instantiate_elim thm = + (case Thm.concl_of thm of + @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm + | Var _ => inst I cpfalse thm + | _ => thm) + +end + + +(** normalize definitions **) + +fun norm_def thm = + (case Thm.prop_of thm of + @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => + norm_def (thm RS @{thm fun_cong}) + | Const (@{const_name "=="}, _) $ _ $ Abs _ => + norm_def (thm RS @{thm meta_eq_to_obj_eq}) + | _ => thm) + + +(** atomization **) + +fun atomize_conv ctxt ct = + (case Thm.term_of ct of + @{const "==>"} $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_imp} + | Const (@{const_name "=="}, _) $ _ $ _ => + Conv.binop_conv (atomize_conv ctxt) then_conv + Conv.rewr_conv @{thm atomize_eq} + | Const (@{const_name all}, _) $ Abs _ => + Conv.binder_conv (atomize_conv o snd) ctxt then_conv + Conv.rewr_conv @{thm atomize_all} + | _ => Conv.all_conv) ct + +val setup_atomize = + fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, + @{const_name "=="}, @{const_name all}, @{const_name Trueprop}] + + +(** unfold special quantifiers **) + +local + val ex1_def = mk_meta_eq @{lemma + "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))" + by (rule ext) (simp only: Ex1_def)} + + val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)" + by (rule ext)+ (rule Ball_def)} + + val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)" + by (rule ext)+ (rule Bex_def)} + + val special_quants = [(@{const_name Ex1}, ex1_def), + (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)] + + fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n + | special_quant _ = NONE + + fun special_quant_conv _ ct = + (case special_quant (Thm.term_of ct) of + SOME thm => Conv.rewr_conv thm + | NONE => Conv.all_conv) ct +in + +fun unfold_special_quants_conv ctxt = + SMT2_Utils.if_exists_conv (is_some o special_quant) + (Conv.top_conv special_quant_conv ctxt) + +val setup_unfolded_quants = + fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants + +end + + +(** trigger inference **) + +local + (*** check trigger syntax ***) + + fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true + | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false + | dest_trigger _ = NONE + + fun eq_list [] = false + | eq_list (b :: bs) = forall (equal b) bs + + fun proper_trigger t = + t + |> these o try HOLogic.dest_list + |> map (map_filter dest_trigger o these o try HOLogic.dest_list) + |> (fn [] => false | bss => forall eq_list bss) + + fun proper_quant inside f t = + (case t of + Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u + | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u + | @{const trigger} $ p $ u => + (if inside then f p else false) andalso proper_quant false f u + | Abs (_, _, u) => proper_quant false f u + | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 + | _ => true) + + fun check_trigger_error ctxt t = + error ("SMT triggers must only occur under quantifier and multipatterns " ^ + "must have the same kind: " ^ Syntax.string_of_term ctxt t) + + fun check_trigger_conv ctxt ct = + if proper_quant false proper_trigger (SMT2_Utils.term_of ct) then + Conv.all_conv ct + else check_trigger_error ctxt (Thm.term_of ct) + + + (*** infer simple triggers ***) + + fun dest_cond_eq ct = + (case Thm.term_of ct of + Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct + | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) + | _ => raise CTERM ("no equation", [ct])) + + fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n) + | get_constrs _ _ = [] + + fun is_constr thy (n, T) = + let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) + in can (the o find_first match o get_constrs thy o Term.body_type) T end + + fun is_constr_pat thy t = + (case Term.strip_comb t of + (Free _, []) => true + | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts + | _ => false) + + fun is_simp_lhs ctxt t = + (case Term.strip_comb t of + (Const c, ts as _ :: _) => + not (SMT2_Builtin.is_builtin_fun_ext ctxt c ts) andalso + forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts + | _ => false) + + fun has_all_vars vs t = + subset (op aconv) (vs, map Free (Term.add_frees t [])) + + fun minimal_pats vs ct = + if has_all_vars vs (Thm.term_of ct) then + (case Thm.term_of ct of + _ $ _ => + (case pairself (minimal_pats vs) (Thm.dest_comb ct) of + ([], []) => [[ct]] + | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') + | _ => []) + else [] + + fun proper_mpat _ _ _ [] = false + | proper_mpat thy gen u cts = + let + val tps = (op ~~) (`gen (map Thm.term_of cts)) + fun some_match u = tps |> exists (fn (t', t) => + Pattern.matches thy (t', u) andalso not (t aconv u)) + in not (Term.exists_subterm some_match u) end + + val pat = + SMT2_Utils.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Utils.destT1 + fun mk_pat ct = Thm.apply (SMT2_Utils.instT' ct pat) ct + + fun mk_clist T = pairself (Thm.cterm_of @{theory}) + (HOLogic.cons_const T, HOLogic.nil_const T) + fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil + val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern}) + val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"}) + fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss + + val trigger_eq = + mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)} + + fun insert_trigger_conv [] ct = Conv.all_conv ct + | insert_trigger_conv ctss ct = + let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct + in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end + + fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = + let + val (lhs, rhs) = dest_cond_eq ct + + val vs = map Thm.term_of cvs + val thy = Proof_Context.theory_of ctxt + + fun get_mpats ct = + if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct + else [] + val gen = Variable.export_terms ctxt outer_ctxt + val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) + + in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end + + fun has_trigger (@{const SMT2.trigger} $ _ $ _) = true + | has_trigger _ = false + + fun try_trigger_conv cv ct = + if SMT2_Utils.under_quant has_trigger (SMT2_Utils.term_of ct) then + Conv.all_conv ct + else Conv.try_conv cv ct + + fun infer_trigger_conv ctxt = + if Config.get ctxt SMT2_Config.infer_triggers then + try_trigger_conv + (SMT2_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) + else Conv.all_conv +in + +fun trigger_conv ctxt = + SMT2_Utils.prop_conv + (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) + +val setup_trigger = + fold SMT2_Builtin.add_builtin_fun_ext'' + [@{const_name SMT2.pat}, @{const_name SMT2.nopat}, @{const_name SMT2.trigger}] + +end + + +(** adding quantifier weights **) + +local + (*** check weight syntax ***) + + val has_no_weight = + not o Term.exists_subterm (fn @{const SMT2.weight} => true | _ => false) + + fun is_weight (@{const SMT2.weight} $ w $ t) = + (case try HOLogic.dest_number w of + SOME (_, i) => i >= 0 andalso has_no_weight t + | _ => false) + | is_weight t = has_no_weight t + + fun proper_trigger (@{const SMT2.trigger} $ _ $ t) = is_weight t + | proper_trigger t = is_weight t + + fun check_weight_error ctxt t = + error ("SMT weight must be a non-negative number and must only occur " ^ + "under the top-most quantifier and an optional trigger: " ^ + Syntax.string_of_term ctxt t) + + fun check_weight_conv ctxt ct = + if SMT2_Utils.under_quant proper_trigger (SMT2_Utils.term_of ct) then + Conv.all_conv ct + else check_weight_error ctxt (Thm.term_of ct) + + + (*** insertion of weights ***) + + fun under_trigger_conv cv ct = + (case Thm.term_of ct of + @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv + | _ => cv) ct + + val weight_eq = + mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)} + fun mk_weight_eq w = + let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) + in + Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq + end + + fun add_weight_conv NONE _ = Conv.all_conv + | add_weight_conv (SOME weight) ctxt = + let val cv = Conv.rewr_conv (mk_weight_eq weight) + in SMT2_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end +in + +fun weight_conv weight ctxt = + SMT2_Utils.prop_conv + (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) + +val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight} + +end + + +(** combined general normalizations **) + +fun gen_normalize1_conv ctxt weight = + atomize_conv ctxt then_conv + unfold_special_quants_conv ctxt then_conv + Thm.beta_conversion true then_conv + trigger_conv ctxt then_conv + weight_conv weight ctxt + +fun gen_normalize1 ctxt weight thm = + thm + |> instantiate_elim + |> norm_def + |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) + |> Drule.forall_intr_vars + |> Conv.fconv_rule (gen_normalize1_conv ctxt weight) + (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *) + |> Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]} + +fun gen_norm1_safe ctxt (i, (weight, thm)) = + (case try (gen_normalize1 ctxt weight) thm of + SOME thm' => SOME (i, thm') + | NONE => (drop_fact_warning ctxt thm; NONE)) + +fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms + + + +(* unfolding of definitions and theory-specific rewritings *) + +fun expand_head_conv cv ct = + (case Thm.term_of ct of + _ $ _ => + Conv.fun_conv (expand_head_conv cv) then_conv + Conv.try_conv (Thm.beta_conversion false) + | _ => cv) ct + + +(** rewrite bool case expressions as if expressions **) + +local + fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true + | is_case_bool _ = false + + val thm = mk_meta_eq @{lemma + "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp} + + fun unfold_conv _ = + SMT2_Utils.if_true_conv (is_case_bool o Term.head_of) + (expand_head_conv (Conv.rewr_conv thm)) +in + +fun rewrite_case_bool_conv ctxt = + SMT2_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt) + +val setup_case_bool = + SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"} + +end + + +(** unfold abs, min and max **) + +local + val abs_def = mk_meta_eq @{lemma + "abs = (%a::'a::abs_if. if a < 0 then - a else a)" + by (rule ext) (rule abs_if)} + + val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)" + by (rule ext)+ (rule min_def)} + + val max_def = mk_meta_eq @{lemma "max = (%a b. if a <= b then b else a)" + by (rule ext)+ (rule max_def)} + + val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), + (@{const_name abs}, abs_def)] + + fun is_builtinT ctxt T = + SMT2_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T) + + fun abs_min_max ctxt (Const (n, T)) = + (case AList.lookup (op =) defs n of + NONE => NONE + | SOME thm => if is_builtinT ctxt T then SOME thm else NONE) + | abs_min_max _ _ = NONE + + fun unfold_amm_conv ctxt ct = + (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of + SOME thm => expand_head_conv (Conv.rewr_conv thm) + | NONE => Conv.all_conv) ct +in + +fun unfold_abs_min_max_conv ctxt = + SMT2_Utils.if_exists_conv (is_some o abs_min_max ctxt) + (Conv.top_conv unfold_amm_conv ctxt) + +val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs + +end + + +(** embedding of standard natural number operations into integer operations **) + +local + val nat_embedding = @{lemma + "ALL n. nat (int n) = n" + "ALL i. i >= 0 --> int (nat i) = i" + "ALL i. i < 0 --> int (nat i) = 0" + by simp_all} + + val simple_nat_ops = [ + @{const less (nat)}, @{const less_eq (nat)}, + @{const Suc}, @{const plus (nat)}, @{const minus (nat)}] + + val mult_nat_ops = + [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}] + + val nat_ops = simple_nat_ops @ mult_nat_ops + + val nat_consts = nat_ops @ [@{const numeral (nat)}, + @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] + + val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] + + val builtin_nat_ops = nat_int_coercions @ simple_nat_ops + + val is_nat_const = member (op aconv) nat_consts + + fun is_nat_const' @{const of_nat (int)} = true + | is_nat_const' t = is_nat_const t + + val expands = map mk_meta_eq @{lemma + "0 = nat 0" + "1 = nat 1" + "(numeral :: num => nat) = (%i. nat (numeral i))" + "op < = (%a b. int a < int b)" + "op <= = (%a b. int a <= int b)" + "Suc = (%a. nat (int a + 1))" + "op + = (%a b. nat (int a + int b))" + "op - = (%a b. nat (int a - int b))" + "op * = (%a b. nat (int a * int b))" + "op div = (%a b. nat (int a div int b))" + "op mod = (%a b. nat (int a mod int b))" + by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+} + + val ints = map mk_meta_eq @{lemma + "int 0 = 0" + "int 1 = 1" + "int (Suc n) = int n + 1" + "int (n + m) = int n + int m" + "int (n - m) = int (nat (int n - int m))" + "int (n * m) = int n * int m" + "int (n div m) = int n div int m" + "int (n mod m) = int n mod int m" + by (auto simp add: int_mult zdiv_int zmod_int)} + + val int_if = mk_meta_eq @{lemma + "int (if P then n else m) = (if P then int n else int m)" + by simp} + + fun mk_number_eq ctxt i lhs = + let + val eq = SMT2_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) + val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_numeral} + val tac = HEADGOAL (Simplifier.simp_tac ctxt') + in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end + + fun ite_conv cv1 cv2 = + Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 + + fun int_conv ctxt ct = + (case Thm.term_of ct of + @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => + Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) + | @{const of_nat (int)} $ _ => + (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv + (Conv.rewr_conv int_if then_conv + ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv + Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt + | _ => Conv.no_conv) ct + + and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt + + and expand_conv ctxt = + SMT2_Utils.if_conv (is_nat_const o Term.head_of) + (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) + (int_conv ctxt) + + and nat_conv ctxt = SMT2_Utils.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt) + + val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) +in + +val nat_as_int_conv = nat_conv + +fun add_nat_embedding thms = + if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) + else (thms, []) + +val setup_nat_as_int = + SMT2_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #> + fold (SMT2_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops + +end + + +(** normalize numerals **) + +local + (* + rewrite Numeral1 into 1 + rewrite - 0 into 0 + *) + + fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) = + true + | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) = + true + | is_irregular_number _ = + false; + + fun is_strange_number ctxt t = is_irregular_number t andalso SMT2_Builtin.is_builtin_num ctxt t; + + val proper_num_ss = + simpset_of (put_simpset HOL_ss @{context} + addsimps @{thms Num.numeral_One minus_zero}) + + fun norm_num_conv ctxt = + SMT2_Utils.if_conv (is_strange_number ctxt) + (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv +in + +fun normalize_numerals_conv ctxt = + SMT2_Utils.if_exists_conv (is_strange_number ctxt) + (Conv.top_sweep_conv norm_num_conv ctxt) + +end + + +(** combined unfoldings and rewritings **) + +fun unfold_conv ctxt = + rewrite_case_bool_conv ctxt then_conv + unfold_abs_min_max_conv ctxt then_conv + nat_as_int_conv ctxt then_conv + Thm.beta_conversion true + +fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) + +fun burrow_ids f ithms = + let + val (is, thms) = split_list ithms + val (thms', extra_thms) = f thms + in (is ~~ thms') @ map (pair ~1) extra_thms end + +fun unfold2 ctxt ithms = + ithms + |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) + |> burrow_ids add_nat_embedding + + + +(* overall normalization *) + +type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list + +structure Extra_Norms = Generic_Data +( + type T = extra_norm SMT2_Utils.dict + val empty = [] + val extend = I + fun merge data = SMT2_Utils.dict_merge fst data +) + +fun add_extra_norm (cs, norm) = + Extra_Norms.map (SMT2_Utils.dict_update (cs, norm)) + +fun apply_extra_norms ctxt ithms = + let + val cs = SMT2_Config.solver_class_of ctxt + val es = SMT2_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs + in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end + +local + val ignored = member (op =) [@{const_name All}, @{const_name Ex}, + @{const_name Let}, @{const_name If}, @{const_name HOL.eq}] + + val schematic_consts_of = + let + fun collect (@{const SMT2.trigger} $ p $ t) = + collect_trigger p #> collect t + | collect (t $ u) = collect t #> collect u + | collect (Abs (_, _, t)) = collect t + | collect (t as Const (n, _)) = + if not (ignored n) then Monomorph.add_schematic_consts_of t else I + | collect _ = I + and collect_trigger t = + let val dest = these o try HOLogic.dest_list + in fold (fold collect_pat o dest) (dest t) end + and collect_pat (Const (@{const_name SMT2.pat}, _) $ t) = collect t + | collect_pat (Const (@{const_name SMT2.nopat}, _) $ t) = collect t + | collect_pat _ = I + in (fn t => collect t Symtab.empty) end +in + +fun monomorph ctxt xthms = + let val (xs, thms) = split_list xthms + in + map (pair 1) thms + |> Monomorph.monomorph schematic_consts_of ctxt + |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) + end + +end + +fun normalize iwthms ctxt = + iwthms + |> gen_normalize ctxt + |> unfold1 ctxt + |> monomorph ctxt + |> unfold2 ctxt + |> apply_extra_norms ctxt + |> rpair ctxt + +val _ = Theory.setup (Context.theory_map ( + setup_atomize #> + setup_unfolded_quants #> + setup_trigger #> + setup_weight #> + setup_case_bool #> + setup_abs_min_max #> + setup_nat_as_int)) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_real.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_real.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,121 @@ +(* Title: HOL/Tools/SMT2/smt2_real.ML + Author: Sascha Boehme, TU Muenchen + +SMT setup for reals. +*) + +structure SMT2_Real: sig end = +struct + + +(* SMT-LIB logic *) + +fun smtlib_logic ts = + if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts + then SOME "AUFLIRA" + else NONE + + +(* SMT-LIB and Z3 built-ins *) + +local + fun real_num _ i = SOME (string_of_int i ^ ".0") + + fun is_linear [t] = SMT2_Utils.is_number t + | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u + | is_linear _ = false + + fun mk_times ts = Term.list_comb (@{const times (real)}, ts) + + fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE +in + +val setup_builtins = + SMT2_Builtin.add_builtin_typ SMTLIB2_Interface.smtlib2C + (@{typ real}, K (SOME "Real"), real_num) #> + fold (SMT2_Builtin.add_builtin_fun' SMTLIB2_Interface.smtlib2C) [ + (@{const less (real)}, "<"), + (@{const less_eq (real)}, "<="), + (@{const uminus (real)}, "~"), + (@{const plus (real)}, "+"), + (@{const minus (real)}, "-") ] #> + SMT2_Builtin.add_builtin_fun SMTLIB2_Interface.smtlib2C + (Term.dest_Const @{const times (real)}, times) #> + SMT2_Builtin.add_builtin_fun' Z3_New_Interface.smtlib2_z3C + (@{const times (real)}, "*") #> + SMT2_Builtin.add_builtin_fun' Z3_New_Interface.smtlib2_z3C + (@{const divide (real)}, "/") + +end + + +(* Z3 constructors *) + +local + fun z3_mk_builtin_typ (Z3_New_Interface.Sym ("Real", _)) = SOME @{typ real} + | z3_mk_builtin_typ (Z3_New_Interface.Sym ("real", _)) = SOME @{typ real} + (*FIXME: delete*) + | z3_mk_builtin_typ _ = NONE + + fun z3_mk_builtin_num _ i T = + if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) + else NONE + + fun mk_nary _ cu [] = cu + | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) + + val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) + val add = Thm.cterm_of @{theory} @{const plus (real)} + val real0 = Numeral.mk_cnumber @{ctyp real} 0 + val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) + val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) + val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) + val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) + val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) + + fun z3_mk_builtin_fun (Z3_New_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("+", _)) cts = + SOME (mk_nary add real0 cts) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("-", _)) [ct, cu] = + SOME (mk_sub ct cu) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("*", _)) [ct, cu] = + SOME (mk_mul ct cu) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("/", _)) [ct, cu] = + SOME (mk_div ct cu) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("<", _)) [ct, cu] = + SOME (mk_lt ct cu) + | z3_mk_builtin_fun (Z3_New_Interface.Sym ("<=", _)) [ct, cu] = + SOME (mk_le ct cu) + | z3_mk_builtin_fun (Z3_New_Interface.Sym (">", _)) [ct, cu] = + SOME (mk_lt cu ct) + | z3_mk_builtin_fun (Z3_New_Interface.Sym (">=", _)) [ct, cu] = + SOME (mk_le cu ct) + | z3_mk_builtin_fun _ _ = NONE +in + +val z3_mk_builtins = { + mk_builtin_typ = z3_mk_builtin_typ, + mk_builtin_num = z3_mk_builtin_num, + mk_builtin_fun = (fn _ => fn sym => fn cts => + (case try (#T o Thm.rep_cterm o hd) cts of + SOME @{typ real} => z3_mk_builtin_fun sym cts + | _ => NONE)) } + +end + + +(* Z3 proof replay *) + +val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ + "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc + + +(* setup *) + +val _ = Theory.setup (Context.theory_map ( + SMTLIB2_Interface.add_logic (10, smtlib_logic) #> + setup_builtins #> + Z3_New_Interface.add_mk_builtins z3_mk_builtins #> + Z3_New_Proof_Tools.add_simproc real_linarith_proc)) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_setup_solvers.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_setup_solvers.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,183 @@ +(* Title: HOL/Tools/SMT2/smt2_setup_solvers.ML + Author: Sascha Boehme, TU Muenchen + +Setup SMT solvers. +*) + +signature SMT2_SETUP_SOLVERS = +sig + datatype z3_non_commercial = + Z3_Non_Commercial_Unknown | + Z3_Non_Commercial_Accepted | + Z3_Non_Commercial_Declined + val z3_non_commercial: unit -> z3_non_commercial + val z3_extensions: bool Config.T +end + +structure SMT2_Setup_Solvers: SMT2_SETUP_SOLVERS = +struct + +(* helper functions *) + +fun make_avail name () = getenv (name ^ "_SOLVER") <> "" + +fun make_command name () = [getenv (name ^ "_SOLVER")] + +fun outcome_of unsat sat unknown solver_name line = + if String.isPrefix unsat line then SMT2_Solver.Unsat + else if String.isPrefix sat line then SMT2_Solver.Sat + else if String.isPrefix unknown line then SMT2_Solver.Unknown + else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^ + quote solver_name ^ " failed. Enable SMT tracing by setting the " ^ + "configuration option " ^ quote (Config.name_of SMT2_Config.trace) ^ " and " ^ + "see the trace for details.")) + +fun on_first_line test_outcome solver_name lines = + let + val empty_line = (fn "" => true | _ => false) + val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) + val (l, ls) = split_first (snd (take_prefix empty_line lines)) + in (test_outcome solver_name l, ls) end + + +(* CVC3 *) + +local + fun cvc3_options ctxt = [ + "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed), + "-lang", "smtlib", "-output-lang", "presentation", + "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))] +in + +val cvc3: SMT2_Solver.solver_config = { + name = "cvc3_new", + class = K SMTLIB2_Interface.smtlib2C, + avail = make_avail "CVC3_NEW", + command = make_command "CVC3_NEW", + options = cvc3_options, + default_max_relevant = 400 (* FUDGE *), + supports_filter = false, + outcome = + on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), + cex_parser = NONE, + replay = NONE } + +end + + +(* Yices *) + +val yices: SMT2_Solver.solver_config = { + name = "yices_new", + class = K SMTLIB2_Interface.smtlib2C, + avail = make_avail "YICES_NEW", + command = make_command "YICES_NEW", + options = (fn ctxt => [ + "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), + "--timeout=" ^ + string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), + "--smtlib"]), + default_max_relevant = 350 (* FUDGE *), + supports_filter = false, + outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), + cex_parser = NONE, + replay = NONE } + + +(* Z3 *) + +datatype z3_non_commercial = + Z3_Non_Commercial_Unknown | + Z3_Non_Commercial_Accepted | + Z3_Non_Commercial_Declined + +local + val accepted = member (op =) ["yes", "Yes", "YES"] + val declined = member (op =) ["no", "No", "NO"] +in + +fun z3_non_commercial () = + let + val flag1 = Options.default_string @{option z3_non_commercial} + val flag2 = getenv "Z3_NON_COMMERCIAL" + in + if accepted flag1 then Z3_Non_Commercial_Accepted + else if declined flag1 then Z3_Non_Commercial_Declined + else if accepted flag2 then Z3_Non_Commercial_Accepted + else if declined flag2 then Z3_Non_Commercial_Declined + else Z3_Non_Commercial_Unknown + end + +fun if_z3_non_commercial f = + (case z3_non_commercial () of + Z3_Non_Commercial_Accepted => f () + | Z3_Non_Commercial_Declined => + error (Pretty.string_of (Pretty.para + "The SMT solver Z3 may only be used for non-commercial applications.")) + | Z3_Non_Commercial_Unknown => + error (Pretty.string_of (Pretty.para + ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ + \system option \"z3_non_commercial\" to \"yes\" (e.g. via \ + \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")))) + +end + +val z3_extensions = Attrib.setup_config_bool @{binding z3_new_extensions} (K false) + +local + fun z3_make_command name () = if_z3_non_commercial (make_command name) + + fun z3_options ctxt = + ["REFINE_INJ_AXIOM=false" (* not supported by replay *), + "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed), + "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), + "-smt2"] + + fun z3_on_first_or_last_line solver_name lines = + let + fun junk l = + if String.isPrefix "WARNING: Out of allocated virtual memory" l + then raise SMT2_Failure.SMT SMT2_Failure.Out_Of_Memory + else + String.isPrefix "WARNING" l orelse + String.isPrefix "ERROR" l orelse + forall Symbol.is_ascii_blank (Symbol.explode l) + val lines = filter_out junk lines + fun outcome split = + the_default ("", []) (try split lines) + |>> outcome_of "unsat" "sat" "unknown" solver_name + in + (* Starting with version 4.0, Z3 puts the outcome on the first line of the + output rather than on the last line. *) + outcome (fn lines => (hd lines, tl lines)) + handle SMT2_Failure.SMT _ => outcome (swap o split_last) + end + + fun select_class ctxt = + if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C + else SMTLIB2_Interface.smtlib2C +in + +val z3: SMT2_Solver.solver_config = { + name = "z3_new", + class = select_class, + avail = make_avail "Z3_NEW", + command = z3_make_command "Z3_NEW", + options = z3_options, + default_max_relevant = 350 (* FUDGE *), + supports_filter = true, + outcome = z3_on_first_or_last_line, + cex_parser = NONE, + replay = SOME Z3_New_Proof_Replay.replay } + +end + + +(* overall setup *) + +val _ = Theory.setup ( + SMT2_Solver.add_solver cvc3 #> + SMT2_Solver.add_solver yices #> + SMT2_Solver.add_solver z3) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_solver.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,367 @@ +(* Title: HOL/Tools/SMT2/smt2_solver.ML + Author: Sascha Boehme, TU Muenchen + +SMT solvers registry and SMT tactic. +*) + +signature SMT2_SOLVER = +sig + (*configuration*) + datatype outcome = Unsat | Sat | Unknown + type solver_config = { + name: string, + class: Proof.context -> SMT2_Utils.class, + avail: unit -> bool, + command: unit -> string list, + options: Proof.context -> string list, + default_max_relevant: int, + supports_filter: bool, + outcome: string -> string list -> outcome * string list, + cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> + term list * term list) option, + replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option } + + (*registry*) + val add_solver: solver_config -> theory -> theory + val solver_name_of: Proof.context -> string + val available_solvers_of: Proof.context -> string list + val apply_solver: Proof.context -> (int * (int option * thm)) list -> + int list * thm + val default_max_relevant: Proof.context -> string -> int + + (*filter*) + type 'a smt2_filter_data = + ('a * thm) list * ((int * thm) list * Proof.context) + val smt2_filter_preprocess: Proof.context -> thm list -> thm -> + ('a * (int option * thm)) list -> int -> 'a smt2_filter_data + val smt2_filter_apply: Time.time -> 'a smt2_filter_data -> + {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list} + + (*tactic*) + val smt2_tac: Proof.context -> thm list -> int -> tactic + val smt2_tac': Proof.context -> thm list -> int -> tactic +end + +structure SMT2_Solver: SMT2_SOLVER = +struct + + +(* interface to external solvers *) + +local + +fun make_cmd command options problem_path proof_path = space_implode " " ( + "(exec 2>&1;" :: map File.shell_quote (command @ options) @ + [File.shell_path problem_path, ")", ">", File.shell_path proof_path]) + +fun trace_and ctxt msg f x = + let val _ = SMT2_Config.trace_msg ctxt (fn () => msg) () + in f x end + +fun run ctxt name mk_cmd input = + (case SMT2_Config.certificates_of ctxt of + NONE => + if not (SMT2_Config.is_available ctxt name) then + error ("The SMT solver " ^ quote name ^ " is not installed.") + else if Config.get ctxt SMT2_Config.debug_files = "" then + trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") + (Cache_IO.run mk_cmd) input + else + let + val base_path = Path.explode (Config.get ctxt SMT2_Config.debug_files) + val in_path = Path.ext "smt2_in" base_path + val out_path = Path.ext "smt2_out" base_path + in Cache_IO.raw_run mk_cmd input in_path out_path end + | SOME certs => + (case Cache_IO.lookup certs input of + (NONE, key) => + if Config.get ctxt SMT2_Config.read_only_certificates then + error ("Bad certificate cache: missing certificate") + else + Cache_IO.run_and_cache certs key mk_cmd input + | (SOME output, _) => + trace_and ctxt ("Using cached certificate from " ^ + File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") + I output)) + +fun run_solver ctxt name mk_cmd input = + let + fun pretty tag ls = Pretty.string_of (Pretty.big_list tag + (map Pretty.str ls)) + + val _ = SMT2_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input + + val {redirected_output=res, output=err, return_code} = + SMT2_Config.with_timeout ctxt (run ctxt name mk_cmd) input + val _ = SMT2_Config.trace_msg ctxt (pretty "Solver:") err + + val output = fst (take_suffix (equal "") res) + val _ = SMT2_Config.trace_msg ctxt (pretty "Result:") output + + val _ = return_code <> 0 andalso + raise SMT2_Failure.SMT (SMT2_Failure.Abnormal_Termination return_code) + in output end + +fun trace_assms ctxt = + SMT2_Config.trace_msg ctxt (Pretty.string_of o + Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) + +fun trace_replay_data ({context=ctxt, typs, terms, ...} : SMT2_Translate.replay_data) = + let + fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] + fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) + fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) + in + SMT2_Config.trace_msg ctxt (fn () => + Pretty.string_of (Pretty.big_list "Names:" [ + Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), + Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () + end + +in + +fun invoke name command ithms ctxt = + let + val options = SMT2_Config.solver_options_of ctxt + val cmd = command () + val comments = [space_implode " " (cmd @ options)] + + val (str, replay_data as {context=ctxt', ...}) = + ithms + |> tap (trace_assms ctxt) + |> SMT2_Translate.translate ctxt comments + ||> tap trace_replay_data + in (run_solver ctxt' name (make_cmd cmd options) str, replay_data) end + +end + + +(* configuration *) + +datatype outcome = Unsat | Sat | Unknown + +type solver_config = { + name: string, + class: Proof.context -> SMT2_Utils.class, + avail: unit -> bool, + command: unit -> string list, + options: Proof.context -> string list, + default_max_relevant: int, + supports_filter: bool, + outcome: string -> string list -> outcome * string list, + cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> + term list * term list) option, + replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option } + + +(* registry *) + +type solver_info = { + command: unit -> string list, + default_max_relevant: int, + supports_filter: bool, + replay: Proof.context -> string list * SMT2_Translate.replay_data -> int list * thm } + +structure Solvers = Generic_Data +( + type T = solver_info Symtab.table + val empty = Symtab.empty + val extend = I + fun merge data = Symtab.merge (K true) data +) + +local + fun finish outcome cex_parser replay ocl outer_ctxt + (output, (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data)) = + (case outcome output of + (Unsat, ls) => + if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay + then the replay outer_ctxt replay_data ls + else ([], ocl ()) + | (result, ls) => + let + val (ts, us) = + (case cex_parser of SOME f => f ctxt replay_data ls | _ => ([], [])) + in + raise SMT2_Failure.SMT (SMT2_Failure.Counterexample { + is_real_cex = (result = Sat), + free_constraints = ts, + const_defs = us}) + end) + + val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False}) +in + +fun add_solver cfg = + let + val {name, class, avail, command, options, default_max_relevant, + supports_filter, outcome, cex_parser, replay} = cfg + + fun core_oracle () = cfalse + + fun solver ocl = { + command = command, + default_max_relevant = default_max_relevant, + supports_filter = supports_filter, + replay = finish (outcome name) cex_parser replay ocl } + + val info = {name=name, class=class, avail=avail, options=options} + in + Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => + Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> + Context.theory_map (SMT2_Config.add_solver info) + end + +end + +fun get_info ctxt name = + the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) + +val solver_name_of = SMT2_Config.solver_of + +val available_solvers_of = SMT2_Config.available_solvers_of + +fun name_and_info_of ctxt = + let val name = solver_name_of ctxt + in (name, get_info ctxt name) end + +fun gen_preprocess ctxt iwthms = SMT2_Normalize.normalize iwthms ctxt + +fun gen_apply (ithms, ctxt) = + let val (name, {command, replay, ...}) = name_and_info_of ctxt + in + (ithms, ctxt) + |-> invoke name command + |> replay ctxt + |>> distinct (op =) + end + +fun apply_solver ctxt = gen_apply o gen_preprocess ctxt + +val default_max_relevant = #default_max_relevant oo get_info + +val supports_filter = #supports_filter o snd o name_and_info_of + + +(* check well-sortedness *) + +val has_topsort = Term.exists_type (Term.exists_subtype (fn + TFree (_, []) => true + | TVar (_, []) => true + | _ => false)) + +(* without this test, we would run into problems when atomizing the rules: *) +fun check_topsort ctxt thm = + if has_topsort (Thm.prop_of thm) then + (SMT2_Normalize.drop_fact_warning ctxt thm; TrueI) + else + thm + +fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms + + +(* filter *) + +val cnot = Thm.cterm_of @{theory} @{const Not} + +fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } + +type 'a smt2_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) + +fun smt2_filter_preprocess ctxt facts goal xwthms i = + let + val ctxt = + ctxt + |> Config.put SMT2_Config.oracle false + |> Config.put SMT2_Config.filter_only_facts true + + val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal + fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply + val cprop = + (case try negate (Thm.rhs_of (SMT2_Normalize.atomize_conv ctxt' concl)) of + SOME ct => ct + | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ( + "goal is not a HOL term"))) + in + map snd xwthms + |> map_index I + |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) + |> check_topsorts ctxt' + |> gen_preprocess ctxt' + |> pair (map (apsnd snd) xwthms) + end + +fun smt2_filter_apply time_limit (xthms, (ithms, ctxt)) = + let + val ctxt' = + ctxt + |> Config.put SMT2_Config.timeout (Time.toReal time_limit) + + fun filter_thms false = K xthms + | filter_thms true = map_filter (try (nth xthms)) o fst + in + (ithms, ctxt') + |> gen_apply + |> filter_thms (supports_filter ctxt') + |> mk_result NONE + end + handle SMT2_Failure.SMT fail => mk_result (SOME fail) [] + + +(* SMT tactic *) + +local + fun trace_assumptions ctxt iwthms idxs = + let + val wthms = + idxs + |> filter (fn i => i >= 0) + |> map_filter (AList.lookup (op =) iwthms) + in + if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 + then + tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" + (map (Display.pretty_thm ctxt o snd) wthms))) + else () + end + + fun solve ctxt iwthms = + iwthms + |> check_topsorts ctxt + |> apply_solver ctxt + |>> trace_assumptions ctxt iwthms + |> snd + + fun str_of ctxt fail = + SMT2_Failure.string_of_failure ctxt fail + |> prefix ("Solver " ^ SMT2_Config.solver_of ctxt ^ ": ") + + fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) + handle + SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) => + (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) + | SMT2_Failure.SMT (fail as SMT2_Failure.Time_Out) => + error ("SMT: Solver " ^ quote (SMT2_Config.solver_of ctxt) ^ ": " ^ + SMT2_Failure.string_of_failure ctxt fail ^ " (setting the " ^ + "configuration option " ^ quote (Config.name_of SMT2_Config.timeout) ^ " might help)") + | SMT2_Failure.SMT fail => error (str_of ctxt fail) + + fun tag_rules thms = map_index (apsnd (pair NONE)) thms + fun tag_prems thms = map (pair ~1 o pair NONE) thms + + fun resolve (SOME thm) = rtac thm 1 + | resolve NONE = no_tac + + fun tac prove ctxt rules = + CONVERSION (SMT2_Normalize.atomize_conv ctxt) + THEN' rtac @{thm ccontr} + THEN' SUBPROOF (fn {context, prems, ...} => + resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt +in + +val smt2_tac = tac safe_solve +val smt2_tac' = tac (SOME oo solve) + +end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,540 @@ +(* Title: HOL/Tools/SMT2/smt2_translate.ML + Author: Sascha Boehme, TU Muenchen + +Translate theorems into an SMT intermediate format and serialize them. +*) + +signature SMT2_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 | + SApp of string * sterm list | + SLet of string * sterm * sterm | + SQua of squant * string list * sterm spattern list * int option * sterm + + (*translation configuration*) + type sign = { + header: string, + sorts: string list, + dtyps: (string * (string * (string * string) list) list) list list, + funcs: (string * (string list * string)) list } + type config = { + header: term list -> string, + has_datatypes: bool, + serialize: string list -> sign -> sterm list -> string } + type replay_data = { + context: Proof.context, + typs: typ Symtab.table, + terms: term Symtab.table, + rewrite_rules: thm list, + assms: (int * thm) list } + + (*translation*) + val add_config: SMT2_Utils.class * (Proof.context -> config) -> Context.generic -> Context.generic + val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data +end + +structure SMT2_Translate: SMT2_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 | + SApp of string * sterm list | + SLet of string * sterm * sterm | + SQua of squant * string list * sterm spattern list * int option * sterm + + + +(* translation configuration *) + +type sign = { + header: string, + sorts: string list, + dtyps: (string * (string * (string * string) list) list) list list, + funcs: (string * (string list * string)) list } + +type config = { + header: term list -> string, + has_datatypes: bool, + serialize: string list -> sign -> sterm list -> string } + +type replay_data = { + context: Proof.context, + typs: typ Symtab.table, + terms: term Symtab.table, + rewrite_rules: thm list, + assms: (int * 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_prefix = "$" + +fun add_typ T proper (cx as (names, typs, terms)) = + (case Typtab.lookup typs T of + SOME (name, _) => (name, cx) + | NONE => + let + val sugg = safe_prefix ^ Name.desymbolize true (suggested_name_of_typ T) + 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 = safe_prefix ^ Name.desymbolize false (suggested_name_of_term t) + val (name, names') = Name.variant sugg names + val terms' = Termtab.update (t, (name, sort)) terms + in (name, (names', typs, terms')) end) + +fun sign_of header dtyps (_, typs, terms) = { + header = header, + 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 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', rewrite_rules=rules, assms=assms} + end + + + +(* preprocessing *) + +(** datatype declarations **) + +fun collect_datatypes_and_records (tr_context, ctxt) ts = + let + val (declss, ctxt') = fold (Term.fold_types SMT2_Datatypes.add_decls) ts ([], ctxt) + + fun is_decl_typ T = exists (exists (equal T o fst)) declss + + fun add_typ' T proper = + (case SMT2_Builtin.dest_builtin_typ ctxt' T of + SOME n => pair n + | 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 (T, cases) = add_typ' T false ##>> fold_map tr_constr cases + val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context + + fun add (constr, selects) = + Termtab.update (constr, length selects) #> + fold (Termtab.update o rpair 1) selects + val funcs = fold (fold (fold add o snd)) declss Termtab.empty + in ((funcs, declss', tr_context', ctxt'), ts) end + (* FIXME: also return necessary datatype and record 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 (SMT2_Utils.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 ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = expand (Term.betapply (Abs a, t)) + | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = expand (u $ t) + | expand ((l as 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 + (u as Const (c as (_, T)), ts) => + (case SMT2_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 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 minimize types t i = + let + fun find_min j [] _ = j + | find_min j (U :: Us) T = + if Typtab.defined types T then j else find_min (j + 1) Us (U --> T) + + val (Ts, T) = Term.strip_type (Term.type_of t) + in find_min 0 (take i (rev Ts)) T end + + fun app u (t, T) = + (Const (@{const_name SMT2.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) = SMT2_Utils.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 (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty) + val arities' = Termtab.map (minimize types) arities (* FIXME: highly suspicious *) + + fun app_func t T ts = + if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) + else apply (the (Termtab.lookup arities' t)) t T ts + + fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_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 SMT2_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 SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ in_weight Ts t + | in_trigger Ts t = in_weight Ts t + and in_pats Ts ps = + in_list @{typ "SMT2.pattern list"} (in_list @{typ SMT2.pattern} (in_pat Ts)) ps + and in_pat Ts ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ traverse Ts t + | in_pat Ts ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = p $ traverse Ts t + | in_pat _ t = raise TERM ("bad pattern", [t]) + and in_weight Ts ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ traverse Ts t + | in_weight Ts t = traverse Ts t + and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) + in map (traverse []) ts end + +val fun_app_eq = mk_meta_eq @{thm SMT2.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}, + @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] + + exception BAD_PATTERN of unit + + fun wrap_in_if pat t = + if pat then raise BAD_PATTERN () + else @{const If (bool)} $ t $ @{const True} $ @{const False} + + fun is_builtin_conn_or_pred ctxt c ts = + is_some (SMT2_Builtin.dest_builtin_conn ctxt c ts) orelse + is_some (SMT2_Builtin.dest_builtin_pred ctxt c ts) +in + +fun folify ctxt = + let + fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t)) + + fun in_term pat t = + (case Term.strip_comb t of + (@{const True}, []) => t + | (@{const False}, []) => t + | (u as Const (@{const_name 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 then wrap_in_if pat (in_form t) + else if is_quant n then wrap_in_if pat (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_weight ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ in_form t + | in_weight t = in_form t + + and in_pat ((p as Const (@{const_name SMT2.pat}, _)) $ t) = + p $ in_term true t + | in_pat ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = + p $ in_term true t + | in_pat t = raise TERM ("bad pattern", [t]) + + and in_pats ps = + in_list @{typ "SMT2.pattern list"} + (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps + + and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = + c $ in_pats p $ in_weight t + | in_trigger t = in_weight 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 SMT2_Builtin.dest_builtin_conn ctxt c ts of + SOME (_, _, us, mk) => mk (map in_form us) + | NONE => + (case SMT2_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 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_weight (@{const SMT2.weight} $ w $ t) = (SOME (snd (HOLogic.dest_number w)), t) + | dest_weight t = (NONE, t) + +fun dest_pat (Const (@{const_name SMT2.pat}, _) $ t) = (t, true) + | dest_pat (Const (@{const_name SMT2.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 SMT2.trigger} $ tl $ t) = + (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_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 + val (w, b) = dest_weight p + in (q, rev Ts, ps, w, b) 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 header 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 SMT2_Builtin.dest_builtin_typ ctxt T of + SOME n => pair n + | NONE => add_typ T true) + + fun app n ts = SApp (n, ts) + + 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, w, b) => + fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> + trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) + | NONE => raise TERM ("unsupported quantifier", [t])) + | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => + transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2)) + | (u as Const (c as (_, T)), ts) => + (case builtin ctxt c ts of + SOME (n, _, us, _) => fold_map trans us #>> app n + | NONE => transs u T ts) + | (u as Free (_, T), ts) => transs u T ts + | (Bound i, []) => pair (SVar i) + | _ => raise TERM ("bad SMT term", [t])) + + and transs t T ts = + let val (Us, U) = SMT2_Utils.dest_funT (length ts) T + in + fold_map transT Us ##>> transT U #-> (fn Up => + add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) + end + + val (us, trx') = fold_map trans ts trx + in ((sign_of (header ts) dtyps trx', us), trx') end + + + +(* translation *) + +structure Configs = Generic_Data +( + type T = (Proof.context -> config) SMT2_Utils.dict + val empty = [] + val extend = I + fun merge data = SMT2_Utils.dict_merge fst data +) + +fun add_config (cs, cfg) = Configs.map (SMT2_Utils.dict_update (cs, cfg)) + +fun get_config ctxt = + let val cs = SMT2_Config.solver_class_of ctxt + in + (case SMT2_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of + SOME cfg => cfg ctxt + | NONE => error ("SMT: no translation configuration found " ^ + "for solver class " ^ quote (SMT2_Utils.string_of_class cs))) + end + +fun translate ctxt comments ithms = + let + val {header, has_datatypes, serialize} = get_config ctxt + + fun no_dtyps (tr_context, ctxt) ts = + ((Termtab.empty, [], tr_context, ctxt), ts) + + val ts1 = map (Envir.beta_eta_contract o SMT2_Utils.prop_of o snd) ithms + + val ((funcs, dtyps, tr_context, ctxt1), ts2) = + ((empty_tr_context, ctxt), ts1) + |-> (if has_datatypes then collect_datatypes_and_records else no_dtyps) + + 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 SMT2.pattern} + |> (fn T => Const (@{const_name SMT2.pat}, T) $ lhs) + |> HOLogic.mk_list @{typ SMT2.pattern} o single + |> HOLogic.mk_list @{typ "SMT2.pattern list"} o single + |> (fn t => @{const SMT2.trigger} $ t $ eq) + | mk_trigger t = t + + val (ctxt2, ts3) = + ts2 + |> eta_expand ctxt1 funcs + |> rpair ctxt1 + |-> Lambda_Lifting.lift_lambdas NONE is_binder + |-> (fn (ts', defs) => fn ctxt' => + map mk_trigger defs @ ts' + |> intro_explicit_application ctxt' funcs + |> pair ctxt') + + val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 + + val rewrite_rules' = fun_app_eq :: rewrite_rules + in + (ts4, tr_context) + |-> intermediate header dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2 + |>> uncurry (serialize comments) + ||> replay_data_of ctxt2 rewrite_rules' ithms + end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smt2_utils.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smt2_utils.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,224 @@ +(* Title: HOL/Tools/SMT2/smt2_utils.ML + Author: Sascha Boehme, TU Muenchen + +General utility functions. +*) + +signature SMT2_UTILS = +sig + (*basic combinators*) + val repeat: ('a -> 'a option) -> 'a -> 'a + val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b + + (*class dictionaries*) + type class = string list + val basicC: class + val string_of_class: class -> string + type 'a dict = (class * 'a) Ord_List.T + val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict + val dict_update: class * 'a -> 'a dict -> 'a dict + val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict + val dict_lookup: 'a dict -> class -> 'a list + val dict_get: 'a dict -> class -> 'a option + + (*types*) + val dest_funT: int -> typ -> typ list * typ + + (*terms*) + val dest_conj: term -> term * term + val dest_disj: term -> term * term + val under_quant: (term -> 'a) -> term -> 'a + val is_number: term -> bool + + (*patterns and instantiations*) + val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm + val destT1: ctyp -> ctyp + val destT2: ctyp -> ctyp + val instTs: ctyp list -> ctyp list * cterm -> cterm + val instT: ctyp -> ctyp * cterm -> cterm + val instT': cterm -> ctyp * cterm -> cterm + + (*certified terms*) + val certify: Proof.context -> term -> cterm + val typ_of: cterm -> typ + val dest_cabs: cterm -> Proof.context -> cterm * Proof.context + val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context + val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context + val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context + val mk_cprop: cterm -> cterm + val dest_cprop: cterm -> cterm + val mk_cequals: cterm -> cterm -> cterm + val term_of: cterm -> term + val prop_of: thm -> term + + (*conversions*) + val if_conv: (term -> bool) -> conv -> conv -> conv + val if_true_conv: (term -> bool) -> conv -> conv + val if_exists_conv: (term -> bool) -> conv -> conv + val binders_conv: (Proof.context -> conv) -> Proof.context -> conv + val under_quant_conv: (Proof.context * cterm list -> conv) -> + Proof.context -> conv + val prop_conv: conv -> conv +end + +structure SMT2_Utils: SMT2_UTILS = +struct + +(* basic combinators *) + +fun repeat f = + let fun rep x = (case f x of SOME y => rep y | NONE => x) + in rep end + +fun repeat_yield f = + let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y)) + in rep end + + +(* class dictionaries *) + +type class = string list + +val basicC = [] + +fun string_of_class [] = "basic" + | string_of_class cs = "basic." ^ space_implode "." cs + +type 'a dict = (class * 'a) Ord_List.T + +fun class_ord ((cs1, _), (cs2, _)) = + rev_order (list_ord fast_string_ord (cs1, cs2)) + +fun dict_insert (cs, x) d = + if AList.defined (op =) d cs then d + else Ord_List.insert class_ord (cs, x) d + +fun dict_map_default (cs, x) f = + dict_insert (cs, x) #> AList.map_entry (op =) cs f + +fun dict_update (e as (_, x)) = dict_map_default e (K x) + +fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) + +fun dict_lookup d cs = + let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE + in map_filter match d end + +fun dict_get d cs = + (case AList.lookup (op =) d cs of + NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs)) + | SOME x => SOME x) + + +(* types *) + +val dest_funT = + let + fun dest Ts 0 T = (rev Ts, T) + | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U + | dest _ _ T = raise TYPE ("not a function type", [T], []) + in dest [] end + + +(* terms *) + +fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u) + | dest_conj t = raise TERM ("not a conjunction", [t]) + +fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u) + | dest_disj t = raise TERM ("not a disjunction", [t]) + +fun under_quant f t = + (case t of + Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u + | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u + | _ => f t) + +val is_number = + let + fun is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = is_num (t :: env) u + | is_num env (Bound i) = i < length env andalso is_num env (nth env i) + | is_num _ t = can HOLogic.dest_number t + in is_num [] end + + +(* patterns and instantiations *) + +fun mk_const_pat thy name destT = + let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name)) + in (destT (Thm.ctyp_of_term cpat), cpat) end + +val destT1 = hd o Thm.dest_ctyp +val destT2 = hd o tl o Thm.dest_ctyp + +fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct +fun instT cU (cT, ct) = instTs [cU] ([cT], ct) +fun instT' ct = instT (Thm.ctyp_of_term ct) + + +(* certified terms *) + +fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt) + +fun typ_of ct = #T (Thm.rep_cterm ct) + +fun dest_cabs ct ctxt = + (case Thm.term_of ct of + Abs _ => + let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt + in (snd (Thm.dest_abs (SOME n) ct), ctxt') end + | _ => raise CTERM ("no abstraction", [ct])) + +val dest_all_cabs = repeat_yield (try o dest_cabs) + +fun dest_cbinder ct ctxt = + (case Thm.term_of ct of + Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt + | _ => raise CTERM ("not a binder", [ct])) + +val dest_all_cbinders = repeat_yield (try o dest_cbinder) + +val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop}) + +fun dest_cprop ct = + (case Thm.term_of ct of + @{const Trueprop} $ _ => Thm.dest_arg ct + | _ => raise CTERM ("not a property", [ct])) + +val equals = mk_const_pat @{theory} @{const_name "=="} destT1 +fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu + +val dest_prop = (fn @{const Trueprop} $ t => t | t => t) +fun term_of ct = dest_prop (Thm.term_of ct) +fun prop_of thm = dest_prop (Thm.prop_of thm) + + +(* conversions *) + +fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct + +fun if_true_conv pred cv = if_conv pred cv Conv.all_conv + +fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred) + +fun binders_conv cv ctxt = + Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt + +fun under_quant_conv cv ctxt = + let + fun quant_conv inside ctxt cvs ct = + (case Thm.term_of ct of + Const (@{const_name All}, _) $ Abs _ => + Conv.binder_conv (under_conv cvs) ctxt + | Const (@{const_name Ex}, _) $ Abs _ => + Conv.binder_conv (under_conv cvs) ctxt + | _ => if inside then cv (ctxt, cvs) else Conv.all_conv) ct + and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs) + in quant_conv false ctxt [] end + +fun prop_conv cv ct = + (case Thm.term_of ct of + @{const Trueprop} $ _ => Conv.arg_conv cv ct + | _ => raise CTERM ("not a property", [ct])) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smtlib2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smtlib2.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,199 @@ +(* Title: HOL/Tools/SMT2/smtlib2.ML + Author: Sascha Boehme, TU Muenchen + +Parsing and generating SMT-LIB 2. +*) + +signature SMTLIB2 = +sig + exception PARSE of int * string + datatype tree = + Num of int | + Dec of int * int | + Str of string | + Sym of string | + Key of string | + S of tree list + val parse: string list -> tree + val pretty_tree: tree -> Pretty.T + val str_of: tree -> string +end + +structure SMTLIB2: SMTLIB2 = +struct + +(* data structures *) + +exception PARSE of int * string + +datatype tree = + Num of int | + Dec of int * int | + Str of string | + Sym of string | + Key of string | + S of tree list + +datatype unfinished = None | String of string | Symbol of string + + + +(* utilities *) + +fun read_raw pred l cs = + (case take_prefix pred cs of + ([], []) => raise PARSE (l, "empty token") + | ([], c :: _) => raise PARSE (l, "unexpected character " ^ quote c) + | x => x) + + + +(* numerals and decimals *) + +fun int_of cs = fst (read_int cs) + +fun read_num l cs = + (case read_raw Symbol.is_ascii_digit l cs of + (cs1, "." :: cs') => + let val (cs2, cs'') = read_raw Symbol.is_ascii_digit l cs' + in (Dec (int_of cs1, int_of cs2), cs'') end + | (cs1, cs2) => (Num (int_of cs1), cs2)) + + + +(* binary numbers *) + +fun is_bin c = (c = "0" orelse c = "1") + +fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2 + + + +(* hex numbers *) + +val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF") + +fun within c1 c2 c = (ord c1 <= ord c andalso ord c <= ord c2) + +fun unhex i [] = i + | unhex i (c :: cs) = + if within "0" "9" c then unhex (i * 16 + (ord c - ord "0")) cs + else if within "a" "f" c then unhex (i * 16 + (ord c - ord "a" + 10)) cs + else if within "A" "F" c then unhex (i * 16 + (ord c - ord "A" + 10)) cs + else raise Fail ("bad hex character " ^ quote c) + +fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0 + + + +(* symbols *) + +val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-" + +fun is_sym c = + Symbol.is_ascii_letter c orelse + Symbol.is_ascii_digit c orelse + member (op =) symbol_chars c + +fun read_sym f l cs = read_raw is_sym l cs |>> f o implode + + + +(* quoted tokens *) + +fun read_quoted stop (escape, replacement) cs = + let + fun read _ [] = NONE + | read rs (cs as (c :: cs')) = + if is_prefix (op =) stop cs then + SOME (implode (rev rs), drop (length stop) cs) + else if not (null escape) andalso is_prefix (op =) escape cs then + read (replacement :: rs) (drop (length escape) cs) + else read (c :: rs) cs' + in read [] cs end + +fun read_string cs = read_quoted ["\\", "\""] (["\\", "\\"], "\\") cs +fun read_symbol cs = read_quoted ["|"] ([], "") cs + + + +(* core parser *) + +fun read _ [] rest tss = (rest, tss) + | read l ("(" :: cs) None tss = read l cs None ([] :: tss) + | read l (")" :: cs) None (ts1 :: ts2 :: tss) = + 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) = + token read_bin l cs ts tss + | read l (":" :: cs) None (ts :: tss) = + token (read_sym Key) l cs ts tss + | read l ("\"" :: cs) None (ts :: tss) = + quoted read_string String Str l "" cs ts tss + | read l ("|" :: cs) None (ts :: tss) = + quoted read_symbol Symbol Sym l "" cs ts tss + | read l ((c as "!") :: cs) None (ts :: tss) = + token (fn _ => pair (Sym c)) l cs ts tss + | read l (c :: cs) None (ts :: tss) = + if Symbol.is_ascii_blank c then read l cs None (ts :: tss) + else if Symbol.is_digit c then token read_num l (c :: cs) ts tss + else token (read_sym Sym) l (c :: cs) ts tss + | read l cs (String s) (ts :: tss) = + quoted read_string String Str l s cs ts tss + | read l cs (Symbol s) (ts :: tss) = + quoted read_symbol Symbol Sym l s cs ts tss + | read l _ _ [] = raise PARSE (l, "bad parser state") + +and token f l cs ts tss = + let val (t, cs') = f l cs + in read l cs' None ((t :: ts) :: tss) end + +and quoted r f g l s cs ts tss = + (case r cs of + NONE => (f (s ^ implode cs), ts :: tss) + | SOME (s', cs') => read l cs' None ((g (s ^ s') :: ts) :: tss)) + + + +(* overall parser *) + +fun read_line l line = read l (raw_explode line) + +fun add_line line (l, (None, tss)) = + if size line = 0 orelse nth_string line 0 = ";" then (l + 1, (None, tss)) + else (l + 1, read_line l line None tss) + | add_line line (l, (unfinished, tss)) = + (l + 1, read_line l line unfinished tss) + +fun finish (_, (None, [[t]])) = t + | finish (l, _) = raise PARSE (l, "bad nesting") + +fun parse lines = finish (fold add_line lines (1, (None, [[]]))) + + + +(* pretty printer *) + +fun pretty_tree (Num i) = Pretty.str (string_of_int i) + | pretty_tree (Dec (i, j)) = + Pretty.str (string_of_int i ^ "." ^ string_of_int j) + | pretty_tree (Str s) = + raw_explode s + |> maps (fn "\"" => ["\\", "\""] | "\\" => ["\\", "\\"] | c => [c]) + |> implode + |> enclose "\"" "\"" + |> Pretty.str + | pretty_tree (Sym s) = + if String.isPrefix "(" s (* for bit vector functions *) orelse + forall is_sym (raw_explode s) then + Pretty.str s + else + Pretty.str ("|" ^ s ^ "|") + | pretty_tree (Key s) = Pretty.str (":" ^ s) + | pretty_tree (S trees) = + Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees)) + +val str_of = Pretty.str_of o pretty_tree + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/smtlib2_interface.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,156 @@ +(* Title: HOL/Tools/SMT2/smtlib2_interface.ML + Author: Sascha Boehme, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Interface to SMT solvers based on the SMT-LIB 2 format. +*) + +signature SMTLIB2_INTERFACE = +sig + val smtlib2C: SMT2_Utils.class + val add_logic: int * (term list -> string option) -> Context.generic -> + Context.generic + val translate_config: Proof.context -> SMT2_Translate.config +end + +structure SMTLIB2_Interface: SMTLIB2_INTERFACE = +struct + +val smtlib2C = ["smtlib2"] + + +(* builtins *) + +local + fun int_num _ i = SOME (string_of_int i) + + fun is_linear [t] = SMT2_Utils.is_number t + | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u + | is_linear _ = false + + fun times _ _ ts = + let val mk = Term.list_comb o pair @{const times (int)} + in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end +in + +val setup_builtins = + fold (SMT2_Builtin.add_builtin_typ smtlib2C) [ + (@{typ bool}, K (SOME "Bool"), K (K NONE)), + (@{typ int}, K (SOME "Int"), int_num)] #> + fold (SMT2_Builtin.add_builtin_fun' smtlib2C) [ + (@{const True}, "true"), + (@{const False}, "false"), + (@{const Not}, "not"), + (@{const HOL.conj}, "and"), + (@{const HOL.disj}, "or"), + (@{const HOL.implies}, "=>"), + (@{const HOL.eq ('a)}, "="), + (@{const If ('a)}, "ite"), + (@{const less (int)}, "<"), + (@{const less_eq (int)}, "<="), + (@{const uminus (int)}, "~"), + (@{const plus (int)}, "+"), + (@{const minus (int)}, "-")] #> + SMT2_Builtin.add_builtin_fun smtlib2C + (Term.dest_Const @{const times (int)}, times) + +end + + +(* serialization *) + +(** header **) + +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) + +structure Logics = Generic_Data +( + type T = (int * (term list -> string option)) list + val empty = [] + val extend = I + fun merge data = Ord_List.merge fst_int_ord data +) + +fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf) + +fun choose_logic ctxt ts = + let + fun choose [] = "AUFLIA" + | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) + in "(set-logic " ^ choose (Logics.get (Context.Proof ctxt)) ^ ")\n" end + + +(** serialization **) + +fun var i = "?v" ^ string_of_int i + +fun tree_of_sterm l (SMT2_Translate.SVar i) = SMTLIB2.Sym (var (l - i - 1)) + | tree_of_sterm _ (SMT2_Translate.SApp (n, [])) = SMTLIB2.Sym n + | tree_of_sterm l (SMT2_Translate.SApp (n, ts)) = + SMTLIB2.S (SMTLIB2.Sym n :: map (tree_of_sterm l) ts) + | tree_of_sterm _ (SMT2_Translate.SLet _) = + raise Fail "SMT-LIB: unsupported let expression" + | tree_of_sterm l (SMT2_Translate.SQua (q, ss, pats, w, t)) = + let + val l' = l + length ss + + fun quant_name SMT2_Translate.SForall = "forall" + | quant_name SMT2_Translate.SExists = "exists" + + fun gen_trees_of_pat keyword ps = + [SMTLIB2.Key keyword, (case map (tree_of_sterm l') ps of [t] => t | ts => SMTLIB2.S ts)] + fun trees_of_pat (SMT2_Translate.SPat ps) = gen_trees_of_pat "pattern" ps + | trees_of_pat (SMT2_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps + fun trees_of_weight NONE = [] + | trees_of_weight (SOME i) = [SMTLIB2.Key "weight", SMTLIB2.Num i] + fun tree_of_pats_weight [] NONE t = t + | tree_of_pats_weight pats w t = + SMTLIB2.S (SMTLIB2.Sym "!" :: t :: maps trees_of_pat pats @ trees_of_weight w) + + val vs = map_index (fn (i, ty) => + SMTLIB2.S [SMTLIB2.Sym (var (l + i)), SMTLIB2.Sym ty]) ss + + val body = t + |> tree_of_sterm l' + |> tree_of_pats_weight pats w + in + SMTLIB2.S [SMTLIB2.Sym (quant_name q), SMTLIB2.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 serialize comments {header, sorts, dtyps, funcs} ts = + Buffer.empty + |> fold (Buffer.add o enclose "; " "\n") comments + |> Buffer.add "(set-option :produce-proofs true)\n" + |> Buffer.add header + |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") + (sort fast_string_ord sorts) + |> (if null dtyps then I + else Buffer.add (enclose "(declare-datatypes () (" "))\n" + (space_implode "\n " (maps (map sdatatype) dtyps)))) + |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun) + (sort (fast_string_ord o pairself fst) funcs) + |> fold (Buffer.add o enclose "(assert " ")\n" o SMTLIB2.str_of o + tree_of_sterm 0) ts + |> Buffer.add "(check-sat)\n" + |> Buffer.add "(get-proof)\n" + |> Buffer.content + +(* interface *) + +fun translate_config ctxt = { + header = choose_logic ctxt, + has_datatypes = false, + serialize = serialize} + +val _ = Theory.setup (Context.theory_map + (setup_builtins #> + SMT2_Translate.add_config (smtlib2C, translate_config))) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_interface.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,220 @@ +(* Title: HOL/Tools/SMT2/z3_new_interface.ML + Author: Sascha Boehme, TU Muenchen + +Interface to Z3 based on a relaxed version of SMT-LIB. +*) + +signature Z3_NEW_INTERFACE = +sig + val smtlib2_z3C: SMT2_Utils.class + + datatype sym = Sym of string * sym list + type mk_builtins = { + mk_builtin_typ: sym -> typ option, + mk_builtin_num: theory -> int -> typ -> cterm option, + mk_builtin_fun: theory -> sym -> cterm list -> cterm option } + val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic + val mk_builtin_typ: Proof.context -> sym -> typ option + val mk_builtin_num: Proof.context -> int -> typ -> cterm option + val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option + + val is_builtin_theory_term: Proof.context -> term -> bool +end + +structure Z3_New_Interface: Z3_NEW_INTERFACE = +struct + +val smtlib2_z3C = SMTLIB2_Interface.smtlib2C @ ["z3"] + + + +(* interface *) + +local + fun translate_config ctxt = + let + val {serialize, ...} = SMTLIB2_Interface.translate_config ctxt + in + {header=K "", serialize=serialize, has_datatypes=true} + end + + fun is_div_mod @{const div (int)} = true + | is_div_mod @{const mod (int)} = true + | is_div_mod _ = false + + val div_as_z3div = @{lemma + "ALL k l. k div l = ( + if k = 0 | l = 0 then 0 + else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l + else z3div (-k) (-l))" + by (simp add: SMT2.z3div_def)} + + val mod_as_z3mod = @{lemma + "ALL k l. k mod l = ( + if l = 0 then k + else if k = 0 then 0 + else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l + else - z3mod (-k) (-l))" + by (simp add: z3mod_def)} + + val have_int_div_mod = + exists (Term.exists_subterm is_div_mod o Thm.prop_of) + + fun add_div_mod _ (thms, extra_thms) = + if have_int_div_mod thms orelse have_int_div_mod extra_thms then + (thms, div_as_z3div :: mod_as_z3mod :: extra_thms) + else (thms, extra_thms) + + val setup_builtins = + SMT2_Builtin.add_builtin_fun' smtlib2_z3C (@{const times (int)}, "*") #> + SMT2_Builtin.add_builtin_fun' smtlib2_z3C (@{const z3div}, "div") #> + SMT2_Builtin.add_builtin_fun' smtlib2_z3C (@{const z3mod}, "mod") +in + +val _ = Theory.setup (Context.theory_map ( + setup_builtins #> + SMT2_Normalize.add_extra_norm (smtlib2_z3C, add_div_mod) #> + SMT2_Translate.add_config (smtlib2_z3C, translate_config))) + +end + + + +(* constructors *) + +datatype sym = Sym of string * sym list + + +(** additional constructors **) + +type mk_builtins = { + mk_builtin_typ: sym -> typ option, + mk_builtin_num: theory -> int -> typ -> cterm option, + mk_builtin_fun: theory -> sym -> cterm list -> cterm option } + +fun chained _ [] = NONE + | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) + +fun chained_mk_builtin_typ bs sym = + chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs + +fun chained_mk_builtin_num ctxt bs i T = + let val thy = Proof_Context.theory_of ctxt + in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end + +fun chained_mk_builtin_fun ctxt bs s cts = + let val thy = Proof_Context.theory_of ctxt + in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end + +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) + +structure Mk_Builtins = Generic_Data +( + type T = (int * mk_builtins) list + val empty = [] + val extend = I + fun merge data = Ord_List.merge fst_int_ord data +) + +fun add_mk_builtins mk = + Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) + +fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) + + +(** basic and additional constructors **) + +fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} + | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} + | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) + | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) + | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym + +fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) + | mk_builtin_num ctxt i T = + chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T + +val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False}) +val mk_false = Thm.cterm_of @{theory} @{const False} +val mk_not = Thm.apply (Thm.cterm_of @{theory} @{const Not}) +val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies}) +val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)}) +val conj = Thm.cterm_of @{theory} @{const HOL.conj} +val disj = Thm.cterm_of @{theory} @{const HOL.disj} + +fun mk_nary _ cu [] = cu + | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) + +val eq = SMT2_Utils.mk_const_pat @{theory} @{const_name HOL.eq} SMT2_Utils.destT1 +fun mk_eq ct cu = Thm.mk_binop (SMT2_Utils.instT' ct eq) ct cu + +val if_term = + SMT2_Utils.mk_const_pat @{theory} @{const_name If} + (SMT2_Utils.destT1 o SMT2_Utils.destT2) +fun mk_if cc ct cu = + Thm.mk_binop (Thm.apply (SMT2_Utils.instT' ct if_term) cc) ct cu + +val access = + SMT2_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT2_Utils.destT1 +fun mk_access array = Thm.apply (SMT2_Utils.instT' array access) array + +val update = SMT2_Utils.mk_const_pat @{theory} @{const_name fun_upd} + (Thm.dest_ctyp o SMT2_Utils.destT1) +fun mk_update array index value = + let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array) + in + Thm.apply (Thm.mk_binop (SMT2_Utils.instTs cTs update) array index) value + end + +val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)}) +val add = Thm.cterm_of @{theory} @{const plus (int)} +val int0 = Numeral.mk_cnumber @{ctyp int} 0 +val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)}) +val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)}) +val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div}) +val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod}) +val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)}) +val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)}) + +fun mk_builtin_fun ctxt sym cts = + (case (sym, cts) of + (Sym ("true", _), []) => SOME mk_true + | (Sym ("false", _), []) => SOME mk_false + | (Sym ("not", _), [ct]) => SOME (mk_not ct) + | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) + | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) + | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) + | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) + | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) + | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) + | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) + | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) + | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu) + | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) + | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) + | _ => + (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of + (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) + | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) + | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) + | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) + | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) + | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) + | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) + | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) + | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) + | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) + | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) + + + +(* abstraction *) + +fun is_builtin_theory_term ctxt t = + if SMT2_Builtin.is_builtin_num ctxt t then true + else + (case Term.strip_comb t of + (Const c, ts) => SMT2_Builtin.is_builtin_fun ctxt c ts + | _ => false) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_isar.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,109 @@ +(* Title: HOL/Tools/SMT2/z3_new_isar.ML + Author: Jasmin Blanchette, TU Muenchen + +Z3 proofs as generic ATP proofs for Isar proof reconstruction. +*) + +signature Z3_NEW_ISAR = +sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + + val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (term, string) atp_step list +end; + +structure Z3_New_Isar: Z3_NEW_ISAR = +struct + +open ATP_Util +open ATP_Problem +open ATP_Proof +open ATP_Proof_Reconstruct + +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 +val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def +val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Lemma + +fun inline_z3_defs _ [] = [] + | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) = + if rule = z3_intro_def_rule then + let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in + inline_z3_defs (insert (op =) def defs) + (map (replace_dependencies_in_line (name, [])) lines) + end + else if rule = z3_apply_def_rule then + inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines) + else + (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines + +fun add_z3_hypotheses [] = I + | add_z3_hypotheses hyps = + HOLogic.dest_Trueprop + #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps)) + #> HOLogic.mk_Trueprop + +fun inline_z3_hypotheses _ _ [] = [] + | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) = + if rule = z3_hypothesis_rule then + inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps) + lines + else + let val deps' = subtract (op =) hyp_names deps in + if rule = z3_lemma_rule then + (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines + else + let + val add_hyps = filter_out (null o inter (op =) deps o snd) hyps + val t' = add_z3_hypotheses (map fst add_hyps) t + val deps' = subtract (op =) hyp_names deps + val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps + in + (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines + end + end + +fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t) + | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u) + | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u) + | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u) + | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u) + | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u + | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t) + | simplify_prop t = t + +fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) + +fun atp_proof_of_z3_proof thy proof = + let + fun step_name_of id = (string_of_int id, []) + + (* FIXME: find actual conjecture *) + val id_of_last_asserted = + proof + |> rev |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted) + |> Option.map (fn Z3_New_Proof.Z3_Step {id, ...} => id) + + fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = + let + val role = + (case rule of + Z3_New_Proof.Asserted => + if id_of_last_asserted = SOME id then Negated_Conjecture else Hypothesis + | Z3_New_Proof.Rewrite => Lemma + | Z3_New_Proof.Rewrite_Star => Lemma + | Z3_New_Proof.Skolemize => Lemma + | Z3_New_Proof.Th_Lemma _ => Lemma + | _ => Plain) + in + (step_name_of id, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl), + Z3_New_Proof.string_of_rule rule, map step_name_of prems) + end + in + proof + |> map step_of + |> inline_z3_defs [] + |> inline_z3_hypotheses [] [] + |> map simplify_line + end + +end; diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,563 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof.ML + Author: Sascha Boehme, TU Muenchen + +Z3 proofs: parsing and abstract syntax tree. +*) + +signature Z3_NEW_PROOF = +sig + (*proof rules*) + datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | + Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | + Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | + Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | + Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | + Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def | + Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | + Modus_Ponens_Oeq | Th_Lemma of string + val string_of_rule: z3_rule -> string + + (*proofs*) + datatype z3_step = Z3_Step of { + id: int, + rule: z3_rule, + prems: int list, + concl: term, + fixes: string list, + is_fix_step: bool} + + (*type and term parsers*) + type type_parser = SMTLIB2.tree * typ list -> typ option + type term_parser = SMTLIB2.tree * term list -> term option + val add_type_parser: type_parser -> Context.generic -> Context.generic + val add_term_parser: term_parser -> Context.generic -> Context.generic + + (*proof parser*) + val parse: typ Symtab.table -> term Symtab.table -> string list -> + Proof.context -> z3_step list * Proof.context +end + +structure Z3_New_Proof: Z3_NEW_PROOF = +struct + +(* proof rules *) + +datatype z3_rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | + Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | + Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | + Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res | + Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False | + Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | + Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq | + Th_Lemma of string + (* TODO: some proof rules come with further information + that is currently dropped by the parser *) + +val rule_names = Symtab.make [ + ("true-axiom", True_Axiom), + ("asserted", Asserted), + ("goal", Goal), + ("mp", Modus_Ponens), + ("refl", Reflexivity), + ("symm", Symmetry), + ("trans", Transitivity), + ("trans*", Transitivity_Star), + ("monotonicity", Monotonicity), + ("quant-intro", Quant_Intro), + ("distributivity", Distributivity), + ("and-elim", And_Elim), + ("not-or-elim", Not_Or_Elim), + ("rewrite", Rewrite), + ("rewrite*", Rewrite_Star), + ("pull-quant", Pull_Quant), + ("pull-quant*", Pull_Quant_Star), + ("push-quant", Push_Quant), + ("elim-unused", Elim_Unused_Vars), + ("der", Dest_Eq_Res), + ("quant-inst", Quant_Inst), + ("hypothesis", Hypothesis), + ("lemma", Lemma), + ("unit-resolution", Unit_Resolution), + ("iff-true", Iff_True), + ("iff-false", Iff_False), + ("commutativity", Commutativity), + ("def-axiom", Def_Axiom), + ("intro-def", Intro_Def), + ("apply-def", Apply_Def), + ("iff~", Iff_Oeq), + ("nnf-pos", Nnf_Pos), + ("nnf-neg", Nnf_Neg), + ("nnf*", Nnf_Star), + ("cnf*", Cnf_Star), + ("sk", Skolemize), + ("mp~", Modus_Ponens_Oeq)] + +fun rule_of_string name = + (case Symtab.lookup rule_names name of + SOME rule => rule + | NONE => error ("unknown Z3 proof rule " ^ quote name)) + +fun string_of_rule (Th_Lemma kind) = "th-lemma " ^ kind + | string_of_rule r = + let fun eq_rule (s, r') = if r = r' then SOME s else NONE + in the (Symtab.get_first eq_rule rule_names) end + + + +(* proofs *) + +datatype z3_node = Z3_Node of { + id: int, + rule: z3_rule, + prems: z3_node list, + concl: term, + bounds: string list} + +fun mk_node id rule prems concl bounds = + Z3_Node {id=id, rule=rule, prems=prems, concl=concl, bounds=bounds} + +datatype z3_step = Z3_Step of { + id: int, + rule: z3_rule, + prems: int list, + concl: term, + fixes: string list, + is_fix_step: bool} + +fun mk_step id rule prems concl fixes is_fix_step = + Z3_Step {id=id, rule=rule, prems=prems, concl=concl, fixes=fixes, + is_fix_step=is_fix_step} + + + +(* core type and term parser *) + +fun core_type_parser (SMTLIB2.Sym "Bool", []) = SOME @{typ HOL.bool} + | core_type_parser (SMTLIB2.Sym "Int", []) = SOME @{typ Int.int} + | core_type_parser _ = NONE + +fun mk_unary n t = + let val T = fastype_of t + in Const (n, T --> T) $ t end + +fun mk_binary' n T U t1 t2 = Const (n, [T, T] ---> U) $ t1 $ t2 + +fun mk_binary n t1 t2 = + let val T = fastype_of t1 + in mk_binary' n T T t1 t2 end + +fun mk_rassoc f t ts = + let val us = rev (t :: ts) + in fold f (tl us) (hd us) end + +fun mk_lassoc f t ts = fold (fn u1 => fn u2 => f u2 u1) ts t + +fun mk_lassoc' n = mk_lassoc (mk_binary n) + +fun mk_binary_pred n S t1 t2 = + let + val T1 = fastype_of t1 + val T2 = fastype_of t2 + val T = + if T1 <> Term.dummyT then T1 + else if T2 <> Term.dummyT then T2 + else TVar (("?a", serial ()), S) + in mk_binary' n T @{typ HOL.bool} t1 t2 end + +fun mk_less t1 t2 = mk_binary_pred @{const_name ord_class.less} @{sort linorder} t1 t2 +fun mk_less_eq t1 t2 = mk_binary_pred @{const_name ord_class.less_eq} @{sort linorder} t1 t2 + +fun core_term_parser (SMTLIB2.Sym "true", _) = SOME @{const HOL.True} + | core_term_parser (SMTLIB2.Sym "false", _) = SOME @{const HOL.False} + | core_term_parser (SMTLIB2.Sym "not", [t]) = SOME (HOLogic.mk_not t) + | core_term_parser (SMTLIB2.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts) + | core_term_parser (SMTLIB2.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts) + | core_term_parser (SMTLIB2.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) + | core_term_parser (SMTLIB2.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) + | core_term_parser (SMTLIB2.Sym "=", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) + | core_term_parser (SMTLIB2.Sym "~", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) + | core_term_parser (SMTLIB2.Sym "ite", [t1, t2, t3]) = + let + val T = fastype_of t2 + val c = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T) + in SOME (c $ t1 $ t2 $ t3) end + | core_term_parser (SMTLIB2.Num i, []) = SOME (HOLogic.mk_number @{typ Int.int} i) + | core_term_parser (SMTLIB2.Sym "-", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t) + | core_term_parser (SMTLIB2.Sym "~", [t]) = SOME (mk_unary @{const_name uminus_class.uminus} t) + | core_term_parser (SMTLIB2.Sym "+", t :: ts) = + SOME (mk_lassoc' @{const_name plus_class.plus} t ts) + | core_term_parser (SMTLIB2.Sym "-", t :: ts) = + SOME (mk_lassoc' @{const_name minus_class.minus} t ts) + | core_term_parser (SMTLIB2.Sym "*", t :: ts) = + SOME (mk_lassoc' @{const_name times_class.times} t ts) + | core_term_parser (SMTLIB2.Sym "div", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3div} t1 t2) + | core_term_parser (SMTLIB2.Sym "mod", [t1, t2]) = SOME (mk_binary @{const_name SMT2.z3mod} t1 t2) + | core_term_parser (SMTLIB2.Sym "<", [t1, t2]) = SOME (mk_less t1 t2) + | core_term_parser (SMTLIB2.Sym ">", [t1, t2]) = SOME (mk_less t2 t1) + | core_term_parser (SMTLIB2.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2) + | core_term_parser (SMTLIB2.Sym ">=", [t1, t2]) = SOME (mk_less_eq t2 t1) + | core_term_parser _ = NONE + + + +(* type and term parsers *) + +type type_parser = SMTLIB2.tree * typ list -> typ option + +type term_parser = SMTLIB2.tree * term list -> term option + +fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2) + +structure Parsers = Generic_Data +( + type T = (int * type_parser) list * (int * term_parser) list + val empty = ([(serial (), core_type_parser)], [(serial (), core_term_parser)]) + val extend = I + fun merge ((tys1, ts1), (tys2, ts2)) = + (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2)) +) + +fun add_type_parser type_parser = + Parsers.map (apfst (Ord_List.insert id_ord (serial (), type_parser))) + +fun add_term_parser term_parser = + Parsers.map (apsnd (Ord_List.insert id_ord (serial (), term_parser))) + +fun get_type_parsers ctxt = map snd (fst (Parsers.get (Context.Proof ctxt))) +fun get_term_parsers ctxt = map snd (snd (Parsers.get (Context.Proof ctxt))) + +fun apply_parsers parsers x = + let + fun apply [] = NONE + | apply (parser :: parsers) = + (case parser x of + SOME y => SOME y + | NONE => apply parsers) + in apply parsers end + + + +(* proof parser context *) + +datatype shared = Tree of SMTLIB2.tree | Term of term | Proof of z3_node | None + +type 'a context = { + ctxt: Proof.context, + id: int, + syms: shared Symtab.table, + typs: typ Symtab.table, + funs: term Symtab.table, + extra: 'a} + +fun mk_context ctxt id syms typs funs extra: 'a context = + {ctxt=ctxt, id=id, syms=syms, typs=typs, funs=funs, extra=extra} + +fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs [] + +fun ctxt_of ({ctxt, ...}: 'a context) = ctxt + +fun next_id ({ctxt, id, syms, typs, funs, extra}: 'a context) = + (id, mk_context ctxt (id + 1) syms typs funs extra) + +fun lookup_binding ({syms, ...}: 'a context) = + the_default None o Symtab.lookup syms + +fun map_syms f ({ctxt, id, syms, typs, funs, extra}: 'a context) = + mk_context ctxt id (f syms) typs funs extra + +fun update_binding b = map_syms (Symtab.update b) + +fun with_bindings bs f cx = + let val bs' = map (lookup_binding cx o fst) bs + in + cx + |> fold update_binding bs + |> f + ||> fold2 (fn (name, _) => update_binding o pair name) bs bs' + end + +fun lookup_typ ({typs, ...}: 'a context) = Symtab.lookup typs +fun lookup_fun ({funs, ...}: 'a context) = Symtab.lookup funs + +fun fresh_fun add name n T ({ctxt, id, syms, typs, funs, extra}: 'a context) = + let + val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt + val t = Free (n', T) + val funs' = Symtab.update (name, t) funs + in (t, mk_context ctxt' id syms typs funs' (add (n', T) extra)) end + +fun declare_fun name n T = snd o fresh_fun cons name n T +fun declare_free name n T = fresh_fun (cons o pair name) name n T + +fun with_fresh_names f ({ctxt, id, syms, typs, funs, extra}: 'a context) = + let + fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t + + val needs_inferT = equal Term.dummyT orf Term.is_TVar + val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT) + fun infer_types ctxt = + singleton (Type_Infer_Context.infer_types ctxt) #> + singleton (Proof_Context.standard_term_check_finish ctxt) + fun infer ctxt t = if needs_infer t then infer_types ctxt t else t + + type bindings = (string * (string * typ)) list + val (t, {ctxt=ctxt', extra=names, ...}: bindings context) = + f (mk_context ctxt id syms typs funs []) + val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t)) + + in ((t', map fst names), mk_context ctxt id syms typs funs extra) end + + + +(* proof parser *) + +exception Z3_PARSE of string * SMTLIB2.tree + +val desymbolize = Name.desymbolize false o perhaps (try (unprefix "?")) + +fun parse_type cx ty Ts = + (case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of + SOME T => T + | NONE => + (case ty of + SMTLIB2.Sym name => + (case lookup_typ cx name of + SOME T => T + | NONE => raise Z3_PARSE ("unknown Z3 type", ty)) + | _ => raise Z3_PARSE ("bad Z3 type format", ty))) + +fun parse_term t ts cx = + (case apply_parsers (get_term_parsers (ctxt_of cx)) (t, ts) of + SOME u => (u, cx) + | NONE => + (case t of + SMTLIB2.Sym name => + (case lookup_fun cx name of + SOME u => (Term.list_comb (u, ts), cx) + | NONE => + if null ts then declare_free name (desymbolize name) Term.dummyT cx + else raise Z3_PARSE ("bad Z3 term", t)) + | _ => raise Z3_PARSE ("bad Z3 term format", t))) + +fun type_of cx ty = + (case try (parse_type cx ty) [] of + SOME T => T + | NONE => + (case ty of + SMTLIB2.S (ty' :: tys) => parse_type cx ty' (map (type_of cx) tys) + | _ => raise Z3_PARSE ("bad Z3 type", ty))) + +fun dest_var cx (SMTLIB2.S [SMTLIB2.Sym name, ty]) = (name, (desymbolize name, type_of cx ty)) + | dest_var _ v = raise Z3_PARSE ("bad Z3 quantifier variable format", v) + +fun dest_body (SMTLIB2.S (SMTLIB2.Sym "!" :: body :: _)) = dest_body body + | dest_body body = body + +fun dest_binding (SMTLIB2.S [SMTLIB2.Sym name, t]) = (name, Tree t) + | dest_binding b = raise Z3_PARSE ("bad Z3 let binding format", b) + +fun term_of t cx = + (case t of + SMTLIB2.S [SMTLIB2.Sym "forall", SMTLIB2.S vars, body] => + quant HOLogic.mk_all vars body cx + | SMTLIB2.S [SMTLIB2.Sym "exists", SMTLIB2.S vars, body] => + quant HOLogic.mk_exists vars body cx + | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, body] => + with_bindings (map dest_binding bindings) (term_of body) cx + | SMTLIB2.S (SMTLIB2.Sym "!" :: t :: _) => term_of t cx + | SMTLIB2.S (f :: args) => + cx + |> fold_map term_of args + |-> parse_term f + | SMTLIB2.Sym name => + (case lookup_binding cx name of + Tree u => + cx + |> term_of u + |-> (fn u' => pair u' o update_binding (name, Term u')) + | Term u => (u, cx) + | None => parse_term t [] cx + | _ => raise Z3_PARSE ("bad Z3 term format", t)) + | _ => parse_term t [] cx) + +and quant q vars body cx = + let val vs = map (dest_var cx) vars + in + cx + |> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body)) + |>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs + end + +fun rule_of (SMTLIB2.Sym name) = rule_of_string name + | rule_of (SMTLIB2.S (SMTLIB2.Sym "_" :: SMTLIB2.Sym name :: args)) = + (case (name, args) of + ("th-lemma", SMTLIB2.Sym kind :: _) => Th_Lemma kind + | _ => rule_of_string name) + | rule_of r = raise Z3_PARSE ("bad Z3 proof rule format", r) + +fun node_of p cx = + (case p of + SMTLIB2.Sym name => + (case lookup_binding cx name of + Proof node => (node, cx) + | Tree p' => + cx + |> node_of p' + |-> (fn node => pair node o update_binding (name, Proof node)) + | _ => raise Z3_PARSE ("bad Z3 proof format", p)) + | SMTLIB2.S [SMTLIB2.Sym "let", SMTLIB2.S bindings, p] => + with_bindings (map dest_binding bindings) (node_of p) cx + | SMTLIB2.S (name :: parts) => + let + val (ps, p) = split_last parts + val r = rule_of name + in + cx + |> fold_map node_of ps + ||>> with_fresh_names (term_of p) + ||>> next_id + |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns) + end + | _ => raise Z3_PARSE ("bad Z3 proof format", p)) + +fun dest_name (SMTLIB2.Sym name) = name + | dest_name t = raise Z3_PARSE ("bad name", t) + +fun dest_seq (SMTLIB2.S ts) = ts + | dest_seq t = raise Z3_PARSE ("bad Z3 proof format", t) + +fun parse' (SMTLIB2.S (SMTLIB2.Sym "set-logic" :: _) :: ts) cx = parse' ts cx + | parse' (SMTLIB2.S [SMTLIB2.Sym "declare-fun", n, tys, ty] :: ts) cx = + let + val name = dest_name n + val Ts = map (type_of cx) (dest_seq tys) + val T = type_of cx ty + in parse' ts (declare_fun name (desymbolize name) (Ts ---> T) cx) end + | parse' (SMTLIB2.S [SMTLIB2.Sym "proof", p] :: _) cx = node_of p cx + | parse' ts _ = raise Z3_PARSE ("bad Z3 proof declarations", SMTLIB2.S ts) + +fun parse_proof typs funs lines ctxt = + let + val ts = dest_seq (SMTLIB2.parse lines) + val (node, cx) = parse' ts (empty_context ctxt typs funs) + in (node, ctxt_of cx) end + handle SMTLIB2.PARSE (l, msg) => + error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg) + | Z3_PARSE (msg, t) => + error (msg ^ ": " ^ SMTLIB2.str_of t) + + + +(* handling of bound variables *) + +fun subst_of tyenv = + let fun add (ix, (S, T)) = cons (TVar (ix, S), T) + in Vartab.fold add tyenv [] end + +fun substTs_same subst = + let val applyT = Same.function (AList.lookup (op =) subst) + in Term_Subst.map_atypsT_same applyT end + +fun subst_types ctxt env bounds t = + let + val match = Sign.typ_match (Proof_Context.theory_of ctxt) + + val t' = singleton (Variable.polymorphic ctxt) t + val patTs = map snd (Term.strip_qnt_vars @{const_name all} t') + val objTs = map (the o Symtab.lookup env) bounds + val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty) + in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end + +fun eq_quant (@{const_name HOL.All}, _) (@{const_name HOL.All}, _) = true + | eq_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.Ex}, _) = true + | eq_quant _ _ = false + +fun opp_quant (@{const_name HOL.All}, _) (@{const_name HOL.Ex}, _) = true + | opp_quant (@{const_name HOL.Ex}, _) (@{const_name HOL.All}, _) = true + | opp_quant _ _ = false + +fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) = + if pred q1 q2 andalso T1 = T2 then + let val t = Var (("", i), T1) + in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end + else NONE + | with_quant _ _ _ = NONE + +fun dest_quant_pair i (@{term HOL.Not} $ t1, t2) = + Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2)) + | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2) + +fun dest_quant i t = + (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of + SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2)) + | NONE => raise TERM ("lift_quant", [t])) + +fun match_types ctxt pat obj = + (Vartab.empty, Vartab.empty) + |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj) + +fun strip_match ctxt pat i obj = + (case try (match_types ctxt pat) obj of + SOME (tyenv, _) => subst_of tyenv + | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj)) + +fun dest_all i (Const (@{const_name all}, _) $ (a as Abs (_, T, _))) = + dest_all (i + 1) (Term.betapply (a, Var (("", i), T))) + | dest_all i t = (i, t) + +fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t + +fun match_rule ctxt env (Z3_Node {bounds=bs', concl=t', ...}) bs t = + let + val t'' = singleton (Variable.polymorphic ctxt) t' + val (i, obj) = dest_alls (subst_types ctxt env bs t) + in + (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of + NONE => NONE + | SOME subst => + let + val applyT = Same.commit (substTs_same subst) + val patTs = map snd (Term.strip_qnt_vars @{const_name all} t'') + in SOME (Symtab.make (bs' ~~ map applyT patTs)) end) + end + + + +(* linearizing proofs and resolving types of bound variables *) + +fun has_step (tab, _) = Inttab.defined tab + +fun add_step id rule bounds concl is_fix_step ids (tab, sts) = + let val step = mk_step id rule ids concl bounds is_fix_step + in (id, (Inttab.update (id, ()) tab, step :: sts)) end + +fun is_fix_rule rule prems = + member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1 + +fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps = + if has_step steps id then (id, steps) + else + let + val t = subst_types ctxt env bounds concl + val add = add_step id rule bounds t + fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b + in + if is_fix_rule rule prems then + (case match_rule ctxt env (hd prems) bounds t of + NONE => rec_apply env false steps + | SOME env' => rec_apply env' true steps) + else rec_apply env false steps + end + +fun linearize ctxt node = + rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, [])))) + + + +(* overall proof parser *) + +fun parse typs funs lines ctxt = + let val (node, ctxt') = parse_proof typs funs lines ctxt + in (linearize ctxt' node, ctxt') end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof_literals.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof_literals.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,357 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof_literals.ML + Author: Sascha Boehme, TU Muenchen + +Proof tools related to conjunctions and disjunctions. +*) + +signature Z3_NEW_PROOF_LITERALS = +sig + (*literal table*) + type littab = thm Termtab.table + val make_littab: thm list -> littab + val insert_lit: thm -> littab -> littab + val delete_lit: thm -> littab -> littab + val lookup_lit: littab -> term -> thm option + val get_first_lit: (term -> bool) -> littab -> thm option + + (*rules*) + val true_thm: thm + val rewrite_true: thm + + (*properties*) + val is_conj: term -> bool + val is_disj: term -> bool + val exists_lit: bool -> (term -> bool) -> term -> bool + val negate: cterm -> cterm + + (*proof tools*) + val explode: bool -> bool -> bool -> term list -> thm -> thm list + val join: bool -> littab -> term -> thm + val prove_conj_disj_eq: cterm -> thm +end + +structure Z3_New_Proof_Literals: Z3_NEW_PROOF_LITERALS = +struct + + + +(* literal table *) + +type littab = thm Termtab.table + +fun make_littab thms = + fold (Termtab.update o `SMT2_Utils.prop_of) thms Termtab.empty + +fun insert_lit thm = Termtab.update (`SMT2_Utils.prop_of thm) +fun delete_lit thm = Termtab.delete (SMT2_Utils.prop_of thm) +fun lookup_lit lits = Termtab.lookup lits +fun get_first_lit f = + Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE) + + + +(* rules *) + +val true_thm = @{lemma "~False" by simp} +val rewrite_true = @{lemma "True == ~ False" by simp} + + + +(* properties and term operations *) + +val is_neg = (fn @{const Not} $ _ => true | _ => false) +fun is_neg' f = (fn @{const Not} $ t => f t | _ => false) +val is_dneg = is_neg' is_neg +val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false) +val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false) + +fun dest_disj_term' f = (fn + @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u) + | _ => NONE) + +val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE) +val dest_disj_term = + dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t) + +fun exists_lit is_conj P = + let + val dest = if is_conj then dest_conj_term else dest_disj_term + fun exists t = P t orelse + (case dest t of + SOME (t1, t2) => exists t1 orelse exists t2 + | NONE => false) + in exists end + +val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not}) + + + +(* proof tools *) + +(** explosion of conjunctions and disjunctions **) + +local + val precomp = Z3_New_Proof_Tools.precompose2 + + fun destc ct = Thm.dest_binop (Thm.dest_arg ct) + val dest_conj1 = precomp destc @{thm conjunct1} + val dest_conj2 = precomp destc @{thm conjunct2} + fun dest_conj_rules t = + dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2)) + + fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct))) + val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg + val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast} + val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast} + val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast} + val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast} + + fun dest_disj_rules t = + (case dest_disj_term' is_neg t of + SOME (true, true) => SOME (dest_disj2, dest_disj4) + | SOME (true, false) => SOME (dest_disj2, dest_disj3) + | SOME (false, true) => SOME (dest_disj1, dest_disj4) + | SOME (false, false) => SOME (dest_disj1, dest_disj3) + | NONE => NONE) + + fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))] + val dneg_rule = Z3_New_Proof_Tools.precompose destn @{thm notnotD} +in + +(* + explode a term into literals and collect all rules to be able to deduce + particular literals afterwards +*) +fun explode_term is_conj = + let + val dest = if is_conj then dest_conj_term else dest_disj_term + val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules + + fun add (t, rs) = Termtab.map_default (t, rs) + (fn rs' => if length rs' < length rs then rs' else rs) + + fun explode1 rules t = + (case dest t of + SOME (t1, t2) => + let val (rule1, rule2) = the (dest_rules t) + in + explode1 (rule1 :: rules) t1 #> + explode1 (rule2 :: rules) t2 #> + add (t, rev rules) + end + | NONE => add (t, rev rules)) + + fun explode0 (@{const Not} $ (@{const Not} $ t)) = + Termtab.make [(t, [dneg_rule])] + | explode0 t = explode1 [] t Termtab.empty + + in explode0 end + +(* + extract a literal by applying previously collected rules +*) +fun extract_lit thm rules = fold Z3_New_Proof_Tools.compose rules thm + + +(* + explode a theorem into its literals +*) +fun explode is_conj full keep_intermediate stop_lits = + let + val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules + val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty + + fun explode1 thm = + if Termtab.defined tab (SMT2_Utils.prop_of thm) then cons thm + else + (case dest_rules (SMT2_Utils.prop_of thm) of + SOME (rule1, rule2) => + explode2 rule1 thm #> + explode2 rule2 thm #> + keep_intermediate ? cons thm + | NONE => cons thm) + + and explode2 dest_rule thm = + if full orelse + exists_lit is_conj (Termtab.defined tab) (SMT2_Utils.prop_of thm) + then explode1 (Z3_New_Proof_Tools.compose dest_rule thm) + else cons (Z3_New_Proof_Tools.compose dest_rule thm) + + fun explode0 thm = + if not is_conj andalso is_dneg (SMT2_Utils.prop_of thm) + then [Z3_New_Proof_Tools.compose dneg_rule thm] + else explode1 thm [] + + in explode0 end + +end + + +(** joining of literals to conjunctions or disjunctions **) + +local + fun on_cprem i f thm = f (Thm.cprem_of thm i) + fun on_cprop f thm = f (Thm.cprop_of thm) + fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm) + fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 = + Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule + |> Z3_New_Proof_Tools.discharge thm1 |> Z3_New_Proof_Tools.discharge thm2 + + fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct) + + val conj_rule = precomp2 d1 d1 @{thm conjI} + fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2 + + val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast} + val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast} + val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast} + val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast} + + fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2 + | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2 + | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2 + | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2 + + fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u)) + | dest_conj t = raise TERM ("dest_conj", [t]) + + val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t)) + fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u) + | dest_disj t = raise TERM ("dest_disj", [t]) + + val precomp = Z3_New_Proof_Tools.precompose + val dnegE = precomp (single o d2 o d1) @{thm notnotD} + val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast} + fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t)) + + val precomp2 = Z3_New_Proof_Tools.precompose2 + fun dni f = apsnd f o Thm.dest_binop o f o d1 + val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast} + val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast} + val iff_const = @{const HOL.eq (bool)} + fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) = + f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t))) + | as_negIff _ _ = NONE +in + +fun join is_conj littab t = + let + val comp = if is_conj then comp_conj else comp_disj + val dest = if is_conj then dest_conj else dest_disj + + val lookup = lookup_lit littab + + fun lookup_rule t = + (case t of + @{const Not} $ (@{const Not} $ t) => + (Z3_New_Proof_Tools.compose dnegI, lookup t) + | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) => + (Z3_New_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t)) + | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) => + let fun rewr lit = lit COMP @{thm not_sym} + in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end + | _ => + (case as_dneg lookup t of + NONE => (Z3_New_Proof_Tools.compose negIffE, as_negIff lookup t) + | x => (Z3_New_Proof_Tools.compose dnegE, x))) + + fun join1 (s, t) = + (case lookup t of + SOME lit => (s, lit) + | NONE => + (case lookup_rule t of + (rewrite, SOME lit) => (s, rewrite lit) + | (_, NONE) => (s, comp (pairself join1 (dest t))))) + + in snd (join1 (if is_conj then (false, t) else (true, t))) end + +end + + +(** proving equality of conjunctions or disjunctions **) + +fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI}) + +local + val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp} + val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastforce} + val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp} +in +fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1 +fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2 +fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3 +end + +local + val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)} + fun contra_left conj thm = + let + val rules = explode_term conj (SMT2_Utils.prop_of thm) + fun contra_lits (t, rs) = + (case t of + @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs) + | _ => NONE) + in + (case Termtab.lookup rules @{const False} of + SOME rs => extract_lit thm rs + | NONE => + the (Termtab.get_first contra_lits rules) + |> pairself (extract_lit thm) + |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) + end + + val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})) + fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE} +in +fun contradict conj ct = + iff_intro (Z3_New_Proof_Tools.under_assumption (contra_left conj) ct) + (contra_right ct) +end + +local + fun prove_eq l r (cl, cr) = + let + fun explode' is_conj = explode is_conj true (l <> r) [] + fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm) + fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct) + + val thm1 = Z3_New_Proof_Tools.under_assumption (prove r cr o make_tab l) cl + val thm2 = Z3_New_Proof_Tools.under_assumption (prove l cl o make_tab r) cr + in iff_intro thm1 thm2 end + + datatype conj_disj = CONJ | DISJ | NCON | NDIS + fun kind_of t = + if is_conj t then SOME CONJ + else if is_disj t then SOME DISJ + else if is_neg' is_conj t then SOME NCON + else if is_neg' is_disj t then SOME NDIS + else NONE +in + +fun prove_conj_disj_eq ct = + let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct) + in + (case (kind_of (Thm.term_of cl), Thm.term_of cr) of + (SOME CONJ, @{const False}) => contradict true cl + | (SOME DISJ, @{const Not} $ @{const False}) => + contrapos2 (contradict false o fst) cp + | (kl, _) => + (case (kl, kind_of (Thm.term_of cr)) of + (SOME CONJ, SOME CONJ) => prove_eq true true cp + | (SOME CONJ, SOME NDIS) => prove_eq true false cp + | (SOME CONJ, _) => prove_eq true true cp + | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp + | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp + | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp + | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp + | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp + | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp + | (SOME NDIS, SOME NDIS) => prove_eq false false cp + | (SOME NDIS, SOME CONJ) => prove_eq false true cp + | (SOME NDIS, NONE) => prove_eq false true cp + | _ => raise CTERM ("prove_conj_disj_eq", [ct]))) + end + +end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof_methods.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof_methods.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,667 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof.ML + Author: Sascha Boehme, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Proof methods for replaying Z3 proofs. +*) + +signature Z3_NEW_PROOF_METHODS = +sig + (*abstraction*) + type abs_context = int * term Termtab.table + type 'a abstracter = term -> abs_context -> 'a * abs_context + val add_arith_abstracter: (term abstracter -> term option abstracter) -> + Context.generic -> Context.generic + + (*theory lemma methods*) + type th_lemma_method = Proof.context -> thm list -> term -> thm + val add_th_lemma_method: string * th_lemma_method -> Context.generic -> + Context.generic + + (*methods for Z3 proof rules*) + type z3_method = Proof.context -> thm list -> term -> thm + val true_axiom: z3_method + val mp: z3_method + val refl: z3_method + val symm: z3_method + val trans: z3_method + val cong: z3_method + val quant_intro: z3_method + val distrib: z3_method + val and_elim: z3_method + val not_or_elim: z3_method + val rewrite: z3_method + val rewrite_star: z3_method + val pull_quant: z3_method + val push_quant: z3_method + val elim_unused: z3_method + val dest_eq_res: z3_method + val quant_inst: z3_method + val lemma: z3_method + val unit_res: z3_method + val iff_true: z3_method + val iff_false: z3_method + val comm: z3_method + val def_axiom: z3_method + val apply_def: z3_method + val iff_oeq: z3_method + val nnf_pos: z3_method + val nnf_neg: z3_method + val mp_oeq: z3_method + val th_lemma: string -> z3_method + val is_assumption: Z3_New_Proof.z3_rule -> bool + val method_for: Z3_New_Proof.z3_rule -> z3_method +end + +structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS = +struct + +type z3_method = Proof.context -> thm list -> term -> thm + + + +(* utility functions *) + +val trace = SMT2_Config.trace_msg + +fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm) + +fun pretty_goal ctxt msg rule thms t = + let + val full_msg = msg ^ ": " ^ quote (Z3_New_Proof.string_of_rule rule) + val assms = + if null thms then [] + else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)] + val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t] + in Pretty.big_list full_msg (assms @ [concl]) end + +fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t)) + +fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step" + +fun trace_goal ctxt rule thms t = + trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t)) + +fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t + | as_prop t = HOLogic.mk_Trueprop t + +fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t + | dest_prop t = t + +fun dest_thm thm = dest_prop (Thm.concl_of thm) + +fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t) + +fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t + | try_provers ctxt rule ((name, prover) :: named_provers) thms t = + (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of + SOME thm => thm + | NONE => try_provers ctxt rule named_provers thms t) + +fun match ctxt pat t = + (Vartab.empty, Vartab.empty) + |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t) + +fun gen_certify_inst sel mk cert ctxt thm t = + let + val inst = match ctxt (dest_thm thm) (dest_prop t) + fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b) + in Vartab.fold (cons o cert_inst) (sel inst) [] end + +fun match_instantiateT ctxt t thm = + if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then + let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt) + in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end + else thm + +fun match_instantiate ctxt t thm = + let + val cert = SMT2_Utils.certify ctxt + val thm' = match_instantiateT ctxt t thm + in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end + +fun apply_rule ctxt t = + (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of + SOME thm => thm + | NONE => raise Fail "apply_rule") + +fun discharge _ [] thm = thm + | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm)) + +fun by_tac ctxt thms ns ts t tac = + Goal.prove ctxt [] (map as_prop ts) (as_prop t) + (fn {context, prems} => HEADGOAL (tac context prems)) + |> Drule.generalize ([], ns) + |> discharge 1 thms + +fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac) + +fun prop_tac ctxt prems = + Method.insert_tac prems THEN' (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) + +fun quant_tac ctxt = Blast.blast_tac ctxt + + + +(* plug-ins *) + +type abs_context = int * term Termtab.table + +type 'a abstracter = term -> abs_context -> 'a * abs_context + +type th_lemma_method = Proof.context -> thm list -> term -> thm + +fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2) + +structure Plugins = Generic_Data +( + type T = + (int * (term abstracter -> term option abstracter)) list * + th_lemma_method Symtab.table + val empty = ([], Symtab.empty) + val extend = I + fun merge ((abss1, ths1), (abss2, ths2)) = ( + Ord_List.merge id_ord (abss1, abss2), + Symtab.merge (K true) (ths1, ths2)) +) + +fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs))) +fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt))) + +fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method)) +fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt)) + + + +(* abstraction *) + +fun prove_abstract ctxt thms t tac f = + let + val ((prems, concl), (_, ts)) = f (1, Termtab.empty) + val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts [] + in + by_tac ctxt [] ns prems concl tac + |> match_instantiate ctxt t + |> discharge 1 thms + end + +fun prove_abstract' ctxt t tac f = + prove_abstract ctxt [] t tac (f #>> pair []) + +fun lookup_term (_, terms) t = Termtab.lookup terms t + +fun abstract_sub t f cx = + (case lookup_term cx t of + SOME v => (v, cx) + | NONE => f cx) + +fun mk_fresh_free t (i, terms) = + let val v = Free ("t" ^ string_of_int i, fastype_of t) + in (v, (i + 1, Termtab.update (t, v) terms)) end + +fun apply_abstracters _ [] _ cx = (NONE, cx) + | apply_abstracters abs (abstracter :: abstracters) t cx = + (case abstracter abs t cx of + (NONE, _) => apply_abstracters abs abstracters t cx + | x as (SOME _, _) => x) + +fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t) + | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t) + | abstract_term t = pair t + +fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f) + +fun abstract_ter abs f t t1 t2 t3 = + abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f)) + +fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not + | abstract_lit t = abstract_term t + +fun abstract_not abs (t as @{const HOL.Not} $ t1) = + abstract_sub t (abs t1 #>> HOLogic.mk_not) + | abstract_not _ t = abstract_lit t + +fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) = + abstract_bin abstract_conj HOLogic.mk_conj t t1 t2 + | abstract_conj t = abstract_lit t + +fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) = + abstract_bin abstract_disj HOLogic.mk_disj t t1 t2 + | abstract_disj t = abstract_lit t + +fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) = + abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3 + | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) = + abstract_bin abstract_prop HOLogic.mk_disj t t1 t2 + | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) = + abstract_bin abstract_prop HOLogic.mk_conj t t1 t2 + | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) = + abstract_bin abstract_prop HOLogic.mk_imp t t1 t2 + | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) = + abstract_bin abstract_prop HOLogic.mk_eq t t1 t2 + | abstract_prop t = abstract_not abstract_prop t + +fun abstract_arith ctxt u = + let + fun abs (t as (c as Const _) $ Abs (s, T, t')) = + abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u'))) + | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) = + abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3 + | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not) + | abs (t as @{const HOL.disj} $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj) + | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) = + abstract_sub t (abs t1 #>> (fn u => c $ u)) + | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) = + abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) + | abs t = abstract_sub t (fn cx => + if can HOLogic.dest_number t then (t, cx) + else + (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of + (SOME u, cx') => (u, cx') + | (NONE, _) => abstract_term t cx)) + in abs u end + + + +(* truth axiom *) + +fun true_axiom _ _ _ = @{thm TrueI} + + + +(* modus ponens *) + +fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1 + | mp ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Modus_Ponens thms t + +val mp_oeq = mp + + + +(* reflexivity *) + +fun refl ctxt _ t = match_instantiate ctxt t @{thm refl} + + + +(* symmetry *) + +fun symm _ [thm] _ = thm RS @{thm sym} + | symm ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Reflexivity thms t + + + +(* transitivity *) + +fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans})) + | trans ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Transitivity thms t + + + +(* congruence *) + +fun ctac prems i st = st |> ( + resolve_tac (@{thm refl} :: prems) i + ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i)) + +fun cong_basic ctxt thms t = + let val st = Thm.trivial (certify_prop ctxt t) + in + (case Seq.pull (ctac thms 1 st) of + SOME (thm, _) => thm + | NONE => raise THM ("cong", 0, thms @ [st])) + end + +val cong_dest_rules = @{lemma + "(~ P | Q) & (P | ~ Q) ==> P = Q" + "(P | ~ Q) & (~ P | Q) ==> P = Q" + by fast+} + +fun cong_full ctxt thms t = prove ctxt t (fn ctxt' => + Method.insert_tac thms + THEN' (Classical.fast_tac ctxt' + ORELSE' dresolve_tac cong_dest_rules + THEN' Classical.fast_tac ctxt')) + +fun cong ctxt thms = try_provers ctxt Z3_New_Proof.Monotonicity [ + ("basic", cong_basic ctxt thms), + ("full", cong_full ctxt thms)] thms + + + +(* quantifier introduction *) + +val quant_intro_rules = @{lemma + "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)" + "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)" + "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)" + "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)" + by fast+} + +fun quant_intro ctxt [thm] t = + prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules)))) + | quant_intro ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Quant_Intro thms t + + + +(* distributivity of conjunctions and disjunctions *) + +(* TODO: there are no tests with this proof rule *) +fun distrib ctxt _ t = + prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t)) + + + +(* elimination of conjunctions *) + +fun and_elim ctxt [thm] t = + prove_abstract ctxt [thm] t prop_tac ( + abstract_lit (dest_prop t) ##>> + abstract_conj (dest_thm thm) #>> + apfst single o swap) + | and_elim ctxt thms t = replay_rule_error ctxt Z3_New_Proof.And_Elim thms t + + + +(* elimination of negated disjunctions *) + +fun not_or_elim ctxt [thm] t = + prove_abstract ctxt [thm] t prop_tac ( + abstract_lit (dest_prop t) ##>> + abstract_not abstract_disj (dest_thm thm) #>> + apfst single o swap) + | not_or_elim ctxt thms t = + replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t + + + +(* rewriting *) + +fun abstract_eq f1 f2 (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = + f1 t1 ##>> f2 t2 #>> HOLogic.mk_eq + | abstract_eq _ _ t = abstract_term t + +fun prove_prop_rewrite ctxt t = + prove_abstract' ctxt t prop_tac ( + abstract_eq abstract_prop abstract_prop (dest_prop t)) + +fun arith_rewrite_tac ctxt _ = + TRY o Simplifier.simp_tac ctxt + THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt) + +fun prove_arith_rewrite ctxt t = + prove_abstract' ctxt t arith_rewrite_tac ( + abstract_eq (abstract_arith ctxt) (abstract_arith ctxt) (dest_prop t)) + +fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [ + ("rules", apply_rule ctxt), + ("prop_rewrite", prove_prop_rewrite ctxt), + ("arith_rewrite", prove_arith_rewrite ctxt)] [] + +fun rewrite_star ctxt = rewrite ctxt + + + +(* pulling quantifiers *) + +fun pull_quant ctxt _ t = prove ctxt t quant_tac + + + +(* pushing quantifiers *) + +fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *) + + + +(* elimination of unused bound variables *) + +val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} +val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} + +fun elim_unused_tac i st = ( + match_tac [@{thm refl}] + ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac) + ORELSE' ( + match_tac [@{thm iff_allI}, @{thm iff_exI}] + THEN' elim_unused_tac)) i st + +fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac) + + + +(* destructive equality resolution *) + +fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *) + + + +(* quantifier instantiation *) + +val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} + +fun quant_inst ctxt _ t = prove ctxt t (fn _ => + REPEAT_ALL_NEW (rtac quant_inst_rule) + THEN' rtac @{thm excluded_middle}) + + + +(* propositional lemma *) + +exception LEMMA of unit + +val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast} +val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} + +fun norm_lemma thm = + (thm COMP_INCR intro_hyp_rule1) + handle THM _ => thm COMP_INCR intro_hyp_rule2 + +fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t + | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t) + +fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx = + lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx + | intro_hyps tab t cx = + lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx + +and lookup_intro_hyps tab t f (cx as (thm, terms)) = + (case Termtab.lookup tab (negated_prop t) of + NONE => f cx + | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms)) + +fun lemma ctxt (thms as [thm]) t = + (let + val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm))) + val (thm', terms) = intro_hyps tab (dest_prop t) (thm, []) + in + prove_abstract ctxt [thm'] t prop_tac ( + fold (snd oo abstract_lit) terms #> + abstract_disj (dest_thm thm') #>> single ##>> + abstract_disj (dest_prop t)) + end + handle LEMMA () => replay_error ctxt "Bad proof state" Z3_New_Proof.Lemma thms t) + | lemma ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Lemma thms t + + + +(* unit resolution *) + +fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) = + abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> + HOLogic.mk_not o HOLogic.mk_disj) + | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) = + abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> + HOLogic.mk_disj) + | abstract_unit t = abstract_lit t + +fun unit_res ctxt thms t = + prove_abstract ctxt thms t prop_tac ( + fold_map (abstract_unit o dest_thm) thms ##>> + abstract_unit (dest_prop t) #>> + (fn (prems, concl) => (prems, concl))) + + + +(* iff-true *) + +val iff_true_rule = @{lemma "P ==> P = True" by fast} + +fun iff_true _ [thm] _ = thm RS iff_true_rule + | iff_true ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_True thms t + + + +(* iff-false *) + +val iff_false_rule = @{lemma "~P ==> P = False" by fast} + +fun iff_false _ [thm] _ = thm RS iff_false_rule + | iff_false ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_False thms t + + + +(* commutativity *) + +fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute} + + + +(* definitional axioms *) + +fun def_axiom_disj ctxt t = + (case dest_prop t of + @{const HOL.disj} $ u1 $ u2 => + prove_abstract' ctxt t prop_tac ( + abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap) + | u => prove_abstract' ctxt t prop_tac (abstract_prop u)) + +fun def_axiom ctxt _ = try_provers ctxt Z3_New_Proof.Def_Axiom [ + ("rules", apply_rule ctxt), + ("disj", def_axiom_disj ctxt)] [] + + + +(* application of definitions *) + +fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *) + | apply_def ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Apply_Def thms t + + + +(* iff-oeq *) + +fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *) + + + +(* negation normal form *) + +fun nnf_prop ctxt thms t = + prove_abstract ctxt thms t prop_tac ( + fold_map (abstract_prop o dest_thm) thms ##>> + abstract_prop (dest_prop t)) + +fun nnf ctxt rule thms = try_provers ctxt rule [ + ("prop", nnf_prop ctxt thms), + ("quant", quant_intro ctxt [hd thms])] thms + +fun nnf_pos ctxt = nnf ctxt Z3_New_Proof.Nnf_Pos +fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg + + + +(* theory lemmas *) + +fun arith_th_lemma_tac ctxt prems = + Method.insert_tac prems + THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def}) + THEN' Arith_Data.arith_tac ctxt + +fun arith_th_lemma ctxt thms t = + prove_abstract ctxt thms t arith_th_lemma_tac ( + fold_map (abstract_arith ctxt o dest_thm) thms ##>> + abstract_arith ctxt (dest_prop t)) + +val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma))) + +fun th_lemma name ctxt thms = + (case Symtab.lookup (get_th_lemma_method ctxt) name of + SOME method => method ctxt thms + | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms) + + + +(* mapping of rules to methods *) + +fun is_assumption Z3_New_Proof.Asserted = true + | is_assumption Z3_New_Proof.Goal = true + | is_assumption Z3_New_Proof.Hypothesis = true + | is_assumption Z3_New_Proof.Intro_Def = true + | is_assumption Z3_New_Proof.Skolemize = true + | is_assumption _ = false + +fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule +fun assumed rule ctxt = replay_error ctxt "Assumed" rule + +fun choose Z3_New_Proof.True_Axiom = true_axiom + | choose (r as Z3_New_Proof.Asserted) = assumed r + | choose (r as Z3_New_Proof.Goal) = assumed r + | choose Z3_New_Proof.Modus_Ponens = mp + | choose Z3_New_Proof.Reflexivity = refl + | choose Z3_New_Proof.Symmetry = symm + | choose Z3_New_Proof.Transitivity = trans + | choose (r as Z3_New_Proof.Transitivity_Star) = unsupported r + | choose Z3_New_Proof.Monotonicity = cong + | choose Z3_New_Proof.Quant_Intro = quant_intro + | choose Z3_New_Proof.Distributivity = distrib + | choose Z3_New_Proof.And_Elim = and_elim + | choose Z3_New_Proof.Not_Or_Elim = not_or_elim + | choose Z3_New_Proof.Rewrite = rewrite + | choose Z3_New_Proof.Rewrite_Star = rewrite_star + | choose Z3_New_Proof.Pull_Quant = pull_quant + | choose (r as Z3_New_Proof.Pull_Quant_Star) = unsupported r + | choose Z3_New_Proof.Push_Quant = push_quant + | choose Z3_New_Proof.Elim_Unused_Vars = elim_unused + | choose Z3_New_Proof.Dest_Eq_Res = dest_eq_res + | choose Z3_New_Proof.Quant_Inst = quant_inst + | choose (r as Z3_New_Proof.Hypothesis) = assumed r + | choose Z3_New_Proof.Lemma = lemma + | choose Z3_New_Proof.Unit_Resolution = unit_res + | choose Z3_New_Proof.Iff_True = iff_true + | choose Z3_New_Proof.Iff_False = iff_false + | choose Z3_New_Proof.Commutativity = comm + | choose Z3_New_Proof.Def_Axiom = def_axiom + | choose (r as Z3_New_Proof.Intro_Def) = assumed r + | choose Z3_New_Proof.Apply_Def = apply_def + | choose Z3_New_Proof.Iff_Oeq = iff_oeq + | choose Z3_New_Proof.Nnf_Pos = nnf_pos + | choose Z3_New_Proof.Nnf_Neg = nnf_neg + | choose (r as Z3_New_Proof.Nnf_Star) = unsupported r + | choose (r as Z3_New_Proof.Cnf_Star) = unsupported r + | choose (r as Z3_New_Proof.Skolemize) = assumed r + | choose Z3_New_Proof.Modus_Ponens_Oeq = mp_oeq + | choose (Z3_New_Proof.Th_Lemma name) = th_lemma name + +fun with_tracing rule method ctxt thms t = + let val _ = trace_goal ctxt rule thms t + in method ctxt thms t end + +fun method_for rule = with_tracing rule (choose rule) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof_replay.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof_replay.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,194 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML + Author: Sascha Boehme, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Z3 proof replay. +*) + +signature Z3_NEW_PROOF_REPLAY = +sig + val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm +end + +structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY = +struct + +fun params_of t = Term.strip_qnt_vars @{const_name all} t + +fun varify ctxt thm = + let + val maxidx = Thm.maxidx_of thm + 1 + val vs = params_of (Thm.prop_of thm) + val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs + in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end + +fun add_paramTs names t = + fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (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, SMT2_Utils.certify ctxt' (Free (n', T))) + in (ctxt', Symtab.make (map2 mk nTs ns)) end + +fun forall_elim_term ct (Const (@{const_name 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 (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_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) = +(tracing ("replay_thm: " ^ @{make_string} (id, rule) ^ " " ^ Syntax.string_of_term ctxt concl); + if Z3_New_Proof_Methods.is_assumption rule then + (case Inttab.lookup assumed id of + SOME (_, thm) => thm + | NONE => Thm.assume (SMT2_Utils.certify ctxt concl)) + else + under_fixes (Z3_New_Proof_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_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs = + let val nthms = map (the o Inttab.lookup proofs) prems + in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end + +local + val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def} + val remove_weight = mk_meta_eq @{thm SMT2.weight_def} + val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def} + + fun rewrite_conv _ [] = Conv.all_conv + | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs) + + val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, + remove_fun_app, Z3_New_Proof_Literals.rewrite_true] + + fun rewrite _ [] = I + | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) + + fun lookup_assm assms_net ct = + Z3_New_Proof_Tools.net_instances assms_net ct + |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) +in + +fun add_asserted outer_ctxt rewrite_rules assms steps ctxt = + let + val eqs = map (rewrite ctxt [Z3_New_Proof_Literals.rewrite_true]) rewrite_rules + val eqs' = union Thm.eq_thm eqs prep_rules + + val assms_net = + assms + |> map (apsnd (rewrite ctxt eqs')) + |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) + |> Z3_New_Proof_Tools.thm_net_of snd + + fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion + + fun assume thm ctxt = + let + val ct = Thm.cprem_of thm 1 + val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt + in (thm' RS thm, ctxt') end + + fun add1 id fixes thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = + let + val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt + val thms' = if exact then thms else th :: thms + in + ((insert (op =) i is, thms'), + (ctxt', Inttab.update (id, (fixes, thm)) ptab)) + end + + fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) + (cx as ((is, thms), (ctxt, ptab))) = + if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then + let + val ct = SMT2_Utils.certify ctxt concl + val thm1 = + Thm.trivial ct + |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) + val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 + in + (case lookup_assm assms_net (Thm.cprem_of thm2 1) of + [] => + let val (thm, ctxt') = assume thm1 ctxt + in ((is, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end + | ithms => fold (add1 id fixes thm1) ithms cx) + end + else + cx + in fold add steps (([], []), (ctxt, Inttab.empty)) end + +end + +(* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *) +local + val sk_rules = @{lemma + "c = (SOME x. P x) ==> (EX x. P x) = P c" + "c = (SOME x. ~ P x) ==> (~ (ALL x. P x)) = (~ P c)" + by (metis someI_ex)+} +in + +fun discharge_sk_tac i st = + (rtac @{thm trans} i + THEN resolve_tac sk_rules i + THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1) + THEN rtac @{thm refl} i) st + +end + +fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, + @{thm reflexive}, Z3_New_Proof_Literals.true_thm] + +val intro_def_rules = @{lemma + "(~ P | P) & (P | ~ P)" + "(P | ~ P) & (~ P | P)" + by fast+} + +fun discharge_assms_tac rules = + REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac)) + +fun discharge_assms ctxt rules thm = + (if Thm.nprems_of thm = 0 then + thm + else + (case Seq.pull (discharge_assms_tac 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 replay outer_ctxt + ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output = + let + val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt + val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1 + val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 + val proofs = fold (replay_step ctxt3 assumed) steps assumed + val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps + in + if Config.get ctxt3 SMT2_Config.filter_only_facts then (is, TrueI) + else ([], Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3) + end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof_rules.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof_rules.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,56 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof_rules.ML + Author: Sascha Boehme, TU Muenchen + +Custom rules for Z3 proof replay. +*) + +signature Z3_NEW_PROOF_RULES = +sig + val apply: Proof.context -> cterm -> thm option +end + +structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES = +struct + +val eq = Thm.eq_thm + +structure Data = Generic_Data +( + type T = thm Net.net + val empty = Net.empty + val extend = I + val merge = Net.merge eq +) + +fun maybe_instantiate ct thm = + try Thm.first_order_match (Thm.cprop_of thm, ct) + |> Option.map (fn inst => Thm.instantiate inst thm) + +fun apply ctxt ct = + let + val net = Data.get (Context.Proof ctxt) + val xthms = Net.match_term net (Thm.term_of ct) + + fun select ct = map_filter (maybe_instantiate ct) xthms + fun select' ct = + let val thm = Thm.trivial ct + in map_filter (try (fn rule => rule COMP thm)) xthms end + + in try hd (case select ct of [] => select' ct | xthms' => xthms') end + +val prep = `Thm.prop_of + +fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net +fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net + +val add = Thm.declaration_attribute (Data.map o ins) +val del = Thm.declaration_attribute (Data.map o del) + +val name = Binding.name "z3_new_rule" + +val description = "declaration of Z3 proof rules" + +val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #> + Global_Theory.add_thms_dynamic (name, Net.content o Data.get)) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_proof_tools.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_proof_tools.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,156 @@ +(* Title: HOL/Tools/SMT2/z3_new_proof_tools.ML + Author: Sascha Boehme, TU Muenchen + +Helper functions required for Z3 proof replay. +*) + +signature Z3_NEW_PROOF_TOOLS = +sig + (*theorem nets*) + val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net + val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list + + (*proof combinators*) + val under_assumption: (thm -> thm) -> cterm -> thm + val discharge: thm -> thm -> thm + + (*a faster COMP*) + type compose_data + val precompose: (cterm -> cterm list) -> thm -> compose_data + val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data + val compose: compose_data -> thm -> thm + + (*simpset*) + val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic + val make_simpset: Proof.context -> thm list -> simpset +end + +structure Z3_New_Proof_Tools: Z3_NEW_PROOF_TOOLS = +struct + + + +(* theorem nets *) + +fun thm_net_of f xthms = + let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm) + in fold insert xthms Net.empty end + +fun maybe_instantiate ct thm = + try Thm.first_order_match (Thm.cprop_of thm, ct) + |> Option.map (fn inst => Thm.instantiate inst thm) + +local + fun instances_from_net match f net ct = + let + val lookup = if match then Net.match_term else Net.unify_term + val xthms = lookup net (Thm.term_of ct) + fun select ct = map_filter (f (maybe_instantiate ct)) xthms + fun select' ct = + let val thm = Thm.trivial ct + in map_filter (f (try (fn rule => rule COMP thm))) xthms end + in (case select ct of [] => select' ct | xthms' => xthms') end +in + +fun net_instances net = + instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm)) + net + +end + + + +(* proof combinators *) + +fun under_assumption f ct = + let val ct' = SMT2_Utils.mk_cprop ct + in Thm.implies_intr ct' (f (Thm.assume ct')) end + +fun discharge p pq = Thm.implies_elim pq p + + + +(* a faster COMP *) + +type compose_data = cterm list * (cterm -> cterm list) * thm + +fun list2 (x, y) = [x, y] + +fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule) +fun precompose2 f rule = precompose (list2 o f) rule + +fun compose (cvs, f, rule) thm = + discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule) + + + +(* simpset *) + +local + val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv} + val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2} + val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1} + val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3} + + fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm + fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) + | dest_binop t = raise TERM ("dest_binop", [t]) + + fun prove_antisym_le ctxt t = + let + val (le, r, s) = dest_binop t + val less = Const (@{const_name less}, Term.fastype_of le) + val prems = Simplifier.prems_of ctxt + in + (case find_first (eq_prop (le $ s $ r)) prems of + NONE => + find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems + |> Option.map (fn thm => thm RS antisym_less1) + | SOME thm => SOME (thm RS antisym_le1)) + end + handle THM _ => NONE + + fun prove_antisym_less ctxt t = + let + val (less, r, s) = dest_binop (HOLogic.dest_not t) + val le = Const (@{const_name less_eq}, Term.fastype_of less) + val prems = Simplifier.prems_of ctxt + in + (case find_first (eq_prop (le $ r $ s)) prems of + NONE => + find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems + |> Option.map (fn thm => thm RS antisym_less2) + | SOME thm => SOME (thm RS antisym_le2)) + end + handle THM _ => NONE + + val basic_simpset = + simpset_of (put_simpset HOL_ss @{context} + addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special + arith_simps rel_simps array_rules z3div_def z3mod_def} + addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod}, + Simplifier.simproc_global @{theory} "fast_int_arith" [ + "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc, + Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le, + Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] + prove_antisym_less]) + + structure Simpset = Generic_Data + ( + type T = simpset + val empty = basic_simpset + val extend = I + val merge = Simplifier.merge_ss + ) +in + +fun add_simproc simproc context = + Simpset.map (simpset_map (Context.proof_of context) + (fn ctxt => ctxt addsimprocs [simproc])) context + +fun make_simpset ctxt rules = + simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules) + +end + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Tools/SMT2/z3_new_real.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT2/z3_new_real.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,32 @@ +(* Title: HOL/Tools/SMT2/z3_new_real.ML + Author: Sascha Boehme, TU Muenchen + +Z3 setup for reals. +*) + +structure Z3_New_Real: sig end = +struct + +fun real_type_parser (SMTLIB2.Sym "Real", []) = SOME @{typ Real.real} + | real_type_parser _ = NONE + +fun real_term_parser (SMTLIB2.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i) + | real_term_parser (SMTLIB2.Sym "/", [t1, t2]) = + SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2) + | real_term_parser (SMTLIB2.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t) + | real_term_parser _ = NONE + +fun abstract abs t = + (case t of + (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 => + abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2)) + | (c as @{term "Real.real :: int => _"}) $ t => + abs t #>> (fn u => SOME (c $ u)) + | _ => pair NONE) + +val _ = Theory.setup (Context.theory_map ( + Z3_New_Proof.add_type_parser real_type_parser #> + Z3_New_Proof.add_term_parser real_term_parser #> + Z3_New_Proof_Methods.add_arith_abstracter abstract)) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Word/Tools/smt2_word.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Word/Tools/smt2_word.ML Thu Mar 13 13:18:13 2014 +0100 @@ -0,0 +1,144 @@ +(* Title: HOL/Word/Tools/smt2_word.ML + Author: Sascha Boehme, TU Muenchen + +SMT setup for words. +*) + +structure SMT2_Word: sig end = +struct + +open Word_Lib + +(* SMT-LIB logic *) + +fun smtlib_logic ts = + if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts + then SOME "QF_AUFBV" + else NONE + + +(* SMT-LIB builtins *) + +local + val smtlib2C = SMTLIB2_Interface.smtlib2C + + val wordT = @{typ "'a::len word"} + + fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")" + fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")" + + fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T) + | word_typ _ = NONE + + fun word_num (Type (@{type_name word}, [T])) k = + Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T) + | word_num _ _ = NONE + + fun if_fixed pred m n T ts = + let val (Us, U) = Term.strip_type T + in + if pred (U, Us) then + SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) + else NONE + end + + fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m + fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m + + fun add_word_fun f (t, n) = + let val (m, _) = Term.dest_Const t + in SMT2_Builtin.add_builtin_fun smtlib2C (Term.dest_Const t, K (f m n)) end + + fun hd2 xs = hd (tl xs) + + fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i + + fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n) + | dest_nat t = raise TERM ("not a natural number", [t]) + + fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u)) + | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) + + fun shift m n T ts = + let val U = Term.domain_type T + in + (case (can dest_wordT U, try (dest_nat o hd2) ts) of + (true, SOME i) => + SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T)) + | _ => NONE) (* FIXME: also support non-numerical shifts *) + end + + fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts) + + fun extract m n T ts = + let val U = Term.range_type (Term.range_type T) + in + (case (try (dest_nat o hd) ts, try dest_wordT U) of + (SOME lb, SOME i) => + SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb) + | _ => NONE) + end + + fun mk_extend c ts = Term.list_comb (Const c, ts) + + fun extend m n T ts = + let val (U1, U2) = Term.dest_funT T + in + (case (try dest_wordT U1, try dest_wordT U2) of + (SOME i, SOME j) => + if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T)) + else NONE + | _ => NONE) + end + + fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts) + + fun rotate m n T ts = + let val U = Term.domain_type (Term.range_type T) + in + (case (can dest_wordT U, try (dest_nat o hd) ts) of + (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i) + | _ => NONE) + end +in + +val setup_builtins = + SMT2_Builtin.add_builtin_typ smtlib2C (wordT, word_typ, word_num) #> + fold (add_word_fun if_fixed_all) [ + (@{term "uminus :: 'a::len word => _"}, "bvneg"), + (@{term "plus :: 'a::len word => _"}, "bvadd"), + (@{term "minus :: 'a::len word => _"}, "bvsub"), + (@{term "times :: 'a::len word => _"}, "bvmul"), + (@{term "bitNOT :: 'a::len word => _"}, "bvnot"), + (@{term "bitAND :: 'a::len word => _"}, "bvand"), + (@{term "bitOR :: 'a::len word => _"}, "bvor"), + (@{term "bitXOR :: 'a::len word => _"}, "bvxor"), + (@{term "word_cat :: 'a::len word => _"}, "concat") ] #> + fold (add_word_fun shift) [ + (@{term "shiftl :: 'a::len word => _ "}, "bvshl"), + (@{term "shiftr :: 'a::len word => _"}, "bvlshr"), + (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #> + add_word_fun extract + (@{term "slice :: _ => 'a::len word => _"}, "extract") #> + fold (add_word_fun extend) [ + (@{term "ucast :: 'a::len word => _"}, "zero_extend"), + (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #> + fold (add_word_fun rotate) [ + (@{term word_rotl}, "rotate_left"), + (@{term word_rotr}, "rotate_right") ] #> + fold (add_word_fun if_fixed_args) [ + (@{term "less :: 'a::len word => _"}, "bvult"), + (@{term "less_eq :: 'a::len word => _"}, "bvule"), + (@{term word_sless}, "bvslt"), + (@{term word_sle}, "bvsle") ] + +end + + +(* setup *) + +val _ = Theory.setup (Context.theory_map ( + SMTLIB2_Interface.add_logic (20, smtlib_logic) #> + setup_builtins)) + +end diff -r d397030fb27e -r 624faeda77b5 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Word/Word.thy Thu Mar 13 13:18:13 2014 +0100 @@ -4738,6 +4738,7 @@ ML_file "Tools/word_lib.ML" ML_file "Tools/smt_word.ML" setup SMT_Word.setup +ML_file "Tools/smt2_word.ML" hide_const (open) Word