From 7e9fd1a363d20d03281e8ead7a43c475601da764 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 20:19:23 -0600 Subject: [PATCH] perf: remove bitfield, implement it manually --- src/core/BitField.ml | 135 ---------------------------------- src/core/BitField.mli | 69 ----------------- src/core/Solver_types.ml | 31 ++++---- src/core/Solver_types.mli | 2 - src/core/Solver_types_intf.ml | 4 +- 5 files changed, 16 insertions(+), 225 deletions(-) delete mode 100644 src/core/BitField.ml delete mode 100644 src/core/BitField.mli diff --git a/src/core/BitField.ml b/src/core/BitField.ml deleted file mode 100644 index 697320a8..00000000 --- a/src/core/BitField.ml +++ /dev/null @@ -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 diff --git a/src/core/BitField.mli b/src/core/BitField.mli deleted file mode 100644 index ac92ffd8..00000000 --- a/src/core/BitField.mli +++ /dev/null @@ -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 -(**/**) diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index 9f3a4f2d..dc73d889 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -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 diff --git a/src/core/Solver_types.mli b/src/core/Solver_types.mli index 62219a3a..fb1e03c3 100644 --- a/src/core/Solver_types.mli +++ b/src/core/Solver_types.mli @@ -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. *) diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml index 61d1727a..c5d0ff37 100644 --- a/src/core/Solver_types_intf.ml +++ b/src/core/Solver_types_intf.ml @@ -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) *)