feat: inner DRUP proof checking for pure-sat-solver

src/bin-lib/Drup_lexer.mll

@@ -1,6 +1,6 @@
 
 {
-  type token = EOF | ZERO | LIT of int | D
+  type token = EOF | ZERO | LIT of int | D | R | I
 }
 
 let number = ['1' - '9'] ['0' - '9']*
@@ -10,6 +10,8 @@ rule token = parse
   | "c"                     { comment lexbuf }
   | [' ' '\t' '\r']         { token lexbuf }
   | "d"                     { D }
+  | "r"                     { R }
+  | "i"                     { I }
   | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
   | '0'                     { ZERO }
   | '-'? number             { LIT (int_of_string (Lexing.lexeme lexbuf)) }

src/bin-lib/Drup_parser.ml

@@ -2,6 +2,7 @@
 module L = Drup_lexer
 
 type event =
+  | Input of int list
   | Add of int list
   | Delete of int list
 
@@ -9,9 +10,10 @@ type t = {
   buf: Lexing.lexbuf;
 }
 
-let create (ic:in_channel) : t =
-  let buf = Lexing.from_channel ic in
-  {buf; }
+let create_string s : t =
+  { buf=Lexing.from_string s }
+let create_chan (ic:in_channel) : t =
+  { buf = Lexing.from_channel ic }
 
 let next self : _ option =
   let rec get_clause acc = match L.token self.buf with
@@ -22,9 +24,15 @@ let next self : _ option =
   in
   begin match L.token self.buf with
     | L.EOF -> None
+    | L.I ->
+      let c = get_clause [] in
+      Some (Input c)
     | L.D ->
       let c = get_clause [] in
       Some (Delete c)
+    | L.R ->
+      let c = get_clause [] in
+      Some (Add c)
     | L.ZERO -> Some (Add [])
     | L.LIT i ->
       let c = get_clause [i] in

src/bin-lib/Drup_parser.mli

@@ -4,10 +4,12 @@
 type t
 
 type event =
+  | Input of int list
   | Add of int list
   | Delete of int list
 
-val create : in_channel -> t
+val create_chan : in_channel -> t
+val create_string : string -> t
 
 val next : t -> event option
 

src/checker/main.ml

@@ -34,9 +34,12 @@ let check ?pb proof : bool =
       Profile.with_ "parse-proof.drup" @@ fun() ->
       CCIO.with_in f
         (fun ic ->
-           let p = BL.Drup_parser.create ic in
+           let p = BL.Drup_parser.create_chan ic in
            BL.Drup_parser.iter p
              (function
+               | BL.Drup_parser.Input c ->
+                 let c = clause_of_int_l cstore c in
+                 Drup_check.Trace.add_input_clause trace c
                | BL.Drup_parser.Add c ->
                  let c = clause_of_int_l cstore c in
                  Drup_check.Trace.add_clause trace c

src/main/dune

@@ -7,6 +7,7 @@
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
             sidekick.smt-solver sidekick-bin.smtlib sidekick.tef
+            sidekick.drup
             sidekick.memtrace sidekick-bin.lib)
  (flags :standard -safe-string -color always -open Sidekick_util))
 

src/main/pure_sat_solver.ml

@@ -15,9 +15,20 @@ module Formula = struct
   let pp = Fmt.int
 end
 
-module Proof
-  : Sidekick_sat.PROOF with type lit = Formula.t
-= struct
+(* TODO: on the fly compression *)
+module Proof : sig
+  include Sidekick_sat.PROOF with type lit = Formula.t
+
+  val dummy : t
+  val create : unit -> t
+  val to_string : t -> string
+  val to_chan : out_channel -> t -> unit
+  type event = Sidekick_bin_lib.Drup_parser.event =
+    | Input of int list
+    | Add of int list
+    | Delete of int list
+  val iter_events : t -> event Iter.t
+end = struct
   let bpf = Printf.bprintf
   type lit = Formula.t
   type t =
@@ -64,6 +75,21 @@ module Proof
   let to_chan oc = function
     | Dummy -> ()
     | Inner {buf} -> Buffer.output_buffer oc buf; flush oc
+
+  module DP = Sidekick_bin_lib.Drup_parser
+
+  type event = DP.event =
+    | Input of int list
+    | Add of int list
+    | Delete of int list
+
+  (* parse the proof back *)
+  let iter_events (self:t) : DP.event Iter.t =
+    match self with
+    | Dummy -> Iter.empty
+    | Inner {buf} ->
+      let dp = DP.create_string (to_string self) in
+      DP.iter dp
 end
 
 module Arg = struct
@@ -96,6 +122,37 @@ module Dimacs = struct
       E.of_exn_trace e
 end
 
+let check_proof proof : bool =
+  Profile.with_ "pure-sat.check-proof" @@ fun () ->
+  let module SDRUP = Sidekick_drup.Make() in
+  let store = SDRUP.Clause.create() in
+  let checker = SDRUP.Checker.create store in
+  let ok = ref true in
+
+  let tr_clause c =
+    let c = List.rev_map SDRUP.Atom.of_int_dimacs c in
+    SDRUP.Clause.of_list store c
+  in
+
+  Proof.iter_events proof
+    (function
+      | Proof.Input c ->
+        let c = tr_clause c in
+        SDRUP.Checker.add_clause checker c
+
+      | Proof.Add c ->
+        let c = tr_clause c in
+        if not (SDRUP.Checker.is_valid_drup checker c) then (
+          ok := false;
+        );
+        SDRUP.Checker.add_clause checker c;
+
+      | Proof.Delete c ->
+        let c = tr_clause c in
+        SDRUP.Checker.del_clause checker c;
+    );
+  !ok
+
 let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
   let res =
     Profile.with_ "solve" (fun () -> SAT.solve solver)
@@ -110,7 +167,10 @@ let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
 
       if check then (
         let proof = SAT.proof solver in
-        Proof.check proof;
+        let ok = check_proof proof in
+        if not ok then (
+          Error.errorf "Proof validation failed"
+        );
       );
 
       let t3 = Sys.time () -. t2 in

src/sat/Solver.ml

@@ -1830,6 +1830,7 @@ module Make(Plugin : PLUGIN)
 
   let[@inline] theory st = st.th
   let[@inline] store st = st.store
+  let[@inline] proof st = st.proof
 
   (* Result type *)
   type res =

src/sat/Solver_intf.ml

@@ -299,6 +299,9 @@ module type S = sig
   val store : t -> store
   (** Store for the solver *)
 
+  val proof : t -> proof
+  (** Access the inner proof *)
+
   (** {2 Types} *)
 
   (** Result type for the solver *)