From 9975a471f73eee7c035088619b27f51f9442922c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 11 Aug 2021 09:30:53 -0400 Subject: [PATCH] perf(drup): restore Atoms as integers --- src/checker/drup_check.ml | 51 +---------------- src/checker/main.ml | 2 +- src/drup/sidekick_drup.ml | 112 +++++++++++++++++++++----------------- 3 files changed, 65 insertions(+), 100 deletions(-) diff --git a/src/checker/drup_check.ml b/src/checker/drup_check.ml index efe2b677..dde952d8 100644 --- a/src/checker/drup_check.ml +++ b/src/checker/drup_check.ml @@ -1,54 +1,5 @@ -module SDrup = Sidekick_drup - -module Atom : sig - include SDrup.ATOM with type t = private int - - val of_int : int -> t -end = struct - type t = int - type atom = t - let hash = CCHash.int - let equal : t -> t -> bool = (=) - let compare : t -> t -> int = compare - let[@inline] neg x = x lxor 1 - let[@inline] of_int x = - let v = abs x lsl 1 in - if x < 0 then neg v else v - let[@inline] sign x = (x land 1) = 0 - let[@inline] to_int x = (if sign x then 1 else -1) * (x lsr 1) - let pp out x = - Fmt.fprintf out "%s%d" (if sign x then "+" else "-") (x lsr 1) - let[@inline] of_int_unsafe i = i - let dummy = 0 - module Assign = struct - type t = Bitvec.t - let create = Bitvec.create - let ensure_size = Bitvec.ensure_size - let is_true = Bitvec.get - let[@inline] is_false self (a:atom) : bool = - is_true self (neg a) - let[@inline] is_unassigned self a = - not (is_true self a) && not (is_false self a) - let set = Bitvec.set - end - module Map = struct - type 'a t = 'a Vec.t - let create () = Vec.create () - let[@inline] ensure_has (self:_ t) a mk : unit = - (* size: 2+atom, because: 1+atom makes atom valid, and if it's positive, - 2+atom is (¬atom)+1 *) - Vec.ensure_size_with self mk (2+(a:atom:>int)) - let get = Vec.get - let set = Vec.set - end - module Stack = struct - include VecI32 - let create()=create() - end -end - -include SDrup.Make(Atom) +include Sidekick_drup.Make() (** A DRUP trace, as a series of operations *) module Trace : sig diff --git a/src/checker/main.ml b/src/checker/main.ml index 8e8b0f81..ff3d5020 100644 --- a/src/checker/main.ml +++ b/src/checker/main.ml @@ -3,7 +3,7 @@ module BL = Sidekick_bin_lib let clause_of_int_l store atoms : Drup_check.clause = atoms - |> CCList.map Drup_check.Atom.of_int + |> CCList.map Drup_check.Atom.of_int_dimacs |> Drup_check.Clause.of_list store let check ?pb proof : bool = diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml index 932f4ea2..07f8eafc 100644 --- a/src/drup/sidekick_drup.ml +++ b/src/drup/sidekick_drup.ml @@ -8,57 +8,30 @@ module Fmt = CCFormat module VecI32 = VecI32 -(** Signature for boolean atoms *) -module type ATOM = sig - type t - val equal : t -> t -> bool - val compare : t -> t -> int - val hash : t -> int - val neg : t -> t - val sign : t -> bool - val pp : t Fmt.printer - - val dummy : t - - type atom = t - - module Assign : sig - type t - val create : unit -> t - - val ensure_size : t -> atom -> unit - val set : t -> atom -> bool -> unit - val is_true : t -> atom -> bool - val is_false : t -> atom -> bool - val is_unassigned : t -> atom -> bool - end - - module Map : sig - type 'a t - val create : unit -> 'a t - val ensure_has : 'a t -> atom -> (unit -> 'a) -> unit - val get : 'a t -> atom -> 'a - end - - module Stack : sig - type t - val create : unit -> t - val get : t -> int -> atom - val set : t -> int -> atom -> unit - val push : t -> atom -> unit - val size : t -> int - val shrink : t -> int -> unit - val to_iter : t -> atom Iter.t - end -end - (* TODO: resolution proof construction, optionally *) (* TODO: backward checking + pruning of traces *) (** An instance of the checker *) module type S = sig - type atom + module Atom : sig + type t = private int + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + val neg : t -> t + val sign : t -> bool + val pp : t Fmt.printer + + type atom = t + + val of_int_dimacs : int -> t + (** Turn a signed integer into an atom. Positive integers are + positive atoms, and [-i] is [neg (of_int i)]. + @raise Invalid_argument if the argument is 0 *) + end + type atom = Atom.t + module Clause : sig @@ -92,10 +65,51 @@ module type S = sig end end -module[@inline] Make(A : ATOM) - : S with type atom = A.t -= struct - module Atom = A +module Make() : S = struct + (** Boolean atoms *) + module Atom = struct + type t = int + type atom = t + let hash = CCHash.int + let equal : t -> t -> bool = (=) + let compare : t -> t -> int = compare + let[@inline] neg x = x lxor 1 + let[@inline] of_int_dimacs x = + if x=0 then invalid_arg "Atom.of_int_dimacs: 0 is not acceptable"; + let v = abs x lsl 1 in + if x < 0 then neg v else v + let[@inline] sign x = (x land 1) = 0 + let[@inline] to_int x = (if sign x then 1 else -1) * (x lsr 1) + let pp out x = + Fmt.fprintf out "%s%d" (if sign x then "+" else "-") (x lsr 1) + let[@inline] of_int_unsafe i = i + let dummy = 0 + module Assign = struct + type t = Bitvec.t + let create = Bitvec.create + let ensure_size = Bitvec.ensure_size + let is_true = Bitvec.get + let[@inline] is_false self (a:atom) : bool = + is_true self (neg a) + let[@inline] is_unassigned self a = + not (is_true self a) && not (is_false self a) + let set = Bitvec.set + end + module Map = struct + type 'a t = 'a Vec.t + let create () = Vec.create () + let[@inline] ensure_has (self:_ t) a mk : unit = + (* size: 2+atom, because: 1+atom makes atom valid, and if it's positive, + 2+atom is (¬atom)+1 *) + Vec.ensure_size_with self mk (2+(a:atom:>int)) + let get = Vec.get + let set = Vec.set + end + module Stack = struct + include VecI32 + let create()=create() + end + end type atom = Atom.t (** Boolean clauses *)