wip: trace checking

- continue Drup checker
- create sidekick-bin.lib to share parsers
- parse problem+proof for sidekick-check

src/bin-lib/Drup_lexer.mll

@@ -0,0 +1,20 @@
+
+{
+  type token = EOF | ZERO | LIT of int | D
+}
+
+let number = ['1' - '9'] ['0' - '9']*
+
+rule token = parse
+  | eof                     { EOF }
+  | "c"                     { comment lexbuf }
+  | [' ' '\t' '\r']         { token lexbuf }
+  | "d"                     { D }
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | '0'                     { ZERO }
+  | '-'? number             { LIT (int_of_string (Lexing.lexeme lexbuf)) }
+  | _                       { Error.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
+
+and comment = parse
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | [^'\n']                 { comment lexbuf }

src/bin-lib/Drup_parser.ml

@@ -0,0 +1,41 @@
+
+module L = Drup_lexer
+
+type event =
+  | Add of int list
+  | Delete of int list
+
+type t = {
+  buf: Lexing.lexbuf;
+}
+
+let create (ic:in_channel) : t =
+  let buf = Lexing.from_channel ic in
+  {buf; }
+
+let next self : _ option =
+  let rec get_clause acc = match L.token self.buf with
+    | L.EOF -> Error.errorf "unexpected EOF in a clause"
+    | L.ZERO -> List.rev acc
+    | L.LIT i -> get_clause (i::acc)
+    | _ -> Error.errorf "expected clause"
+  in
+  begin match L.token self.buf with
+    | L.EOF -> None
+    | L.D ->
+      let c = get_clause [] in
+      Some (Delete c)
+    | L.ZERO -> Some (Add [])
+    | L.LIT i ->
+      let c = get_clause [i] in
+      Some (Add c)
+  end
+
+let iter self k =
+  let rec loop () =
+    match next self with
+    | None -> ()
+    | Some ev -> k ev; loop ()
+  in
+  loop ()
+

src/bin-lib/Drup_parser.mli

@@ -0,0 +1,16 @@
+
+(** {1 DRUP parser} *)
+
+type t
+
+type event =
+  | Add of int list
+  | Delete of int list
+
+val create : in_channel -> t
+
+val next : t -> event option
+
+val iter : t -> event Iter.t
+
+

src/bin-lib/Sidekick_bin_lib.ml

@@ -0,0 +1,8 @@
+
+(** Library for the Sidekick executables *)
+
+module Dimacs_lexer = Dimacs_lexer
+module Dimacs_parser = Dimacs_parser
+
+module Drup_lexer = Drup_lexer
+module Drup_parser = Drup_parser

src/bin-lib/dune

@@ -0,0 +1,9 @@
+
+(library
+  (name sidekick_bin_lib)
+  (public_name sidekick-bin.lib)
+  (synopsis "Utils for the sidekick binaries")
+  (libraries containers sidekick.util)
+  (flags :standard -warn-error -a+8 -open Sidekick_util))
+
+(ocamllex (modules Dimacs_lexer Drup_lexer))

src/checker/dune

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

src/checker/main.ml

@@ -1,4 +1,81 @@
 
+module BL = Sidekick_bin_lib
+module SDrup = Sidekick_drup
+
+let clause_of_int_l atoms : SDrup.clause =
+  Array.of_list atoms
+  |> Array.map SDrup.Atom.of_int
+  |> SDrup.Clause.of_array
+
+let check ?pb proof : bool =
+  let trace = SDrup.Trace.create() in
+
+  (* add problem to trace, if provided *)
+  begin match pb with
+    | None -> ()
+    | Some f when Filename.extension f = ".cnf" ->
+      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
+                SDrup.Trace.add_input_clause trace c))
+    | Some f ->
+      (* TODO: handle .cnf.gz *)
+      Error.errorf "unknown problem file extension '%s'" (Filename.extension f)
+  end;
+
+  (* add proof to trace *)
+  begin match proof with
+    | f when Filename.extension f = ".drup" ->
+      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
+                 SDrup.Trace.add_clause trace c
+               | BL.Drup_parser.Delete c ->
+                 let c = clause_of_int_l c in
+                 SDrup.Trace.del_clause trace c))
+    | f ->
+      (* TODO: handle .drup.gz *)
+      Error.errorf "unknown proof file extension '%s'" (Filename.extension f)
+  end;
+
+  (* check proof *)
+  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 ->
+      assert (VecI32.size bad > 0);
+      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
 
 let () =
-  assert false
+  let files = ref [] in
+  let opts = [
+    "-d", Arg.Int Log.set_debug, " set debug level";
+  ] |> Arg.align in
+  Printexc.record_backtrace true;
+
+  Arg.parse opts (fun f -> files := f :: !files) "checker [opt]* [file]+";
+
+  begin match List.rev !files with
+    | [pb; proof] ->
+      Log.debugf 1 (fun k->k"checker: problem `%s`, proof `%s`" pb proof);
+      let ok = check ~pb proof in
+      if not ok then exit 1
+    | [proof] ->
+      Log.debugf 1 (fun k->k"checker: proof `%s`" proof);
+      let ok = check ?pb:None proof in
+      if not ok then exit 1
+    | _ -> failwith "expected <problem>? <proof>"
+  end

src/drup/sidekick_drup.ml

@@ -33,12 +33,22 @@ end = struct
 end
 type atom = Atom.t
 
-type clause = atom array
-module Clause = struct
-  type t = clause
+module Clause : sig
+  type t
+  val size : t -> int
+  val get : t -> int -> atom
+  val iter : f:(atom -> unit) -> t -> unit
+  val pp : t Fmt.printer
+  val of_array : atom array -> t
+end = struct
+  type t = atom array
+  let size = Array.length
+  let get = Array.get
   let iter ~f c = Array.iter f c
   let pp out (self:t) = Fmt.Dump.array Atom.pp out self
+  let of_array a = a
 end
+type clause = Clause.t
 
 module Trace : sig
   type t
@@ -46,7 +56,7 @@ module Trace : sig
   val create : unit -> t
 
   val add_clause : t -> clause -> unit
-
+  val add_input_clause : t -> clause -> unit
   val del_clause : t -> clause -> unit
 
   type event =
@@ -56,6 +66,8 @@ module Trace : sig
 
   val iteri : t -> f:(int -> event -> unit) -> unit
   val events : t -> event Iter.t
+  val size : t -> int
+  val get : t -> int -> event
 
   val pp_event : event Fmt.printer
 
@@ -74,18 +86,21 @@ end = struct
     { evs=Vec.create() }
 
   let add_clause self c = Vec.push self.evs (A c)
+  let add_input_clause self c = Vec.push self.evs (I c)
   let del_clause self c = Vec.push self.evs (D c)
+  let get self i = Vec.get self.evs i
+  let size self = Vec.size self.evs
   let events self = Vec.to_seq self.evs
   let iteri self ~f = Vec.iteri f self.evs
 
   let pp_event out = function
-    | I c -> Fmt.fprintf out "(@[input %a@])" Clause.pp c
-    | A c -> Fmt.fprintf out "(@[add %a@])" Clause.pp c
-    | D c -> Fmt.fprintf out "(@[del %a@])" Clause.pp c
+    | I c -> Fmt.fprintf out "(@[Input %a@])" Clause.pp c
+    | A c -> Fmt.fprintf out "(@[Add %a@])" Clause.pp c
+    | D c -> Fmt.fprintf out "(@[Del %a@])" Clause.pp c
 
   let dump oc self : unit =
     let fpf = Printf.fprintf in
-    let pp_c out c = Array.iter (fun a -> fpf oc "%d " (Atom.to_int a)) c; in
+    let pp_c out c = Clause.iter c ~f:(fun a -> fpf oc "%d " (Atom.to_int a)); in
     Vec.iter
       (function
         | I c -> fpf oc "i %a0\n" pp_c c;
@@ -95,6 +110,20 @@ end = struct
       self.evs
 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. *)
@@ -129,15 +158,16 @@ end = struct
 
   let ensure_atom_ self (a:atom) =
     Bitvec.ensure_size self.assign (a:atom:>int);
-    Vec.ensure_size self.watches ISet.empty (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));
     ()
 
   let[@inline] is_true self (a:atom) : bool =
     Bitvec.get self.assign (a:atom:>int)
-  let[@inline] is_false self (a:atom) : bool = is_true self (Atom.neg a)
-  let[@inline] set_true self (a:atom) : unit =
-    Bitvec.set self.assign (a:atom:>int) true
 
+  let[@inline] is_false self (a:atom) : bool =
+    is_true self (Atom.neg a)
 
   let add_watch_ self (a:atom) cid =
     let set = Vec.get self.watches (a:atom:>int) in
@@ -149,6 +179,19 @@ end = struct
 
   exception Conflict
 
+  let raise_conflict_ self a =
+    Log.debugf 5 (fun k->k"conflict on atom %a" Atom.pp a);
+    raise Conflict
+
+  (* set atom to true *)
+  let set_atom_true (self:t) (a:atom) : unit =
+    if is_true self a then ()
+    else if is_false self a then raise_conflict_ self a
+    else (
+      Bitvec.set self.assign (a:atom:>int) true;
+      VecI32.push self.trail (a:atom:>int)
+    )
+
   (* TODO *)
   let propagate_in_clause_ (self:t) (cid:int) : unit =
     ()
@@ -169,20 +212,31 @@ end = struct
   let with_restore_trail_ self f =
     let trail_size0 = VecI32.size self.trail in
     let ptr = self.trail_ptr in
-    CCFun.finally
-      ~h:(fun () ->
-        VecI32.shrink self.trail trail_size0;
-        self.trail_ptr <- ptr)
-      ~f
+
+    let restore () =
+      (* unassign new literals *)
+      for i=trail_size0 to VecI32.size self.trail - 1 do
+        let a = Atom.of_int_unsafe (VecI32.get self.trail i) in
+        assert (is_true self a);
+        Bitvec.set self.assign (a:atom:>int) false;
+      done;
+
+      (* remove literals from trail *)
+      VecI32.shrink self.trail trail_size0;
+      self.trail_ptr <- ptr
+    in
+
+    CCFun.finally ~h:restore ~f
 
   (* check event, return [true] if it's valid *)
-  let check_ev (self:t) (ev:Trace.event) : bool =
-    Log.debugf 20 (fun k->k"(@[check-ev@ %a@])" Trace.pp_event ev);
+  let check_ev (self:t) i (ev:Trace.event) : bool =
+    Log.debugf 20 (fun k->k"(@[check-ev[%d]@ %a@])" i Trace.pp_event ev);
 
     (* add clause to the state *)
-    let add_c_ c =
-      Array.iter (ensure_atom_ self) c;
+    let add_c_ (c:Clause.t) =
+      Clause.iter c ~f:(ensure_atom_ self);
 
+      (* allocate clause *)
       let cid =
         match Vec.pop_exn self.cs_recycle with
         | cid ->
@@ -193,8 +247,15 @@ end = struct
           Vec.push self.cs c;
           cid
       in
-      add_watch_ self (Atom.neg c.(0)) cid;
-      add_watch_ self (Atom.neg c.(1)) cid;
+
+      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;
+          add_watch_ self (Atom.neg (Clause.get c 1)) cid;
+      end;
       propagate_in_clause_ self cid; (* make sure watches are valid *)
       ()
     in
@@ -216,8 +277,7 @@ end = struct
                 if is_true self a then raise_notrace Conflict; (* tautology *)
                 let a' = Atom.neg a in
                 if is_true self a' then () else (
-                  VecI32.push self.trail (a':atom:>int);
-                  set_true self a'
+                  set_atom_true self a'
                 ));
           propagate_ self;
           false
@@ -237,9 +297,10 @@ end = struct
     (* check each event in turn *)
     Trace.iteri trace
       ~f:(fun i ev ->
-          let ok = check_ev self ev in
+          let ok = check_ev self i ev in
           if not ok then (
-            Log.debugf 10 (fun k->k"(@[check.step.fail@ :n %d@ %a@])" i Trace.pp_event ev);
+            Log.debugf 10
+              (fun k->k"(@[check.step.fail@ event[%d]@ :def %a@])" i Trace.pp_event ev);
             VecI32.push self.errors i
           ));
 

src/main/dune

@@ -7,7 +7,7 @@
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
             sidekick.msat-solver sidekick-bin.smtlib sidekick.tef
-            sidekick.memtrace)
+            sidekick.memtrace sidekick-bin.lib)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule
@@ -18,4 +18,3 @@
     (with-stdout-to %{targets}
        (echo "let version = {git|%{version:sidekick}|git}"))))
 
-(ocamllex (modules Dimacs_lexer))

src/main/pure_sat_solver.ml

@@ -22,6 +22,7 @@ module SAT = Sidekick_sat.Make_pure_sat(Arg)
 
 module Dimacs = struct
   open Sidekick_base
+  module BL = Sidekick_bin_lib
   module T = Term
 
   let parse_file (solver:SAT.t) (file:string) : (unit, string) result =
@@ -30,8 +31,8 @@ module Dimacs = struct
     try
       CCIO.with_in file
         (fun ic ->
-           let p = Dimacs_parser.create ic in
-           Dimacs_parser.iter p
+           let p = BL.Dimacs_parser.create ic in
+           BL.Dimacs_parser.iter p
              (fun c ->
                 let atoms = List.rev_map get_lit c in
                 SAT.add_clause solver atoms ());