From 8bc1f1c864a2680c1f55c52a9db4877a17891ff1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 19 Aug 2021 00:15:00 -0400 Subject: [PATCH] feat: inner DRUP proof checking for pure-sat-solver --- src/bin-lib/Drup_lexer.mll | 4 ++- src/bin-lib/Drup_parser.ml | 14 ++++++-- src/bin-lib/Drup_parser.mli | 4 ++- src/checker/main.ml | 5 ++- src/main/dune | 1 + src/main/pure_sat_solver.ml | 68 ++++++++++++++++++++++++++++++++++--- src/sat/Solver.ml | 1 + src/sat/Solver_intf.ml | 3 ++ 8 files changed, 90 insertions(+), 10 deletions(-) diff --git a/src/bin-lib/Drup_lexer.mll b/src/bin-lib/Drup_lexer.mll index 31f43e0f..34164858 100644 --- a/src/bin-lib/Drup_lexer.mll +++ b/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)) } diff --git a/src/bin-lib/Drup_parser.ml b/src/bin-lib/Drup_parser.ml index 85eeaf0b..adbcdc35 100644 --- a/src/bin-lib/Drup_parser.ml +++ b/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 diff --git a/src/bin-lib/Drup_parser.mli b/src/bin-lib/Drup_parser.mli index 7665cfc1..702dff2f 100644 --- a/src/bin-lib/Drup_parser.mli +++ b/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 diff --git a/src/checker/main.ml b/src/checker/main.ml index ff3d5020..14131789 100644 --- a/src/checker/main.ml +++ b/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 diff --git a/src/main/dune b/src/main/dune index 5f64834f..2fe0d695 100644 --- a/src/main/dune +++ b/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)) diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 8846b594..b8717608 100644 --- a/src/main/pure_sat_solver.ml +++ b/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 diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index de6aec7d..85d3734c 100644 --- a/src/sat/Solver.ml +++ b/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 = diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 7cc51199..0ce069d2 100644 --- a/src/sat/Solver_intf.ml +++ b/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 *)