src/HOL/SMT.thy
author boehmes
Wed May 12 23:54:02 2010 +0200 (2010-05-12)
changeset 36898 8e55aa1306c5
child 36899 bcd6fce5bf06
permissions -rw-r--r--
integrated SMT into the HOL image
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@36898
    10
  "~~/src/Tools/cache_io.ML"
boehmes@36898
    11
  ("Tools/SMT/smt_additional_facts.ML")
boehmes@36898
    12
  ("Tools/SMT/smt_monomorph.ML")
boehmes@36898
    13
  ("Tools/SMT/smt_normalize.ML")
boehmes@36898
    14
  ("Tools/SMT/smt_translate.ML")
boehmes@36898
    15
  ("Tools/SMT/smt_solver.ML")
boehmes@36898
    16
  ("Tools/SMT/smtlib_interface.ML")
boehmes@36898
    17
  ("Tools/SMT/z3_proof_parser.ML")
boehmes@36898
    18
  ("Tools/SMT/z3_proof_tools.ML")
boehmes@36898
    19
  ("Tools/SMT/z3_proof_literals.ML")
boehmes@36898
    20
  ("Tools/SMT/z3_proof_reconstruction.ML")
boehmes@36898
    21
  ("Tools/SMT/z3_model.ML")
boehmes@36898
    22
  ("Tools/SMT/z3_interface.ML")
boehmes@36898
    23
  ("Tools/SMT/z3_solver.ML")
boehmes@36898
    24
  ("Tools/SMT/cvc3_solver.ML")
boehmes@36898
    25
  ("Tools/SMT/yices_solver.ML")
boehmes@36898
    26
begin
boehmes@36898
    27
boehmes@36898
    28
boehmes@36898
    29
boehmes@36898
    30
section {* Triggers for quantifier instantiation *}
boehmes@36898
    31
boehmes@36898
    32
text {*
boehmes@36898
    33
Some SMT solvers support triggers for quantifier instantiation.
boehmes@36898
    34
Each trigger consists of one ore more patterns.  A pattern may either
boehmes@36898
    35
be a list of positive subterms (the first being tagged by "pat" and
boehmes@36898
    36
the consecutive subterms tagged by "andpat"), or a list of negative
boehmes@36898
    37
subterms (the first being tagged by "nopat" and the consecutive
boehmes@36898
    38
subterms tagged by "andpat").
boehmes@36898
    39
*}
boehmes@36898
    40
boehmes@36898
    41
datatype pattern = Pattern
boehmes@36898
    42
boehmes@36898
    43
definition pat :: "'a \<Rightarrow> pattern"
boehmes@36898
    44
where "pat _ = Pattern"
boehmes@36898
    45
boehmes@36898
    46
definition nopat :: "'a \<Rightarrow> pattern"
boehmes@36898
    47
where "nopat _ = Pattern"
boehmes@36898
    48
boehmes@36898
    49
definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
boehmes@36898
    50
where "_ andpat _ = Pattern"
boehmes@36898
    51
boehmes@36898
    52
definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
boehmes@36898
    53
where "trigger _ P = P"
boehmes@36898
    54
boehmes@36898
    55
boehmes@36898
    56
boehmes@36898
    57
section {* Higher-order encoding *}
boehmes@36898
    58
boehmes@36898
    59
text {*
boehmes@36898
    60
Application is made explicit for constants occurring with varying
boehmes@36898
    61
numbers of arguments.  This is achieved by the introduction of the
boehmes@36898
    62
following constant.
boehmes@36898
    63
*}
boehmes@36898
    64
boehmes@36898
    65
definition "apply" where "apply f x = f x"
boehmes@36898
    66
boehmes@36898
    67
text {*
boehmes@36898
    68
Some solvers support a theory of arrays which can be used to encode
boehmes@36898
    69
higher-order functions.  The following set of lemmas specifies the
boehmes@36898
    70
properties of such (extensional) arrays.
boehmes@36898
    71
*}
boehmes@36898
    72
boehmes@36898
    73
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
boehmes@36898
    74
  fun_upd_upd
boehmes@36898
    75
boehmes@36898
    76
boehmes@36898
    77
boehmes@36898
    78
section {* First-order logic *}
boehmes@36898
    79
boehmes@36898
    80
text {*
boehmes@36898
    81
Some SMT solvers require a strict separation between formulas and
boehmes@36898
    82
terms.  When translating higher-order into first-order problems,
boehmes@36898
    83
all uninterpreted constants (those not builtin in the target solver)
boehmes@36898
    84
are treated as function symbols in the first-order sense.  Their
boehmes@36898
    85
occurrences as head symbols in atoms (i.e., as predicate symbols) is
boehmes@36898
    86
turned into terms by equating such atoms with @{term True} using the
boehmes@36898
    87
following term-level equation symbol.
boehmes@36898
    88
*}
boehmes@36898
    89
boehmes@36898
    90
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
boehmes@36898
    91
  where "(x term_eq y) = (x = y)"
boehmes@36898
    92
boehmes@36898
    93
boehmes@36898
    94
boehmes@36898
    95
section {* Setup *}
boehmes@36898
    96
boehmes@36898
    97
use "Tools/SMT/smt_monomorph.ML"
boehmes@36898
    98
use "Tools/SMT/smt_normalize.ML"
boehmes@36898
    99
use "Tools/SMT/smt_translate.ML"
boehmes@36898
   100
use "Tools/SMT/smt_solver.ML"
boehmes@36898
   101
use "Tools/SMT/smtlib_interface.ML"
boehmes@36898
   102
use "Tools/SMT/z3_interface.ML"
boehmes@36898
   103
use "Tools/SMT/z3_proof_parser.ML"
boehmes@36898
   104
use "Tools/SMT/z3_proof_tools.ML"
boehmes@36898
   105
use "Tools/SMT/z3_proof_literals.ML"
boehmes@36898
   106
use "Tools/SMT/z3_proof_reconstruction.ML"
boehmes@36898
   107
use "Tools/SMT/z3_model.ML"
boehmes@36898
   108
use "Tools/SMT/z3_solver.ML"
boehmes@36898
   109
use "Tools/SMT/cvc3_solver.ML"
boehmes@36898
   110
use "Tools/SMT/yices_solver.ML"
boehmes@36898
   111
boehmes@36898
   112
setup {*
boehmes@36898
   113
  SMT_Solver.setup #>
boehmes@36898
   114
  Z3_Proof_Reconstruction.setup #>
boehmes@36898
   115
  Z3_Solver.setup #>
boehmes@36898
   116
  CVC3_Solver.setup #>
boehmes@36898
   117
  Yices_Solver.setup
boehmes@36898
   118
*}
boehmes@36898
   119
boehmes@36898
   120
boehmes@36898
   121
boehmes@36898
   122
section {* Configuration *}
boehmes@36898
   123
boehmes@36898
   124
text {*
boehmes@36898
   125
The current configuration can be printed by the following command
boehmes@36898
   126
(which shows the values of most options):
boehmes@36898
   127
*}
boehmes@36898
   128
boehmes@36898
   129
smt_status
boehmes@36898
   130
boehmes@36898
   131
boehmes@36898
   132
boehmes@36898
   133
subsection {* General configuration options *}
boehmes@36898
   134
boehmes@36898
   135
text {*
boehmes@36898
   136
The option @{text smt_solver} can be used to change the target SMT
boehmes@36898
   137
solver.  The possible values are @{text cvc3}, @{text yices}, and
boehmes@36898
   138
@{text z3}.  It is advisable to locally install the selected solver,
boehmes@36898
   139
although this is not necessary for @{text cvc3} and @{text z3}, which
boehmes@36898
   140
can also be used over an Internet-based service.
boehmes@36898
   141
boehmes@36898
   142
When using local SMT solvers, the path to their binaries should be
boehmes@36898
   143
declared by setting the following environment variables:
boehmes@36898
   144
@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
boehmes@36898
   145
*}
boehmes@36898
   146
boehmes@36898
   147
declare [[ smt_solver = z3 ]]
boehmes@36898
   148
boehmes@36898
   149
text {*
boehmes@36898
   150
Since SMT solvers are potentially non-terminating, there is a timeout
boehmes@36898
   151
(given in seconds) to restrict their runtime.  A value greater than
boehmes@36898
   152
120 (seconds) is in most cases not advisable.
boehmes@36898
   153
*}
boehmes@36898
   154
boehmes@36898
   155
declare [[ smt_timeout = 20 ]]
boehmes@36898
   156
boehmes@36898
   157
boehmes@36898
   158
boehmes@36898
   159
subsection {* Certificates *}
boehmes@36898
   160
boehmes@36898
   161
text {*
boehmes@36898
   162
By setting the option @{text smt_certificates} to the name of a file,
boehmes@36898
   163
all following applications of an SMT solver a cached in that file.
boehmes@36898
   164
Any further application of the same SMT solver (using the very same
boehmes@36898
   165
configuration) re-uses the cached certificate instead of invoking the
boehmes@36898
   166
solver.  An empty string disables caching certificates.
boehmes@36898
   167
boehmes@36898
   168
The filename should be given as an explicit path.  It is good
boehmes@36898
   169
practice to use the name of the current theory (with ending
boehmes@36898
   170
@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
boehmes@36898
   171
*}
boehmes@36898
   172
boehmes@36898
   173
declare [[ smt_certificates = "" ]]
boehmes@36898
   174
boehmes@36898
   175
text {*
boehmes@36898
   176
The option @{text smt_fixed} controls whether only stored
boehmes@36898
   177
certificates are should be used or invocation of an SMT solver is
boehmes@36898
   178
allowed.  When set to @{text true}, no SMT solver will ever be
boehmes@36898
   179
invoked and only the existing certificates found in the configured
boehmes@36898
   180
cache are used;  when set to @{text false} and there is no cached
boehmes@36898
   181
certificate for some proposition, then the configured SMT solver is
boehmes@36898
   182
invoked.
boehmes@36898
   183
*}
boehmes@36898
   184
boehmes@36898
   185
declare [[ smt_fixed = false ]]
boehmes@36898
   186
boehmes@36898
   187
boehmes@36898
   188
boehmes@36898
   189
subsection {* Tracing *}
boehmes@36898
   190
boehmes@36898
   191
text {*
boehmes@36898
   192
For tracing the generated problem file given to the SMT solver as
boehmes@36898
   193
well as the returned result of the solver, the option
boehmes@36898
   194
@{text smt_trace} should be set to @{text true}.
boehmes@36898
   195
*}
boehmes@36898
   196
boehmes@36898
   197
declare [[ smt_trace = false ]]
boehmes@36898
   198
boehmes@36898
   199
boehmes@36898
   200
boehmes@36898
   201
subsection {* Z3-specific options *}
boehmes@36898
   202
boehmes@36898
   203
text {*
boehmes@36898
   204
Z3 is the only SMT solver whose proofs are checked (or reconstructed)
boehmes@36898
   205
in Isabelle (all other solvers are implemented as oracles).  Enabling
boehmes@36898
   206
or disabling proof reconstruction for Z3 is controlled by the option
boehmes@36898
   207
@{text z3_proofs}. 
boehmes@36898
   208
*}
boehmes@36898
   209
boehmes@36898
   210
declare [[ z3_proofs = true ]]
boehmes@36898
   211
boehmes@36898
   212
text {*
boehmes@36898
   213
From the set of assumptions given to Z3, those assumptions used in
boehmes@36898
   214
the proof are traced when the option @{text z3_trace_assms} is set to
boehmes@36898
   215
@{term true}.
boehmes@36898
   216
*}
boehmes@36898
   217
boehmes@36898
   218
declare [[ z3_trace_assms = false ]]
boehmes@36898
   219
boehmes@36898
   220
text {*
boehmes@36898
   221
Z3 provides several commandline options to tweak its behaviour.  They
boehmes@36898
   222
can be configured by writing them literally as value for the option
boehmes@36898
   223
@{text z3_options}.
boehmes@36898
   224
*}
boehmes@36898
   225
boehmes@36898
   226
declare [[ z3_options = "" ]]
boehmes@36898
   227
boehmes@36898
   228
boehmes@36898
   229
boehmes@36898
   230
section {* Schematic rules for Z3 proof reconstruction *}
boehmes@36898
   231
boehmes@36898
   232
text {*
boehmes@36898
   233
Several prof rules of Z3 are not very well documented.  There are two
boehmes@36898
   234
lemma groups which can turn failing Z3 proof reconstruction attempts
boehmes@36898
   235
into succeeding ones: the facts in @{text z3_rule} are tried prior to
boehmes@36898
   236
any implemented reconstruction procedure for all uncertain Z3 proof
boehmes@36898
   237
rules;  the facts in @{text z3_simp} are only fed to invocations of
boehmes@36898
   238
the simplifier when reconstructing theory-specific proof steps.
boehmes@36898
   239
*}
boehmes@36898
   240
boehmes@36898
   241
lemmas [z3_rule] =
boehmes@36898
   242
  refl eq_commute conj_commute disj_commute simp_thms nnf_simps
boehmes@36898
   243
  ring_distribs field_simps times_divide_eq_right times_divide_eq_left
boehmes@36898
   244
  if_True if_False not_not
boehmes@36898
   245
boehmes@36898
   246
lemma [z3_rule]:
boehmes@36898
   247
  "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
boehmes@36898
   248
  "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
boehmes@36898
   249
  "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
boehmes@36898
   250
  by auto
boehmes@36898
   251
boehmes@36898
   252
lemma [z3_rule]:
boehmes@36898
   253
  "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
boehmes@36898
   254
  by auto
boehmes@36898
   255
boehmes@36898
   256
lemma [z3_rule]:
boehmes@36898
   257
  "((\<not>P) = P) = False"
boehmes@36898
   258
  "(P = (\<not>P)) = False"
boehmes@36898
   259
  "(P \<noteq> Q) = (Q = (\<not>P))"
boehmes@36898
   260
  "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
boehmes@36898
   261
  "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
boehmes@36898
   262
  by auto
boehmes@36898
   263
boehmes@36898
   264
lemma [z3_rule]:
boehmes@36898
   265
  "(if P then P else \<not>P) = True"
boehmes@36898
   266
  "(if \<not>P then \<not>P else P) = True"
boehmes@36898
   267
  "(if P then True else False) = P"
boehmes@36898
   268
  "(if P then False else True) = (\<not>P)"
boehmes@36898
   269
  "(if \<not>P then x else y) = (if P then y else x)"
boehmes@36898
   270
  by auto
boehmes@36898
   271
boehmes@36898
   272
lemma [z3_rule]:
boehmes@36898
   273
  "P = Q \<or> P \<or> Q"
boehmes@36898
   274
  "P = Q \<or> \<not>P \<or> \<not>Q"
boehmes@36898
   275
  "(\<not>P) = Q \<or> \<not>P \<or> Q"
boehmes@36898
   276
  "(\<not>P) = Q \<or> P \<or> \<not>Q"
boehmes@36898
   277
  "P = (\<not>Q) \<or> \<not>P \<or> Q"
boehmes@36898
   278
  "P = (\<not>Q) \<or> P \<or> \<not>Q"
boehmes@36898
   279
  "P \<noteq> Q \<or> P \<or> \<not>Q"
boehmes@36898
   280
  "P \<noteq> Q \<or> \<not>P \<or> Q"
boehmes@36898
   281
  "P \<noteq> (\<not>Q) \<or> P \<or> Q"
boehmes@36898
   282
  "(\<not>P) \<noteq> Q \<or> P \<or> Q"
boehmes@36898
   283
  "P \<or> Q \<or> P \<noteq> (\<not>Q)"
boehmes@36898
   284
  "P \<or> Q \<or> (\<not>P) \<noteq> Q"
boehmes@36898
   285
  "P \<or> \<not>Q \<or> P \<noteq> Q"
boehmes@36898
   286
  "\<not>P \<or> Q \<or> P \<noteq> Q"
boehmes@36898
   287
  by auto
boehmes@36898
   288
boehmes@36898
   289
lemma [z3_rule]:
boehmes@36898
   290
  "0 + (x::int) = x"
boehmes@36898
   291
  "x + 0 = x"
boehmes@36898
   292
  "0 * x = 0"
boehmes@36898
   293
  "1 * x = x"
boehmes@36898
   294
  "x + y = y + x"
boehmes@36898
   295
  by auto
boehmes@36898
   296
boehmes@36898
   297
lemma [z3_rule]:
boehmes@36898
   298
  "0 + (x::real) = x"
boehmes@36898
   299
  "x + 0 = x"
boehmes@36898
   300
  "0 * x = 0"
boehmes@36898
   301
  "1 * x = x"
boehmes@36898
   302
  "x + y = y + x"
boehmes@36898
   303
  by auto
boehmes@36898
   304
boehmes@36898
   305
boehmes@36898
   306
end