feat(drup): first version of checker

src/checker/dune

@@ -4,5 +4,5 @@
   (public_name sidekick-checker)
   (package sidekick-bin)
   (libraries containers sidekick-bin.lib
-             sidekick.util sidekick.drup)
+             sidekick.util sidekick.tef sidekick.drup)
   (flags :standard -warn-error -a+8 -open Sidekick_util))

src/checker/main.ml

@@ -2,24 +2,27 @@
 module BL = Sidekick_bin_lib
 module SDrup = Sidekick_drup
 
-let clause_of_int_l atoms : SDrup.clause =
+let clause_of_int_l store atoms : SDrup.clause =
-  Array.of_list atoms
+  atoms
-  |> Array.map SDrup.Atom.of_int
+  |> CCList.map SDrup.Atom.of_int
-  |> SDrup.Clause.of_array
+  |> SDrup.Clause.of_list store
 
 let check ?pb proof : bool =
-  let trace = SDrup.Trace.create() in
+  Profile.with_ "check" @@ fun() ->
+  let cstore = SDrup.Clause.create() in
+  let trace = SDrup.Trace.create cstore in
 
   (* add problem to trace, if provided *)
   begin match pb with
     | None -> ()
     | Some f when Filename.extension f = ".cnf" ->
+      Profile.with_ "parse-pb.cnf" @@ fun() ->
       CCIO.with_in f
         (fun ic ->
            let parser_ = BL.Dimacs_parser.create ic in
            BL.Dimacs_parser.iter parser_
              (fun atoms ->
-                let c = clause_of_int_l atoms in
+                let c = clause_of_int_l cstore atoms in
                 SDrup.Trace.add_input_clause trace c))
     | Some f ->
       (* TODO: handle .cnf.gz *)
@@ -29,16 +32,17 @@ let check ?pb proof : bool =
   (* add proof to trace *)
   begin match proof with
     | f when Filename.extension f = ".drup" ->
+      Profile.with_ "parse-proof.drup" @@ fun() ->
       CCIO.with_in f
         (fun ic ->
            let p = BL.Drup_parser.create ic in
            BL.Drup_parser.iter p
              (function
                | BL.Drup_parser.Add c ->
-                 let c = clause_of_int_l c in
+                 let c = clause_of_int_l cstore c in
                  SDrup.Trace.add_clause trace c
                | BL.Drup_parser.Delete c ->
-                 let c = clause_of_int_l c in
+                 let c = clause_of_int_l cstore c in
                  SDrup.Trace.del_clause trace c))
     | f ->
       (* TODO: handle .drup.gz *)
@@ -49,13 +53,8 @@ let check ?pb proof : bool =
   Log.debugf 1 (fun k->k"checking proof (%d steps)" (SDrup.Trace.size trace));
   begin match SDrup.Fwd_check.check trace with
     | Ok () -> true
-    | Error bad ->
+    | Error err ->
-      assert (VecI32.size bad > 0);
+      Format.eprintf "%a@." (SDrup.Fwd_check.pp_error trace) err;
-      let n0 = VecI32.get bad 0 in
-      Format.eprintf
-        "checking failed on %d events.@.@[<2>First failure is event[%d]:@ %a@]@."
-        (VecI32.size bad) n0
-        SDrup.Trace.pp_event (SDrup.Trace.get trace n0);
       false
   end
 
@@ -65,6 +64,7 @@ let () =
     "-d", Arg.Int Log.set_debug, " set debug level";
   ] |> Arg.align in
   Printexc.record_backtrace true;
+  Sidekick_tef.setup();
 
   Arg.parse opts (fun f -> files := f :: !files) "checker [opt]* [file]+";
 

src/drup/sidekick_drup.ml

@@ -33,70 +33,117 @@ end = struct
 end
 type atom = Atom.t
 
+(** Boolean clauses *)
 module Clause : sig
+  type store
+  val create : unit -> store
   type t
   val size : t -> int
   val get : t -> int -> atom
   val iter : f:(atom -> unit) -> t -> unit
+  val watches: t -> (atom * atom) option
+  val set_watches : t -> atom * atom -> unit
   val pp : t Fmt.printer
-  val of_array : atom array -> t
+  val of_list : store -> atom list -> t
+  module Set : CCSet.S with type elt = t
+  module Tbl : CCHashtbl.S with type key = t
 end = struct
-  type t = atom array
+  module I_arr_tbl = CCHashtbl.Make(struct
-  let size = Array.length
+      type t = atom array
-  let get = Array.get
+      let equal = CCEqual.(array Atom.equal)
-  let iter ~f c = Array.iter f c
+      let hash = CCHash.(array Atom.hash)
-  let pp out (self:t) = Fmt.Dump.array Atom.pp out self
+    end)
-  let of_array a = a
+  type t = {
+    id: int;
+    atoms: atom array;
+    mutable watches: (atom * atom) option;
+  }
+  type store = {
+    mutable n: int;
+  }
+  let create(): store =
+    { n=0; }
+  let size self = Array.length self.atoms
+  let get self i = Array.get self.atoms i
+  let watches self = self.watches
+  let set_watches self w = self.watches <- Some w
+  let iter ~f self = Array.iter f self.atoms
+  let pp out (self:t) =
+    let pp_watches out = function
+      | None -> ()
+      | Some (p,q) -> Fmt.fprintf out "@ :watches (%a,%a)" Atom.pp p Atom.pp q in
+    Fmt.fprintf out "(@[cl[%d]@ %a%a])"
+      self.id (Fmt.Dump.array Atom.pp) self.atoms pp_watches self.watches
+  let of_list self atoms : t =
+    (* normalize + find in table *)
+    let atoms = List.sort_uniq Atom.compare atoms |> Array.of_list in
+    let id = self.n in
+    self.n <- 1 + self.n;
+    let c = {atoms; id; watches=None} in
+    c
+  module As_key = struct
+    type nonrec t=t
+    let hash a = CCHash.int a.id
+    let equal a b = a.id = b.id
+    let compare a b = compare a.id b.id
+  end
+  module Set = CCSet.Make(As_key)
+  module Tbl = CCHashtbl.Make(As_key)
 end
 type clause = Clause.t
 
+(** A DRUP trace, as a series of operations *)
 module Trace : sig
   type t
 
-  val create : unit -> t
+  val create : Clause.store -> t
+  val cstore : t -> Clause.store
 
   val add_clause : t -> clause -> unit
   val add_input_clause : t -> clause -> unit
   val del_clause : t -> clause -> unit
 
-  type event =
+  (** Operator on the set of clauses *)
+  type op =
     | Input of clause
     | Redundant of clause
     | Delete of clause
 
-  val iteri : t -> f:(int -> event -> unit) -> unit
+  val iteri : t -> f:(int -> op -> unit) -> unit
-  val events : t -> event Iter.t
+  val ops : t -> op Iter.t
   val size : t -> int
-  val get : t -> int -> event
+  val get : t -> int -> op
 
-  val pp_event : event Fmt.printer
+  val pp_op : op Fmt.printer
 
   val dump : out_channel -> t -> unit
 end = struct
-  type event =
+  type op =
     | Input of clause
     | Redundant of clause
     | Delete of clause
 
   type t = {
-    evs: event Vec.t;
+    cstore: Clause.store;
+    ops: op Vec.t;
   }
 
-  let create() : t =
+  let create cstore : t =
-    { evs=Vec.create() }
+    { cstore; ops=Vec.create() }
 
-  let add_clause self c = Vec.push self.evs (Redundant c)
+  let cstore self = self.cstore
-  let add_input_clause self c = Vec.push self.evs (Input c)
+  let add_clause self c = Vec.push self.ops (Redundant c)
-  let del_clause self c = Vec.push self.evs (Delete c)
+  let add_input_clause self c = Vec.push self.ops (Input c)
-  let get self i = Vec.get self.evs i
+  let del_clause self c = Vec.push self.ops (Delete c)
-  let size self = Vec.size self.evs
+  let get self i = Vec.get self.ops i
-  let events self = Vec.to_seq self.evs
+  let size self = Vec.size self.ops
-  let iteri self ~f = Vec.iteri f self.evs
+  let ops self = Vec.to_seq self.ops
+  let iteri self ~f = Vec.iteri f self.ops
 
-  let pp_event out = function
+  let pp_op out = function
     | Input c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c
     | Redundant c -> Fmt.fprintf out "(@[Redundant %a@])" Clause.pp c
-    | Delete c -> Fmt.fprintf out "(@[Del %a@])" Clause.pp c
+    | Delete c -> Fmt.fprintf out "(@[Delete %a@])" Clause.pp c
 
   let dump oc self : unit =
     let fpf = Printf.fprintf in
@@ -107,60 +154,55 @@ end = struct
         | Redundant c -> fpf oc "%a0\n" pp_c c;
         | Delete c -> fpf oc "d %a0\n" pp_c c;
       )
-      self.evs
+      self.ops
 end
 
-(*
-module Checker : sig
-  type t
-
-  val create : unit -> t
-
-  val add_clause : t -> clause -> unit
-  val remove_clause : t -> clause -> unit
-end = struct
-  type t = {
-    clauses: unit Clause.Tbl.t;
-  }
-   *)
-
 (** Forward checking.
 
     Each event is checked by reverse-unit propagation on previous events. *)
 module Fwd_check : sig
+
+  type error =
+    [ `Bad_steps of VecI32.t
+    | `No_empty_clause
+    ]
+
+  val pp_error : Trace.t -> error Fmt.printer
+
   (** [check tr] checks the trace and returns [Ok ()] in case of
       success. In case of error it returns [Error idxs] where [idxs] are the
       indexes in the trace of the steps that failed. *)
-  val check : Trace.t -> (unit, VecI32.t) result
+  val check : Trace.t -> (unit, error) result
 
 end = struct
   module ISet = CCSet.Make(CCInt)
 
   type t = {
+    cstore: Clause.store;
     assign: Bitvec.t; (* atom -> is_true(atom) *)
     trail: VecI32.t; (* current assignment *)
-    mutable trail_ptr : int; (* offset in trail *)
+    mutable trail_ptr : int; (* offset in trail for propagation *)
-    cs: clause Vec.t; (* index -> clause *)
+    active_clauses: unit Clause.Tbl.t;
-    cs_recycle: int Vec.t; (* free elements in [cs] *)
+    watches: Clause.Set.t Vec.t; (* atom -> clauses it watches *)
-    watches: ISet.t Vec.t; (* atom -> clauses it watches *)
     errors: VecI32.t;
   }
 
-  let create() : t =
+  let create cstore : t =
     { trail=VecI32.create();
       trail_ptr = 0;
+      cstore;
+      active_clauses=Clause.Tbl.create 32;
       assign=Bitvec.create();
-      cs=Vec.create();
-      cs_recycle=Vec.create();
       watches=Vec.create();
       errors=VecI32.create();
     }
 
+  (* ensure data structures are big enough to handle [a] *)
   let ensure_atom_ self (a:atom) =
     Bitvec.ensure_size self.assign (a:atom:>int);
     (* size: 2+atom, because: 1+atom makes atom valid, and if it's positive,
        2+atom is (¬atom)+1 *)
-    Vec.ensure_size self.watches ISet.empty (2+(a:atom:>int));
+    Vec.ensure_size self.watches Clause.Set.empty (2+(a:atom:>int));
     ()
 
   let[@inline] is_true self (a:atom) : bool =
@@ -169,13 +211,16 @@ end = struct
   let[@inline] is_false self (a:atom) : bool =
     is_true self (Atom.neg a)
 
-  let add_watch_ self (a:atom) cid =
+  let is_unassigned self a =
-    let set = Vec.get self.watches (a:atom:>int) in
+    not (is_true self a) && not (is_false self a)
-    Vec.set self.watches (a:atom:>int) (ISet.add cid set)
 
-  let remove_watch_ self (a:atom) cid =
+  let add_watch_ self (a:atom) (c:clause) =
     let set = Vec.get self.watches (a:atom:>int) in
-    Vec.set self.watches (a:atom:>int) (ISet.remove cid set)
+    Vec.set self.watches (a:atom:>int) (Clause.Set.add c set)
+
+  let remove_watch_ self (a:atom) (c:clause) =
+    let set = Vec.get self.watches (a:atom:>int) in
+    Vec.set self.watches (a:atom:>int) (Clause.Set.remove c set)
 
   exception Conflict
 
@@ -192,18 +237,86 @@ end = struct
       VecI32.push self.trail (a:atom:>int)
     )
 
-  (* TODO *)
+  (* print the trail *)
-  let propagate_in_clause_ (self:t) (cid:int) : unit =
+  let pp_trail_ out self =
-    ()
+    let pp_a out i = Atom.pp out (Atom.of_int_unsafe i) in
+    Fmt.fprintf out "(@[%a@])" (Fmt.iter pp_a) (VecI32.to_iter self.trail)
+
+  exception Found_watch of atom
+  exception Is_sat
+  exception Is_undecided
+
+  (* check if [c] is false in current trail *)
+  let c_is_false_ self c =
+    try Clause.iter c ~f:(fun a -> if not (is_false self a) then raise Exit); true
+    with Exit -> false
+
+  (* do boolean propagation in [c], which is watched by the true literal [a] *)
+  let propagate_in_clause_ (self:t) (a:atom) (c:clause) : unit =
+    assert (is_true self a);
+    let a1, a2 =
+      match Clause.watches c with
+      | None -> assert false
+      | Some tup -> tup
+    in
+    let na = Atom.neg a in
+    (* [q] is the other literal in [c] such that [¬q] watches [c]. *)
+    let q = if Atom.equal a1 na then a2 else (assert(a2==na); a1) in
+    try
+      if is_true self q then () (* clause is satisfied *)
+      else (
+        let n_unassigned = ref 0 in
+        let unassigned_a = ref a in (* an unassigned atom, if [!n_unassigned > 0] *)
+        if not (is_false self q) then unassigned_a := q;
+        begin
+          try
+            Clause.iter c
+              ~f:(fun ai ->
+                  if is_true self ai then raise Is_sat (* no watch update *)
+                  else if is_unassigned self ai then (
+                    incr n_unassigned;
+                    if q <> ai then unassigned_a := ai;
+                    if !n_unassigned >= 2 then raise Is_undecided; (* early exit *)
+                  );
+                )
+          with Is_undecided -> ()
+        end;
+
+        if !n_unassigned = 0 then (
+          (* if we reach this point it means no literal is true, and none is
+             unassigned. So they're all false and we have a conflict. *)
+          assert (is_false self q);
+          raise_conflict_ self a;
+        ) else if !n_unassigned = 1 then (
+          (* no lit is true, only one is unassigned: propagate it.
+             no need to update the watches as the clause is satisfied. *)
+          assert (is_unassigned self !unassigned_a);
+          let p = !unassigned_a in
+          Log.debugf 30 (fun k->k"(@[propagate@ :atom %a@ :reason %a@])" Atom.pp p Clause.pp c);
+          set_atom_true self p;
+        ) else (
+          (* at least 2 unassigned, just update the watch literal to [¬p] *)
+          let p = !unassigned_a in
+          assert (p <> q);
+          Clause.set_watches c (q, p);
+          remove_watch_ self a c;
+          add_watch_ self (Atom.neg p) c;
+        );
+      )
+    with
+    | Is_sat -> ()
 
   let propagate_atom_ self (a:atom) : unit =
     let set = Vec.get self.watches (a:atom:>int) in
-    ISet.iter (propagate_in_clause_ self) set
+    Clause.Set.iter (propagate_in_clause_ self a) set
 
-  (* @raise Conflict if a clause is false *)
+  (* perform boolean propagation in a fixpoint
-  let propagate_ (self:t) : unit =
+     @raise Conflict if a clause is false *)
+  let bcp_fixpoint_ (self:t) : unit =
+    Profile.with_ "bcp-fixpoint" @@ fun() ->
     while self.trail_ptr < VecI32.size self.trail do
       let a = Atom.of_int_unsafe (VecI32.get self.trail self.trail_ptr) in
+      Log.debugf 50 (fun k->k"(@[bcp@ :atom %a@])" Atom.pp a);
       self.trail_ptr <- 1 + self.trail_ptr;
       propagate_atom_ self a;
     done
@@ -211,7 +324,7 @@ end = struct
   (* calls [f] and then restore trail to what it was *)
   let with_restore_trail_ self f =
     let trail_size0 = VecI32.size self.trail in
-    let ptr = self.trail_ptr in
+    let ptr0 = self.trail_ptr in
 
     let restore () =
       (* unassign new literals *)
@@ -223,44 +336,45 @@ end = struct
 
       (* remove literals from trail *)
       VecI32.shrink self.trail trail_size0;
-      self.trail_ptr <- ptr
+      self.trail_ptr <- ptr0
     in
 
     CCFun.finally ~h:restore ~f
 
   (* check event, return [true] if it's valid *)
-  let check_ev (self:t) i (ev:Trace.event) : bool =
+  let check_op (self:t) i (op:Trace.op) : bool =
-    Log.debugf 20 (fun k->k"(@[check-ev[%d]@ %a@])" i Trace.pp_event ev);
+    Profile.with_ "check-op" @@ fun() ->
+    Log.debugf 20 (fun k->k"(@[check-op :idx %d@ :op %a@])" i Trace.pp_op op);
 
     (* add clause to the state *)
     let add_c_ (c:Clause.t) =
+      Log.debugf 50 (fun k->k"(@[add-clause@ %a@])" Clause.pp c);
       Clause.iter c ~f:(ensure_atom_ self);
-
+      Clause.Tbl.add self.active_clauses c ();
-      (* allocate clause *)
-      let cid =
-        match Vec.pop_exn self.cs_recycle with
-        | cid ->
-          Vec.set self.cs cid c;
-          cid
-        | exception _ ->
-          let cid = Vec.size self.cs in
-          Vec.push self.cs c;
-          cid
-      in
 
       begin match Clause.size c with
         | 0 -> ()
         | 1 ->
           set_atom_true self (Clause.get c 0);
         | _ ->
-          add_watch_ self (Atom.neg (Clause.get c 0)) cid;
+          let c0 = Clause.get c 0 in
-          add_watch_ self (Atom.neg (Clause.get c 1)) cid;
+          let c1 = Clause.get c 1 in
+          assert (c0 <> c1);
+          add_watch_ self (Atom.neg c0) c;
+          add_watch_ self (Atom.neg c1) c;
+          Clause.set_watches c (c0,c1);
+          (* make sure watches are valid *)
+          if is_false self c0 then (
+            propagate_in_clause_ self (Atom.neg c0) c;
+          );
+          if is_false self c1 then (
+            propagate_in_clause_ self (Atom.neg c1) c;
+          )
       end;
-      propagate_in_clause_ self cid; (* make sure watches are valid *)
       ()
     in
 
-    match ev with
+    match op with
     | Trace.Input c ->
       add_c_ c;
       true
@@ -279,37 +393,72 @@ end = struct
                 if is_true self a' then () else (
                   set_atom_true self a'
                 ));
-          propagate_ self;
+          bcp_fixpoint_ self;
+
+          (*
+          (* slow sanity check *)
+          Clause.Tbl.iter
+            (fun c () ->
+               if c_is_false_ self c then
+                Log.debugf 0 (fun k->k"clause is false: %a" Clause.pp c))
+            self.active_clauses;
+             *)
+
           false
         with Conflict ->
           true
       in
 
+      (* now add clause *)
       add_c_ c;
       ok
 
     | Trace.Delete _c ->
-      true (* TODO*)
+      true (* TODO: actually remove the clause *)
+
+  type error =
+    [ `Bad_steps of VecI32.t
+    | `No_empty_clause
+    ]
+
+  let pp_error trace out = function
+    | `No_empty_clause -> Fmt.string out "no empty clause found"
+    | `Bad_steps bad ->
+      let n0 = VecI32.get bad 0 in
+      Fmt.fprintf out
+        "@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
+        (VecI32.size bad) n0
+        Trace.pp_op (Trace.get trace n0)
 
   let check trace : _ result =
-    let self = create() in
+    let self = create (Trace.cstore trace) in
 
     (* check each event in turn *)
+    let has_false = ref false in
     Trace.iteri trace
-      ~f:(fun i ev ->
+      ~f:(fun i op ->
-          let ok = check_ev self i ev in
+          let ok = check_op self i op in
-          if not ok then (
+          if ok then (
+            Log.debugf 50
+              (fun k->k"(@[check.step.ok@ :idx %d@ :op %a@])" i Trace.pp_op op);
+
+            (* check if op adds the empty clause *)
+            begin match op with
+              | (Trace.Redundant c | Trace.Input c) when Clause.size c = 0 ->
+                has_false := true
+              | _ -> ()
+            end;
+          ) else (
             Log.debugf 10
-              (fun k->k"(@[check.step.fail@ :on event[%d]@ :def %a@])" i Trace.pp_event ev);
+              (fun k->k"(@[check.step.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
+            Log.debugf 50 (fun k->k"(@[trail: %a@])" pp_trail_ self);
             VecI32.push self.errors i
           ));
 
-    (* TODO: check that the last event is empty clause *)
-
     Log.debugf 10 (fun k->k"found %d errors" (VecI32.size self.errors));
-    if VecI32.is_empty self.errors
+    if not !has_false then Error `No_empty_clause
-    then Ok ()
+    else if VecI32.size self.errors > 0 then Error (`Bad_steps self.errors)
-    else Error self.errors
+    else Ok ()
 end