author | boehmes |
Tue, 07 Dec 2010 15:01:37 +0100 | |
changeset 41062 | 304cfdbc6475 |
parent 41059 | d2b1fc1b8e19 |
child 41065 | 13424972ade4 |
permissions | -rw-r--r-- |
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 |
|
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:
40357
diff
changeset
|
9 |
(*configuration*) |
36898 | 10 |
type interface = { |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
11 |
class: SMT_Config.class, |
36898 | 12 |
extra_norm: SMT_Normalize.extra_norm, |
13 |
translate: SMT_Translate.config } |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
14 |
datatype outcome = Unsat | Sat | Unknown |
36898 | 15 |
type solver_config = { |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
16 |
name: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
17 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
18 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
19 |
options: Proof.context -> string list, |
36898 | 20 |
interface: interface, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
21 |
outcome: string -> string list -> outcome * string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
23 |
term list * term list) option, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
25 |
(int list * thm) * Proof.context) option, |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
26 |
default_max_relevant: int } |
36898 | 27 |
|
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:
40357
diff
changeset
|
28 |
(*registry*) |
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
|
29 |
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
|
30 |
int list * thm |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
val add_solver: solver_config -> theory -> theory |
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
32 |
val solver_name_of: Proof.context -> string |
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:
40357
diff
changeset
|
33 |
val solver_of: Proof.context -> solver |
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
34 |
val available_solvers_of: Proof.context -> string list |
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
35 |
val is_locally_installed: Proof.context -> string -> bool |
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
36 |
val is_remotely_available: Proof.context -> string -> bool |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
37 |
val default_max_relevant: Proof.context -> string -> int |
36898 | 38 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
39 |
(*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
|
40 |
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int -> |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40579
diff
changeset
|
41 |
{outcome: SMT_Failure.failure option, used_facts: ('a * thm) list, |
40197
d99f74ed95be
capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1
boehmes
parents:
40196
diff
changeset
|
42 |
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
|
43 |
|
36898 | 44 |
(*tactic*) |
45 |
val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic |
|
46 |
val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic |
|
47 |
||
48 |
(*setup*) |
|
49 |
val setup: theory -> theory |
|
50 |
end |
|
51 |
||
52 |
structure SMT_Solver: SMT_SOLVER = |
|
53 |
struct |
|
54 |
||
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:
40357
diff
changeset
|
55 |
structure C = SMT_Config |
36898 | 56 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
57 |
|
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:
40357
diff
changeset
|
58 |
(* configuration *) |
36898 | 59 |
|
60 |
type interface = { |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
61 |
class: SMT_Config.class, |
36898 | 62 |
extra_norm: SMT_Normalize.extra_norm, |
63 |
translate: SMT_Translate.config } |
|
64 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
65 |
datatype outcome = Unsat | Sat | Unknown |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
66 |
|
36898 | 67 |
type solver_config = { |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
68 |
name: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
69 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
70 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
71 |
options: Proof.context -> string list, |
36898 | 72 |
interface: interface, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
73 |
outcome: string -> string list -> outcome * string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
74 |
cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
75 |
term list * term list) option, |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
76 |
reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
77 |
(int list * thm) * Proof.context) option, |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
78 |
default_max_relevant: int } |
36898 | 79 |
|
80 |
||
81 |
(* interface to external solvers *) |
|
82 |
||
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
83 |
fun get_local_solver env_var = |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
|
36898 | 87 |
local |
88 |
||
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
|
89 |
fun choose (rm, env_var, is_remote, name) = |
36898 | 90 |
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
|
91 |
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
|
92 |
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
|
93 |
val lsolver = get_local_solver env_var |
36898 | 94 |
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
|
95 |
val trace = if is_some rm then K () else tracing |
36898 | 96 |
in |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
97 |
if not force_remote andalso is_some lsolver |
36898 | 98 |
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
|
99 |
(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
|
100 |
[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
|
101 |
else if not force_local andalso is_remote |
36898 | 102 |
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
|
103 |
(trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ |
36898 | 104 |
quote remote_url ^ " ..."); |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
105 |
[getenv "REMOTE_SMT", name]) |
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
"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
|
110 |
quote env_var ^ ".") |
36898 | 111 |
end |
112 |
||
113 |
fun make_cmd solver args problem_path proof_path = space_implode " " ( |
|
114 |
map File.shell_quote (solver @ args) @ |
|
115 |
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
|
116 |
||
117 |
fun run ctxt cmd args input = |
|
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:
40357
diff
changeset
|
118 |
(case C.certificates_of ctxt of |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
119 |
NONE => |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
120 |
if Config.get ctxt C.debug_files = "" then |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
121 |
Cache_IO.run (make_cmd (choose cmd) args) input |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
122 |
else |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
123 |
let |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
124 |
val base_path = Path.explode (Config.get ctxt C.debug_files) |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
125 |
val in_path = Path.ext "smt_in" base_path |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
126 |
val out_path = Path.ext "smt_out" base_path |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
127 |
in |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
128 |
Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset
|
129 |
end |
36898 | 130 |
| SOME certs => |
131 |
(case Cache_IO.lookup certs input of |
|
132 |
(NONE, key) => |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
133 |
if Config.get ctxt C.fixed then |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
134 |
error ("Bad certificates cache: missing certificate") |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
135 |
else |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
136 |
Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input |
36898 | 137 |
| (SOME output, _) => |
138 |
(tracing ("Using cached certificate from " ^ |
|
139 |
File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); |
|
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
140 |
output))) |
36898 | 141 |
|
142 |
in |
|
143 |
||
144 |
fun run_solver ctxt cmd args input = |
|
145 |
let |
|
146 |
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag |
|
147 |
(map Pretty.str ls)) |
|
148 |
||
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:
40357
diff
changeset
|
149 |
val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input |
36898 | 150 |
|
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
151 |
val {redirected_output=res, output=err, return_code} = |
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
152 |
C.with_timeout ctxt (run ctxt cmd args) input |
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:
40357
diff
changeset
|
153 |
val _ = C.trace_msg ctxt (pretty "Solver:") err |
36898 | 154 |
|
39811 | 155 |
val ls = rev (snd (chop_while (equal "") (rev res))) |
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:
40357
diff
changeset
|
156 |
val _ = C.trace_msg ctxt (pretty "Result:") ls |
40550
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
157 |
|
f84c664ece8e
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset
|
158 |
val _ = null ls andalso return_code <> 0 andalso |
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40560
diff
changeset
|
159 |
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) |
36898 | 160 |
in ls end |
161 |
||
162 |
end |
|
163 |
||
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:
40357
diff
changeset
|
164 |
fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o |
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:
40357
diff
changeset
|
165 |
Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
166 |
|
36940 | 167 |
fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) = |
36898 | 168 |
let |
169 |
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] |
|
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:
40357
diff
changeset
|
170 |
fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) |
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:
40357
diff
changeset
|
171 |
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) |
36898 | 172 |
in |
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:
40357
diff
changeset
|
173 |
C.trace_msg ctxt (fn () => |
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:
40357
diff
changeset
|
174 |
Pretty.string_of (Pretty.big_list "Names:" [ |
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:
40357
diff
changeset
|
175 |
Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), |
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:
40357
diff
changeset
|
176 |
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () |
36898 | 177 |
end |
178 |
||
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:
40357
diff
changeset
|
179 |
fun invoke translate_config name cmd options irules ctxt = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
180 |
let |
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:
40357
diff
changeset
|
181 |
val args = C.solver_options_of ctxt @ options ctxt |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
182 |
val comments = ("solver: " ^ name) :: |
41062 | 183 |
("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) :: |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
184 |
"arguments:" :: args |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
185 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
186 |
irules |
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset
|
187 |
|> tap (trace_assms ctxt) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
188 |
|> SMT_Translate.translate translate_config ctxt comments |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
189 |
||> tap (trace_recon_data ctxt) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
190 |
|>> run_solver ctxt cmd args |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
191 |
|> rpair ctxt |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
192 |
end |
36898 | 193 |
|
194 |
fun discharge_definitions thm = |
|
195 |
if Thm.nprems_of thm = 0 then thm |
|
196 |
else discharge_definitions (@{thm reflexive} RS thm) |
|
197 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
198 |
fun set_has_datatypes with_datatypes translate = |
36898 | 199 |
let |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
200 |
val {prefixes, header, is_fol, has_datatypes, serialize} = translate |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
201 |
val with_datatypes' = has_datatypes andalso with_datatypes |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
202 |
val translate' = {prefixes=prefixes, header=header, is_fol=is_fol, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
203 |
has_datatypes=with_datatypes', serialize=serialize} |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
204 |
in (with_datatypes', translate') end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
205 |
|
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
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
|> 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
|
210 |
in |
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:
40357
diff
changeset
|
211 |
if Config.get ctxt C.trace_used_facts andalso length thms > 0 |
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
|
212 |
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
|
213 |
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
|
214 |
(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
|
215 |
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
|
216 |
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
|
217 |
|
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
|
218 |
fun gen_solver name info rm ctxt irules = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
219 |
let |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
220 |
val {env_var, is_remote, options, interface, reconstruct, ...} = info |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
221 |
val {extra_norm, translate, ...} = interface |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
222 |
val (with_datatypes, translate') = |
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:
40357
diff
changeset
|
223 |
set_has_datatypes (Config.get ctxt C.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
|
224 |
val cmd = (rm, env_var, is_remote, name) |
36898 | 225 |
in |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
226 |
(irules, ctxt) |
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:
40357
diff
changeset
|
227 |
|-> SMT_Normalize.normalize extra_norm with_datatypes |
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:
40357
diff
changeset
|
228 |
|-> invoke translate' name cmd options |
36898 | 229 |
|-> 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
|
230 |
|-> (fn (idxs, thm) => fn ctxt' => thm |
36898 | 231 |
|> 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
|
232 |
|> 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
|
233 |
|> 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
|
234 |
|> pair idxs) |
36898 | 235 |
end |
236 |
||
237 |
||
238 |
||
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:
40357
diff
changeset
|
239 |
(* registry *) |
36898 | 240 |
|
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
|
241 |
type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
242 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
243 |
type solver_info = { |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
244 |
env_var: string, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
245 |
is_remote: bool, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
246 |
options: Proof.context -> string list, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
247 |
interface: interface, |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
248 |
reconstruct: string list * SMT_Translate.recon -> Proof.context -> |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
249 |
(int list * thm) * Proof.context, |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
250 |
default_max_relevant: int } |
36898 | 251 |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
252 |
structure Solvers = Generic_Data |
36898 | 253 |
( |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
type T = solver_info Symtab.table |
36898 | 255 |
val empty = Symtab.empty |
256 |
val extend = I |
|
257 |
fun merge data = Symtab.merge (K true) data |
|
258 |
handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name) |
|
259 |
) |
|
260 |
||
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
local |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
(case outcome output of |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
(Unsat, ls) => |
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:
40357
diff
changeset
|
265 |
if not (Config.get ctxt C.oracle) andalso is_some reconstruct |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
266 |
then the reconstruct ctxt recon ls |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
267 |
else (([], ocl ()), ctxt) |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
268 |
| (result, ls) => |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
269 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
270 |
val (ts, us) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
271 |
(case cex_parser of SOME f => f ctxt recon ls | _ => ([], [])) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
272 |
in |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
273 |
raise SMT_Failure.SMT (SMT_Failure.Counterexample { |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
274 |
is_real_cex = (result = Sat), |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
275 |
free_constraints = ts, |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
276 |
const_defs = us}) |
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:
40357
diff
changeset
|
277 |
end) |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
278 |
|
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
279 |
val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False}) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
281 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
282 |
fun add_solver cfg = |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
283 |
let |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
284 |
val {name, env_var, is_remote, options, interface, outcome, cex_parser, |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
285 |
reconstruct, default_max_relevant} = cfg |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
286 |
val {class, ...} = interface |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
287 |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
288 |
fun core_oracle () = cfalse |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
289 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
290 |
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, |
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:
40357
diff
changeset
|
291 |
interface=interface, |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
292 |
reconstruct=finish (outcome name) cex_parser reconstruct ocl, |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
293 |
default_max_relevant=default_max_relevant } |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
in |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40981
diff
changeset
|
297 |
Context.theory_map (C.add_solver (name, class)) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
|
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
300 |
end |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
301 |
|
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
302 |
fun get_info ctxt name = |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
303 |
the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
304 |
|
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:
40357
diff
changeset
|
305 |
fun name_and_solver_of ctxt = |
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:
40357
diff
changeset
|
306 |
let val name = C.solver_of ctxt |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
307 |
in (name, get_info ctxt name) end |
36898 | 308 |
|
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
309 |
val solver_name_of = fst o name_and_solver_of |
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:
40357
diff
changeset
|
310 |
fun solver_of ctxt = |
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:
40357
diff
changeset
|
311 |
let val (name, raw_solver) = name_and_solver_of ctxt |
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:
40357
diff
changeset
|
312 |
in gen_solver name raw_solver end |
36898 | 313 |
|
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
314 |
val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof |
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
315 |
|
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset
|
316 |
fun is_locally_installed ctxt name = |
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
317 |
let val {env_var, ...} = get_info ctxt name |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
318 |
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
|
319 |
|
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
320 |
val is_remotely_available = #is_remote oo get_info |
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
321 |
|
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset
|
322 |
val default_max_relevant = #default_max_relevant oo get_info |
36898 | 323 |
|
324 |
||
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:
40357
diff
changeset
|
325 |
(* 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
|
326 |
|
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
|
327 |
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
|
328 |
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
|
329 |
| 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
|
330 |
| _ => 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
|
331 |
|
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
|
332 |
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
|
333 |
(* without this test, we would run into problems when atomizing the rules: *) |
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:
40357
diff
changeset
|
334 |
if exists (has_topsort o Thm.prop_of o snd) irules then |
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:
40357
diff
changeset
|
335 |
raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ |
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:
40357
diff
changeset
|
336 |
"contains the universal sort {}")) |
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:
40357
diff
changeset
|
337 |
else solver_of ctxt rm ctxt irules |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
338 |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
339 |
val cnot = Thm.cterm_of @{theory} @{const Not} |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
340 |
|
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
|
341 |
fun smt_filter run_remote time_limit st xrules i = |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
let |
40199 | 343 |
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
|
344 |
val ctxt = |
40199 | 345 |
Proof.context_of st |
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:
40357
diff
changeset
|
346 |
|> Config.put C.oracle false |
40560
b57f7fee72ee
honour timeouts which are not rounded to full seconds
boehmes
parents:
40550
diff
changeset
|
347 |
|> Config.put C.timeout (Time.toReal time_limit) |
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:
40357
diff
changeset
|
348 |
|> Config.put C.drop_bad_facts true |
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:
40357
diff
changeset
|
349 |
|> Config.put C.filter_only_facts true |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
350 |
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal |
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
351 |
fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset
|
352 |
val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
353 |
val irs = map (pair ~1) (Thm.assume cprop :: prems @ 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
|
354 |
val rm = SOME run_remote |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
40666
8db6c2b1591d
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates
blanchet
parents:
40579
diff
changeset
|
356 |
(xrules, map snd xrules) |
40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset
|
357 |
||> 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
|
358 |
|-> map_filter o try o nth |
40980
3ea3124b0a2b
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
blanchet
parents:
40940
diff
changeset
|
359 |
|> (fn xs => {outcome=NONE, used_facts=if solver_name_of ctxt = "z3" (* FIXME *) then xs |
3ea3124b0a2b
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
blanchet
parents:
40940
diff
changeset
|
360 |
else xrules, run_time_in_msecs=NONE}) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific 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 |
end |
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:
40357
diff
changeset
|
362 |
handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[], |
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:
40357
diff
changeset
|
363 |
run_time_in_msecs=NONE} |
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset
|
364 |
(* 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
|
365 |
|
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
|
366 |
|
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
|
367 |
|
36898 | 368 |
(* SMT tactic *) |
369 |
||
370 |
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
|
371 |
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
|
372 |
THEN' Tactic.rtac @{thm ccontr} |
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:
40357
diff
changeset
|
373 |
THEN' SUBPROOF (fn {context=ctxt', prems, ...} => |
40165 | 374 |
let |
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:
40357
diff
changeset
|
375 |
fun solve irules = snd (smt_solver NONE ctxt' irules) |
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:
40357
diff
changeset
|
376 |
val tag = "Solver " ^ C.solver_of ctxt' ^ ": " |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
377 |
val str_of = prefix tag o SMT_Failure.string_of_failure ctxt' |
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:
40357
diff
changeset
|
378 |
fun safe_solve irules = |
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:
40357
diff
changeset
|
379 |
if pass_exns then SOME (solve irules) |
40515
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
380 |
else (SOME (solve irules) |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
381 |
handle |
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40425
diff
changeset
|
382 |
SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
383 |
(C.verbose_msg ctxt' str_of fail; NONE) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset
|
384 |
| SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE)) |
40165 | 385 |
in |
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:
40357
diff
changeset
|
386 |
safe_solve (map (pair ~1) (rules @ prems)) |
40165 | 387 |
|> (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
|
388 |
end) ctxt |
36898 | 389 |
|
390 |
val smt_tac = smt_tac' false |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset
|
391 |
|
36898 | 392 |
val smt_method = |
393 |
Scan.optional Attrib.thms [] >> |
|
394 |
(fn thms => fn ctxt => METHOD (fn facts => |
|
395 |
HEADGOAL (smt_tac ctxt (thms @ facts)))) |
|
396 |
||
397 |
||
398 |
||
399 |
(* setup *) |
|
400 |
||
401 |
val setup = |
|
38808 | 402 |
Method.setup @{binding smt} smt_method |
36898 | 403 |
"Applies an SMT solver to the current goal." |
404 |
||
405 |
end |