15 val solver_name = "yices" |
15 val solver_name = "yices" |
16 val env_var = "YICES_SOLVER" |
16 val env_var = "YICES_SOLVER" |
17 |
17 |
18 val options = ["--smtlib"] |
18 val options = ["--smtlib"] |
19 |
19 |
20 fun cex_kind true = "Counterexample" |
20 fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, []) |
21 | cex_kind false = "Possible counterexample" |
|
22 |
|
23 fun raise_cex real = error (cex_kind real ^ " found.") |
|
24 |
|
25 structure S = SMT_Solver |
|
26 |
21 |
27 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) = |
22 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) = |
28 let |
23 let |
29 val empty_line = (fn "" => true | _ => false) |
24 val empty_line = (fn "" => true | _ => false) |
30 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
25 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) |
31 val (l, ls) = split_first (dropwhile empty_line output) |
26 val (l, ls) = split_first (dropwhile empty_line output) |
32 in |
27 in |
33 if String.isPrefix "unsat" l then @{cprop False} |
28 if String.isPrefix "unsat" l then @{cprop False} |
34 else if String.isPrefix "sat" l then raise_cex true |
29 else if String.isPrefix "sat" l then raise_cex true |
35 else if String.isPrefix "unknown" l then raise_cex false |
30 else if String.isPrefix "unknown" l then raise_cex false |
36 else error (solver_name ^ " failed") |
31 else raise SMT_Solver.SMT (solver_name ^ " failed") |
37 end |
32 end |
38 |
33 |
39 fun smtlib_solver oracle _ = { |
34 fun smtlib_solver oracle _ = { |
40 command = {env_var=env_var, remote_name=solver_name}, |
35 command = {env_var=env_var, remote_name=solver_name}, |
41 arguments = options, |
36 arguments = options, |