author | wenzelm |
Thu, 02 Sep 2010 16:31:50 +0200 | |
changeset 39046 | 5b38730f3e12 |
parent 36899 | bcd6fce5bf06 |
child 39809 | dac3c3106746 |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/yices_solver.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Interface of the SMT solver Yices. |
|
5 |
*) |
|
6 |
||
7 |
signature YICES_SOLVER = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
10 |
end |
|
11 |
||
12 |
structure Yices_Solver: YICES_SOLVER = |
|
13 |
struct |
|
14 |
||
15 |
val solver_name = "yices" |
|
16 |
val env_var = "YICES_SOLVER" |
|
17 |
||
18 |
val options = ["--smtlib"] |
|
19 |
||
20 |
fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, []) |
|
21 |
||
22 |
fun core_oracle (output, _) = |
|
23 |
let |
|
24 |
val empty_line = (fn "" => true | _ => false) |
|
25 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
|
26 |
val (l, _) = split_first (dropwhile empty_line output) |
|
27 |
in |
|
28 |
if String.isPrefix "unsat" l then @{cprop False} |
|
29 |
else if String.isPrefix "sat" l then raise_cex true |
|
30 |
else if String.isPrefix "unknown" l then raise_cex false |
|
31 |
else raise SMT_Solver.SMT (solver_name ^ " failed") |
|
32 |
end |
|
33 |
||
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
34 |
fun solver oracle _ = { |
36898 | 35 |
command = {env_var=env_var, remote_name=NONE}, |
36 |
arguments = options, |
|
37 |
interface = SMTLIB_Interface.interface, |
|
38 |
reconstruct = pair o oracle } |
|
39 |
||
40 |
val setup = |
|
41 |
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
|
42 |
Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) |
36898 | 43 |
|
44 |
end |