src/HOL/Tools/SMT/cvc3_solver.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36899 bcd6fce5bf06
child 39809 dac3c3106746
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/cvc3_solver.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Interface of the SMT solver CVC3.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature CVC3_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  val setup: theory -> theory
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
structure CVC3_Solver: CVC3_SOLVER =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
val solver_name = "cvc3"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
val env_var = "CVC3_SOLVER"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
val options = ["-lang", "smtlib", "-output-lang", "presentation"]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
val is_sat = String.isPrefix "Satisfiable."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
val is_unsat = String.isPrefix "Unsatisfiable."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
val is_unknown = String.isPrefix "Unknown."
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
fun core_oracle (output, _) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
    val empty_line = (fn "" => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
    val (l, _) = split_first (dropwhile empty_line output)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
    if is_unsat l then @{cprop False}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
    else if is_sat l then raise_cex true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
    else if is_unknown l then raise_cex false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
    else raise SMT_Solver.SMT (solver_name ^ " failed")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    38
fun solver oracle _ = {
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
  command = {env_var=env_var, remote_name=SOME solver_name},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  arguments = options,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  interface = SMTLIB_Interface.interface,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
  reconstruct = pair o oracle }
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
val setup =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    46
  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
end