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

feat(mini-cc): add clear operation

Browse source
This commit is contained in:
Simon Cruanes 2019-10-30 15:32:45 -05:00
parent 71db47f9ac
commit 09ead7c41a
3 changed files with 39 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/mini-cc/Sidekick_mini_cc.ml
View file

@ -15,6 +15,8 @@ module type S = sig
val create : term_state -> t val create : term_state -> t
val clear : t -> unit
val add_lit : t -> term -> bool -> unit val add_lit : t -> term -> bool -> unit
val check_sat : t -> bool val check_sat : t -> bool
@ -144,6 +146,16 @@ module Make(A: ARG) = struct
T_tbl.add self.tbl false_ self.false_; T_tbl.add self.tbl false_ self.false_;
self self
let clear (self:t) : unit =
self.ok <- true;
T_tbl.clear self.tbl;
Sig_tbl.clear self.sig_tbl;
self.pending <- [];
self.combine <- [];
T_tbl.add self.tbl self.true_.n_t self.true_;
T_tbl.add self.tbl self.false_.n_t self.false_;
()
let sub_ t k : unit = let sub_ t k : unit =
match A.cc_view t with match A.cc_view t with
| Bool _ | Opaque _ -> () | Bool _ | Opaque _ -> ()

3
src/mini-cc/Sidekick_mini_cc.mli
View file

@ -22,6 +22,9 @@ module type S = sig
val create : term_state -> t val create : term_state -> t
val clear : t -> unit
(** Fully reset the congruence closure's state *)
val add_lit : t -> term -> bool -> unit val add_lit : t -> term -> bool -> unit
(** [add_lit cc p sign] asserts that [p=sign] *) (** [add_lit cc p sign] asserts that [p=sign] *)

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

@ -70,6 +70,18 @@ let () = mk_test "test_f_f_f_a" @@ fun () ->
A.(check bool) "is-unsat" (CC.check_sat cc) false; A.(check bool) "is-unsat" (CC.check_sat cc) false;
() ()
let () = mk_test "test_repeated_f_f_f_a" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
for _i = 0 to 10 do
CC.add_lit cc S.(neq a (f (f (f (f (f (f a))))))) true;
A.(check bool) "is-sat" (CC.check_sat cc) true;
CC.add_lit cc S.(eq a (f a)) true;
A.(check bool) "is-unsat" (CC.check_sat cc) false;
CC.clear cc;
done;
()
let () = mk_test "test_trans" @@ fun () -> let () = mk_test "test_trans" @@ fun () ->
let module S = Setup() in let module S = Setup() in
let cc = CC.create S.tst in let cc = CC.create S.tst in
@ -89,6 +101,18 @@ let () = mk_test "test_true" @@ fun () ->
A.(check bool) "is-unsat" (CC.check_sat cc) false; A.(check bool) "is-unsat" (CC.check_sat cc) false;
() ()
let () = mk_test "test_repeated_true" @@ fun () ->
let module S = Setup() in
let cc = CC.create S.tst in
for _i = 0 to 10 do
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;
CC.clear cc;
done;
()
let () = mk_test "test_false" @@ fun () -> let () = mk_test "test_false" @@ fun () ->
let module S = Setup() in let module S = Setup() in
let cc = CC.create S.tst in let cc = CC.create S.tst in