simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-03-10 23:48:37 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: remove code that checks invariants

Browse source
This commit is contained in:
Simon Cruanes 2019-06-10 14:27:41 -05:00
parent b2f6a30cc8
commit 6c603d5589
5 changed files with 1 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/cc/Sidekick_cc.ml
View file

@ -739,8 +739,6 @@ module Make(CC_A: ARG) = struct
() ()
module Debug_ = struct module Debug_ = struct
let[@inline] check_invariants (cc:t) : unit =
if Util._CHECK_INVARIANTS then check_invariants_ cc
let pp out _ = Fmt.string out "cc" let pp out _ = Fmt.string out "cc"
end end

7
src/core/Sidekick_core.ml
View file

@ -277,7 +277,6 @@ module type CC_S = sig
(**/**) (**/**)
module Debug_ : sig module Debug_ : sig
val check_invariants : t -> unit
val pp : t Fmt.printer val pp : t Fmt.printer
end end
(**/**) (**/**)
@ -624,10 +623,4 @@ module type SOLVER = sig
val pp_term_graph: t CCFormat.printer val pp_term_graph: t CCFormat.printer
val pp_stats : t CCFormat.printer val pp_stats : t CCFormat.printer
(**/**)
module Debug_ : sig
val check_invariants : t -> unit
end
(**/**)
end end

9
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -436,16 +436,9 @@ module Make(A : ARG)
end; end;
self self
module Debug_ = struct
let check_invariants (self:t) =
if Util._CHECK_INVARIANTS then (
CC.Debug_.check_invariants (Solver_internal.cc self.si);
)
end
let[@inline] solver self = self.solver let[@inline] solver self = self.solver
let[@inline] cc self = Solver_internal.cc self.si let[@inline] cc self = Solver_internal.cc self.si
let stats self = self.stat let[@inline] stats self = self.stat
let[@inline] tst self = Solver_internal.tst self.si let[@inline] tst self = Solver_internal.tst self.si
let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit let[@inline] mk_atom_lit_ self lit : Atom.t = Sat_solver.make_atom self.solver lit

3
src/util/Util.ml
View file

@ -1,4 +1,3 @@
(* This file is free software. See file "license" for more details. *) (* This file is free software. See file "license" for more details. *)
(** {1 Util} *) (** {1 Util} *)
@ -38,5 +37,3 @@ module Int_set = CCSet.Make(CCInt)
module Int_map = CCMap.Make(CCInt) module Int_map = CCMap.Make(CCInt)
module Int_tbl = CCHashtbl.Make(CCInt) module Int_tbl = CCHashtbl.Make(CCInt)
(* NOTE: if true, can have a big impact on performance *)
let _CHECK_INVARIANTS = false

6
src/util/Util.mli
View file

@ -1,4 +1,3 @@
(* This file is free software. See file "license" for more details. *) (* This file is free software. See file "license" for more details. *)
(** {1 Utils} *) (** {1 Utils} *)
@ -23,8 +22,3 @@ val setup_gc : unit -> unit
module Int_set : CCSet.S with type elt = int module Int_set : CCSet.S with type elt = int
module Int_map : CCMap.S with type key = int module Int_map : CCMap.S with type key = int
module Int_tbl : CCHashtbl.S with type key = int module Int_tbl : CCHashtbl.S with type key = int
(* compile time config for internal checking of invariants *)
val _CHECK_INVARIANTS : bool