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