author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64078  0b22328a353c 
permissions  rwrr 
58057  1 
(* Title: HOL/Library/Old_SMT.thy 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 
*) 

4 

60500  5 
section \<open>Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers\<close> 
36898  6 

58057  7 
theory Old_SMT 
58056  8 
imports "../Real" "../Word/Word" 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

9 
keywords "old_smt_status" :: diag 
36898  10 
begin 
11 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

12 
ML_file "Old_SMT/old_smt_utils.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

13 
ML_file "Old_SMT/old_smt_failure.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

14 
ML_file "Old_SMT/old_smt_config.ML" 
36898  15 

16 

60500  17 
subsection \<open>Triggers for quantifier instantiation\<close> 
36898  18 

60500  19 
text \<open> 
41125  20 
Some SMT solvers support patterns as a quantifier instantiation 
21 
heuristics. Patterns may either be positive terms (tagged by "pat") 

22 
triggering quantifier instantiations  when the solver finds a 

23 
term matching a positive pattern, it instantiates the corresponding 

24 
quantifier accordingly  or negative terms (tagged by "nopat") 

25 
inhibiting quantifier instantiations. A list of patterns 

26 
of the same kind is called a multipattern, and all patterns in a 

27 
multipattern are considered conjunctively for quantifier instantiation. 

28 
A list of multipatterns is called a trigger, and their multipatterns 

29 
act disjunctively during quantifier instantiation. Each multipattern 

30 
should mention at least all quantified variables of the preceding 

31 
quantifier block. 

60500  32 
\<close> 
36898  33 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

34 
typedecl pattern 
36898  35 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

36 
consts 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

37 
pat :: "'a \<Rightarrow> pattern" 
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

38 
nopat :: "'a \<Rightarrow> pattern" 
36898  39 

56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

40 
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" 
36898  41 

42 

60500  43 
subsection \<open>Quantifier weights\<close> 
40664  44 

60500  45 
text \<open> 
40664  46 
Weight annotations to quantifiers influence the priority of quantifier 
47 
instantiations. They should be handled with care for solvers, which support 

48 
them, because incorrect choices of weights might render a problem unsolvable. 

60500  49 
\<close> 
40664  50 

51 
definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P" 

52 

60500  53 
text \<open> 
61585  54 
Weights must be nonnegative. The value \<open>0\<close> is equivalent to providing 
40664  55 
no weight at all. 
56 

57 
Weights should only be used at quantifiers and only inside triggers (if the 

58 
quantifier has triggers). Valid usages of weights are as follows: 

59 

60 
\begin{itemize} 

61 
\item 

62 
@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"} 

63 
\item 

64 
@{term "\<forall>x. weight 3 (P x)"} 

65 
\end{itemize} 

60500  66 
\<close> 
40664  67 

68 

60500  69 
subsection \<open>Higherorder encoding\<close> 
36898  70 

60500  71 
text \<open> 
36898  72 
Application is made explicit for constants occurring with varying 
73 
numbers of arguments. This is achieved by the introduction of the 

74 
following constant. 

60500  75 
\<close> 
36898  76 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

77 
definition fun_app where "fun_app f = f" 
36898  78 

60500  79 
text \<open> 
36898  80 
Some solvers support a theory of arrays which can be used to encode 
81 
higherorder functions. The following set of lemmas specifies the 

82 
properties of such (extensional) arrays. 

60500  83 
\<close> 
36898  84 

85 
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other 

37157  86 
fun_upd_upd fun_app_def 
36898  87 

88 

60500  89 
subsection \<open>Firstorder logic\<close> 
36898  90 

60500  91 
text \<open> 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

92 
Some SMT solvers only accept problems in firstorder logic, i.e., 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

93 
where formulas and terms are syntactically separated. When 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

94 
translating higherorder into firstorder problems, all 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

95 
uninterpreted constants (those not builtin in the target solver) 
36898  96 
are treated as function symbols in the firstorder sense. Their 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40806
diff
changeset

97 
occurrences as head symbols in atoms (i.e., as predicate symbols) are 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

98 
turned into terms by logically equating such atoms with @{term True}. 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

99 
For technical reasons, @{term True} and @{term False} occurring inside 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

100 
terms are replaced by the following constants. 
60500  101 
\<close> 
36898  102 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

103 
definition term_true where "term_true = True" 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

104 
definition term_false where "term_false = False" 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

105 

36898  106 

60500  107 
subsection \<open>Integer division and modulo for Z3\<close> 
37151  108 

109 
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 

110 
"z3div k l = (if 0 \<le> l then k div l else (k div (l)))" 

111 

112 
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 

113 
"z3mod k l = (if 0 \<le> l then k mod l else k mod (l))" 

114 

115 

60500  116 
subsection \<open>Setup\<close> 
36898  117 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

118 
ML_file "Old_SMT/old_smt_builtin.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

119 
ML_file "Old_SMT/old_smt_datatypes.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

120 
ML_file "Old_SMT/old_smt_normalize.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

121 
ML_file "Old_SMT/old_smt_translate.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

122 
ML_file "Old_SMT/old_smt_solver.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

123 
ML_file "Old_SMT/old_smtlib_interface.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

124 
ML_file "Old_SMT/old_z3_interface.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

125 
ML_file "Old_SMT/old_z3_proof_parser.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

126 
ML_file "Old_SMT/old_z3_proof_tools.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

127 
ML_file "Old_SMT/old_z3_proof_literals.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

128 
ML_file "Old_SMT/old_z3_proof_methods.ML" 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

129 
named_theorems old_z3_simp "simplification rules for Z3 proof reconstruction" 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

130 
ML_file "Old_SMT/old_z3_proof_reconstruction.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

131 
ML_file "Old_SMT/old_z3_model.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

132 
ML_file "Old_SMT/old_smt_setup_solvers.ML" 
36898  133 

60500  134 
setup \<open> 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

135 
Old_SMT_Config.setup #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

136 
Old_SMT_Normalize.setup #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

137 
Old_SMTLIB_Interface.setup #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

138 
Old_Z3_Interface.setup #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

139 
Old_SMT_Setup_Solvers.setup 
60500  140 
\<close> 
36898  141 

60500  142 
method_setup old_smt = \<open> 
47701  143 
Scan.optional Attrib.thms [] >> 
144 
(fn thms => fn ctxt => 

64078  145 
(legacy_feature "Proof method \"old_smt\" will be discontinued soon  use \"smt\" instead"; 
146 
METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))) 

60500  147 
\<close> "apply an SMT solver to the current goal" 
36898  148 

149 

60500  150 
subsection \<open>Configuration\<close> 
36898  151 

60500  152 
text \<open> 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

153 
The current configuration can be printed by the command 
61585  154 
\<open>old_smt_status\<close>, which shows the values of most options. 
60500  155 
\<close> 
36898  156 

157 

158 

60500  159 
subsection \<open>General configuration options\<close> 
36898  160 

60500  161 
text \<open> 
61585  162 
The option \<open>old_smt_solver\<close> can be used to change the target SMT 
163 
solver. The possible values can be obtained from the \<open>old_smt_status\<close> 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

164 
command. 
41459
f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

165 

f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

166 
Due to licensing restrictions, Yices and Z3 are not installed/enabled 
f0db8f40d656
added hints about licensing restrictions and how to enable Z3
boehmes
parents:
41432
diff
changeset

167 
by default. Z3 is free for noncommercial applications and can be enabled 
61585  168 
by setting the \<open>OLD_Z3_NON_COMMERCIAL\<close> environment variable to 
169 
\<open>yes\<close>. 

60500  170 
\<close> 
36898  171 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

172 
declare [[ old_smt_solver = z3 ]] 
36898  173 

60500  174 
text \<open> 
36898  175 
Since SMT solvers are potentially nonterminating, there is a timeout 
176 
(given in seconds) to restrict their runtime. A value greater than 

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

60500  178 
\<close> 
36898  179 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

180 
declare [[ old_smt_timeout = 20 ]] 
36898  181 

60500  182 
text \<open> 
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

183 
SMT solvers apply randomized heuristics. In case a problem is not 
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

184 
solvable by an SMT solver, changing the following option might help. 
60500  185 
\<close> 
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

186 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

187 
declare [[ old_smt_random_seed = 1 ]] 
41121
5c5d05963f93
added option to modify the random seed of SMT solvers
boehmes
parents:
41059
diff
changeset

188 

60500  189 
text \<open> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

190 
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

191 
solvers are fully trusted without additional checks. The following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

192 
option can cause the SMT solver to run in proofproducing mode, giving 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

193 
a checkable certificate. This is currently only implemented for Z3. 
60500  194 
\<close> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

195 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

196 
declare [[ old_smt_oracle = false ]] 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

197 

60500  198 
text \<open> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

199 
Each SMT solver provides several commandline options to tweak its 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

200 
behaviour. They can be passed to the solver by setting the following 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

201 
options. 
60500  202 
\<close> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

203 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

204 
declare [[ old_cvc3_options = "" ]] 
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

205 
declare [[ old_yices_options = "" ]] 
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

206 
declare [[ old_z3_options = "" ]] 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

207 

60500  208 
text \<open> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

209 
Enable the following option to use builtin support for datatypes and 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

210 
records. Currently, this is only implemented for Z3 running in oracle 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

211 
mode. 
60500  212 
\<close> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

213 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

214 
declare [[ old_smt_datatypes = false ]] 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

215 

60500  216 
text \<open> 
41125  217 
The SMT method provides an inference mechanism to detect simple triggers 
218 
in quantified formulas, which might increase the number of problems 

219 
solvable by SMT solvers (note: triggers guide quantifier instantiations 

220 
in the SMT solver). To turn it on, set the following option. 

60500  221 
\<close> 
41125  222 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

223 
declare [[ old_smt_infer_triggers = false ]] 
41125  224 

60500  225 
text \<open> 
41125  226 
The SMT method monomorphizes the given facts, that is, it tries to 
227 
instantiate all schematic type variables with fixed types occurring 

228 
in the problem. This is a (possibly nonterminating) fixedpoint 

229 
construction whose cycles are limited by the following option. 

60500  230 
\<close> 
41125  231 

43230
dabf6e311213
clarified meaning of monomorphization configuration option by renaming it
boehmes
parents:
41762
diff
changeset

232 
declare [[ monomorph_max_rounds = 5 ]] 
41125  233 

60500  234 
text \<open> 
41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

235 
In addition, the number of generated monomorphic instances is limited 
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

236 
by the following option. 
60500  237 
\<close> 
41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

238 

43230
dabf6e311213
clarified meaning of monomorphization configuration option by renaming it
boehmes
parents:
41762
diff
changeset

239 
declare [[ monomorph_max_new_instances = 500 ]] 
41762
00060198de12
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
boehmes
parents:
41601
diff
changeset

240 

36898  241 

242 

60500  243 
subsection \<open>Certificates\<close> 
36898  244 

60500  245 
text \<open> 
61585  246 
By setting the option \<open>old_smt_certificates\<close> to the name of a file, 
36898  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) reuses 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 

61585  254 
\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file. 
50317
4d1590544b91
synchronized read access to cache file  avoid potential conflict with ongoing write (which is nonatomic);
wenzelm
parents:
48892
diff
changeset

255 
Certificate files should be used at most once in a certain theory context, 
4d1590544b91
synchronized read access to cache file  avoid potential conflict with ongoing write (which is nonatomic);
wenzelm
parents:
48892
diff
changeset

256 
to avoid race conditions with other concurrent accesses. 
60500  257 
\<close> 
36898  258 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

259 
declare [[ old_smt_certificates = "" ]] 
36898  260 

60500  261 
text \<open> 
61585  262 
The option \<open>old_smt_read_only_certificates\<close> controls whether only 
47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

263 
stored certificates are should be used or invocation of an SMT solver 
61585  264 
is allowed. When set to \<open>true\<close>, no SMT solver will ever be 
36898  265 
invoked and only the existing certificates found in the configured 
61585  266 
cache are used; when set to \<open>false\<close> and there is no cached 
36898  267 
certificate for some proposition, then the configured SMT solver is 
268 
invoked. 

60500  269 
\<close> 
36898  270 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

271 
declare [[ old_smt_read_only_certificates = false ]] 
36898  272 

273 

274 

60500  275 
subsection \<open>Tracing\<close> 
36898  276 

60500  277 
text \<open> 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

278 
The SMT method, when applied, traces important information. To 
61585  279 
make it entirely silent, set the following option to \<open>false\<close>. 
60500  280 
\<close> 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

281 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

282 
declare [[ old_smt_verbose = true ]] 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40277
diff
changeset

283 

60500  284 
text \<open> 
36898  285 
For tracing the generated problem file given to the SMT solver as 
286 
well as the returned result of the solver, the option 

61585  287 
\<open>old_smt_trace\<close> should be set to \<open>true\<close>. 
60500  288 
\<close> 
36898  289 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

290 
declare [[ old_smt_trace = false ]] 
36898  291 

60500  292 
text \<open> 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

293 
From the set of assumptions given to the SMT solver, those assumptions 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

294 
used in the proof are traced when the following option is set to 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
39483
diff
changeset

295 
@{term true}. This only works for Z3 when it runs in nonoracle mode 
61585  296 
(see options \<open>old_smt_solver\<close> and \<open>old_smt_oracle\<close> above). 
60500  297 
\<close> 
36898  298 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

299 
declare [[ old_smt_trace_used_facts = false ]] 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37818
diff
changeset

300 

36898  301 

302 

60500  303 
subsection \<open>Schematic rules for Z3 proof reconstruction\<close> 
36898  304 

60500  305 
text \<open> 
36898  306 
Several prof rules of Z3 are not very well documented. There are two 
307 
lemma groups which can turn failing Z3 proof reconstruction attempts 

61585  308 
into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to 
36898  309 
any implemented reconstruction procedure for all uncertain Z3 proof 
61585  310 
rules; the facts in \<open>z3_simp\<close> are only fed to invocations of 
36898  311 
the simplifier when reconstructing theoryspecific proof steps. 
60500  312 
\<close> 
36898  313 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

314 
lemmas [old_z3_rule] = 
36898  315 
refl eq_commute conj_commute disj_commute simp_thms nnf_simps 
316 
ring_distribs field_simps times_divide_eq_right times_divide_eq_left 

317 
if_True if_False not_not 

318 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

319 
lemma [old_z3_rule]: 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

320 
"(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

321 
"(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

322 
"(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

323 
"(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

324 
"(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

325 
"(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

326 
"(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

327 
"(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

328 
by auto 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

329 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

330 
lemma [old_z3_rule]: 
36898  331 
"(P \<longrightarrow> Q) = (Q \<or> \<not>P)" 
332 
"(\<not>P \<longrightarrow> Q) = (P \<or> Q)" 

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

334 
"(True \<longrightarrow> P) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

335 
"(P \<longrightarrow> True) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

336 
"(False \<longrightarrow> P) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

337 
"(P \<longrightarrow> P) = True" 
36898  338 
by auto 
339 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

340 
lemma [old_z3_rule]: 
36898  341 
"((P = Q) \<longrightarrow> R) = (R  (Q = (\<not>P)))" 
342 
by auto 

343 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

344 
lemma [old_z3_rule]: 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

345 
"(\<not>True) = False" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

346 
"(\<not>False) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

347 
"(x = x) = True" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

348 
"(P = True) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

349 
"(True = P) = P" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

350 
"(P = False) = (\<not>P)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

351 
"(False = P) = (\<not>P)" 
36898  352 
"((\<not>P) = P) = False" 
353 
"(P = (\<not>P)) = False" 

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

354 
"((\<not>P) = (\<not>Q)) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

355 
"\<not>(P = (\<not>Q)) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

356 
"\<not>((\<not>P) = Q) = (P = Q)" 
36898  357 
"(P \<noteq> Q) = (Q = (\<not>P))" 
358 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

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

360 
by auto 

361 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

362 
lemma [old_z3_rule]: 
36898  363 
"(if P then P else \<not>P) = True" 
364 
"(if \<not>P then \<not>P else P) = True" 

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

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

367 
"(if P then Q else True) = ((\<not>P) \<or> Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

368 
"(if P then Q else True) = (Q \<or> (\<not>P))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

369 
"(if P then Q else \<not>Q) = (P = Q)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

370 
"(if P then Q else \<not>Q) = (Q = P)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

371 
"(if P then \<not>Q else Q) = (P = (\<not>Q))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

372 
"(if P then \<not>Q else Q) = ((\<not>Q) = P)" 
36898  373 
"(if \<not>P then x else y) = (if P then y else x)" 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

374 
"(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

375 
"(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

376 
"(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

377 
"(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

378 
"(if P then x else if P then y else z) = (if P then x else z)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

379 
"(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

380 
"(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

381 
"(if P then x = y else x = z) = (x = (if P then y else z))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

382 
"(if P then x = y else y = z) = (y = (if P then x else z))" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

383 
"(if P then x = y else z = y) = (y = (if P then x else z))" 
36898  384 
by auto 
385 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

386 
lemma [old_z3_rule]: 
44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

387 
"0 + (x::int) = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

388 
"x + 0 = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

389 
"x + x = 2 * x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

390 
"0 * x = 0" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

391 
"1 * x = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

392 
"x + y = y + x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

393 
by auto 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

394 

58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

395 
lemma [old_z3_rule]: (* for defaxiom *) 
36898  396 
"P = Q \<or> P \<or> Q" 
397 
"P = Q \<or> \<not>P \<or> \<not>Q" 

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

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

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

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

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

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

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

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

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

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

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

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

44488
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

410 
"P \<or> y = (if P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

411 
"P \<or> (if P then x else y) = y" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

412 
"\<not>P \<or> x = (if P then x else y)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

413 
"\<not>P \<or> (if P then x else y) = x" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

414 
"P \<or> R \<or> \<not>(if P then Q else R)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

415 
"\<not>P \<or> Q \<or> \<not>(if P then Q else R)" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

416 
"\<not>(if P then Q else R) \<or> \<not>P \<or> Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

417 
"\<not>(if P then Q else R) \<or> P \<or> R" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

418 
"(if P then Q else R) \<or> \<not>P \<or> \<not>Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

419 
"(if P then Q else R) \<or> P \<or> \<not>R" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

420 
"(if P then \<not>Q else R) \<or> \<not>P \<or> Q" 
587bf61a00a1
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents:
44087
diff
changeset

421 
"(if P then Q else \<not>R) \<or> P \<or> R" 
36898  422 
by auto 
423 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

424 
ML_file "Old_SMT/old_smt_real.ML" 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

425 
ML_file "Old_SMT/old_smt_word.ML" 
58056  426 

37124  427 
hide_type (open) pattern 
56078
624faeda77b5
moved 'SMT2' (SMTLIB2based SMT module) into Isabelle
blanchet
parents:
56046
diff
changeset

428 
hide_const fun_app term_true term_false z3div z3mod 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41174
diff
changeset

429 
hide_const (open) trigger pat nopat weight 
37124  430 

36898  431 
end 