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@41426: imports Record wenzelm@46950: keywords "smt_status" :: diag boehmes@36898: begin boehmes@36898: wenzelm@48892: ML_file "Tools/SMT/smt_utils.ML" wenzelm@48892: ML_file "Tools/SMT/smt_failure.ML" wenzelm@48892: ML_file "Tools/SMT/smt_config.ML" boehmes@36898: boehmes@36898: huffman@36902: subsection {* Triggers for quantifier instantiation *} boehmes@36898: boehmes@36898: text {* boehmes@41125: Some SMT solvers support patterns as a quantifier instantiation boehmes@41125: heuristics. Patterns may either be positive terms (tagged by "pat") boehmes@41125: triggering quantifier instantiations -- when the solver finds a boehmes@41125: term matching a positive pattern, it instantiates the corresponding boehmes@41125: quantifier accordingly -- or negative terms (tagged by "nopat") boehmes@41125: inhibiting quantifier instantiations. A list of patterns boehmes@41125: of the same kind is called a multipattern, and all patterns in a boehmes@41125: multipattern are considered conjunctively for quantifier instantiation. boehmes@41125: A list of multipatterns is called a trigger, and their multipatterns boehmes@41125: act disjunctively during quantifier instantiation. Each multipattern boehmes@41125: should mention at least all quantified variables of the preceding boehmes@41125: quantifier block. boehmes@36898: *} boehmes@36898: boehmes@36898: datatype pattern = Pattern boehmes@36898: boehmes@37124: definition pat :: "'a \ pattern" where "pat _ = Pattern" boehmes@37124: definition nopat :: "'a \ pattern" where "nopat _ = Pattern" boehmes@36898: boehmes@37124: definition trigger :: "pattern list list \ bool \ bool" boehmes@36898: where "trigger _ P = P" boehmes@36898: boehmes@36898: boehmes@36898: boehmes@40664: subsection {* Quantifier weights *} boehmes@40664: boehmes@40664: text {* boehmes@40664: Weight annotations to quantifiers influence the priority of quantifier boehmes@40664: instantiations. They should be handled with care for solvers, which support boehmes@40664: them, because incorrect choices of weights might render a problem unsolvable. boehmes@40664: *} boehmes@40664: boehmes@40664: definition weight :: "int \ bool \ bool" where "weight _ P = P" boehmes@40664: boehmes@40664: text {* boehmes@40664: Weights must be non-negative. The value @{text 0} is equivalent to providing boehmes@40664: no weight at all. boehmes@40664: boehmes@40664: Weights should only be used at quantifiers and only inside triggers (if the boehmes@40664: quantifier has triggers). Valid usages of weights are as follows: boehmes@40664: boehmes@40664: \begin{itemize} boehmes@40664: \item boehmes@40664: @{term "\x. trigger [[pat (P x)]] (weight 2 (P x))"} boehmes@40664: \item boehmes@40664: @{term "\x. weight 3 (P x)"} boehmes@40664: \end{itemize} boehmes@40664: *} boehmes@40664: boehmes@40664: boehmes@40664: 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@41127: definition fun_app where "fun_app f = f" 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@41059: Some SMT solvers only accept problems in first-order logic, i.e., boehmes@41059: where formulas and terms are syntactically separated. When boehmes@41059: translating higher-order into first-order problems, all boehmes@41059: uninterpreted constants (those not built-in in the target solver) boehmes@36898: are treated as function symbols in the first-order sense. Their boehmes@41059: occurrences as head symbols in atoms (i.e., as predicate symbols) are boehmes@41281: turned into terms by logically equating such atoms with @{term True}. boehmes@41281: For technical reasons, @{term True} and @{term False} occurring inside boehmes@41281: terms are replaced by the following constants. boehmes@36898: *} boehmes@36898: boehmes@41281: definition term_true where "term_true = True" boehmes@41281: definition term_false where "term_false = False" boehmes@41281: boehmes@36898: boehmes@36898: boehmes@37151: subsection {* Integer division and modulo for Z3 *} boehmes@37151: boehmes@37151: definition z3div :: "int \ int \ int" where boehmes@37151: "z3div k l = (if 0 \ l then k div l else -(k div (-l)))" boehmes@37151: boehmes@37151: definition z3mod :: "int \ int \ int" where boehmes@37151: "z3mod k l = (if 0 \ l then k mod l else k mod (-l))" boehmes@37151: boehmes@37151: boehmes@37151: huffman@36902: subsection {* Setup *} boehmes@36898: wenzelm@48892: ML_file "Tools/SMT/smt_builtin.ML" wenzelm@48892: ML_file "Tools/SMT/smt_datatypes.ML" wenzelm@48892: ML_file "Tools/SMT/smt_normalize.ML" wenzelm@48892: ML_file "Tools/SMT/smt_translate.ML" wenzelm@48892: ML_file "Tools/SMT/smt_solver.ML" wenzelm@48892: ML_file "Tools/SMT/smtlib_interface.ML" wenzelm@48892: ML_file "Tools/SMT/z3_interface.ML" wenzelm@48892: ML_file "Tools/SMT/z3_proof_parser.ML" wenzelm@48892: ML_file "Tools/SMT/z3_proof_tools.ML" wenzelm@48892: ML_file "Tools/SMT/z3_proof_literals.ML" wenzelm@48892: ML_file "Tools/SMT/z3_proof_methods.ML" wenzelm@48892: ML_file "Tools/SMT/z3_proof_reconstruction.ML" wenzelm@48892: ML_file "Tools/SMT/z3_model.ML" wenzelm@48892: ML_file "Tools/SMT/smt_setup_solvers.ML" boehmes@36898: boehmes@36898: setup {* boehmes@40424: SMT_Config.setup #> boehmes@41059: SMT_Normalize.setup #> boehmes@41059: SMTLIB_Interface.setup #> boehmes@41059: Z3_Interface.setup #> boehmes@36898: Z3_Proof_Reconstruction.setup #> boehmes@40162: SMT_Setup_Solvers.setup boehmes@36898: *} boehmes@36898: wenzelm@47701: method_setup smt = {* wenzelm@47701: Scan.optional Attrib.thms [] >> wenzelm@47701: (fn thms => fn ctxt => wenzelm@47701: METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) wenzelm@47701: *} "apply an SMT solver to the current goal" 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@41432: solver. The possible values can be obtained from the @{text smt_status} boehmes@41432: command. boehmes@41459: boehmes@41459: Due to licensing restrictions, Yices and Z3 are not installed/enabled boehmes@41459: by default. Z3 is free for non-commercial applications and can be enabled boehmes@41462: by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to boehmes@41462: @{text yes}. boehmes@36898: *} boehmes@36898: boehmes@41601: 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@41121: SMT solvers apply randomized heuristics. In case a problem is not boehmes@41121: solvable by an SMT solver, changing the following option might help. boehmes@41121: *} boehmes@41121: boehmes@41121: declare [[ smt_random_seed = 1 ]] boehmes@41121: boehmes@41121: 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@41432: declare [[ cvc3_options = "", remote_cvc3_options = "" ]] boehmes@41432: declare [[ yices_options = "" ]] boehmes@41432: declare [[ z3_options = "", remote_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@41125: text {* boehmes@41125: The SMT method provides an inference mechanism to detect simple triggers boehmes@41125: in quantified formulas, which might increase the number of problems boehmes@41125: solvable by SMT solvers (note: triggers guide quantifier instantiations boehmes@41125: in the SMT solver). To turn it on, set the following option. boehmes@41125: *} boehmes@41125: boehmes@41125: declare [[ smt_infer_triggers = false ]] boehmes@41125: boehmes@41125: text {* boehmes@41125: The SMT method monomorphizes the given facts, that is, it tries to boehmes@41125: instantiate all schematic type variables with fixed types occurring boehmes@41125: in the problem. This is a (possibly nonterminating) fixed-point boehmes@41125: construction whose cycles are limited by the following option. boehmes@41125: *} boehmes@41125: boehmes@43230: declare [[ monomorph_max_rounds = 5 ]] boehmes@41125: boehmes@41762: text {* boehmes@41762: In addition, the number of generated monomorphic instances is limited boehmes@41762: by the following option. boehmes@41762: *} boehmes@41762: boehmes@43230: declare [[ monomorph_max_new_instances = 500 ]] boehmes@41762: 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 {* blanchet@47152: The option @{text smt_read_only_certificates} controls whether only blanchet@47152: stored certificates are should be used or invocation of an SMT solver blanchet@47152: is 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: blanchet@47152: declare [[ smt_read_only_certificates = 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@44488: "(P \ Q) = (\(\P \ \Q))" boehmes@44488: "(P \ Q) = (\(\Q \ \P))" boehmes@44488: "(\P \ Q) = (\(P \ \Q))" boehmes@44488: "(\P \ Q) = (\(\Q \ P))" boehmes@44488: "(P \ \Q) = (\(\P \ Q))" boehmes@44488: "(P \ \Q) = (\(Q \ \P))" boehmes@44488: "(\P \ \Q) = (\(P \ Q))" boehmes@44488: "(\P \ \Q) = (\(Q \ P))" boehmes@44488: by auto boehmes@44488: boehmes@44488: lemma [z3_rule]: boehmes@36898: "(P \ Q) = (Q \ \P)" boehmes@36898: "(\P \ Q) = (P \ Q)" boehmes@36898: "(\P \ Q) = (Q \ P)" boehmes@44488: "(True \ P) = P" boehmes@44488: "(P \ True) = True" boehmes@44488: "(False \ P) = True" boehmes@44488: "(P \ P) = True" boehmes@36898: by auto boehmes@36898: boehmes@36898: lemma [z3_rule]: boehmes@36898: "((P = Q) \ R) = (R | (Q = (\P)))" boehmes@36898: by auto boehmes@36898: boehmes@36898: lemma [z3_rule]: boehmes@44488: "(\True) = False" boehmes@44488: "(\False) = True" boehmes@44488: "(x = x) = True" boehmes@44488: "(P = True) = P" boehmes@44488: "(True = P) = P" boehmes@44488: "(P = False) = (\P)" boehmes@44488: "(False = P) = (\P)" boehmes@36898: "((\P) = P) = False" boehmes@36898: "(P = (\P)) = False" boehmes@44488: "((\P) = (\Q)) = (P = Q)" boehmes@44488: "\(P = (\Q)) = (P = Q)" boehmes@44488: "\((\P) = Q) = (P = Q)" boehmes@36898: "(P \ Q) = (Q = (\P))" boehmes@36898: "(P = Q) = ((\P \ Q) \ (P \ \Q))" boehmes@36898: "(P \ Q) = ((\P \ \Q) \ (P \ Q))" boehmes@36898: by auto boehmes@36898: boehmes@36898: lemma [z3_rule]: boehmes@36898: "(if P then P else \P) = True" boehmes@36898: "(if \P then \P else P) = True" boehmes@36898: "(if P then True else False) = P" boehmes@36898: "(if P then False else True) = (\P)" boehmes@44488: "(if P then Q else True) = ((\P) \ Q)" boehmes@44488: "(if P then Q else True) = (Q \ (\P))" boehmes@44488: "(if P then Q else \Q) = (P = Q)" boehmes@44488: "(if P then Q else \Q) = (Q = P)" boehmes@44488: "(if P then \Q else Q) = (P = (\Q))" boehmes@44488: "(if P then \Q else Q) = ((\Q) = P)" boehmes@36898: "(if \P then x else y) = (if P then y else x)" boehmes@44488: "(if P then (if Q then x else y) else x) = (if P \ (\Q) then y else x)" boehmes@44488: "(if P then (if Q then x else y) else x) = (if (\Q) \ P then y else x)" boehmes@44488: "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" boehmes@44488: "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" boehmes@44488: "(if P then x else if P then y else z) = (if P then x else z)" boehmes@44488: "(if P then x else if Q then x else y) = (if P \ Q then x else y)" boehmes@44488: "(if P then x else if Q then x else y) = (if Q \ P then x else y)" boehmes@44488: "(if P then x = y else x = z) = (x = (if P then y else z))" boehmes@44488: "(if P then x = y else y = z) = (y = (if P then x else z))" boehmes@44488: "(if P then x = y else z = y) = (y = (if P then x else z))" boehmes@36898: by auto boehmes@36898: boehmes@36898: lemma [z3_rule]: boehmes@44488: "0 + (x::int) = x" boehmes@44488: "x + 0 = x" boehmes@44488: "x + x = 2 * x" boehmes@44488: "0 * x = 0" boehmes@44488: "1 * x = x" boehmes@44488: "x + y = y + x" boehmes@44488: by auto boehmes@44488: boehmes@44488: lemma [z3_rule]: (* for def-axiom *) boehmes@36898: "P = Q \ P \ Q" boehmes@36898: "P = Q \ \P \ \Q" boehmes@36898: "(\P) = Q \ \P \ Q" boehmes@36898: "(\P) = Q \ P \ \Q" boehmes@36898: "P = (\Q) \ \P \ Q" boehmes@36898: "P = (\Q) \ P \ \Q" boehmes@36898: "P \ Q \ P \ \Q" boehmes@36898: "P \ Q \ \P \ Q" boehmes@36898: "P \ (\Q) \ P \ Q" boehmes@36898: "(\P) \ Q \ P \ Q" boehmes@36898: "P \ Q \ P \ (\Q)" boehmes@36898: "P \ Q \ (\P) \ Q" boehmes@36898: "P \ \Q \ P \ Q" boehmes@36898: "\P \ Q \ P \ Q" boehmes@44488: "P \ y = (if P then x else y)" boehmes@44488: "P \ (if P then x else y) = y" boehmes@44488: "\P \ x = (if P then x else y)" boehmes@44488: "\P \ (if P then x else y) = x" boehmes@44488: "P \ R \ \(if P then Q else R)" boehmes@44488: "\P \ Q \ \(if P then Q else R)" boehmes@44488: "\(if P then Q else R) \ \P \ Q" boehmes@44488: "\(if P then Q else R) \ P \ R" boehmes@44488: "(if P then Q else R) \ \P \ \Q" boehmes@44488: "(if P then Q else R) \ P \ \R" boehmes@44488: "(if P then \Q else R) \ \P \ Q" boehmes@44488: "(if P then Q else \R) \ P \ R" boehmes@36898: by auto boehmes@36898: boehmes@37124: boehmes@37124: boehmes@37124: hide_type (open) pattern boehmes@41281: hide_const Pattern fun_app term_true term_false z3div z3mod boehmes@41280: hide_const (open) trigger pat nopat weight boehmes@37124: boehmes@36898: end