1 (* Title: HOL/SMT/SMT.thy |
1 (* Title: HOL/SMT/SMT.thy |
2 Author: Sascha Boehme, TU Muenchen |
2 Author: Sascha Boehme, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* SMT method using external SMT solvers (CVC3, Yices, Z3) *} |
5 header {* Bindings to several SMT solvers *} |
6 |
6 |
7 theory SMT |
7 theory SMT |
8 imports SMT_Definitions |
8 imports SMT_Base Z3 |
9 uses |
9 uses |
10 "Tools/smt_normalize.ML" |
|
11 "Tools/smt_monomorph.ML" |
|
12 "Tools/smt_translate.ML" |
|
13 "Tools/smt_solver.ML" |
|
14 "Tools/smtlib_interface.ML" |
|
15 "Tools/cvc3_solver.ML" |
10 "Tools/cvc3_solver.ML" |
16 "Tools/yices_solver.ML" |
11 "Tools/yices_solver.ML" |
17 "Tools/z3_model.ML" |
|
18 "Tools/z3_interface.ML" |
|
19 "Tools/z3_solver.ML" |
|
20 begin |
12 begin |
21 |
13 |
22 setup {* |
14 setup {* CVC3_Solver.setup #> Yices_Solver.setup *} |
23 SMT_Normalize.setup #> |
|
24 SMT_Solver.setup #> |
|
25 CVC3_Solver.setup #> |
|
26 Yices_Solver.setup #> |
|
27 Z3_Solver.setup |
|
28 *} |
|
29 |
15 |
30 ML {* |
16 declare [[ smt_solver = z3, smt_timeout = 20 ]] |
31 OuterSyntax.improper_command "smt_status" |
|
32 "Show the available SMT solvers and the currently selected solver." |
|
33 OuterKeyword.diag |
|
34 (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => |
|
35 SMT_Solver.print_setup (Context.Proof (Toplevel.context_of state))))) |
|
36 *} |
|
37 |
|
38 method_setup smt = {* |
|
39 let fun solver thms ctxt = SMT_Solver.smt_tac ctxt thms |
|
40 in |
|
41 Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >> |
|
42 (Method.SIMPLE_METHOD' oo solver) |
|
43 end |
|
44 *} "Applies an SMT solver to the current goal." |
|
45 |
|
46 declare [[ smt_solver = z3, smt_timeout = 20, smt_trace = false ]] |
|
47 declare [[ smt_unfold_defs = true ]] |
17 declare [[ smt_unfold_defs = true ]] |
48 declare [[ z3_proofs = false ]] |
18 declare [[ smt_trace = false, smt_keep = "", smt_cert = "" ]] |
|
19 declare [[ z3_proofs = false, z3_options = "" ]] |
49 |
20 |
50 end |
21 end |
51 |
|