feat: move Int_id into its own module

This commit is contained in:
Simon Cruanes 2021-08-25 09:36:24 -04:00
parent 68250603c4
commit 782afa4415
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
3 changed files with 31 additions and 24 deletions

View file

@ -13,24 +13,6 @@ module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
let invalid_argf fmt = let invalid_argf fmt =
Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) 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) module Make(Plugin : PLUGIN)
= struct = struct
type lit = Plugin.lit type lit = Plugin.lit
@ -45,17 +27,17 @@ module Make(Plugin : PLUGIN)
(* a boolean variable (positive int) *) (* a boolean variable (positive int) *)
module Var0 : sig module Var0 : sig
include INT_ID include Int_id.S
module Set : Set.S with type elt = t module Set : Set.S with type elt = t
end = struct end = struct
include Mk_int_id() include Int_id.Make()
module Set = Util.Int_set module Set = Util.Int_set
end end
type var = Var0.t type var = Var0.t
(* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *) (* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
module Atom0 : sig module Atom0 : sig
include INT_ID include Int_id.S
val neg : t -> t val neg : t -> t
val sign : t -> bool val sign : t -> bool
@ -66,7 +48,7 @@ module Make(Plugin : PLUGIN)
val na : var -> t val na : var -> t
module Set : CCSet.S with type elt = t module Set : CCSet.S with type elt = t
end = struct end = struct
include Mk_int_id() include Int_id.Make()
let[@inline] neg i = (i lxor 1) let[@inline] neg i = (i lxor 1)
let[@inline] sign i = (i land 1) = 0 let[@inline] sign i = (i land 1) = 0
@ -80,11 +62,11 @@ module Make(Plugin : PLUGIN)
type atom = Atom0.t type atom = Atom0.t
module Clause0 : sig module Clause0 : sig
include INT_ID include Int_id.S
module Tbl : Hashtbl.S with type key = t module Tbl : Hashtbl.S with type key = t
module CVec : Vec_sig.S with type elt := t module CVec : Vec_sig.S with type elt := t
end = struct end = struct
include Mk_int_id() include Int_id.Make()
module Tbl = Util.Int_tbl module Tbl = Util.Int_tbl
module CVec = VecI32 module CVec = VecI32
end end

18
src/util/Int_id.ml Normal file
View file

@ -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

View file

@ -8,6 +8,13 @@ module VecI32 = VecI32
module Vec_float = Vec_float module Vec_float = Vec_float
module Vec_sig = Vec_sig module Vec_sig = Vec_sig
module Bitvec = Bitvec 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 IArray = IArray
module Backtrack_stack = Backtrack_stack module Backtrack_stack = Backtrack_stack