src/HOL/SMT.thy
author boehmes
Mon Nov 22 23:37:00 2010 +0100 (2010-11-22)
changeset 40664 e023788a91a1
parent 40662 798aad2229c0
child 40681 872b08416fb4
permissions -rw-r--r--
added support for quantifier weight annotations
     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 {* Distinctness *}
    85 
    86 text {*
    87 As an abbreviation for a quadratic number of inequalities, SMT solvers
    88 provide a built-in @{text distinct}.  To avoid confusion with the
    89 already defined (and more general) @{term List.distinct}, a separate
    90 constant is defined.
    91 *}
    92 
    93 definition distinct :: "'a list \<Rightarrow> bool"
    94 where "distinct xs = List.distinct xs"
    95 
    96 
    97 
    98 subsection {* Higher-order encoding *}
    99 
   100 text {*
   101 Application is made explicit for constants occurring with varying
   102 numbers of arguments.  This is achieved by the introduction of the
   103 following constant.
   104 *}
   105 
   106 definition fun_app where "fun_app f x = f x"
   107 
   108 text {*
   109 Some solvers support a theory of arrays which can be used to encode
   110 higher-order functions.  The following set of lemmas specifies the
   111 properties of such (extensional) arrays.
   112 *}
   113 
   114 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
   115   fun_upd_upd fun_app_def
   116 
   117 
   118 
   119 subsection {* First-order logic *}
   120 
   121 text {*
   122 Some SMT solvers require a strict separation between formulas and
   123 terms.  When translating higher-order into first-order problems,
   124 all uninterpreted constants (those not builtin in the target solver)
   125 are treated as function symbols in the first-order sense.  Their
   126 occurrences as head symbols in atoms (i.e., as predicate symbols) is
   127 turned into terms by equating such atoms with @{term True} using the
   128 following term-level equation symbol.
   129 *}
   130 
   131 definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
   132 
   133 
   134 
   135 subsection {* Integer division and modulo for Z3 *}
   136 
   137 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
   138   "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
   139 
   140 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
   141   "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
   142 
   143 lemma div_by_z3div: "k div l = (
   144      if k = 0 \<or> l = 0 then 0
   145      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
   146      else z3div (-k) (-l))"
   147   by (auto simp add: z3div_def)
   148 
   149 lemma mod_by_z3mod: "k mod l = (
   150      if l = 0 then k
   151      else if k = 0 then 0
   152      else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
   153      else - z3mod (-k) (-l))"
   154   by (auto simp add: z3mod_def)
   155 
   156 
   157 
   158 subsection {* Setup *}
   159 
   160 use "Tools/SMT/smt_builtin.ML"
   161 use "Tools/SMT/smt_normalize.ML"
   162 use "Tools/SMT/smt_translate.ML"
   163 use "Tools/SMT/smt_solver.ML"
   164 use "Tools/SMT/smtlib_interface.ML"
   165 use "Tools/SMT/z3_interface.ML"
   166 use "Tools/SMT/z3_proof_parser.ML"
   167 use "Tools/SMT/z3_proof_tools.ML"
   168 use "Tools/SMT/z3_proof_literals.ML"
   169 use "Tools/SMT/z3_proof_methods.ML"
   170 use "Tools/SMT/z3_proof_reconstruction.ML"
   171 use "Tools/SMT/z3_model.ML"
   172 use "Tools/SMT/smt_setup_solvers.ML"
   173 
   174 setup {*
   175   SMT_Config.setup #>
   176   SMT_Solver.setup #>
   177   Z3_Proof_Reconstruction.setup #>
   178   SMT_Setup_Solvers.setup
   179 *}
   180 
   181 
   182 
   183 subsection {* Configuration *}
   184 
   185 text {*
   186 The current configuration can be printed by the command
   187 @{text smt_status}, which shows the values of most options.
   188 *}
   189 
   190 
   191 
   192 subsection {* General configuration options *}
   193 
   194 text {*
   195 The option @{text smt_solver} can be used to change the target SMT
   196 solver.  The possible values are @{text cvc3}, @{text yices}, and
   197 @{text z3}.  It is advisable to locally install the selected solver,
   198 although this is not necessary for @{text cvc3} and @{text z3}, which
   199 can also be used over an Internet-based service.
   200 
   201 When using local SMT solvers, the path to their binaries should be
   202 declared by setting the following environment variables:
   203 @{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
   204 *}
   205 
   206 declare [[ smt_solver = z3 ]]
   207 
   208 text {*
   209 Since SMT solvers are potentially non-terminating, there is a timeout
   210 (given in seconds) to restrict their runtime.  A value greater than
   211 120 (seconds) is in most cases not advisable.
   212 *}
   213 
   214 declare [[ smt_timeout = 20 ]]
   215 
   216 text {*
   217 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
   218 solvers are fully trusted without additional checks.  The following
   219 option can cause the SMT solver to run in proof-producing mode, giving
   220 a checkable certificate.  This is currently only implemented for Z3.
   221 *}
   222 
   223 declare [[ smt_oracle = false ]]
   224 
   225 text {*
   226 Each SMT solver provides several commandline options to tweak its
   227 behaviour.  They can be passed to the solver by setting the following
   228 options.
   229 *}
   230 
   231 declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
   232 
   233 text {*
   234 Enable the following option to use built-in support for datatypes and
   235 records.  Currently, this is only implemented for Z3 running in oracle
   236 mode.
   237 *}
   238 
   239 declare [[ smt_datatypes = false ]]
   240 
   241 
   242 
   243 subsection {* Certificates *}
   244 
   245 text {*
   246 By setting the option @{text smt_certificates} to the name of a file,
   247 all following applications of an SMT solver a cached in that file.
   248 Any further application of the same SMT solver (using the very same
   249 configuration) re-uses the cached certificate instead of invoking the
   250 solver.  An empty string disables caching certificates.
   251 
   252 The filename should be given as an explicit path.  It is good
   253 practice to use the name of the current theory (with ending
   254 @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   255 *}
   256 
   257 declare [[ smt_certificates = "" ]]
   258 
   259 text {*
   260 The option @{text smt_fixed} controls whether only stored
   261 certificates are should be used or invocation of an SMT solver is
   262 allowed.  When set to @{text true}, no SMT solver will ever be
   263 invoked and only the existing certificates found in the configured
   264 cache are used;  when set to @{text false} and there is no cached
   265 certificate for some proposition, then the configured SMT solver is
   266 invoked.
   267 *}
   268 
   269 declare [[ smt_fixed = false ]]
   270 
   271 
   272 
   273 subsection {* Tracing *}
   274 
   275 text {*
   276 The SMT method, when applied, traces important information.  To
   277 make it entirely silent, set the following option to @{text false}.
   278 *}
   279 
   280 declare [[ smt_verbose = true ]]
   281 
   282 text {*
   283 For tracing the generated problem file given to the SMT solver as
   284 well as the returned result of the solver, the option
   285 @{text smt_trace} should be set to @{text true}.
   286 *}
   287 
   288 declare [[ smt_trace = false ]]
   289 
   290 text {*
   291 From the set of assumptions given to the SMT solver, those assumptions
   292 used in the proof are traced when the following option is set to
   293 @{term true}.  This only works for Z3 when it runs in non-oracle mode
   294 (see options @{text smt_solver} and @{text smt_oracle} above).
   295 *}
   296 
   297 declare [[ smt_trace_used_facts = false ]]
   298 
   299 
   300 
   301 subsection {* Schematic rules for Z3 proof reconstruction *}
   302 
   303 text {*
   304 Several prof rules of Z3 are not very well documented.  There are two
   305 lemma groups which can turn failing Z3 proof reconstruction attempts
   306 into succeeding ones: the facts in @{text z3_rule} are tried prior to
   307 any implemented reconstruction procedure for all uncertain Z3 proof
   308 rules;  the facts in @{text z3_simp} are only fed to invocations of
   309 the simplifier when reconstructing theory-specific proof steps.
   310 *}
   311 
   312 lemmas [z3_rule] =
   313   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   314   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
   315   if_True if_False not_not
   316 
   317 lemma [z3_rule]:
   318   "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
   319   "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
   320   "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
   321   by auto
   322 
   323 lemma [z3_rule]:
   324   "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
   325   by auto
   326 
   327 lemma [z3_rule]:
   328   "((\<not>P) = P) = False"
   329   "(P = (\<not>P)) = False"
   330   "(P \<noteq> Q) = (Q = (\<not>P))"
   331   "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
   332   "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
   333   by auto
   334 
   335 lemma [z3_rule]:
   336   "(if P then P else \<not>P) = True"
   337   "(if \<not>P then \<not>P else P) = True"
   338   "(if P then True else False) = P"
   339   "(if P then False else True) = (\<not>P)"
   340   "(if \<not>P then x else y) = (if P then y else x)"
   341   by auto
   342 
   343 lemma [z3_rule]:
   344   "P = Q \<or> P \<or> Q"
   345   "P = Q \<or> \<not>P \<or> \<not>Q"
   346   "(\<not>P) = Q \<or> \<not>P \<or> Q"
   347   "(\<not>P) = Q \<or> P \<or> \<not>Q"
   348   "P = (\<not>Q) \<or> \<not>P \<or> Q"
   349   "P = (\<not>Q) \<or> P \<or> \<not>Q"
   350   "P \<noteq> Q \<or> P \<or> \<not>Q"
   351   "P \<noteq> Q \<or> \<not>P \<or> Q"
   352   "P \<noteq> (\<not>Q) \<or> P \<or> Q"
   353   "(\<not>P) \<noteq> Q \<or> P \<or> Q"
   354   "P \<or> Q \<or> P \<noteq> (\<not>Q)"
   355   "P \<or> Q \<or> (\<not>P) \<noteq> Q"
   356   "P \<or> \<not>Q \<or> P \<noteq> Q"
   357   "\<not>P \<or> Q \<or> P \<noteq> Q"
   358   by auto
   359 
   360 lemma [z3_rule]:
   361   "0 + (x::int) = x"
   362   "x + 0 = x"
   363   "0 * x = 0"
   364   "1 * x = x"
   365   "x + y = y + x"
   366   by auto
   367 
   368 
   369 
   370 hide_type (open) pattern
   371 hide_const Pattern term_eq
   372 hide_const (open) trigger pat nopat weight distinct fun_app 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