1 (* Title: HOL/Tools/SMT/z3_solver.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Interface of the SMT solver Z3. |
|
5 *) |
|
6 |
|
7 signature Z3_SOLVER = |
|
8 sig |
|
9 val proofs: bool Config.T |
|
10 val options: string Config.T |
|
11 val datatypes: bool Config.T |
|
12 val setup: theory -> theory |
|
13 end |
|
14 |
|
15 structure Z3_Solver: Z3_SOLVER = |
|
16 struct |
|
17 |
|
18 val solver_name = "z3" |
|
19 val env_var = "Z3_SOLVER" |
|
20 |
|
21 val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false) |
|
22 val (options, options_setup) = Attrib.config_string "z3_options" (K "") |
|
23 val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false) |
|
24 |
|
25 fun add xs ys = ys @ xs |
|
26 |
|
27 fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s |
|
28 |
|
29 fun get_options ctxt = |
|
30 ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"] |
|
31 |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"] |
|
32 |> add (explode_options (Config.get ctxt options)) |
|
33 |
|
34 fun pretty_config context = [ |
|
35 Pretty.str ("With proofs: " ^ |
|
36 (if Config.get_generic context proofs then "true" else "false")), |
|
37 Pretty.str ("Options: " ^ |
|
38 space_implode " " (get_options (Context.proof_of context))) ] |
|
39 |
|
40 fun cmdline_options ctxt = |
|
41 get_options ctxt |
|
42 |> add ["-smt"] |
|
43 |
|
44 fun raise_cex ctxt real recon ls = |
|
45 let val cex = Z3_Model.parse_counterex ctxt recon ls |
|
46 in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end |
|
47 |
|
48 fun if_unsat f (output, recon) ctxt = |
|
49 let |
|
50 fun jnk l = |
|
51 String.isPrefix "WARNING" l orelse |
|
52 String.isPrefix "ERROR" l orelse |
|
53 forall Symbol.is_ascii_blank (Symbol.explode l) |
|
54 val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output)) |
|
55 in |
|
56 if String.isPrefix "unsat" l then f (ls, recon) ctxt |
|
57 else if String.isPrefix "sat" l then raise_cex ctxt true recon ls |
|
58 else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls |
|
59 else raise SMT_Solver.SMT (solver_name ^ " failed") |
|
60 end |
|
61 |
|
62 val core_oracle = uncurry (if_unsat (K (K @{cprop False}))) |
|
63 |
|
64 val prover = if_unsat Z3_Proof_Reconstruction.reconstruct |
|
65 |
|
66 fun solver oracle ctxt = |
|
67 let |
|
68 val with_datatypes = Config.get ctxt datatypes |
|
69 val with_proof = not with_datatypes andalso Config.get ctxt proofs |
|
70 (* FIXME: implement proof reconstruction for datatypes *) |
|
71 in |
|
72 {command = {env_var=env_var, remote_name=SOME solver_name}, |
|
73 arguments = cmdline_options ctxt, |
|
74 interface = Z3_Interface.interface with_datatypes, |
|
75 reconstruct = |
|
76 if with_proof then prover else (fn r => `(pair [] o oracle o pair r))} |
|
77 end |
|
78 |
|
79 val setup = |
|
80 proofs_setup #> |
|
81 options_setup #> |
|
82 datatypes_setup #> |
|
83 Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => |
|
84 Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #> |
|
85 Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config)) |
|
86 |
|
87 end |
|