diff --git a/src/core/lit.ml b/src/core/lit.ml index 9ba770b6..a9479a62 100644 --- a/src/core/lit.ml +++ b/src/core/lit.ml @@ -28,12 +28,24 @@ let hash a = let pp out l = if l.lit_sign then - T.pp_debug out l.lit_term + T_printer.pp out l.lit_term else - Format.fprintf out "(@[@<1>¬@ %a@])" T.pp_debug l.lit_term + Format.fprintf out "(@[@<1>¬@ %a@])" T_printer.pp l.lit_term let norm_sign l = if l.lit_sign then l, true else neg l, false + +module As_key = struct + type nonrec t = t + + let equal = equal + let hash = hash + let compare = compare +end + +module Map = CCMap.Make (As_key) +module Set = CCSet.Make (As_key) +module Tbl = CCHashtbl.Make (As_key) diff --git a/src/core/lit.mli b/src/core/lit.mli index bf012a59..6b3b42c1 100644 --- a/src/core/lit.mli +++ b/src/core/lit.mli @@ -42,3 +42,5 @@ val norm_sign : t -> t * bool (** [norm_sign (+t)] is [+t, true], and [norm_sign (-t)] is [+t, false]. In both cases the term is positive, and the boolean reflects the initial sign. *) + +include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t