simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

check proofs in test_api

Browse source
This commit is contained in:
Simon Cruanes 2016-07-28 11:10:31 +02:00
parent 5a04fa49ed
commit d6c6331d85
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
tests/test_api.ml
View file

@ -57,22 +57,32 @@ module type BASIC_SOLVER = sig
val assume : ?tag:int -> F.t list list -> unit val assume : ?tag:int -> F.t list list -> unit
end end
exception Incorrect_model
let mk_solver (s:solver): (module BASIC_SOLVER) = let mk_solver (s:solver): (module BASIC_SOLVER) =
match s with match s with
| Smt -> | Smt ->
let module S = struct let module S = struct
include Smt.Make(struct end) include Smt.Make(struct end)
let solve ?assumptions ()= match solve ?assumptions() with let solve ?assumptions ()= match solve ?assumptions() with
| Sat _ -> R_sat | Sat _ ->
| Unsat _ -> R_unsat R_sat
| Unsat us ->
let p = us.Solver_intf.get_proof () in
Proof.check p;
R_unsat
end end
in (module S) in (module S)
| Mcsat -> | Mcsat ->
let module S = struct let module S = struct
include Mcsat.Make(struct end) include Mcsat.Make(struct end)
let solve ?assumptions ()= match solve ?assumptions() with let solve ?assumptions ()= match solve ?assumptions() with
| Sat _ -> R_sat | Sat _ ->
| Unsat _ -> R_unsat R_sat
| Unsat us ->
let p = us.Solver_intf.get_proof () in
Proof.check p;
R_unsat
end end
in (module S) in (module S)