author | haftmann |
Fri, 01 Oct 2010 10:25:36 +0200 | |
changeset 39811 | 0659e84bdc5f |
parent 39809 | dac3c3106746 |
child 40161 | 539d07b00e5f |
permissions | -rw-r--r-- |
36898 | 1 |
(* Title: HOL/Tools/SMT/cvc3_solver.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Interface of the SMT solver CVC3. |
|
5 |
*) |
|
6 |
||
7 |
signature CVC3_SOLVER = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
10 |
end |
|
11 |
||
12 |
structure CVC3_Solver: CVC3_SOLVER = |
|
13 |
struct |
|
14 |
||
15 |
val solver_name = "cvc3" |
|
16 |
val env_var = "CVC3_SOLVER" |
|
17 |
||
18 |
val options = ["-lang", "smtlib", "-output-lang", "presentation"] |
|
19 |
||
20 |
val is_sat = String.isPrefix "Satisfiable." |
|
21 |
val is_unsat = String.isPrefix "Unsatisfiable." |
|
22 |
val is_unknown = String.isPrefix "Unknown." |
|
23 |
||
24 |
fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, []) |
|
25 |
||
26 |
fun core_oracle (output, _) = |
|
27 |
let |
|
28 |
val empty_line = (fn "" => true | _ => false) |
|
29 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
|
39811 | 30 |
val (l, _) = split_first (snd (chop_while empty_line output)) |
36898 | 31 |
in |
32 |
if is_unsat l then @{cprop False} |
|
33 |
else if is_sat l then raise_cex true |
|
34 |
else if is_unknown l then raise_cex false |
|
35 |
else raise SMT_Solver.SMT (solver_name ^ " failed") |
|
36 |
end |
|
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 | 39 |
command = {env_var=env_var, remote_name=SOME solver_name}, |
40 |
arguments = options, |
|
41 |
interface = SMTLIB_Interface.interface, |
|
42 |
reconstruct = pair o oracle } |
|
43 |
||
44 |
val setup = |
|
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 | 47 |
|
48 |
end |