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

test: more CC tests

Browse source
This commit is contained in:
Simon Cruanes 2019-10-30 15:03:24 -05:00
parent c9f0141591
commit 71db47f9ac
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/mini-cc/tests/tests.ml
View file

@ -80,5 +80,28 @@ let () = mk_test "test_trans" @@ fun () ->
A.(check bool) "is-unsat" (CC.check_sat cc) false;
()
let () = mk_test "test_true" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
CC.add_lit cc S.true_ true;
A.(check bool) "is-sat" (CC.check_sat cc) true;
CC.add_lit cc S.false_ true;
A.(check bool) "is-unsat" (CC.check_sat cc) false;
()
let () = mk_test "test_false" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
CC.add_lit cc S.false_ true;
A.(check bool) "is-unsat" (CC.check_sat cc) false;
()
let () = mk_test "test_not_false" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
CC.add_lit cc S.(not_ false_) true;
A.(check bool) "is-sat" (CC.check_sat cc) true;
()
(* run alcotest *)
let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]