--- 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
--- 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 \<Rightarrow> pattern" where "pat _ = Pattern"
-definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
+consts
+ pat :: "'a \<Rightarrow> pattern"
+ nopat :: "'a \<Rightarrow> pattern"
-definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
-where "trigger _ P = P"
-
+definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> 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 \<Rightarrow> int \<Rightarrow> int" where
@@ -117,7 +113,6 @@
"z3mod k l = (if 0 \<le> 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
--- /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 \<Rightarrow> pattern"
+ nopat :: "'a \<Rightarrow> pattern"
+
+definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> 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 \<Rightarrow> bool \<Rightarrow> 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 "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
+\item
+@{term "\<forall>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 \<Rightarrow> '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 \<Rightarrow> int \<Rightarrow> int" where
+ "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
+
+definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
+ "z3mod k l = (if 0 \<le> 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 \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
+ "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
+ "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
+ "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
+ "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
+ "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
+ "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
+ by auto
+
+lemma [z3_new_rule]:
+ "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
+ "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
+ "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+ "(True \<longrightarrow> P) = P"
+ "(P \<longrightarrow> True) = True"
+ "(False \<longrightarrow> P) = True"
+ "(P \<longrightarrow> P) = True"
+ by auto
+
+lemma [z3_new_rule]:
+ "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
+ by auto
+
+lemma [z3_new_rule]:
+ "(\<not>True) = False"
+ "(\<not>False) = True"
+ "(x = x) = True"
+ "(P = True) = P"
+ "(True = P) = P"
+ "(P = False) = (\<not>P)"
+ "(False = P) = (\<not>P)"
+ "((\<not>P) = P) = False"
+ "(P = (\<not>P)) = False"
+ "((\<not>P) = (\<not>Q)) = (P = Q)"
+ "\<not>(P = (\<not>Q)) = (P = Q)"
+ "\<not>((\<not>P) = Q) = (P = Q)"
+ "(P \<noteq> Q) = (Q = (\<not>P))"
+ "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
+ "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
+ by auto
+
+lemma [z3_new_rule]:
+ "(if P then P else \<not>P) = True"
+ "(if \<not>P then \<not>P else P) = True"
+ "(if P then True else False) = P"
+ "(if P then False else True) = (\<not>P)"
+ "(if P then Q else True) = ((\<not>P) \<or> Q)"
+ "(if P then Q else True) = (Q \<or> (\<not>P))"
+ "(if P then Q else \<not>Q) = (P = Q)"
+ "(if P then Q else \<not>Q) = (Q = P)"
+ "(if P then \<not>Q else Q) = (P = (\<not>Q))"
+ "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
+ "(if \<not>P then x else y) = (if P then y else x)"
+ "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
+ "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
+ "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
+ "(if P then (if Q then x else y) else y) = (if Q \<and> 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 \<or> Q then x else y)"
+ "(if P then x else if Q then x else y) = (if Q \<or> 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 \<or> P \<or> Q"
+ "P = Q \<or> \<not>P \<or> \<not>Q"
+ "(\<not>P) = Q \<or> \<not>P \<or> Q"
+ "(\<not>P) = Q \<or> P \<or> \<not>Q"
+ "P = (\<not>Q) \<or> \<not>P \<or> Q"
+ "P = (\<not>Q) \<or> P \<or> \<not>Q"
+ "P \<noteq> Q \<or> P \<or> \<not>Q"
+ "P \<noteq> Q \<or> \<not>P \<or> Q"
+ "P \<noteq> (\<not>Q) \<or> P \<or> Q"
+ "(\<not>P) \<noteq> Q \<or> P \<or> Q"
+ "P \<or> Q \<or> P \<noteq> (\<not>Q)"
+ "P \<or> Q \<or> (\<not>P) \<noteq> Q"
+ "P \<or> \<not>Q \<or> P \<noteq> Q"
+ "\<not>P \<or> Q \<or> P \<noteq> Q"
+ "P \<or> y = (if P then x else y)"
+ "P \<or> (if P then x else y) = y"
+ "\<not>P \<or> x = (if P then x else y)"
+ "\<not>P \<or> (if P then x else y) = x"
+ "P \<or> R \<or> \<not>(if P then Q else R)"
+ "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
+ "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
+ "\<not>(if P then Q else R) \<or> P \<or> R"
+ "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
+ "(if P then Q else R) \<or> P \<or> \<not>R"
+ "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
+ "(if P then Q else \<not>R) \<or> P \<or> R"
+ by auto
+
+hide_type (open) pattern
+hide_const fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight
+
+end
--- 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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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;
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- 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