1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT/SMT.thy	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -0,0 +1,51 @@
     1.4 +(*  Title:      HOL/SMT/SMT.thy
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* SMT method using external SMT solvers (CVC3, Yices, Z3) *}
     1.9 +
    1.10 +theory SMT
    1.11 +imports SMT_Definitions
    1.12 +uses
    1.13 +  "Tools/smt_normalize.ML"
    1.14 +  "Tools/smt_monomorph.ML"
    1.15 +  "Tools/smt_translate.ML"
    1.16 +  "Tools/smt_solver.ML"
    1.17 +  "Tools/smtlib_interface.ML"
    1.18 +  "Tools/cvc3_solver.ML"
    1.19 +  "Tools/yices_solver.ML"
    1.20 +  "Tools/z3_model.ML"
    1.21 +  "Tools/z3_interface.ML"
    1.22 +  "Tools/z3_solver.ML"
    1.23 +begin
    1.24 +
    1.25 +setup {*
    1.26 +  SMT_Normalize.setup #>
    1.27 +  SMT_Solver.setup #>
    1.28 +  CVC3_Solver.setup #>
    1.29 +  Yices_Solver.setup #>
    1.30 +  Z3_Solver.setup
    1.31 +*}
    1.32 +
    1.33 +ML {*
    1.34 +OuterSyntax.improper_command "smt_status"
    1.35 +  "Show the available SMT solvers and the currently selected solver."
    1.36 +  OuterKeyword.diag
    1.37 +    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
    1.38 +      SMT_Solver.print_setup (Context.Proof (Toplevel.context_of state)))))
    1.39 +*}
    1.40 +
    1.41 +method_setup smt = {*
    1.42 +  let fun solver thms ctxt = SMT_Solver.smt_tac ctxt thms
    1.43 +  in
    1.44 +    Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
    1.45 +    (Method.SIMPLE_METHOD' oo solver)
    1.46 +  end
    1.47 +*} "Applies an SMT solver to the current goal."
    1.48 +
    1.49 +declare [[ smt_solver = z3, smt_timeout = 20, smt_trace = false ]]
    1.50 +declare [[ smt_unfold_defs = true ]]
    1.51 +declare [[ z3_proofs = false ]]
    1.52 +
    1.53 +end
    1.54 +