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

add test case to mini-cc

Browse source
This commit is contained in:
Simon Cruanes 2021-06-16 20:10:26 -04:00
parent a223b6cd5c
commit 952740f66f
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -147,5 +147,25 @@ let () = mk_test "test_ite" @@ fun () ->
done;
()
(* from the following PO:
`cl (- a = (g a c)),
(- b = (g a c)),
(- c = (g c b)),
(- a = (g c c)),
(- (g c (g c b)) = (g (g c c) b)),
(+ (g a b) = (g a c))))`
*)
let () = mk_test "test_reg_1" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
CC.add_lit cc S.(eq a (g a c)) true;
CC.add_lit cc S.(eq b (g a c)) true;
CC.add_lit cc S.(eq c (g c b)) true;
CC.add_lit cc S.(eq a (g c c)) true;
CC.add_lit cc S.(eq (g c (g c b)) (g (g c c) b)) true;
CC.add_lit cc S.(eq (g a b) (g a c)) false; (* goal *)
A.(check bool) "is-unsat" (CC.check_sat cc) false;
()
(* run alcotest *)
let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]