src/HOL/Tools/SMT/yices_solver.ML
author wenzelm
Thu, 02 Sep 2010 16:31:50 +0200
changeset 39046 5b38730f3e12
parent 36899 bcd6fce5bf06
child 39809 dac3c3106746
permissions -rw-r--r--
tuned whitespace and indentation, emphasizing the logical structure of this long text;

(*  Title:      HOL/Tools/SMT/yices_solver.ML
    Author:     Sascha Boehme, TU Muenchen

Interface of the SMT solver Yices.
*)

signature YICES_SOLVER =
sig
  val setup: theory -> theory
end

structure Yices_Solver: YICES_SOLVER =
struct

val solver_name = "yices"
val env_var = "YICES_SOLVER"

val options = ["--smtlib"]

fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])

fun core_oracle (output, _) =
  let
    val empty_line = (fn "" => true | _ => false)
    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    val (l, _) = split_first (dropwhile empty_line output)
  in
    if String.isPrefix "unsat" l then @{cprop False}
    else if String.isPrefix "sat" l then raise_cex true
    else if String.isPrefix "unknown" l then raise_cex false
    else raise SMT_Solver.SMT (solver_name ^ " failed")
  end

fun solver oracle _ = {
  command = {env_var=env_var, remote_name=NONE},
  arguments = options,
  interface = SMTLIB_Interface.interface,
  reconstruct = pair o oracle }

val setup =
  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))

end