author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 59966  c01cea2ba71e 
child 61585  a9599d3d7610 
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> 
40664  54 
Weights must be nonnegative. The value @{text 0} is equivalent to providing 
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 => 

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

145 
METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) 
60500  146 
\<close> "apply an SMT solver to the current goal" 
36898  147 

148 

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

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

152 
The current configuration can be printed by the command 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

153 
@{text old_smt_status}, which shows the values of most options. 
60500  154 
\<close> 
36898  155 

156 

157 

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

60500  160 
text \<open> 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

161 
The option @{text old_smt_solver} can be used to change the target SMT 
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

162 
solver. The possible values can be obtained from the @{text old_smt_status} 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41426
diff
changeset

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

164 

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

165 
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

166 
by default. Z3 is free for noncommercial applications and can be enabled 
59966
c01cea2ba71e
updated 'old_smt' to loss of 'z3_non_commercial' option
blanchet
parents:
58881
diff
changeset

167 
by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to 
c01cea2ba71e
updated 'old_smt' to loss of 'z3_non_commercial' option
blanchet
parents:
58881
diff
changeset

168 
@{text yes}. 
60500  169 
\<close> 
36898  170 

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

171 
declare [[ old_smt_solver = z3 ]] 
36898  172 

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

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

60500  177 
\<close> 
36898  178 

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

179 
declare [[ old_smt_timeout = 20 ]] 
36898  180 

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

182 
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

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

185 

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

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

187 

60500  188 
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

189 
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

190 
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

191 
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

192 
a checkable certificate. This is currently only implemented for Z3. 
60500  193 
\<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

194 

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

195 
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

196 

60500  197 
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

198 
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

199 
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

200 
options. 
60500  201 
\<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

202 

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

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

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

205 
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

206 

60500  207 
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

208 
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

209 
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

210 
mode. 
60500  211 
\<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

212 

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

213 
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

214 

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

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

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

60500  220 
\<close> 
41125  221 

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

222 
declare [[ old_smt_infer_triggers = false ]] 
41125  223 

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

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

228 
construction whose cycles are limited by the following option. 

60500  229 
\<close> 
41125  230 

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

231 
declare [[ monomorph_max_rounds = 5 ]] 
41125  232 

60500  233 
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

234 
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

235 
by the following option. 
60500  236 
\<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

237 

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

238 
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

239 

36898  240 

241 

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

60500  244 
text \<open> 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

245 
By setting the option @{text old_smt_certificates} to the name of a file, 
36898  246 
all following applications of an SMT solver a cached in that file. 
247 
Any further application of the same SMT solver (using the very same 

248 
configuration) reuses the cached certificate instead of invoking the 

249 
solver. An empty string disables caching certificates. 

250 

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

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

253 
@{text ".certs"} instead of @{text ".thy"}) 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

254 
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

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

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

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

60500  260 
text \<open> 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

261 
The option @{text old_smt_read_only_certificates} controls whether only 
47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

262 
stored certificates are should be used or invocation of an SMT solver 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46950
diff
changeset

263 
is allowed. When set to @{text true}, no SMT solver will ever be 
36898  264 
invoked and only the existing certificates found in the configured 
265 
cache are used; when set to @{text false} and there is no cached 

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

267 
invoked. 

60500  268 
\<close> 
36898  269 

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

270 
declare [[ old_smt_read_only_certificates = false ]] 
36898  271 

272 

273 

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

60500  276 
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

277 
The SMT method, when applied, traces important information. To 
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 
make it entirely silent, set the following option to @{text false}. 
60500  279 
\<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

280 

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

281 
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

282 

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

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

286 
@{text old_smt_trace} should be set to @{text true}. 
60500  287 
\<close> 
36898  288 

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

289 
declare [[ old_smt_trace = false ]] 
36898  290 

60500  291 
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

292 
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

293 
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

294 
@{term true}. This only works for Z3 when it runs in nonoracle mode 
58059
4e477dcd050a
prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents:
58058
diff
changeset

295 
(see options @{text old_smt_solver} and @{text old_smt_oracle} above). 
60500  296 
\<close> 
36898  297 

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

298 
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

299 

36898  300 

301 

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

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

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

308 
any implemented reconstruction procedure for all uncertain Z3 proof 

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

310 
the simplifier when reconstructing theoryspecific proof steps. 

60500  311 
\<close> 
36898  312 

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

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

316 
if_True if_False not_not 

317 

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

318 
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

319 
"(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

320 
"(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

321 
"(\<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

322 
"(\<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

323 
"(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

324 
"(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

325 
"(\<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

326 
"(\<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

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

328 

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

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

332 
"(\<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

333 
"(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

334 
"(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

335 
"(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

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

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

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

342 

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

343 
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

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

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

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

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

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

349 
"(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

350 
"(False = P) = (\<not>P)" 
36898  351 
"((\<not>P) = P) = False" 
352 
"(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

353 
"((\<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

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>((\<not>P) = Q) = (P = Q)" 
36898  356 
"(P \<noteq> Q) = (Q = (\<not>P))" 
357 
"(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))" 

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

359 
by auto 

360 

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

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

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

365 
"(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

366 
"(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

367 
"(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

368 
"(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

369 
"(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

370 
"(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

371 
"(if P then \<not>Q else Q) = ((\<not>Q) = P)" 
36898  372 
"(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

373 
"(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

374 
"(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

375 
"(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

376 
"(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

377 
"(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

378 
"(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

379 
"(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

380 
"(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

381 
"(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

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

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

385 
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

386 
"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

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

388 
"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

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

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

391 
"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

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

393 

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

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

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

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

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

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

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

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

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

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

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

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

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

408 
"\<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

409 
"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

410 
"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

411 
"\<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

412 
"\<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

413 
"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

414 
"\<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

415 
"\<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

416 
"\<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

417 
"(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

418 
"(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

419 
"(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

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

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

423 
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

424 
ML_file "Old_SMT/old_smt_word.ML" 
58056  425 

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

427 
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

428 
hide_const (open) trigger pat nopat weight 
37124  429 

36898  430 
end 