simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 04:35:35 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

perf: remove bitfield, implement it manually

Browse source
This commit is contained in:
Simon Cruanes 2019-01-18 20:19:23 -06:00 • committed by Guillaume Bury
parent 8b4458b066
commit 7e9fd1a363
5 changed files with 16 additions and 225 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

135
src/core/BitField.ml
View file

@ -1,135 +0,0 @@
(* This file is free software, part of containers. See file "license" for more details. *)
(** {1 Bit Field} *)
exception TooManyFields
exception Frozen
let max_width = Sys.word_size - 2
(*$R
let module B = CCBitField.Make(struct end) in
let x = B.mk_field () in
let y = B.mk_field () in
let z = B.mk_field () in
let f = B.empty |> B.set x true |> B.set y true in
assert_bool "z_false" (not (B.get z f)) ;
assert_bool "z_true" (f |> B.set z true |> B.get z);
*)
(*$R
let module B = CCBitField.Make(struct end) in
let _ = B.mk_field () in
B.freeze();
assert_bool "must raise"
(try ignore (B.mk_field()); false with Frozen -> true);
*)
(*$R
let module B = CCBitField.Make(struct end) in
let x = B.mk_field () in
let y = B.mk_field () in
let z = B.mk_field () in
let u = B.mk_field () in
B.freeze();
let f = B.empty
|> B.set y true
|> B.set z true
in
assert_equal ~printer:CCInt.to_string 6 (f :> int) ;
assert_equal false (B.get x f) ;
assert_equal true (B.get y f) ;
assert_equal true (B.get z f);
let f' = B.set u true f in
assert_equal false (B.get x f') ;
assert_equal true (B.get y f') ;
assert_equal true (B.get z f');
assert_equal true (B.get u f');
()
*)
module type S = sig
type t = private int
(** Generative type of bitfields. Each instantiation of the functor
should create a new, incompatible type *)
val empty : t
(** Empty bitfields (all bits 0) *)
type field
val get : field -> t -> bool
(** Get the value of this field *)
val set : field -> bool -> t -> t
(** Set the value of this field *)
val mk_field : unit -> field
(** Make a new field *)
val freeze : unit -> unit
(** Prevent new fields from being added. From now on, creating
a field will raise Frozen *)
val total_width : unit -> int
(** Current width of the bitfield *)
end
(* all bits from 0 to w-1 set to true *)
let rec all_bits_ acc w =
if w=0 then acc
else
let acc = acc lor (1 lsl w-1) in
all_bits_ acc (w-1)
(*$T
all_bits_ 0 1 = 1
all_bits_ 0 2 = 3
all_bits_ 0 3 = 7
all_bits_ 0 4 = 15
*)
(* increment and return previous value *)
let get_then_incr n =
let x = !n in
incr n;
x
module Make() : S = struct
type t = int
let empty = 0
let width_ = ref 0
let frozen_ = ref false
type field = int (* a mask *)
let[@inline] get field x = (x land field) <> 0
let[@inline] set field b x =
if b then x lor field else x land (lnot field)
let mk_field () =
if !frozen_ then raise Frozen;
let n = get_then_incr width_ in
if n > max_width then raise TooManyFields;
let mask = 1 lsl n in
mask
let freeze () = frozen_ := true
let total_width () = !width_
end

69
src/core/BitField.mli
View file

@ -1,69 +0,0 @@
(* This file is free software, part of containers. See file "license" for more details. *)
(** {1 Bit Field}
This module defines efficient bitfields
up to 30 or 62 bits (depending on the architecture) in
a relatively type-safe way.
{[
module B = CCBitField.Make(struct end);;
#install_printer B.pp;;
let x = B.mk_field ()
let y = B.mk_field ()
let z = B.mk_field ()
let f = B.empty |> B.set x true |> B.set y true;;
assert (not (B.get z f)) ;;
assert (f |> B.set z true |> B.get z);;
]}
*)
exception TooManyFields
(** Raised when too many fields are packed into one bitfield *)
exception Frozen
(** Raised when a frozen bitfield is modified *)
val max_width : int
(** System-dependent maximum width for a bitfield, typically 30 or 62 *)
(** {2 Bitfield Signature} *)
module type S = sig
type t = private int
(** Generative type of bitfields. Each instantiation of the functor
should create a new, incompatible type *)
val empty : t
(** Empty bitfields (all bits 0) *)
type field
val get : field -> t -> bool
(** Get the value of this field *)
val set : field -> bool -> t -> t
(** Set the value of this field *)
val mk_field : unit -> field
(** Make a new field *)
val freeze : unit -> unit
(** Prevent new fields from being added. From now on, creating
a field will raise Frozen *)
val total_width : unit -> int
(** Current width of the bitfield *)
end
(** Create a new bitfield type *)
module Make() : S
(**/**)
val all_bits_ : int -> int -> int
(**/**)

31
src/core/Solver_types.ml
View file

@ -6,12 +6,6 @@ Copyright 2016 Simon Cruanes
module type S = Solver_types_intf.S
module Var_fields = Solver_types_intf.Var_fields
let v_field_seen_neg = Var_fields.mk_field()
let v_field_seen_pos = Var_fields.mk_field()
let () = Var_fields.freeze()
(* Solver types for McSat Solving *)
(* ************************************************************************ *)
@ -43,7 +37,7 @@ module McMake (E : Expr_intf.S) = struct
vid : int;
pa : atom;
na : atom;
mutable v_fields : Var_fields.t;
mutable v_fields : int;
mutable v_level : int;
mutable v_idx: int; (** position in heap *)
mutable v_weight : float; (** Weight (for the heap), tracking activity *)
@ -165,6 +159,9 @@ module McMake (E : Expr_intf.S) = struct
(v.lid+1) debug_assign v E.Term.print v.term
end
let seen_pos = 0b1
let seen_neg = 0b10
module Var = struct
type t = var
let[@inline] level v = v.v_level
@ -184,7 +181,7 @@ module McMake (E : Expr_intf.S) = struct
{ vid = st.cpt_mk_var;
pa = pa;
na = na;
v_fields = Var_fields.empty;
v_fields = 0;
v_level = -1;
v_idx= -1;
v_weight = 0.;
@ -212,11 +209,11 @@ module McMake (E : Expr_intf.S) = struct
(* Marking helpers *)
let[@inline] clear v =
v.v_fields <- Var_fields.empty
v.v_fields <- 0
let[@inline] seen_both v =
Var_fields.get v_field_seen_pos v.v_fields &&
Var_fields.get v_field_seen_neg v.v_fields
(seen_pos land v.v_fields <> 0) &&
(seen_neg land v.v_fields <> 0)
end
module Atom = struct
@ -237,14 +234,16 @@ module McMake (E : Expr_intf.S) = struct
let[@inline] seen a =
let pos = equal a (abs a) in
if pos
then Var_fields.get v_field_seen_pos a.var.v_fields
else Var_fields.get v_field_seen_neg a.var.v_fields
then (seen_pos land a.var.v_fields <> 0)
else (seen_neg land a.var.v_fields <> 0)
let[@inline] mark a =
let pos = equal a (abs a) in
if pos
then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields
else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields
if pos then (
a.var.v_fields <- seen_pos lor a.var.v_fields
) else (
a.var.v_fields <- seen_neg lor a.var.v_fields
)
let[@inline] make st lit =
let var, negated = Var.make st lit in

2
src/core/Solver_types.mli
View file

@ -16,8 +16,6 @@ Copyright 2016 Simon Cruanes
module type S = Solver_types_intf.S
(** Interface for the internal types. *)
module Var_fields = Solver_types_intf.Var_fields
module McMake (E : Expr_intf.S):
S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
(** Functor to instantiate the types of clauses for a solver. *)

4
src/core/Solver_types_intf.ml
View file

@ -10,8 +10,6 @@ Copyright 2016 Simon Cruanes
used in the core solver.
*)
module Var_fields = BitField.Make()
type 'a printer = Format.formatter -> 'a -> unit
module type S = sig
@ -56,7 +54,7 @@ module type S = sig
vid : int; (** Unique identifier *)
pa : atom; (** Link for the positive atom *)
na : atom; (** Link for the negative atom *)
mutable v_fields : Var_fields.t; (** bool fields *)
mutable v_fields : int; (** bool fields *)
mutable v_level : int; (** Level of decision/propagation *)
mutable v_idx: int; (** rank in variable heap *)
mutable v_weight : float; (** Variable weight (for the heap) *)