author | boehmes |
Fri, 18 Sep 2009 18:13:19 +0200 | |
changeset 32618 | 42865636d006 |
child 33010 | 39f73a59e855 |
permissions | -rw-r--r-- |
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/SMT/Tools/cvc3_solver.ML |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
3 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
4 |
Interface of the SMT solver CVC3. |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
5 |
*) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
6 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
7 |
signature CVC3_SOLVER = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
8 |
sig |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
9 |
val setup: theory -> theory |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
10 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
11 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
12 |
structure CVC3_Solver: CVC3_SOLVER = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
13 |
struct |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
14 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
15 |
val solver_name = "cvc3" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
16 |
val env_var = "CVC3_SOLVER" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
17 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
18 |
val options = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
19 |
["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
20 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
21 |
val is_sat = String.isPrefix "Satisfiable." |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
22 |
val is_unsat = String.isPrefix "Unsatisfiable." |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
23 |
val is_unknown = String.isPrefix "Unknown." |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
24 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
25 |
fun cex_kind true = "Counterexample" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
26 |
| cex_kind false = "Possible counterexample" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
27 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
28 |
fun raise_cex real ctxt recon ls = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
29 |
let |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
30 |
val start = String.isPrefix "%Satisfiable Variable Assignment: %" |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
31 |
val index = find_index start ls |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
32 |
val ls = if index > 0 then Library.drop (index + 1, ls) else [] |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
33 |
val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
34 |
in error (Pretty.string_of p) end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
35 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
36 |
fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
37 |
let |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
38 |
val empty_line = (fn "" => true | _ => false) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
39 |
val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
40 |
val (l, ls) = split_first (dropwhile empty_line output) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
41 |
in |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
42 |
if is_unsat l then @{cprop False} |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
43 |
else if is_sat l then raise_cex true context recon ls |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
44 |
else if is_unknown l then raise_cex false context recon ls |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
45 |
else error (solver_name ^ " failed") |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
46 |
end |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
47 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
48 |
fun smtlib_solver oracle _ = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
49 |
SMT_Solver.SolverConfig { |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
50 |
name = {env_var=env_var, remote_name=solver_name}, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
51 |
interface = SMTLIB_Interface.interface, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
52 |
arguments = options, |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
53 |
reconstruct = oracle } |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
54 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
55 |
val setup = |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
56 |
Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
57 |
SMT_Solver.add_solver (solver_name, smtlib_solver oracle)) |
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
58 |
|
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
diff
changeset
|
59 |
end |