src/HOL/SMT.thy
author boehmes
Wed Dec 15 08:39:24 2010 +0100 (2010-12-15)
changeset 41124 1de17a2de5ad
parent 41121 5c5d05963f93
child 41125 4a9eec045f2a
permissions -rw-r--r--
moved SMT classes and dictionary functions to SMT_Utils
     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_utils.ML"
    12   "Tools/SMT/smt_failure.ML"
    13   "Tools/SMT/smt_config.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 SMT solvers apply randomized heuristics.  In case a problem is not
   209 solvable by an SMT solver, changing the following option might help.
   210 *}
   211 
   212 declare [[ smt_random_seed = 1 ]]
   213 
   214 text {*
   215 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
   216 solvers are fully trusted without additional checks.  The following
   217 option can cause the SMT solver to run in proof-producing mode, giving
   218 a checkable certificate.  This is currently only implemented for Z3.
   219 *}
   220 
   221 declare [[ smt_oracle = false ]]
   222 
   223 text {*
   224 Each SMT solver provides several commandline options to tweak its
   225 behaviour.  They can be passed to the solver by setting the following
   226 options.
   227 *}
   228 
   229 declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
   230 
   231 text {*
   232 Enable the following option to use built-in support for datatypes and
   233 records.  Currently, this is only implemented for Z3 running in oracle
   234 mode.
   235 *}
   236 
   237 declare [[ smt_datatypes = false ]]
   238 
   239 
   240 
   241 subsection {* Certificates *}
   242 
   243 text {*
   244 By setting the option @{text smt_certificates} to the name of a file,
   245 all following applications of an SMT solver a cached in that file.
   246 Any further application of the same SMT solver (using the very same
   247 configuration) re-uses the cached certificate instead of invoking the
   248 solver.  An empty string disables caching certificates.
   249 
   250 The filename should be given as an explicit path.  It is good
   251 practice to use the name of the current theory (with ending
   252 @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   253 *}
   254 
   255 declare [[ smt_certificates = "" ]]
   256 
   257 text {*
   258 The option @{text smt_fixed} controls whether only stored
   259 certificates are should be used or invocation of an SMT solver is
   260 allowed.  When set to @{text true}, no SMT solver will ever be
   261 invoked and only the existing certificates found in the configured
   262 cache are used;  when set to @{text false} and there is no cached
   263 certificate for some proposition, then the configured SMT solver is
   264 invoked.
   265 *}
   266 
   267 declare [[ smt_fixed = false ]]
   268 
   269 
   270 
   271 subsection {* Tracing *}
   272 
   273 text {*
   274 The SMT method, when applied, traces important information.  To
   275 make it entirely silent, set the following option to @{text false}.
   276 *}
   277 
   278 declare [[ smt_verbose = true ]]
   279 
   280 text {*
   281 For tracing the generated problem file given to the SMT solver as
   282 well as the returned result of the solver, the option
   283 @{text smt_trace} should be set to @{text true}.
   284 *}
   285 
   286 declare [[ smt_trace = false ]]
   287 
   288 text {*
   289 From the set of assumptions given to the SMT solver, those assumptions
   290 used in the proof are traced when the following option is set to
   291 @{term true}.  This only works for Z3 when it runs in non-oracle mode
   292 (see options @{text smt_solver} and @{text smt_oracle} above).
   293 *}
   294 
   295 declare [[ smt_trace_used_facts = false ]]
   296 
   297 
   298 
   299 subsection {* Schematic rules for Z3 proof reconstruction *}
   300 
   301 text {*
   302 Several prof rules of Z3 are not very well documented.  There are two
   303 lemma groups which can turn failing Z3 proof reconstruction attempts
   304 into succeeding ones: the facts in @{text z3_rule} are tried prior to
   305 any implemented reconstruction procedure for all uncertain Z3 proof
   306 rules;  the facts in @{text z3_simp} are only fed to invocations of
   307 the simplifier when reconstructing theory-specific proof steps.
   308 *}
   309 
   310 lemmas [z3_rule] =
   311   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   312   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
   313   if_True if_False not_not
   314 
   315 lemma [z3_rule]:
   316   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
   317   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
   318   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
   319   by auto
   320 
   321 lemma [z3_rule]:
   322   "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
   323   by auto
   324 
   325 lemma [z3_rule]:
   326   "((\<not>P) = P) = False"
   327   "(P = (\<not>P)) = False"
   328   "(P \<noteq> Q) = (Q = (\<not>P))"
   329   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
   330   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
   331   by auto
   332 
   333 lemma [z3_rule]:
   334   "(if P then P else \<not>P) = True"
   335   "(if \<not>P then \<not>P else P) = True"
   336   "(if P then True else False) = P"
   337   "(if P then False else True) = (\<not>P)"
   338   "(if \<not>P then x else y) = (if P then y else x)"
   339   "f (if P then x else y) = (if P then f x else f y)"
   340   by auto
   341 
   342 lemma [z3_rule]:
   343   "P = Q \<or> P \<or> Q"
   344   "P = Q \<or> \<not>P \<or> \<not>Q"
   345   "(\<not>P) = Q \<or> \<not>P \<or> Q"
   346   "(\<not>P) = Q \<or> P \<or> \<not>Q"
   347   "P = (\<not>Q) \<or> \<not>P \<or> Q"
   348   "P = (\<not>Q) \<or> P \<or> \<not>Q"
   349   "P \<noteq> Q \<or> P \<or> \<not>Q"
   350   "P \<noteq> Q \<or> \<not>P \<or> Q"
   351   "P \<noteq> (\<not>Q) \<or> P \<or> Q"
   352   "(\<not>P) \<noteq> Q \<or> P \<or> Q"
   353   "P \<or> Q \<or> P \<noteq> (\<not>Q)"
   354   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
   355   "P \<or> \<not>Q \<or> P \<noteq> Q"
   356   "\<not>P \<or> Q \<or> P \<noteq> Q"
   357   by auto
   358 
   359 lemma [z3_rule]:
   360   "0 + (x::int) = x"
   361   "x + 0 = x"
   362   "0 * x = 0"
   363   "1 * x = x"
   364   "x + y = y + x"
   365   by auto
   366 
   367 
   368 
   369 hide_type term_bool
   370 hide_type (open) pattern
   371 hide_const Pattern fun_app
   372 hide_const (open) trigger pat nopat weight z3div z3mod
   373 
   374 
   375 
   376 subsection {* Selectors for datatypes *}
   377 
   378 setup {* Datatype_Selectors.setup *}
   379 
   380 declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
   381 declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
   382 
   383 end