1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -0,0 +1,52 @@
     1.4 +(*  Title:      HOL/SMT/Tools/yices_solver.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Interface of the SMT solver Yices.
     1.8 +*)
     1.9 +
    1.10 +signature YICES_SOLVER =
    1.11 +sig
    1.12 +  val setup: theory -> theory
    1.13 +end
    1.14 +
    1.15 +structure Yices_Solver: YICES_SOLVER =
    1.16 +struct
    1.17 +
    1.18 +val solver_name = "yices"
    1.19 +val env_var = "YICES_SOLVER"
    1.20 +
    1.21 +val options = ["--evidence", "--smtlib"]
    1.22 +
    1.23 +fun cex_kind true = "Counterexample"
    1.24 +  | cex_kind false = "Possible counterexample"
    1.25 +
    1.26 +fun raise_cex real ctxt rtab ls =
    1.27 +  let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
    1.28 +  in error (Pretty.string_of p) end
    1.29 +
    1.30 +structure S = SMT_Solver
    1.31 +
    1.32 +fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
    1.33 +  let
    1.34 +    val empty_line = (fn "" => true | _ => false)
    1.35 +    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    1.36 +    val (l, ls) = split_first (dropwhile empty_line output)
    1.37 +  in
    1.38 +    if String.isPrefix "unsat" l then @{cprop False}
    1.39 +    else if String.isPrefix "sat" l then raise_cex true context recon ls
    1.40 +    else if String.isPrefix "unknown" l then raise_cex false context recon ls
    1.41 +    else error (solver_name ^ " failed")
    1.42 +  end
    1.43 +
    1.44 +fun smtlib_solver oracle _ =
    1.45 +  SMT_Solver.SolverConfig {
    1.46 +    name = {env_var=env_var, remote_name=solver_name},
    1.47 +    interface = SMTLIB_Interface.interface,
    1.48 +    arguments = options,
    1.49 +    reconstruct = oracle }
    1.50 +
    1.51 +val setup =
    1.52 +  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
    1.53 +  SMT_Solver.add_solver (solver_name, smtlib_solver oracle))
    1.54 +
    1.55 +end