author  boehmes 
Wed, 03 Nov 2010 16:44:38 +0100  
changeset 40332  5edeb5d269fa 
parent 40278  0fc78bb54f18 
child 40357  82ebdd19c4a4 
permissions  rwrr 
36898  1 
(* Title: HOL/Tools/SMT/smt_solver.ML 
2 
Author: Sascha Boehme, TU Muenchen 

3 

4 
SMT solvers registry and SMT tactic. 

5 
*) 

6 

7 
signature SMT_SOLVER = 

8 
sig 

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:
40161
diff
changeset

9 
datatype failure = 
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:
40161
diff
changeset

10 
Counterexample of bool * term list  
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:
40161
diff
changeset

11 
Time_Out  
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

12 
Out_Of_Memory  
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:
40161
diff
changeset

13 
Other_Failure of string 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

14 
val string_of_failure: Proof.context > string > failure > string 
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:
40161
diff
changeset

15 
exception SMT of failure 
36898  16 

17 
type interface = { 

18 
extra_norm: SMT_Normalize.extra_norm, 

19 
translate: SMT_Translate.config } 

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:
40161
diff
changeset

20 
datatype outcome = Unsat  Sat  Unknown 
36898  21 
type solver_config = { 
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:
40161
diff
changeset

22 
name: string, 
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:
40161
diff
changeset

23 
env_var: string, 
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:
40161
diff
changeset

24 
is_remote: bool, 
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:
40161
diff
changeset

25 
options: Proof.context > string list, 
36898  26 
interface: interface, 
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:
40161
diff
changeset

27 
outcome: string > string list > outcome * string list, 
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:
40161
diff
changeset

28 
cex_parser: (Proof.context > SMT_Translate.recon > string list > 
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:
40161
diff
changeset

29 
term list) option, 
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:
40161
diff
changeset

30 
reconstruct: (Proof.context > SMT_Translate.recon > string list > 
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:
40161
diff
changeset

31 
(int list * thm) * Proof.context) option } 
36898  32 

33 
(*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:
40161
diff
changeset

34 
val oracle: bool Config.T 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

35 
val filter_only: bool Config.T 
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:
40161
diff
changeset

36 
val datatypes: bool Config.T 
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

37 
val keep_assms: bool Config.T 
40332  38 
val timeout: real Config.T 
36898  39 
val with_timeout: Proof.context > ('a > 'b) > 'a > 'b 
40276  40 
val traceN: string 
36898  41 
val trace: bool Config.T 
42 
val trace_msg: Proof.context > ('a > string) > 'a > unit 

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:
40161
diff
changeset

43 
val trace_used_facts: bool Config.T 
36898  44 

45 
(*certificates*) 

46 
val fixed_certificates: bool Config.T 

47 
val select_certificates: string > Context.generic > Context.generic 

48 

49 
(*solvers*) 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

50 
type solver = bool option > Proof.context > (int * thm) list > 
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

51 
int list * thm 
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:
40161
diff
changeset

52 
val add_solver: solver_config > theory > theory 
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:
40161
diff
changeset

53 
val set_solver_options: string > string > Context.generic > 
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:
40161
diff
changeset

54 
Context.generic 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

55 
val all_solver_names_of: Context.generic > string list 
36898  56 
val solver_name_of: Context.generic > string 
57 
val select_solver: string > Context.generic > Context.generic 

58 
val solver_of: Context.generic > solver 

40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

59 
val is_locally_installed: Proof.context > bool 
36898  60 

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:
40161
diff
changeset

61 
(*filter*) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

62 
val smt_filter: bool > Time.time > Proof.state > ('a * thm) list > int > 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

63 
{outcome: failure option, used_facts: 'a list, 
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

64 
run_time_in_msecs: int option} 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

65 

36898  66 
(*tactic*) 
67 
val smt_tac': bool > Proof.context > thm list > int > Tactical.tactic 

68 
val smt_tac: Proof.context > thm list > int > Tactical.tactic 

69 

70 
(*setup*) 

71 
val setup: theory > theory 

72 
val print_setup: Context.generic > unit 

73 
end 

74 

75 
structure SMT_Solver: SMT_SOLVER = 

76 
struct 

77 

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:
40161
diff
changeset

78 
datatype failure = 
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:
40161
diff
changeset

79 
Counterexample of bool * term list  
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:
40161
diff
changeset

80 
Time_Out  
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

81 
Out_Of_Memory  
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:
40161
diff
changeset

82 
Other_Failure of string 
36898  83 

40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

84 
fun string_of_failure ctxt _ (Counterexample (real, ex)) = 
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:
40161
diff
changeset

85 
let 
40165  86 
val msg = (if real then "C" else "Potential c") ^ "ounterexample found" 
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:
40161
diff
changeset

87 
in 
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:
40161
diff
changeset

88 
if null ex then msg ^ "." 
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:
40161
diff
changeset

89 
else Pretty.string_of (Pretty.big_list (msg ^ ":") 
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:
40161
diff
changeset

90 
(map (Syntax.pretty_term ctxt) ex)) 
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:
40161
diff
changeset

91 
end 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

92 
 string_of_failure _ name Time_Out = name ^ " timed out." 
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

93 
 string_of_failure _ name Out_Of_Memory = name ^ " ran out of memory." 
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

94 
 string_of_failure _ _ (Other_Failure msg) = msg 
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:
40161
diff
changeset

95 

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:
40161
diff
changeset

96 
exception SMT of failure 
36898  97 

98 
type interface = { 

99 
extra_norm: SMT_Normalize.extra_norm, 

100 
translate: SMT_Translate.config } 

101 

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:
40161
diff
changeset

102 
datatype outcome = Unsat  Sat  Unknown 
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:
40161
diff
changeset

103 

36898  104 
type solver_config = { 
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:
40161
diff
changeset

105 
name: string, 
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:
40161
diff
changeset

106 
env_var: string, 
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:
40161
diff
changeset

107 
is_remote: bool, 
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:
40161
diff
changeset

108 
options: Proof.context > string list, 
36898  109 
interface: interface, 
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:
40161
diff
changeset

110 
outcome: string > string list > outcome * string list, 
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:
40161
diff
changeset

111 
cex_parser: (Proof.context > SMT_Translate.recon > string list > 
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:
40161
diff
changeset

112 
term list) option, 
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:
40161
diff
changeset

113 
reconstruct: (Proof.context > SMT_Translate.recon > string list > 
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:
40161
diff
changeset

114 
(int list * thm) * Proof.context) option } 
36898  115 

116 

117 

118 
(* SMT options *) 

119 

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:
40161
diff
changeset

120 
val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true) 
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:
40161
diff
changeset

121 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

122 
val (filter_only, setup_filter_only) = 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

123 
Attrib.config_bool "smt_filter_only" (K false) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

124 

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:
40161
diff
changeset

125 
val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false) 
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:
40161
diff
changeset

126 

40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

127 
val (keep_assms, setup_keep_assms) = 
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

128 
Attrib.config_bool "smt_keep_assms" (K true) 
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

129 

40332  130 
val (timeout, setup_timeout) = Attrib.config_real "smt_timeout" (K 30.0) 
36898  131 

132 
fun with_timeout ctxt f x = 

40332  133 
TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f x 
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:
40161
diff
changeset

134 
handle TimeLimit.TimeOut => raise SMT Time_Out 
36898  135 

40276  136 
val traceN = "smt_trace" 
137 
val (trace, setup_trace) = Attrib.config_bool traceN (K false) 

36898  138 

139 
fun trace_msg ctxt f x = 

140 
if Config.get ctxt trace then tracing (f x) else () 

141 

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:
40161
diff
changeset

142 
val (trace_used_facts, setup_trace_used_facts) = 
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:
40161
diff
changeset

143 
Attrib.config_bool "smt_trace_used_facts" (K false) 
36898  144 

145 

146 
(* SMT certificates *) 

147 

148 
val (fixed_certificates, setup_fixed_certificates) = 

149 
Attrib.config_bool "smt_fixed" (K false) 

150 

151 
structure Certificates = Generic_Data 

152 
( 

153 
type T = Cache_IO.cache option 

154 
val empty = NONE 

155 
val extend = I 

156 
fun merge (s, _) = s 

157 
) 

158 

159 
val get_certificates_path = 

160 
Option.map (Cache_IO.cache_path_of) o Certificates.get 

161 

162 
fun select_certificates name = Certificates.put ( 

163 
if name = "" then NONE 

164 
else SOME (Cache_IO.make (Path.explode name))) 

165 

166 

167 

168 
(* interface to external solvers *) 

169 

40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

170 
fun get_local_solver env_var = 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

171 
let val local_solver = getenv env_var 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

172 
in if local_solver <> "" then SOME local_solver else NONE end 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

173 

36898  174 
local 
175 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

176 
fun choose (rm, env_var, is_remote, name) = 
36898  177 
let 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

178 
val force_local = (case rm of SOME false => true  _ => false) 
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

179 
val force_remote = (case rm of SOME true => true  _ => false) 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

180 
val lsolver = get_local_solver env_var 
36898  181 
val remote_url = getenv "REMOTE_SMT_URL" 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

182 
val trace = if is_some rm then K () else tracing 
36898  183 
in 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

184 
if not force_remote andalso is_some lsolver 
36898  185 
then 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

186 
(trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ..."); 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

187 
[the lsolver]) 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

188 
else if not force_local andalso is_remote 
36898  189 
then 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

190 
(trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ 
36898  191 
quote remote_url ^ " ..."); 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

192 
[getenv "REMOTE_SMT", name]) 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

193 
else if force_remote 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

194 
then error ("The SMT solver " ^ quote name ^ " is not remotely available.") 
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

195 
else error ("The SMT solver " ^ quote name ^ " has not been found " ^ 
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

196 
"on this computer. Please set the Isabelle environment variable " ^ 
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

197 
quote env_var ^ ".") 
36898  198 
end 
199 

200 
fun make_cmd solver args problem_path proof_path = space_implode " " ( 

201 
map File.shell_quote (solver @ args) @ 

202 
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) 

203 

204 
fun run ctxt cmd args input = 

205 
(case Certificates.get (Context.Proof ctxt) of 

206 
NONE => Cache_IO.run (make_cmd (choose cmd) args) input 

207 
 SOME certs => 

208 
(case Cache_IO.lookup certs input of 

209 
(NONE, key) => 

210 
if Config.get ctxt fixed_certificates 

211 
then error ("Bad certificates cache: missing certificate") 

212 
else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) 

213 
input 

214 
 (SOME output, _) => 

215 
(tracing ("Using cached certificate from " ^ 

216 
File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); 

217 
output))) 

218 

219 
in 

220 

221 
fun run_solver ctxt cmd args input = 

222 
let 

223 
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag 

224 
(map Pretty.str ls)) 

225 

226 
val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input 

227 

228 
val (res, err) = with_timeout ctxt (run ctxt cmd args) input 

229 
val _ = trace_msg ctxt (pretty "SMT solver:") err 

230 

39811  231 
val ls = rev (snd (chop_while (equal "") (rev res))) 
36898  232 
val _ = trace_msg ctxt (pretty "SMT result:") ls 
233 
in ls end 

234 

235 
end 

236 

40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset

237 
fun trace_assms ctxt = trace_msg ctxt (Pretty.string_of o 
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset

238 
Pretty.big_list "SMT assertions:" o map (Display.pretty_thm ctxt o snd)) 
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset

239 

36940  240 
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) = 
36898  241 
let 
242 
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] 

243 
fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) 

244 
fun pretty_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) 

245 
in 

246 
trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "SMT names:" [ 

247 
Pretty.big_list "sorts:" (map pretty_typ (Symtab.dest typs)), 

248 
Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () 

249 
end 

250 

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:
40161
diff
changeset

251 
fun invoke translate_config name cmd more_opts options irules ctxt = 
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:
40161
diff
changeset

252 
let 
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:
40161
diff
changeset

253 
val args = more_opts @ options ctxt 
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:
40161
diff
changeset

254 
val comments = ("solver: " ^ name) :: 
40332  255 
("timeout: " ^ Time.toString (seconds (Config.get ctxt timeout))) :: 
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:
40161
diff
changeset

256 
"arguments:" :: args 
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:
40161
diff
changeset

257 
in 
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:
40161
diff
changeset

258 
irules 
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset

259 
> tap (trace_assms ctxt) 
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:
40161
diff
changeset

260 
> SMT_Translate.translate translate_config ctxt comments 
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:
40161
diff
changeset

261 
> tap (trace_recon_data ctxt) 
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:
40161
diff
changeset

262 
>> run_solver ctxt cmd args 
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:
40161
diff
changeset

263 
> rpair ctxt 
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:
40161
diff
changeset

264 
end 
36898  265 

266 
fun discharge_definitions thm = 

267 
if Thm.nprems_of thm = 0 then thm 

268 
else discharge_definitions (@{thm reflexive} RS thm) 

269 

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:
40161
diff
changeset

270 
fun set_has_datatypes with_datatypes translate = 
36898  271 
let 
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:
40161
diff
changeset

272 
val {prefixes, header, strict, builtins, serialize} = translate 
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:
40161
diff
changeset

273 
val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins 
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:
40161
diff
changeset

274 
val with_datatypes' = has_datatypes andalso with_datatypes 
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:
40161
diff
changeset

275 
val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num, 
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:
40161
diff
changeset

276 
builtin_fun=builtin_fun, has_datatypes=with_datatypes} 
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:
40161
diff
changeset

277 
val translate' = {prefixes=prefixes, header=header, strict=strict, 
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:
40161
diff
changeset

278 
builtins=builtins', serialize=serialize} 
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:
40161
diff
changeset

279 
in (with_datatypes', translate') end 
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:
40161
diff
changeset

280 

40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

281 
fun trace_assumptions ctxt irules idxs = 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

282 
let 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

283 
val thms = filter (fn i => i >= 0) idxs 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

284 
> map_filter (AList.lookup (op =) irules) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

285 
in 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

286 
if Config.get ctxt trace_used_facts andalso length thms > 0 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

287 
then 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

288 
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

289 
(map (Display.pretty_thm ctxt) thms))) 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

290 
else () 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

291 
end 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

292 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

293 
fun gen_solver name info rm ctxt irules = 
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:
40161
diff
changeset

294 
let 
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:
40161
diff
changeset

295 
val {env_var, is_remote, options, more_options, interface, reconstruct} = 
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:
40161
diff
changeset

296 
info 
36898  297 
val {extra_norm, translate} = interface 
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:
40161
diff
changeset

298 
val (with_datatypes, translate') = 
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:
40161
diff
changeset

299 
set_has_datatypes (Config.get ctxt datatypes) translate 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

300 
val cmd = (rm, env_var, is_remote, name) 
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

301 
val keep = Config.get ctxt keep_assms 
36898  302 
in 
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:
40161
diff
changeset

303 
(irules, ctxt) 
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

304 
> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

305 
> invoke translate' name cmd more_options options 
36898  306 
> reconstruct 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

307 
> (fn (idxs, thm) => fn ctxt' => thm 
36898  308 
> singleton (ProofContext.export ctxt' ctxt) 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

309 
> discharge_definitions 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

310 
> tap (fn _ => trace_assumptions ctxt irules idxs) 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

311 
> pair idxs) 
36898  312 
end 
313 

314 

315 

316 
(* solver store *) 

317 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

318 
type solver = bool option > Proof.context > (int * thm) list > int list * thm 
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:
40161
diff
changeset

319 

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:
40161
diff
changeset

320 
type solver_info = { 
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:
40161
diff
changeset

321 
env_var: string, 
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:
40161
diff
changeset

322 
is_remote: bool, 
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:
40161
diff
changeset

323 
options: Proof.context > string list, 
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:
40161
diff
changeset

324 
more_options: string list, 
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:
40161
diff
changeset

325 
interface: interface, 
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:
40161
diff
changeset

326 
reconstruct: string list * SMT_Translate.recon > Proof.context > 
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:
40161
diff
changeset

327 
(int list * thm) * Proof.context } 
36898  328 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

329 
structure Solvers = Generic_Data 
36898  330 
( 
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:
40161
diff
changeset

331 
type T = solver_info Symtab.table 
36898  332 
val empty = Symtab.empty 
333 
val extend = I 

334 
fun merge data = Symtab.merge (K true) data 

335 
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) 

336 
) 

337 

338 
val no_solver = "(none)" 

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:
40161
diff
changeset

339 

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:
40161
diff
changeset

340 
fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn 
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:
40161
diff
changeset

341 
{env_var, is_remote, options, interface, reconstruct, ...} => 
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:
40161
diff
changeset

342 
{env_var=env_var, is_remote=is_remote, options=options, 
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:
40161
diff
changeset

343 
more_options=String.tokens (Symbol.is_ascii_blank o str) opts, 
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:
40161
diff
changeset

344 
interface=interface, reconstruct=reconstruct})) 
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:
40161
diff
changeset

345 

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:
40161
diff
changeset

346 
local 
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:
40161
diff
changeset

347 
fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt = 
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:
40161
diff
changeset

348 
(case outcome output of 
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:
40161
diff
changeset

349 
(Unsat, ls) => 
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:
40161
diff
changeset

350 
if not (Config.get ctxt oracle) andalso is_some reconstruct 
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:
40161
diff
changeset

351 
then the reconstruct ctxt recon ls 
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:
40161
diff
changeset

352 
else (([], ocl ()), ctxt) 
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:
40161
diff
changeset

353 
 (result, ls) => 
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:
40161
diff
changeset

354 
let val ts = (case cex_parser of SOME f => f ctxt recon ls  _ => []) 
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:
40161
diff
changeset

355 
in raise SMT (Counterexample (result = Sat, ts)) end) 
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:
40161
diff
changeset

356 
in 
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:
40161
diff
changeset

357 

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:
40161
diff
changeset

358 
fun add_solver cfg = 
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:
40161
diff
changeset

359 
let 
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:
40161
diff
changeset

360 
val {name, env_var, is_remote, options, interface, outcome, cex_parser, 
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:
40161
diff
changeset

361 
reconstruct} = cfg 
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:
40161
diff
changeset

362 

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:
40161
diff
changeset

363 
fun core_oracle () = @{cprop False} 
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:
40161
diff
changeset

364 

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:
40161
diff
changeset

365 
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, 
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:
40161
diff
changeset

366 
more_options=[], interface=interface, 
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:
40161
diff
changeset

367 
reconstruct=finish (outcome name) cex_parser reconstruct ocl } 
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:
40161
diff
changeset

368 
in 
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:
40161
diff
changeset

369 
Thm.add_oracle (Binding.name name, core_oracle) #> (fn (_, ocl) => 
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:
40161
diff
changeset

370 
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> 
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:
40161
diff
changeset

371 
Attrib.setup (Binding.name (name ^ "_options")) 
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:
40161
diff
changeset

372 
(Scan.lift (Parse.$$$ "="  Args.name) >> 
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:
40161
diff
changeset

373 
(Thm.declaration_attribute o K o set_solver_options name)) 
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:
40161
diff
changeset

374 
("Additional command line options for SMT solver " ^ quote name) 
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:
40161
diff
changeset

375 
end 
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:
40161
diff
changeset

376 

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:
40161
diff
changeset

377 
end 
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:
40161
diff
changeset

378 

36898  379 
val all_solver_names_of = Symtab.keys o Solvers.get 
380 
val lookup_solver = Symtab.lookup o Solvers.get 

381 

382 

383 

384 
(* selected solver *) 

385 

386 
structure Selected_Solver = Generic_Data 

387 
( 

388 
type T = string 

389 
val empty = no_solver 

390 
val extend = I 

391 
fun merge (s, _) = s 

392 
) 

393 

394 
val solver_name_of = Selected_Solver.get 

395 

396 
fun select_solver name context = 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

397 
if is_none (lookup_solver context name) 
36898  398 
then error ("SMT solver not registered: " ^ quote name) 
399 
else Selected_Solver.map (K name) context 

400 

401 
fun raw_solver_of context name = 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

402 
(case lookup_solver context name of 
36898  403 
NONE => error "No SMT solver selected" 
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:
40161
diff
changeset

404 
 SOME s => s) 
36898  405 

406 
fun solver_of context = 

407 
let val name = solver_name_of context 

408 
in gen_solver name (raw_solver_of context name) end 

409 

40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

410 
fun is_locally_installed ctxt = 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

411 
let 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

412 
val name = solver_name_of (Context.Proof ctxt) 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

413 
val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

414 
in is_some (get_local_solver env_var) end 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

415 

36898  416 

417 

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:
40161
diff
changeset

418 
(* SMT filter *) 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

419 

539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

420 
val has_topsort = Term.exists_type (Term.exists_subtype (fn 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

421 
TFree (_, []) => true 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

422 
 TVar (_, []) => true 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

423 
 _ => false)) 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

424 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

425 
fun smt_solver rm ctxt irules = 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

426 
(* without this test, we would run into problems when atomizing the rules: *) 
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:
40161
diff
changeset

427 
if exists (has_topsort o Thm.prop_of o snd) irules 
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:
40161
diff
changeset

428 
then raise SMT (Other_Failure "proof state contains the universal sort {}") 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

429 
else solver_of (Context.Proof ctxt) rm ctxt irules 
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:
40161
diff
changeset

430 

40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

431 
fun smt_filter run_remote time_limit st xrules i = 
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:
40161
diff
changeset

432 
let 
40199  433 
val {facts, goal, ...} = Proof.goal st 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

434 
val ctxt = 
40199  435 
Proof.context_of st 
40332  436 
> Config.put timeout (Real.fromInt (Time.toSeconds time_limit)) 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

437 
> Config.put oracle false 
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

438 
> Config.put filter_only true 
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

439 
> Config.put keep_assms 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:
40161
diff
changeset

440 
val cprop = 
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:
40161
diff
changeset

441 
Thm.cprem_of goal i 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

442 
> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt 
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:
40161
diff
changeset

443 
> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg 
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:
40161
diff
changeset

444 
val irs = map (pair ~1) (Thm.assume cprop :: facts) 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

445 
val rm = SOME run_remote 
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:
40161
diff
changeset

446 
in 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

447 
split_list xrules 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

448 
> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

449 
> map_filter o try o nth 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

450 
> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE}) 
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:
40161
diff
changeset

451 
end 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

452 
handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs=NONE} 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

453 
(* FIXME: measure runtime *) 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

454 

539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

455 

539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

456 

36898  457 
(* SMT tactic *) 
458 

459 
fun smt_tac' pass_exns ctxt rules = 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

460 
CONVERSION (SMT_Normalize.atomize_conv ctxt) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

461 
THEN' Tactic.rtac @{thm ccontr} 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

462 
THEN' SUBPROOF (fn {context=cx, prems, ...} => 
40165  463 
let 
40196
123b6fe379f6
honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter
boehmes
parents:
40166
diff
changeset

464 
fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems))) 
40197
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

465 
val name = solver_name_of (Context.Proof cx) 
d99f74ed95be
capture outofmemory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver runtime: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset

466 
val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx name) 
40165  467 
in 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

468 
(if pass_exns then SOME (solve ()) 
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

469 
else (SOME (solve ()) handle SMT fail => (trace fail; NONE))) 
40165  470 
> (fn SOME thm => Tactic.rtac thm 1  _ => Tactical.no_tac) 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

471 
end) ctxt 
36898  472 

473 
val smt_tac = smt_tac' 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:
40161
diff
changeset

474 

36898  475 
val smt_method = 
476 
Scan.optional Attrib.thms [] >> 

477 
(fn thms => fn ctxt => METHOD (fn facts => 

478 
HEADGOAL (smt_tac ctxt (thms @ facts)))) 

479 

480 

481 

482 
(* setup *) 

483 

484 
val setup = 

38808  485 
Attrib.setup @{binding smt_solver} 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset

486 
(Scan.lift (Parse.$$$ "="  Args.name) >> 
36898  487 
(Thm.declaration_attribute o K o select_solver)) 
488 
"SMT solver configuration" #> 

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:
40161
diff
changeset

489 
setup_oracle #> 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

490 
setup_filter_only #> 
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:
40161
diff
changeset

491 
setup_datatypes #> 
40278
0fc78bb54f18
optionally drop assumptions which cannot be preprocessed
boehmes
parents:
40276
diff
changeset

492 
setup_keep_assms #> 
36898  493 
setup_timeout #> 
494 
setup_trace #> 

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:
40161
diff
changeset

495 
setup_trace_used_facts #> 
36898  496 
setup_fixed_certificates #> 
38808  497 
Attrib.setup @{binding smt_certificates} 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset

498 
(Scan.lift (Parse.$$$ "="  Args.name) >> 
36898  499 
(Thm.declaration_attribute o K o select_certificates)) 
500 
"SMT certificates" #> 

38808  501 
Method.setup @{binding smt} smt_method 
36898  502 
"Applies an SMT solver to the current goal." 
503 

504 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

505 
fun print_setup context = 
36898  506 
let 
40332  507 
val t = Time.toString (seconds (Config.get_generic context timeout)) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

508 
val names = sort_strings (all_solver_names_of context) 
36898  509 
val ns = if null names then [no_solver] else names 
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:
40161
diff
changeset

510 
val n = solver_name_of context 
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:
40161
diff
changeset

511 
val opts = 
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:
40161
diff
changeset

512 
(case Symtab.lookup (Solvers.get context) n of 
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:
40161
diff
changeset

513 
NONE => [] 
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:
40161
diff
changeset

514 
 SOME {more_options, options, ...} => 
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:
40161
diff
changeset

515 
more_options @ options (Context.proof_of context)) 
36898  516 
val certs_filename = 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

517 
(case get_certificates_path context of 
36898  518 
SOME path => Path.implode path 
519 
 NONE => "(disabled)") 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

520 
val fixed = if Config.get_generic context fixed_certificates then "true" 
36898  521 
else "false" 
522 
in 

523 
Pretty.writeln (Pretty.big_list "SMT setup:" [ 

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:
40161
diff
changeset

524 
Pretty.str ("Current SMT solver: " ^ n), 
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:
40161
diff
changeset

525 
Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), 
36898  526 
Pretty.str_list "Available SMT solvers: " "" ns, 
527 
Pretty.str ("Current timeout: " ^ t ^ " seconds"), 

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:
40161
diff
changeset

528 
Pretty.str ("With proofs: " ^ 
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:
40161
diff
changeset

529 
(if Config.get_generic context oracle then "false" else "true")), 
36898  530 
Pretty.str ("Certificates cache: " ^ certs_filename), 
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:
40161
diff
changeset

531 
Pretty.str ("Fixed certificates: " ^ fixed)]) 
36898  532 
end 
533 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset

534 
val _ = 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36940
diff
changeset

535 
Outer_Syntax.improper_command "smt_status" 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

536 
"show the available SMT solvers and the currently selected solver" 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

537 
Keyword.diag 
36898  538 
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => 
539 
print_setup (Context.Proof (Toplevel.context_of state))))) 

540 

541 
end 