10 exception SMT_COUNTEREXAMPLE of bool * term list |
10 exception SMT_COUNTEREXAMPLE of bool * term list |
11 |
11 |
12 type proof_data = { |
12 type proof_data = { |
13 context: Proof.context, |
13 context: Proof.context, |
14 output: string list, |
14 output: string list, |
15 recon: SMT_Translate.recon, |
15 recon: SMT_Translate.recon } |
16 assms: thm list option } |
|
17 type solver_config = { |
16 type solver_config = { |
18 command: {env_var: string, remote_name: string option}, |
17 command: {env_var: string, remote_name: string option}, |
19 arguments: string list, |
18 arguments: string list, |
20 interface: string list -> SMT_Translate.config, |
19 interface: string list -> SMT_Translate.config, |
21 reconstruct: proof_data -> thm } |
20 reconstruct: proof_data -> thm } |
58 |
57 |
59 |
58 |
60 type proof_data = { |
59 type proof_data = { |
61 context: Proof.context, |
60 context: Proof.context, |
62 output: string list, |
61 output: string list, |
63 recon: SMT_Translate.recon, |
62 recon: SMT_Translate.recon } |
64 assms: thm list option } |
|
65 |
63 |
66 type solver_config = { |
64 type solver_config = { |
67 command: {env_var: string, remote_name: string option}, |
65 command: {env_var: string, remote_name: string option}, |
68 arguments: string list, |
66 arguments: string list, |
69 interface: string list -> SMT_Translate.config, |
67 interface: string list -> SMT_Translate.config, |
162 val _ = trace_msg ctxt (pretty "SMT result:") ls |
160 val _ = trace_msg ctxt (pretty "SMT result:") ls |
163 in ls end |
161 in ls end |
164 |
162 |
165 end |
163 end |
166 |
164 |
167 fun make_proof_data ctxt (ls, (recon, thms)) = |
165 fun invoke translate_config command arguments ctxt thms = |
168 {context=ctxt, output=ls, recon=recon, assms=SOME thms} |
166 thms |
|
167 |> SMT_Translate.translate translate_config ctxt |
|
168 |>> run_solver ctxt command arguments |
|
169 |> (fn (ls, recon) => {context=ctxt, output=ls, recon=recon}) |
169 |
170 |
170 fun gen_solver name solver ctxt prems = |
171 fun gen_solver name solver ctxt prems = |
171 let |
172 let |
172 val {command, arguments, interface, reconstruct} = solver ctxt |
173 val {command, arguments, interface, reconstruct} = solver ctxt |
173 val comments = ("solver: " ^ name) :: |
174 val comments = ("solver: " ^ name) :: |
174 ("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: |
175 ("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: |
175 "arguments:" :: arguments |
176 "arguments:" :: arguments |
176 val tc = interface comments |
|
177 val thy = ProofContext.theory_of ctxt |
|
178 in |
177 in |
179 SMT_Additional_Facts.add_facts prems |
178 SMT_Additional_Facts.add_facts prems |
180 |> SMT_Normalize.normalize ctxt |
179 |> SMT_Normalize.normalize ctxt |
181 ||> SMT_Translate.translate tc thy |
180 ||> invoke (interface comments) command arguments ctxt |
182 ||> apfst (run_solver ctxt command arguments) |
181 ||> reconstruct |
183 ||> reconstruct o make_proof_data ctxt |
|
184 |-> fold SMT_Normalize.discharge_definition |
182 |-> fold SMT_Normalize.discharge_definition |
185 end |
183 end |
186 |
184 |
187 |
185 |
188 |
186 |