boehmes@36898: (*  Title:      HOL/SMT.thy
boehmes@36898:     Author:     Sascha Boehme, TU Muenchen
boehmes@36898: *)
boehmes@36898: 
boehmes@36898: header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
boehmes@36898: 
boehmes@36898: theory SMT
boehmes@36898: imports List
boehmes@36898: uses
boehmes@39483:   "Tools/Datatype/datatype_selectors.ML"
boehmes@40424:   "Tools/SMT/smt_failure.ML"
boehmes@40424:   "Tools/SMT/smt_config.ML"
boehmes@40424:   "Tools/SMT/smt_monomorph.ML"
boehmes@40277:   ("Tools/SMT/smt_builtin.ML")
boehmes@36898:   ("Tools/SMT/smt_normalize.ML")
boehmes@36898:   ("Tools/SMT/smt_translate.ML")
boehmes@36898:   ("Tools/SMT/smt_solver.ML")
boehmes@36898:   ("Tools/SMT/smtlib_interface.ML")
boehmes@36898:   ("Tools/SMT/z3_proof_parser.ML")
boehmes@36898:   ("Tools/SMT/z3_proof_tools.ML")
boehmes@36898:   ("Tools/SMT/z3_proof_literals.ML")
boehmes@36898:   ("Tools/SMT/z3_proof_reconstruction.ML")
boehmes@36898:   ("Tools/SMT/z3_model.ML")
boehmes@36898:   ("Tools/SMT/z3_interface.ML")
boehmes@40162:   ("Tools/SMT/smt_setup_solvers.ML")
boehmes@36898: begin
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
huffman@36902: subsection {* Triggers for quantifier instantiation *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Some SMT solvers support triggers for quantifier instantiation.
boehmes@36898: Each trigger consists of one ore more patterns.  A pattern may either
boehmes@37124: be a list of positive subterms (each being tagged by "pat"), or a
boehmes@37124: list of negative subterms (each being tagged by "nopat").
boehmes@37124: 
boehmes@37124: When an SMT solver finds a term matching a positive pattern (a
boehmes@37124: pattern with positive subterms only), it instantiates the
boehmes@37124: corresponding quantifier accordingly.  Negative patterns inhibit
boehmes@37124: quantifier instantiations.  Each pattern should mention all preceding
boehmes@37124: bound variables.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: datatype pattern = Pattern
boehmes@36898: 
boehmes@37124: definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
boehmes@37124: definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
boehmes@36898: 
boehmes@37124: definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
boehmes@36898: where "trigger _ P = P"
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@40274: subsection {* Distinctness *}
boehmes@40274: 
boehmes@40274: text {*
boehmes@40274: As an abbreviation for a quadratic number of inequalities, SMT solvers
boehmes@40274: provide a built-in @{text distinct}.  To avoid confusion with the
boehmes@40274: already defined (and more general) @{term List.distinct}, a separate
boehmes@40274: constant is defined.
boehmes@40274: *}
boehmes@40274: 
boehmes@40274: definition distinct :: "'a list \<Rightarrow> bool"
boehmes@40274: where "distinct xs = List.distinct xs"
boehmes@40274: 
boehmes@40274: 
boehmes@40274: 
huffman@36902: subsection {* Higher-order encoding *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Application is made explicit for constants occurring with varying
boehmes@36898: numbers of arguments.  This is achieved by the introduction of the
boehmes@36898: following constant.
boehmes@36898: *}
boehmes@36898: 
boehmes@37153: definition fun_app where "fun_app f x = f x"
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Some solvers support a theory of arrays which can be used to encode
boehmes@36898: higher-order functions.  The following set of lemmas specifies the
boehmes@36898: properties of such (extensional) arrays.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
boehmes@37157:   fun_upd_upd fun_app_def
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
huffman@36902: subsection {* First-order logic *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Some SMT solvers require a strict separation between formulas and
boehmes@36898: terms.  When translating higher-order into first-order problems,
boehmes@36898: all uninterpreted constants (those not builtin in the target solver)
boehmes@36898: are treated as function symbols in the first-order sense.  Their
boehmes@36898: occurrences as head symbols in atoms (i.e., as predicate symbols) is
boehmes@36898: turned into terms by equating such atoms with @{term True} using the
boehmes@36898: following term-level equation symbol.
boehmes@36898: *}
boehmes@36898: 
boehmes@37124: definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@37151: subsection {* Integer division and modulo for Z3 *}
boehmes@37151: 
boehmes@37151: definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151:   "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
boehmes@37151: 
boehmes@37151: definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151:   "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
boehmes@37151: 
boehmes@37151: lemma div_by_z3div: "k div l = (
boehmes@37151:      if k = 0 \<or> l = 0 then 0
boehmes@37151:      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
boehmes@37151:      else z3div (-k) (-l))"
boehmes@37151:   by (auto simp add: z3div_def)
boehmes@37151: 
boehmes@37151: lemma mod_by_z3mod: "k mod l = (
boehmes@37151:      if l = 0 then k
boehmes@37151:      else if k = 0 then 0
boehmes@37151:      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
boehmes@37151:      else - z3mod (-k) (-l))"
boehmes@37151:   by (auto simp add: z3mod_def)
boehmes@37151: 
boehmes@37151: 
boehmes@37151: 
huffman@36902: subsection {* Setup *}
boehmes@36898: 
boehmes@40277: use "Tools/SMT/smt_builtin.ML"
boehmes@36898: use "Tools/SMT/smt_normalize.ML"
boehmes@36898: use "Tools/SMT/smt_translate.ML"
boehmes@36898: use "Tools/SMT/smt_solver.ML"
boehmes@36898: use "Tools/SMT/smtlib_interface.ML"
boehmes@36898: use "Tools/SMT/z3_interface.ML"
boehmes@36898: use "Tools/SMT/z3_proof_parser.ML"
boehmes@36898: use "Tools/SMT/z3_proof_tools.ML"
boehmes@36898: use "Tools/SMT/z3_proof_literals.ML"
boehmes@36898: use "Tools/SMT/z3_proof_reconstruction.ML"
boehmes@36898: use "Tools/SMT/z3_model.ML"
boehmes@40162: use "Tools/SMT/smt_setup_solvers.ML"
boehmes@36898: 
boehmes@36898: setup {*
boehmes@40424:   SMT_Config.setup #>
boehmes@36898:   SMT_Solver.setup #>
boehmes@36898:   Z3_Proof_Reconstruction.setup #>
boehmes@40162:   SMT_Setup_Solvers.setup
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
huffman@36902: subsection {* Configuration *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36899: The current configuration can be printed by the command
boehmes@36899: @{text smt_status}, which shows the values of most options.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: subsection {* General configuration options *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: The option @{text smt_solver} can be used to change the target SMT
boehmes@36898: solver.  The possible values are @{text cvc3}, @{text yices}, and
boehmes@36898: @{text z3}.  It is advisable to locally install the selected solver,
boehmes@36898: although this is not necessary for @{text cvc3} and @{text z3}, which
boehmes@36898: can also be used over an Internet-based service.
boehmes@36898: 
boehmes@36898: When using local SMT solvers, the path to their binaries should be
boehmes@36898: declared by setting the following environment variables:
boehmes@36898: @{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: declare [[ smt_solver = z3 ]]
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Since SMT solvers are potentially non-terminating, there is a timeout
boehmes@36898: (given in seconds) to restrict their runtime.  A value greater than
boehmes@36898: 120 (seconds) is in most cases not advisable.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: declare [[ smt_timeout = 20 ]]
boehmes@36898: 
boehmes@40162: text {*
boehmes@40162: In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
boehmes@40162: solvers are fully trusted without additional checks.  The following
boehmes@40162: option can cause the SMT solver to run in proof-producing mode, giving
boehmes@40162: a checkable certificate.  This is currently only implemented for Z3.
boehmes@40162: *}
boehmes@40162: 
boehmes@40162: declare [[ smt_oracle = false ]]
boehmes@40162: 
boehmes@40162: text {*
boehmes@40162: Each SMT solver provides several commandline options to tweak its
boehmes@40162: behaviour.  They can be passed to the solver by setting the following
boehmes@40162: options.
boehmes@40162: *}
boehmes@40162: 
boehmes@40162: declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
boehmes@40162: 
boehmes@40162: text {*
boehmes@40162: Enable the following option to use built-in support for datatypes and
boehmes@40162: records.  Currently, this is only implemented for Z3 running in oracle
boehmes@40162: mode.
boehmes@40162: *}
boehmes@40162: 
boehmes@40162: declare [[ smt_datatypes = false ]]
boehmes@40162: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: subsection {* Certificates *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: By setting the option @{text smt_certificates} to the name of a file,
boehmes@36898: all following applications of an SMT solver a cached in that file.
boehmes@36898: Any further application of the same SMT solver (using the very same
boehmes@36898: configuration) re-uses the cached certificate instead of invoking the
boehmes@36898: solver.  An empty string disables caching certificates.
boehmes@36898: 
boehmes@36898: The filename should be given as an explicit path.  It is good
boehmes@36898: practice to use the name of the current theory (with ending
boehmes@36898: @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: declare [[ smt_certificates = "" ]]
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: The option @{text smt_fixed} controls whether only stored
boehmes@36898: certificates are should be used or invocation of an SMT solver is
boehmes@36898: allowed.  When set to @{text true}, no SMT solver will ever be
boehmes@36898: invoked and only the existing certificates found in the configured
boehmes@36898: cache are used;  when set to @{text false} and there is no cached
boehmes@36898: certificate for some proposition, then the configured SMT solver is
boehmes@36898: invoked.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: declare [[ smt_fixed = false ]]
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: subsection {* Tracing *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@40424: The SMT method, when applied, traces important information.  To
boehmes@40424: make it entirely silent, set the following option to @{text false}.
boehmes@40424: *}
boehmes@40424: 
boehmes@40424: declare [[ smt_verbose = true ]]
boehmes@40424: 
boehmes@40424: text {*
boehmes@36898: For tracing the generated problem file given to the SMT solver as
boehmes@36898: well as the returned result of the solver, the option
boehmes@36898: @{text smt_trace} should be set to @{text true}.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: declare [[ smt_trace = false ]]
boehmes@36898: 
boehmes@36898: text {*
boehmes@40162: From the set of assumptions given to the SMT solver, those assumptions
boehmes@40162: used in the proof are traced when the following option is set to
boehmes@40162: @{term true}.  This only works for Z3 when it runs in non-oracle mode
boehmes@40162: (see options @{text smt_solver} and @{text smt_oracle} above).
boehmes@36898: *}
boehmes@36898: 
boehmes@40162: declare [[ smt_trace_used_facts = false ]]
boehmes@39298: 
boehmes@36898: 
boehmes@36898: 
huffman@36902: subsection {* Schematic rules for Z3 proof reconstruction *}
boehmes@36898: 
boehmes@36898: text {*
boehmes@36898: Several prof rules of Z3 are not very well documented.  There are two
boehmes@36898: lemma groups which can turn failing Z3 proof reconstruction attempts
boehmes@36898: into succeeding ones: the facts in @{text z3_rule} are tried prior to
boehmes@36898: any implemented reconstruction procedure for all uncertain Z3 proof
boehmes@36898: rules;  the facts in @{text z3_simp} are only fed to invocations of
boehmes@36898: the simplifier when reconstructing theory-specific proof steps.
boehmes@36898: *}
boehmes@36898: 
boehmes@36898: lemmas [z3_rule] =
boehmes@36898:   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
boehmes@36898:   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
boehmes@36898:   if_True if_False not_not
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
boehmes@36898:   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
boehmes@36898:   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "((\<not>P) = P) = False"
boehmes@36898:   "(P = (\<not>P)) = False"
boehmes@36898:   "(P \<noteq> Q) = (Q = (\<not>P))"
boehmes@36898:   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
boehmes@36898:   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "(if P then P else \<not>P) = True"
boehmes@36898:   "(if \<not>P then \<not>P else P) = True"
boehmes@36898:   "(if P then True else False) = P"
boehmes@36898:   "(if P then False else True) = (\<not>P)"
boehmes@36898:   "(if \<not>P then x else y) = (if P then y else x)"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "P = Q \<or> P \<or> Q"
boehmes@36898:   "P = Q \<or> \<not>P \<or> \<not>Q"
boehmes@36898:   "(\<not>P) = Q \<or> \<not>P \<or> Q"
boehmes@36898:   "(\<not>P) = Q \<or> P \<or> \<not>Q"
boehmes@36898:   "P = (\<not>Q) \<or> \<not>P \<or> Q"
boehmes@36898:   "P = (\<not>Q) \<or> P \<or> \<not>Q"
boehmes@36898:   "P \<noteq> Q \<or> P \<or> \<not>Q"
boehmes@36898:   "P \<noteq> Q \<or> \<not>P \<or> Q"
boehmes@36898:   "P \<noteq> (\<not>Q) \<or> P \<or> Q"
boehmes@36898:   "(\<not>P) \<noteq> Q \<or> P \<or> Q"
boehmes@36898:   "P \<or> Q \<or> P \<noteq> (\<not>Q)"
boehmes@36898:   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
boehmes@36898:   "P \<or> \<not>Q \<or> P \<noteq> Q"
boehmes@36898:   "\<not>P \<or> Q \<or> P \<noteq> Q"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@36898: lemma [z3_rule]:
boehmes@36898:   "0 + (x::int) = x"
boehmes@36898:   "x + 0 = x"
boehmes@36898:   "0 * x = 0"
boehmes@36898:   "1 * x = x"
boehmes@36898:   "x + y = y + x"
boehmes@36898:   by auto
boehmes@36898: 
boehmes@37124: 
boehmes@37124: 
boehmes@37124: hide_type (open) pattern
boehmes@37153: hide_const Pattern term_eq
boehmes@40274: hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
boehmes@37124: 
boehmes@39483: 
boehmes@39483: 
boehmes@39483: subsection {* Selectors for datatypes *}
boehmes@39483: 
boehmes@39483: setup {* Datatype_Selectors.setup *}
boehmes@39483: 
boehmes@39483: declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
boehmes@39483: declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
boehmes@39483: 
boehmes@36898: end