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

updates to tests

Browse source
This commit is contained in:
Simon Cruanes 2016-07-27 19:09:11 +02:00
parent 3e54fac7f9
commit 98d5074da6
1 changed files with 15 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
tests/test_api.ml
View file

@ -9,6 +9,8 @@ Copyright 2014 Simon Cruanes
module F = Expr module F = Expr
module T = Cnf.S module T = Cnf.S
let (|>) x f = f x
type solver = Smt | Mcsat type solver = Smt | Mcsat
let solver_list = [ let solver_list = [
"smt", Smt; "smt", Smt;
@ -64,7 +66,7 @@ let mk_solver (s:solver): (module BASIC_SOLVER) =
| Sat _ -> R_sat | Sat _ -> R_sat
| Unsat _ -> R_unsat | Unsat _ -> 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)
@ -72,7 +74,7 @@ let mk_solver (s:solver): (module BASIC_SOLVER) =
| Sat _ -> R_sat | Sat _ -> R_sat
| Unsat _ -> R_unsat | Unsat _ -> R_unsat
end end
in (module S) in (module S)
exception Error of string exception Error of string
@ -115,7 +117,7 @@ module Test = struct
| R_unsat, `Expect_sat -> | R_unsat, `Expect_sat ->
error "expect sat, got unsat" error "expect sat, got unsat"
| R_sat, `Expect_unsat -> | R_sat, `Expect_unsat ->
error "expect sat, got unsat" error "expect unsat, got sat"
) )
t.actions; t.actions;
Pass Pass
@ -134,7 +136,8 @@ module Test = struct
(* same as test1 but with assumptions *) (* same as test1 but with assumptions *)
let test2 = let test2 =
[ assume [[-1;2]; [-1;3]]; [ solve `Expect_sat;
assume [[-1;2]; [-1;3]];
solve `Expect_sat; solve `Expect_sat;
assume [[-2;4]; [-3;-4]]; assume [[-2;4]; [-3;-4]];
solve `Expect_sat; solve `Expect_sat;
@ -155,12 +158,20 @@ module Test = struct
solve ~assumptions:[1] `Expect_unsat; solve ~assumptions:[1] `Expect_unsat;
solve `Expect_sat; solve `Expect_sat;
solve ~assumptions:[2] `Expect_sat; solve ~assumptions:[2] `Expect_sat;
assume [[1]];
solve `Expect_unsat;
] |> mk_test "test3" ] |> mk_test "test3"
(* just check that we do create new solvers *)
let test_clean =
[ solve `Expect_sat
] |> mk_test "test_clean"
let suite = let suite =
[ test1; [ test1;
test2; test2;
test3; test3;
test_clean; (* after test3 *)
] ]
end end