From 782afa44158bcc1d817cfb0a540038196933615f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 25 Aug 2021 09:36:24 -0400 Subject: [PATCH] feat: move `Int_id` into its own module --- src/sat/Solver.ml | 30 ++++++------------------------ src/util/Int_id.ml | 18 ++++++++++++++++++ src/util/Sidekick_util.ml | 7 +++++++ 3 files changed, 31 insertions(+), 24 deletions(-) create mode 100644 src/util/Int_id.ml diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index c121a1ad..c8c0cf04 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -13,24 +13,6 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T let invalid_argf fmt = Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt -module type INT_ID = sig - type t = private int - val equal : t -> t -> bool - val compare : t -> t -> int - val hash : t -> int - val to_int : t -> int - val of_int_unsafe : int -> t -end - -module Mk_int_id() = struct - type t = int - let equal : t -> t -> bool = (=) - let compare : t -> t -> int = compare - let hash = CCHash.int - let[@inline] to_int i = i - external of_int_unsafe : int -> t = "%identity" -end - module Make(Plugin : PLUGIN) = struct type lit = Plugin.lit @@ -45,17 +27,17 @@ module Make(Plugin : PLUGIN) (* a boolean variable (positive int) *) module Var0 : sig - include INT_ID + include Int_id.S module Set : Set.S with type elt = t end = struct - include Mk_int_id() + include Int_id.Make() module Set = Util.Int_set end type var = Var0.t (* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *) module Atom0 : sig - include INT_ID + include Int_id.S val neg : t -> t val sign : t -> bool @@ -66,7 +48,7 @@ module Make(Plugin : PLUGIN) val na : var -> t module Set : CCSet.S with type elt = t end = struct - include Mk_int_id() + include Int_id.Make() let[@inline] neg i = (i lxor 1) let[@inline] sign i = (i land 1) = 0 @@ -80,11 +62,11 @@ module Make(Plugin : PLUGIN) type atom = Atom0.t module Clause0 : sig - include INT_ID + include Int_id.S module Tbl : Hashtbl.S with type key = t module CVec : Vec_sig.S with type elt := t end = struct - include Mk_int_id() + include Int_id.Make() module Tbl = Util.Int_tbl module CVec = VecI32 end diff --git a/src/util/Int_id.ml b/src/util/Int_id.ml new file mode 100644 index 00000000..eadc78f4 --- /dev/null +++ b/src/util/Int_id.ml @@ -0,0 +1,18 @@ + +module type S = sig + type t = private int + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + val to_int : t -> int + val of_int_unsafe : int -> t +end + +module Make() = struct + type t = int + let equal : t -> t -> bool = (=) + let compare : t -> t -> int = compare + let hash = CCHash.int + let[@inline] to_int i = i + external of_int_unsafe : int -> t = "%identity" +end diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 33f20506..52121c62 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -8,6 +8,13 @@ module VecI32 = VecI32 module Vec_float = Vec_float module Vec_sig = Vec_sig module Bitvec = Bitvec +module Int_id = Int_id + +(* TODO: a specialized representation *) +module Int_tbl = Util.Int_tbl + +module Int_set = Util.Int_set +module Int_map = Util.Int_map module IArray = IArray module Backtrack_stack = Backtrack_stack