src/HOL/SMT.thy
author boehmes
Tue Dec 07 14:53:12 2010 +0100 (2010-12-07)
changeset 41059 d2b1fc1b8e19
parent 40806 59d96f777da3
child 41121 5c5d05963f93
permissions -rw-r--r--
centralized handling of built-in types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
     1 (*  Title:      HOL/SMT.thy
     2     Author:     Sascha Boehme, TU Muenchen
     3 *)
     4 
     5 header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     6 
     7 theory SMT
     8 imports List
     9 uses
    10   "Tools/Datatype/datatype_selectors.ML"
    11   "Tools/SMT/smt_failure.ML"
    12   "Tools/SMT/smt_config.ML"
    13   "Tools/SMT/smt_utils.ML"
    14   "Tools/SMT/smt_monomorph.ML"
    15   ("Tools/SMT/smt_builtin.ML")
    16   ("Tools/SMT/smt_normalize.ML")
    17   ("Tools/SMT/smt_translate.ML")
    18   ("Tools/SMT/smt_solver.ML")
    19   ("Tools/SMT/smtlib_interface.ML")
    20   ("Tools/SMT/z3_proof_parser.ML")
    21   ("Tools/SMT/z3_proof_tools.ML")
    22   ("Tools/SMT/z3_proof_literals.ML")
    23   ("Tools/SMT/z3_proof_methods.ML")
    24   ("Tools/SMT/z3_proof_reconstruction.ML")
    25   ("Tools/SMT/z3_model.ML")
    26   ("Tools/SMT/z3_interface.ML")
    27   ("Tools/SMT/smt_setup_solvers.ML")
    28 begin
    29 
    30 
    31 
    32 subsection {* Triggers for quantifier instantiation *}
    33 
    34 text {*
    35 Some SMT solvers support triggers for quantifier instantiation.
    36 Each trigger consists of one ore more patterns.  A pattern may either
    37 be a list of positive subterms (each being tagged by "pat"), or a
    38 list of negative subterms (each being tagged by "nopat").
    39 
    40 When an SMT solver finds a term matching a positive pattern (a
    41 pattern with positive subterms only), it instantiates the
    42 corresponding quantifier accordingly.  Negative patterns inhibit
    43 quantifier instantiations.  Each pattern should mention all preceding
    44 bound variables.
    45 *}
    46 
    47 datatype pattern = Pattern
    48 
    49 definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
    50 definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
    51 
    52 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
    53 where "trigger _ P = P"
    54 
    55 
    56 
    57 subsection {* Quantifier weights *}
    58 
    59 text {*
    60 Weight annotations to quantifiers influence the priority of quantifier
    61 instantiations.  They should be handled with care for solvers, which support
    62 them, because incorrect choices of weights might render a problem unsolvable.
    63 *}
    64 
    65 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
    66 
    67 text {*
    68 Weights must be non-negative.  The value @{text 0} is equivalent to providing
    69 no weight at all.
    70 
    71 Weights should only be used at quantifiers and only inside triggers (if the
    72 quantifier has triggers).  Valid usages of weights are as follows:
    73 
    74 \begin{itemize}
    75 \item
    76 @{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
    77 \item
    78 @{term "\<forall>x. weight 3 (P x)"}
    79 \end{itemize}
    80 *}
    81 
    82 
    83 
    84 subsection {* Higher-order encoding *}
    85 
    86 text {*
    87 Application is made explicit for constants occurring with varying
    88 numbers of arguments.  This is achieved by the introduction of the
    89 following constant.
    90 *}
    91 
    92 definition fun_app where "fun_app f x = f x"
    93 
    94 text {*
    95 Some solvers support a theory of arrays which can be used to encode
    96 higher-order functions.  The following set of lemmas specifies the
    97 properties of such (extensional) arrays.
    98 *}
    99 
   100 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
   101   fun_upd_upd fun_app_def
   102 
   103 
   104 
   105 subsection {* First-order logic *}
   106 
   107 text {*
   108 Some SMT solvers only accept problems in first-order logic, i.e.,
   109 where formulas and terms are syntactically separated. When
   110 translating higher-order into first-order problems, all
   111 uninterpreted constants (those not built-in in the target solver)
   112 are treated as function symbols in the first-order sense.  Their
   113 occurrences as head symbols in atoms (i.e., as predicate symbols) are
   114 turned into terms by equating such atoms with @{term True}.
   115 Whenever the boolean type occurs in first-order terms, it is replaced
   116 by the following type.
   117 *}
   118 
   119 typedecl term_bool
   120 
   121 
   122 
   123 subsection {* Integer division and modulo for Z3 *}
   124 
   125 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
   126   "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
   127 
   128 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
   129   "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
   130 
   131 lemma div_by_z3div: "k div l = (
   132      if k = 0 \<or> l = 0 then 0
   133      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
   134      else z3div (-k) (-l))"
   135   by (auto simp add: z3div_def)
   136 
   137 lemma mod_by_z3mod: "k mod l = (
   138      if l = 0 then k
   139      else if k = 0 then 0
   140      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
   141      else - z3mod (-k) (-l))"
   142   by (auto simp add: z3mod_def)
   143 
   144 
   145 
   146 subsection {* Setup *}
   147 
   148 use "Tools/SMT/smt_builtin.ML"
   149 use "Tools/SMT/smt_normalize.ML"
   150 use "Tools/SMT/smt_translate.ML"
   151 use "Tools/SMT/smt_solver.ML"
   152 use "Tools/SMT/smtlib_interface.ML"
   153 use "Tools/SMT/z3_interface.ML"
   154 use "Tools/SMT/z3_proof_parser.ML"
   155 use "Tools/SMT/z3_proof_tools.ML"
   156 use "Tools/SMT/z3_proof_literals.ML"
   157 use "Tools/SMT/z3_proof_methods.ML"
   158 use "Tools/SMT/z3_proof_reconstruction.ML"
   159 use "Tools/SMT/z3_model.ML"
   160 use "Tools/SMT/smt_setup_solvers.ML"
   161 
   162 setup {*
   163   SMT_Config.setup #>
   164   SMT_Normalize.setup #>
   165   SMT_Solver.setup #>
   166   SMTLIB_Interface.setup #>
   167   Z3_Interface.setup #>
   168   Z3_Proof_Reconstruction.setup #>
   169   SMT_Setup_Solvers.setup
   170 *}
   171 
   172 
   173 
   174 subsection {* Configuration *}
   175 
   176 text {*
   177 The current configuration can be printed by the command
   178 @{text smt_status}, which shows the values of most options.
   179 *}
   180 
   181 
   182 
   183 subsection {* General configuration options *}
   184 
   185 text {*
   186 The option @{text smt_solver} can be used to change the target SMT
   187 solver.  The possible values are @{text cvc3}, @{text yices}, and
   188 @{text z3}.  It is advisable to locally install the selected solver,
   189 although this is not necessary for @{text cvc3} and @{text z3}, which
   190 can also be used over an Internet-based service.
   191 
   192 When using local SMT solvers, the path to their binaries should be
   193 declared by setting the following environment variables:
   194 @{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
   195 *}
   196 
   197 declare [[ smt_solver = z3 ]]
   198 
   199 text {*
   200 Since SMT solvers are potentially non-terminating, there is a timeout
   201 (given in seconds) to restrict their runtime.  A value greater than
   202 120 (seconds) is in most cases not advisable.
   203 *}
   204 
   205 declare [[ smt_timeout = 20 ]]
   206 
   207 text {*
   208 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
   209 solvers are fully trusted without additional checks.  The following
   210 option can cause the SMT solver to run in proof-producing mode, giving
   211 a checkable certificate.  This is currently only implemented for Z3.
   212 *}
   213 
   214 declare [[ smt_oracle = false ]]
   215 
   216 text {*
   217 Each SMT solver provides several commandline options to tweak its
   218 behaviour.  They can be passed to the solver by setting the following
   219 options.
   220 *}
   221 
   222 declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
   223 
   224 text {*
   225 Enable the following option to use built-in support for datatypes and
   226 records.  Currently, this is only implemented for Z3 running in oracle
   227 mode.
   228 *}
   229 
   230 declare [[ smt_datatypes = false ]]
   231 
   232 
   233 
   234 subsection {* Certificates *}
   235 
   236 text {*
   237 By setting the option @{text smt_certificates} to the name of a file,
   238 all following applications of an SMT solver a cached in that file.
   239 Any further application of the same SMT solver (using the very same
   240 configuration) re-uses the cached certificate instead of invoking the
   241 solver.  An empty string disables caching certificates.
   242 
   243 The filename should be given as an explicit path.  It is good
   244 practice to use the name of the current theory (with ending
   245 @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   246 *}
   247 
   248 declare [[ smt_certificates = "" ]]
   249 
   250 text {*
   251 The option @{text smt_fixed} controls whether only stored
   252 certificates are should be used or invocation of an SMT solver is
   253 allowed.  When set to @{text true}, no SMT solver will ever be
   254 invoked and only the existing certificates found in the configured
   255 cache are used;  when set to @{text false} and there is no cached
   256 certificate for some proposition, then the configured SMT solver is
   257 invoked.
   258 *}
   259 
   260 declare [[ smt_fixed = false ]]
   261 
   262 
   263 
   264 subsection {* Tracing *}
   265 
   266 text {*
   267 The SMT method, when applied, traces important information.  To
   268 make it entirely silent, set the following option to @{text false}.
   269 *}
   270 
   271 declare [[ smt_verbose = true ]]
   272 
   273 text {*
   274 For tracing the generated problem file given to the SMT solver as
   275 well as the returned result of the solver, the option
   276 @{text smt_trace} should be set to @{text true}.
   277 *}
   278 
   279 declare [[ smt_trace = false ]]
   280 
   281 text {*
   282 From the set of assumptions given to the SMT solver, those assumptions
   283 used in the proof are traced when the following option is set to
   284 @{term true}.  This only works for Z3 when it runs in non-oracle mode
   285 (see options @{text smt_solver} and @{text smt_oracle} above).
   286 *}
   287 
   288 declare [[ smt_trace_used_facts = false ]]
   289 
   290 
   291 
   292 subsection {* Schematic rules for Z3 proof reconstruction *}
   293 
   294 text {*
   295 Several prof rules of Z3 are not very well documented.  There are two
   296 lemma groups which can turn failing Z3 proof reconstruction attempts
   297 into succeeding ones: the facts in @{text z3_rule} are tried prior to
   298 any implemented reconstruction procedure for all uncertain Z3 proof
   299 rules;  the facts in @{text z3_simp} are only fed to invocations of
   300 the simplifier when reconstructing theory-specific proof steps.
   301 *}
   302 
   303 lemmas [z3_rule] =
   304   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   305   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
   306   if_True if_False not_not
   307 
   308 lemma [z3_rule]:
   309   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
   310   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
   311   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
   312   by auto
   313 
   314 lemma [z3_rule]:
   315   "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
   316   by auto
   317 
   318 lemma [z3_rule]:
   319   "((\<not>P) = P) = False"
   320   "(P = (\<not>P)) = False"
   321   "(P \<noteq> Q) = (Q = (\<not>P))"
   322   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
   323   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
   324   by auto
   325 
   326 lemma [z3_rule]:
   327   "(if P then P else \<not>P) = True"
   328   "(if \<not>P then \<not>P else P) = True"
   329   "(if P then True else False) = P"
   330   "(if P then False else True) = (\<not>P)"
   331   "(if \<not>P then x else y) = (if P then y else x)"
   332   "f (if P then x else y) = (if P then f x else f y)"
   333   by auto
   334 
   335 lemma [z3_rule]:
   336   "P = Q \<or> P \<or> Q"
   337   "P = Q \<or> \<not>P \<or> \<not>Q"
   338   "(\<not>P) = Q \<or> \<not>P \<or> Q"
   339   "(\<not>P) = Q \<or> P \<or> \<not>Q"
   340   "P = (\<not>Q) \<or> \<not>P \<or> Q"
   341   "P = (\<not>Q) \<or> P \<or> \<not>Q"
   342   "P \<noteq> Q \<or> P \<or> \<not>Q"
   343   "P \<noteq> Q \<or> \<not>P \<or> Q"
   344   "P \<noteq> (\<not>Q) \<or> P \<or> Q"
   345   "(\<not>P) \<noteq> Q \<or> P \<or> Q"
   346   "P \<or> Q \<or> P \<noteq> (\<not>Q)"
   347   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
   348   "P \<or> \<not>Q \<or> P \<noteq> Q"
   349   "\<not>P \<or> Q \<or> P \<noteq> Q"
   350   by auto
   351 
   352 lemma [z3_rule]:
   353   "0 + (x::int) = x"
   354   "x + 0 = x"
   355   "0 * x = 0"
   356   "1 * x = x"
   357   "x + y = y + x"
   358   by auto
   359 
   360 
   361 
   362 hide_type term_bool
   363 hide_type (open) pattern
   364 hide_const Pattern fun_app
   365 hide_const (open) trigger pat nopat weight z3div z3mod
   366 
   367 
   368 
   369 subsection {* Selectors for datatypes *}
   370 
   371 setup {* Datatype_Selectors.setup *}
   372 
   373 declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
   374 declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
   375 
   376 end