36898

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 
"~~/src/Tools/cache_io.ML"


11 
("Tools/SMT/smt_additional_facts.ML")


12 
("Tools/SMT/smt_monomorph.ML")


13 
("Tools/SMT/smt_normalize.ML")


14 
("Tools/SMT/smt_translate.ML")


15 
("Tools/SMT/smt_solver.ML")


16 
("Tools/SMT/smtlib_interface.ML")


17 
("Tools/SMT/z3_proof_parser.ML")


18 
("Tools/SMT/z3_proof_tools.ML")


19 
("Tools/SMT/z3_proof_literals.ML")


20 
("Tools/SMT/z3_proof_reconstruction.ML")


21 
("Tools/SMT/z3_model.ML")


22 
("Tools/SMT/z3_interface.ML")


23 
("Tools/SMT/z3_solver.ML")


24 
("Tools/SMT/cvc3_solver.ML")


25 
("Tools/SMT/yices_solver.ML")


26 
begin


27 


28 


29 


30 
section {* Triggers for quantifier instantiation *}


31 


32 
text {*


33 
Some SMT solvers support triggers for quantifier instantiation.


34 
Each trigger consists of one ore more patterns. A pattern may either


35 
be a list of positive subterms (the first being tagged by "pat" and


36 
the consecutive subterms tagged by "andpat"), or a list of negative


37 
subterms (the first being tagged by "nopat" and the consecutive


38 
subterms tagged by "andpat").


39 
*}


40 


41 
datatype pattern = Pattern


42 


43 
definition pat :: "'a \<Rightarrow> pattern"


44 
where "pat _ = Pattern"


45 


46 
definition nopat :: "'a \<Rightarrow> pattern"


47 
where "nopat _ = Pattern"


48 


49 
definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)


50 
where "_ andpat _ = Pattern"


51 


52 
definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"


53 
where "trigger _ P = P"


54 


55 


56 


57 
section {* Higherorder encoding *}


58 


59 
text {*


60 
Application is made explicit for constants occurring with varying


61 
numbers of arguments. This is achieved by the introduction of the


62 
following constant.


63 
*}


64 


65 
definition "apply" where "apply f x = f x"


66 


67 
text {*


68 
Some solvers support a theory of arrays which can be used to encode


69 
higherorder functions. The following set of lemmas specifies the


70 
properties of such (extensional) arrays.


71 
*}


72 


73 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other


74 
fun_upd_upd


75 


76 


77 


78 
section {* Firstorder logic *}


79 


80 
text {*


81 
Some SMT solvers require a strict separation between formulas and


82 
terms. When translating higherorder into firstorder problems,


83 
all uninterpreted constants (those not builtin in the target solver)


84 
are treated as function symbols in the firstorder sense. Their


85 
occurrences as head symbols in atoms (i.e., as predicate symbols) is


86 
turned into terms by equating such atoms with @{term True} using the


87 
following termlevel equation symbol.


88 
*}


89 


90 
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)


91 
where "(x term_eq y) = (x = y)"


92 


93 


94 


95 
section {* Setup *}


96 


97 
use "Tools/SMT/smt_monomorph.ML"


98 
use "Tools/SMT/smt_normalize.ML"


99 
use "Tools/SMT/smt_translate.ML"


100 
use "Tools/SMT/smt_solver.ML"


101 
use "Tools/SMT/smtlib_interface.ML"


102 
use "Tools/SMT/z3_interface.ML"


103 
use "Tools/SMT/z3_proof_parser.ML"


104 
use "Tools/SMT/z3_proof_tools.ML"


105 
use "Tools/SMT/z3_proof_literals.ML"


106 
use "Tools/SMT/z3_proof_reconstruction.ML"


107 
use "Tools/SMT/z3_model.ML"


108 
use "Tools/SMT/z3_solver.ML"


109 
use "Tools/SMT/cvc3_solver.ML"


110 
use "Tools/SMT/yices_solver.ML"


111 


112 
setup {*


113 
SMT_Solver.setup #>


114 
Z3_Proof_Reconstruction.setup #>


115 
Z3_Solver.setup #>


116 
CVC3_Solver.setup #>


117 
Yices_Solver.setup


118 
*}


119 


120 


121 


122 
section {* Configuration *}


123 


124 
text {*


125 
The current configuration can be printed by the following command


126 
(which shows the values of most options):


127 
*}


128 


129 
smt_status


130 


131 


132 


133 
subsection {* General configuration options *}


134 


135 
text {*


136 
The option @{text smt_solver} can be used to change the target SMT


137 
solver. The possible values are @{text cvc3}, @{text yices}, and


138 
@{text z3}. It is advisable to locally install the selected solver,


139 
although this is not necessary for @{text cvc3} and @{text z3}, which


140 
can also be used over an Internetbased service.


141 


142 
When using local SMT solvers, the path to their binaries should be


143 
declared by setting the following environment variables:


144 
@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.


145 
*}


146 


147 
declare [[ smt_solver = z3 ]]


148 


149 
text {*


150 
Since SMT solvers are potentially nonterminating, there is a timeout


151 
(given in seconds) to restrict their runtime. A value greater than


152 
120 (seconds) is in most cases not advisable.


153 
*}


154 


155 
declare [[ smt_timeout = 20 ]]


156 


157 


158 


159 
subsection {* Certificates *}


160 


161 
text {*


162 
By setting the option @{text smt_certificates} to the name of a file,


163 
all following applications of an SMT solver a cached in that file.


164 
Any further application of the same SMT solver (using the very same


165 
configuration) reuses the cached certificate instead of invoking the


166 
solver. An empty string disables caching certificates.


167 


168 
The filename should be given as an explicit path. It is good


169 
practice to use the name of the current theory (with ending


170 
@{text ".certs"} instead of @{text ".thy"}) as the certificates file.


171 
*}


172 


173 
declare [[ smt_certificates = "" ]]


174 


175 
text {*


176 
The option @{text smt_fixed} controls whether only stored


177 
certificates are should be used or invocation of an SMT solver is


178 
allowed. When set to @{text true}, no SMT solver will ever be


179 
invoked and only the existing certificates found in the configured


180 
cache are used; when set to @{text false} and there is no cached


181 
certificate for some proposition, then the configured SMT solver is


182 
invoked.


183 
*}


184 


185 
declare [[ smt_fixed = false ]]


186 


187 


188 


189 
subsection {* Tracing *}


190 


191 
text {*


192 
For tracing the generated problem file given to the SMT solver as


193 
well as the returned result of the solver, the option


194 
@{text smt_trace} should be set to @{text true}.


195 
*}


196 


197 
declare [[ smt_trace = false ]]


198 


199 


200 


201 
subsection {* Z3specific options *}


202 


203 
text {*


204 
Z3 is the only SMT solver whose proofs are checked (or reconstructed)


205 
in Isabelle (all other solvers are implemented as oracles). Enabling


206 
or disabling proof reconstruction for Z3 is controlled by the option


207 
@{text z3_proofs}.


208 
*}


209 


210 
declare [[ z3_proofs = true ]]


211 


212 
text {*


213 
From the set of assumptions given to Z3, those assumptions used in


214 
the proof are traced when the option @{text z3_trace_assms} is set to


215 
@{term true}.


216 
*}


217 


218 
declare [[ z3_trace_assms = false ]]


219 


220 
text {*


221 
Z3 provides several commandline options to tweak its behaviour. They


222 
can be configured by writing them literally as value for the option


223 
@{text z3_options}.


224 
*}


225 


226 
declare [[ z3_options = "" ]]


227 


228 


229 


230 
section {* Schematic rules for Z3 proof reconstruction *}


231 


232 
text {*


233 
Several prof rules of Z3 are not very well documented. There are two


234 
lemma groups which can turn failing Z3 proof reconstruction attempts


235 
into succeeding ones: the facts in @{text z3_rule} are tried prior to


236 
any implemented reconstruction procedure for all uncertain Z3 proof


237 
rules; the facts in @{text z3_simp} are only fed to invocations of


238 
the simplifier when reconstructing theoryspecific proof steps.


239 
*}


240 


241 
lemmas [z3_rule] =


242 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps


243 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left


244 
if_True if_False not_not


245 


246 
lemma [z3_rule]:


247 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)"


248 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)"


249 
"(\<not>P \<longrightarrow> Q) = (Q \<or> P)"


250 
by auto


251 


252 
lemma [z3_rule]:


253 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not>P)))"


254 
by auto


255 


256 
lemma [z3_rule]:


257 
"((\<not>P) = P) = False"


258 
"(P = (\<not>P)) = False"


259 
"(P \<noteq> Q) = (Q = (\<not>P))"


260 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"


261 
"(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"


262 
by auto


263 


264 
lemma [z3_rule]:


265 
"(if P then P else \<not>P) = True"


266 
"(if \<not>P then \<not>P else P) = True"


267 
"(if P then True else False) = P"


268 
"(if P then False else True) = (\<not>P)"


269 
"(if \<not>P then x else y) = (if P then y else x)"


270 
by auto


271 


272 
lemma [z3_rule]:


273 
"P = Q \<or> P \<or> Q"


274 
"P = Q \<or> \<not>P \<or> \<not>Q"


275 
"(\<not>P) = Q \<or> \<not>P \<or> Q"


276 
"(\<not>P) = Q \<or> P \<or> \<not>Q"


277 
"P = (\<not>Q) \<or> \<not>P \<or> Q"


278 
"P = (\<not>Q) \<or> P \<or> \<not>Q"


279 
"P \<noteq> Q \<or> P \<or> \<not>Q"


280 
"P \<noteq> Q \<or> \<not>P \<or> Q"


281 
"P \<noteq> (\<not>Q) \<or> P \<or> Q"


282 
"(\<not>P) \<noteq> Q \<or> P \<or> Q"


283 
"P \<or> Q \<or> P \<noteq> (\<not>Q)"


284 
"P \<or> Q \<or> (\<not>P) \<noteq> Q"


285 
"P \<or> \<not>Q \<or> P \<noteq> Q"


286 
"\<not>P \<or> Q \<or> P \<noteq> Q"


287 
by auto


288 


289 
lemma [z3_rule]:


290 
"0 + (x::int) = x"


291 
"x + 0 = x"


292 
"0 * x = 0"


293 
"1 * x = x"


294 
"x + y = y + x"


295 
by auto


296 


297 
lemma [z3_rule]:


298 
"0 + (x::real) = x"


299 
"x + 0 = x"


300 
"0 * x = 0"


301 
"1 * x = x"


302 
"x + y = y + x"


303 
by auto


304 


305 


306 
end
