src/HOL/SMT.thy
author blanchet
Tue Aug 09 09:05:21 2011 +0200 (2011-08-09)
changeset 44087 8e491cb8841c
parent 43929 61d432e51aff
child 44488 587bf61a00a1
permissions -rw-r--r--
load lambda-lifting structure earlier, so it can be used in Metis
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@41426
     8
imports Record
boehmes@36898
     9
uses
boehmes@41124
    10
  "Tools/SMT/smt_utils.ML"
boehmes@40424
    11
  "Tools/SMT/smt_failure.ML"
boehmes@40424
    12
  "Tools/SMT/smt_config.ML"
boehmes@40277
    13
  ("Tools/SMT/smt_builtin.ML")
boehmes@41426
    14
  ("Tools/SMT/smt_datatypes.ML")
boehmes@36898
    15
  ("Tools/SMT/smt_normalize.ML")
boehmes@36898
    16
  ("Tools/SMT/smt_translate.ML")
boehmes@36898
    17
  ("Tools/SMT/smt_solver.ML")
boehmes@36898
    18
  ("Tools/SMT/smtlib_interface.ML")
boehmes@41328
    19
  ("Tools/SMT/z3_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@40162
    26
  ("Tools/SMT/smt_setup_solvers.ML")
boehmes@36898
    27
begin
boehmes@36898
    28
boehmes@36898
    29
boehmes@36898
    30
huffman@36902
    31
subsection {* Triggers for quantifier instantiation *}
boehmes@36898
    32
boehmes@36898
    33
text {*
boehmes@41125
    34
Some SMT solvers support patterns as a quantifier instantiation
boehmes@41125
    35
heuristics.  Patterns may either be positive terms (tagged by "pat")
boehmes@41125
    36
triggering quantifier instantiations -- when the solver finds a
boehmes@41125
    37
term matching a positive pattern, it instantiates the corresponding
boehmes@41125
    38
quantifier accordingly -- or negative terms (tagged by "nopat")
boehmes@41125
    39
inhibiting quantifier instantiations.  A list of patterns
boehmes@41125
    40
of the same kind is called a multipattern, and all patterns in a
boehmes@41125
    41
multipattern are considered conjunctively for quantifier instantiation.
boehmes@41125
    42
A list of multipatterns is called a trigger, and their multipatterns
boehmes@41125
    43
act disjunctively during quantifier instantiation.  Each multipattern
boehmes@41125
    44
should mention at least all quantified variables of the preceding
boehmes@41125
    45
quantifier block.
boehmes@36898
    46
*}
boehmes@36898
    47
boehmes@36898
    48
datatype pattern = Pattern
boehmes@36898
    49
boehmes@37124
    50
definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
boehmes@37124
    51
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
boehmes@36898
    52
boehmes@37124
    53
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
boehmes@36898
    54
where "trigger _ P = P"
boehmes@36898
    55
boehmes@36898
    56
boehmes@36898
    57
boehmes@40664
    58
subsection {* Quantifier weights *}
boehmes@40664
    59
boehmes@40664
    60
text {*
boehmes@40664
    61
Weight annotations to quantifiers influence the priority of quantifier
boehmes@40664
    62
instantiations.  They should be handled with care for solvers, which support
boehmes@40664
    63
them, because incorrect choices of weights might render a problem unsolvable.
boehmes@40664
    64
*}
boehmes@40664
    65
boehmes@40664
    66
definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
boehmes@40664
    67
boehmes@40664
    68
text {*
boehmes@40664
    69
Weights must be non-negative.  The value @{text 0} is equivalent to providing
boehmes@40664
    70
no weight at all.
boehmes@40664
    71
boehmes@40664
    72
Weights should only be used at quantifiers and only inside triggers (if the
boehmes@40664
    73
quantifier has triggers).  Valid usages of weights are as follows:
boehmes@40664
    74
boehmes@40664
    75
\begin{itemize}
boehmes@40664
    76
\item
boehmes@40664
    77
@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
boehmes@40664
    78
\item
boehmes@40664
    79
@{term "\<forall>x. weight 3 (P x)"}
boehmes@40664
    80
\end{itemize}
boehmes@40664
    81
*}
boehmes@40664
    82
boehmes@40664
    83
boehmes@40664
    84
huffman@36902
    85
subsection {* Higher-order encoding *}
boehmes@36898
    86
boehmes@36898
    87
text {*
boehmes@36898
    88
Application is made explicit for constants occurring with varying
boehmes@36898
    89
numbers of arguments.  This is achieved by the introduction of the
boehmes@36898
    90
following constant.
boehmes@36898
    91
*}
boehmes@36898
    92
boehmes@41127
    93
definition fun_app where "fun_app f = f"
boehmes@36898
    94
boehmes@36898
    95
text {*
boehmes@36898
    96
Some solvers support a theory of arrays which can be used to encode
boehmes@36898
    97
higher-order functions.  The following set of lemmas specifies the
boehmes@36898
    98
properties of such (extensional) arrays.
boehmes@36898
    99
*}
boehmes@36898
   100
boehmes@36898
   101
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
boehmes@37157
   102
  fun_upd_upd fun_app_def
boehmes@36898
   103
boehmes@36898
   104
boehmes@36898
   105
huffman@36902
   106
subsection {* First-order logic *}
boehmes@36898
   107
boehmes@36898
   108
text {*
boehmes@41059
   109
Some SMT solvers only accept problems in first-order logic, i.e.,
boehmes@41059
   110
where formulas and terms are syntactically separated. When
boehmes@41059
   111
translating higher-order into first-order problems, all
boehmes@41059
   112
uninterpreted constants (those not built-in in the target solver)
boehmes@36898
   113
are treated as function symbols in the first-order sense.  Their
boehmes@41059
   114
occurrences as head symbols in atoms (i.e., as predicate symbols) are
boehmes@41281
   115
turned into terms by logically equating such atoms with @{term True}.
boehmes@41281
   116
For technical reasons, @{term True} and @{term False} occurring inside
boehmes@41281
   117
terms are replaced by the following constants.
boehmes@36898
   118
*}
boehmes@36898
   119
boehmes@41281
   120
definition term_true where "term_true = True"
boehmes@41281
   121
definition term_false where "term_false = False"
boehmes@41281
   122
boehmes@36898
   123
boehmes@36898
   124
boehmes@37151
   125
subsection {* Integer division and modulo for Z3 *}
boehmes@37151
   126
boehmes@37151
   127
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151
   128
  "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
boehmes@37151
   129
boehmes@37151
   130
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151
   131
  "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
boehmes@37151
   132
boehmes@37151
   133
boehmes@37151
   134
huffman@36902
   135
subsection {* Setup *}
boehmes@36898
   136
boehmes@40277
   137
use "Tools/SMT/smt_builtin.ML"
boehmes@41426
   138
use "Tools/SMT/smt_datatypes.ML"
boehmes@36898
   139
use "Tools/SMT/smt_normalize.ML"
boehmes@36898
   140
use "Tools/SMT/smt_translate.ML"
boehmes@36898
   141
use "Tools/SMT/smt_solver.ML"
boehmes@36898
   142
use "Tools/SMT/smtlib_interface.ML"
boehmes@36898
   143
use "Tools/SMT/z3_interface.ML"
boehmes@36898
   144
use "Tools/SMT/z3_proof_parser.ML"
boehmes@36898
   145
use "Tools/SMT/z3_proof_tools.ML"
boehmes@36898
   146
use "Tools/SMT/z3_proof_literals.ML"
boehmes@40662
   147
use "Tools/SMT/z3_proof_methods.ML"
boehmes@36898
   148
use "Tools/SMT/z3_proof_reconstruction.ML"
boehmes@36898
   149
use "Tools/SMT/z3_model.ML"
boehmes@40162
   150
use "Tools/SMT/smt_setup_solvers.ML"
boehmes@36898
   151
boehmes@36898
   152
setup {*
boehmes@40424
   153
  SMT_Config.setup #>
boehmes@41059
   154
  SMT_Normalize.setup #>
boehmes@36898
   155
  SMT_Solver.setup #>
boehmes@41059
   156
  SMTLIB_Interface.setup #>
boehmes@41059
   157
  Z3_Interface.setup #>
boehmes@36898
   158
  Z3_Proof_Reconstruction.setup #>
boehmes@40162
   159
  SMT_Setup_Solvers.setup
boehmes@36898
   160
*}
boehmes@36898
   161
boehmes@36898
   162
boehmes@36898
   163
huffman@36902
   164
subsection {* Configuration *}
boehmes@36898
   165
boehmes@36898
   166
text {*
boehmes@36899
   167
The current configuration can be printed by the command
boehmes@36899
   168
@{text smt_status}, which shows the values of most options.
boehmes@36898
   169
*}
boehmes@36898
   170
boehmes@36898
   171
boehmes@36898
   172
boehmes@36898
   173
subsection {* General configuration options *}
boehmes@36898
   174
boehmes@36898
   175
text {*
boehmes@36898
   176
The option @{text smt_solver} can be used to change the target SMT
boehmes@41432
   177
solver.  The possible values can be obtained from the @{text smt_status}
boehmes@41432
   178
command.
boehmes@41459
   179
boehmes@41459
   180
Due to licensing restrictions, Yices and Z3 are not installed/enabled
boehmes@41459
   181
by default.  Z3 is free for non-commercial applications and can be enabled
boehmes@41462
   182
by simply setting the environment variable @{text Z3_NON_COMMERCIAL} to
boehmes@41462
   183
@{text yes}.
boehmes@36898
   184
*}
boehmes@36898
   185
boehmes@41601
   186
declare [[ smt_solver = z3 ]]
boehmes@36898
   187
boehmes@36898
   188
text {*
boehmes@36898
   189
Since SMT solvers are potentially non-terminating, there is a timeout
boehmes@36898
   190
(given in seconds) to restrict their runtime.  A value greater than
boehmes@36898
   191
120 (seconds) is in most cases not advisable.
boehmes@36898
   192
*}
boehmes@36898
   193
boehmes@36898
   194
declare [[ smt_timeout = 20 ]]
boehmes@36898
   195
boehmes@40162
   196
text {*
boehmes@41121
   197
SMT solvers apply randomized heuristics.  In case a problem is not
boehmes@41121
   198
solvable by an SMT solver, changing the following option might help.
boehmes@41121
   199
*}
boehmes@41121
   200
boehmes@41121
   201
declare [[ smt_random_seed = 1 ]]
boehmes@41121
   202
boehmes@41121
   203
text {*
boehmes@40162
   204
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
boehmes@40162
   205
solvers are fully trusted without additional checks.  The following
boehmes@40162
   206
option can cause the SMT solver to run in proof-producing mode, giving
boehmes@40162
   207
a checkable certificate.  This is currently only implemented for Z3.
boehmes@40162
   208
*}
boehmes@40162
   209
boehmes@40162
   210
declare [[ smt_oracle = false ]]
boehmes@40162
   211
boehmes@40162
   212
text {*
boehmes@40162
   213
Each SMT solver provides several commandline options to tweak its
boehmes@40162
   214
behaviour.  They can be passed to the solver by setting the following
boehmes@40162
   215
options.
boehmes@40162
   216
*}
boehmes@40162
   217
boehmes@41432
   218
declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
boehmes@41432
   219
declare [[ yices_options = "" ]]
boehmes@41432
   220
declare [[ z3_options = "", remote_z3_options = "" ]]
boehmes@40162
   221
boehmes@40162
   222
text {*
boehmes@40162
   223
Enable the following option to use built-in support for datatypes and
boehmes@40162
   224
records.  Currently, this is only implemented for Z3 running in oracle
boehmes@40162
   225
mode.
boehmes@40162
   226
*}
boehmes@40162
   227
boehmes@40162
   228
declare [[ smt_datatypes = false ]]
boehmes@40162
   229
boehmes@41125
   230
text {*
boehmes@41125
   231
The SMT method provides an inference mechanism to detect simple triggers
boehmes@41125
   232
in quantified formulas, which might increase the number of problems
boehmes@41125
   233
solvable by SMT solvers (note: triggers guide quantifier instantiations
boehmes@41125
   234
in the SMT solver).  To turn it on, set the following option.
boehmes@41125
   235
*}
boehmes@41125
   236
boehmes@41125
   237
declare [[ smt_infer_triggers = false ]]
boehmes@41125
   238
boehmes@41125
   239
text {*
boehmes@41125
   240
The SMT method monomorphizes the given facts, that is, it tries to
boehmes@41125
   241
instantiate all schematic type variables with fixed types occurring
boehmes@41125
   242
in the problem.  This is a (possibly nonterminating) fixed-point
boehmes@41125
   243
construction whose cycles are limited by the following option.
boehmes@41125
   244
*}
boehmes@41125
   245
boehmes@43230
   246
declare [[ monomorph_max_rounds = 5 ]]
boehmes@41125
   247
boehmes@41762
   248
text {*
boehmes@41762
   249
In addition, the number of generated monomorphic instances is limited
boehmes@41762
   250
by the following option.
boehmes@41762
   251
*}
boehmes@41762
   252
boehmes@43230
   253
declare [[ monomorph_max_new_instances = 500 ]]
boehmes@41762
   254
boehmes@36898
   255
boehmes@36898
   256
boehmes@36898
   257
subsection {* Certificates *}
boehmes@36898
   258
boehmes@36898
   259
text {*
boehmes@36898
   260
By setting the option @{text smt_certificates} to the name of a file,
boehmes@36898
   261
all following applications of an SMT solver a cached in that file.
boehmes@36898
   262
Any further application of the same SMT solver (using the very same
boehmes@36898
   263
configuration) re-uses the cached certificate instead of invoking the
boehmes@36898
   264
solver.  An empty string disables caching certificates.
boehmes@36898
   265
boehmes@36898
   266
The filename should be given as an explicit path.  It is good
boehmes@36898
   267
practice to use the name of the current theory (with ending
boehmes@36898
   268
@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
boehmes@36898
   269
*}
boehmes@36898
   270
boehmes@36898
   271
declare [[ smt_certificates = "" ]]
boehmes@36898
   272
boehmes@36898
   273
text {*
boehmes@36898
   274
The option @{text smt_fixed} controls whether only stored
boehmes@36898
   275
certificates are should be used or invocation of an SMT solver is
boehmes@36898
   276
allowed.  When set to @{text true}, no SMT solver will ever be
boehmes@36898
   277
invoked and only the existing certificates found in the configured
boehmes@36898
   278
cache are used;  when set to @{text false} and there is no cached
boehmes@36898
   279
certificate for some proposition, then the configured SMT solver is
boehmes@36898
   280
invoked.
boehmes@36898
   281
*}
boehmes@36898
   282
boehmes@36898
   283
declare [[ smt_fixed = false ]]
boehmes@36898
   284
boehmes@36898
   285
boehmes@36898
   286
boehmes@36898
   287
subsection {* Tracing *}
boehmes@36898
   288
boehmes@36898
   289
text {*
boehmes@40424
   290
The SMT method, when applied, traces important information.  To
boehmes@40424
   291
make it entirely silent, set the following option to @{text false}.
boehmes@40424
   292
*}
boehmes@40424
   293
boehmes@40424
   294
declare [[ smt_verbose = true ]]
boehmes@40424
   295
boehmes@40424
   296
text {*
boehmes@36898
   297
For tracing the generated problem file given to the SMT solver as
boehmes@36898
   298
well as the returned result of the solver, the option
boehmes@36898
   299
@{text smt_trace} should be set to @{text true}.
boehmes@36898
   300
*}
boehmes@36898
   301
boehmes@36898
   302
declare [[ smt_trace = false ]]
boehmes@36898
   303
boehmes@36898
   304
text {*
boehmes@40162
   305
From the set of assumptions given to the SMT solver, those assumptions
boehmes@40162
   306
used in the proof are traced when the following option is set to
boehmes@40162
   307
@{term true}.  This only works for Z3 when it runs in non-oracle mode
boehmes@40162
   308
(see options @{text smt_solver} and @{text smt_oracle} above).
boehmes@36898
   309
*}
boehmes@36898
   310
boehmes@40162
   311
declare [[ smt_trace_used_facts = false ]]
boehmes@39298
   312
boehmes@36898
   313
boehmes@36898
   314
huffman@36902
   315
subsection {* Schematic rules for Z3 proof reconstruction *}
boehmes@36898
   316
boehmes@36898
   317
text {*
boehmes@36898
   318
Several prof rules of Z3 are not very well documented.  There are two
boehmes@36898
   319
lemma groups which can turn failing Z3 proof reconstruction attempts
boehmes@36898
   320
into succeeding ones: the facts in @{text z3_rule} are tried prior to
boehmes@36898
   321
any implemented reconstruction procedure for all uncertain Z3 proof
boehmes@36898
   322
rules;  the facts in @{text z3_simp} are only fed to invocations of
boehmes@36898
   323
the simplifier when reconstructing theory-specific proof steps.
boehmes@36898
   324
*}
boehmes@36898
   325
boehmes@36898
   326
lemmas [z3_rule] =
boehmes@36898
   327
  refl eq_commute conj_commute disj_commute simp_thms nnf_simps
boehmes@36898
   328
  ring_distribs field_simps times_divide_eq_right times_divide_eq_left
boehmes@36898
   329
  if_True if_False not_not
boehmes@36898
   330
boehmes@36898
   331
lemma [z3_rule]:
boehmes@36898
   332
  "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
boehmes@36898
   333
  "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
boehmes@36898
   334
  "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
boehmes@36898
   335
  by auto
boehmes@36898
   336
boehmes@36898
   337
lemma [z3_rule]:
boehmes@36898
   338
  "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
boehmes@36898
   339
  by auto
boehmes@36898
   340
boehmes@36898
   341
lemma [z3_rule]:
boehmes@36898
   342
  "((\<not>P) = P) = False"
boehmes@36898
   343
  "(P = (\<not>P)) = False"
boehmes@36898
   344
  "(P \<noteq> Q) = (Q = (\<not>P))"
boehmes@36898
   345
  "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
boehmes@36898
   346
  "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
boehmes@36898
   347
  by auto
boehmes@36898
   348
boehmes@36898
   349
lemma [z3_rule]:
boehmes@36898
   350
  "(if P then P else \<not>P) = True"
boehmes@36898
   351
  "(if \<not>P then \<not>P else P) = True"
boehmes@36898
   352
  "(if P then True else False) = P"
boehmes@36898
   353
  "(if P then False else True) = (\<not>P)"
boehmes@36898
   354
  "(if \<not>P then x else y) = (if P then y else x)"
boehmes@40806
   355
  "f (if P then x else y) = (if P then f x else f y)"
boehmes@36898
   356
  by auto
boehmes@36898
   357
boehmes@36898
   358
lemma [z3_rule]:
boehmes@36898
   359
  "P = Q \<or> P \<or> Q"
boehmes@36898
   360
  "P = Q \<or> \<not>P \<or> \<not>Q"
boehmes@36898
   361
  "(\<not>P) = Q \<or> \<not>P \<or> Q"
boehmes@36898
   362
  "(\<not>P) = Q \<or> P \<or> \<not>Q"
boehmes@36898
   363
  "P = (\<not>Q) \<or> \<not>P \<or> Q"
boehmes@36898
   364
  "P = (\<not>Q) \<or> P \<or> \<not>Q"
boehmes@36898
   365
  "P \<noteq> Q \<or> P \<or> \<not>Q"
boehmes@36898
   366
  "P \<noteq> Q \<or> \<not>P \<or> Q"
boehmes@36898
   367
  "P \<noteq> (\<not>Q) \<or> P \<or> Q"
boehmes@36898
   368
  "(\<not>P) \<noteq> Q \<or> P \<or> Q"
boehmes@36898
   369
  "P \<or> Q \<or> P \<noteq> (\<not>Q)"
boehmes@36898
   370
  "P \<or> Q \<or> (\<not>P) \<noteq> Q"
boehmes@36898
   371
  "P \<or> \<not>Q \<or> P \<noteq> Q"
boehmes@36898
   372
  "\<not>P \<or> Q \<or> P \<noteq> Q"
boehmes@36898
   373
  by auto
boehmes@36898
   374
boehmes@36898
   375
lemma [z3_rule]:
boehmes@36898
   376
  "0 + (x::int) = x"
boehmes@36898
   377
  "x + 0 = x"
boehmes@36898
   378
  "0 * x = 0"
boehmes@36898
   379
  "1 * x = x"
boehmes@36898
   380
  "x + y = y + x"
boehmes@36898
   381
  by auto
boehmes@36898
   382
boehmes@37124
   383
boehmes@37124
   384
boehmes@37124
   385
hide_type (open) pattern
boehmes@41281
   386
hide_const Pattern fun_app term_true term_false z3div z3mod
boehmes@41280
   387
hide_const (open) trigger pat nopat weight
boehmes@37124
   388
boehmes@36898
   389
end