|
1 (* Title: HOL/SMT/Tools/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 = |
|
19 ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"] |
|
20 |
|
21 val is_sat = String.isPrefix "Satisfiable." |
|
22 val is_unsat = String.isPrefix "Unsatisfiable." |
|
23 val is_unknown = String.isPrefix "Unknown." |
|
24 |
|
25 fun cex_kind true = "Counterexample" |
|
26 | cex_kind false = "Possible counterexample" |
|
27 |
|
28 fun raise_cex real ctxt recon ls = |
|
29 let |
|
30 val start = String.isPrefix "%Satisfiable Variable Assignment: %" |
|
31 val index = find_index start ls |
|
32 val ls = if index > 0 then Library.drop (index + 1, ls) else [] |
|
33 val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls) |
|
34 in error (Pretty.string_of p) end |
|
35 |
|
36 fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) = |
|
37 let |
|
38 val empty_line = (fn "" => true | _ => false) |
|
39 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
|
40 val (l, ls) = split_first (dropwhile empty_line output) |
|
41 in |
|
42 if is_unsat l then @{cprop False} |
|
43 else if is_sat l then raise_cex true context recon ls |
|
44 else if is_unknown l then raise_cex false context recon ls |
|
45 else error (solver_name ^ " failed") |
|
46 end |
|
47 |
|
48 fun smtlib_solver oracle _ = |
|
49 SMT_Solver.SolverConfig { |
|
50 name = {env_var=env_var, remote_name=solver_name}, |
|
51 interface = SMTLIB_Interface.interface, |
|
52 arguments = options, |
|
53 reconstruct = oracle } |
|
54 |
|
55 val setup = |
|
56 Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => |
|
57 SMT_Solver.add_solver (solver_name, smtlib_solver oracle)) |
|
58 |
|
59 end |