feat: handle parsing of .cnf files

src/base-term/Base_types.ml

@@ -132,6 +132,7 @@ type statement =
   | Stmt_decl of ID.t * ty list * ty
   | Stmt_define of definition list
   | Stmt_assert of term
+  | Stmt_assert_clause of term list
   | Stmt_check_sat
   | Stmt_exit
 
@@ -1002,6 +1003,7 @@ module Statement = struct
     | Stmt_decl of ID.t * ty list * ty
     | Stmt_define of definition list
     | Stmt_assert of term
+    | Stmt_assert_clause of term list
     | Stmt_check_sat
     | Stmt_exit
 
@@ -1015,6 +1017,7 @@ module Statement = struct
       Fmt.fprintf out "(@[<1>declare-fun@ %a (@[%a@])@ %a@])"
         ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret
     | Stmt_assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t
+    | Stmt_assert_clause c -> Fmt.fprintf out "(@[assert-clause@ %a@])" (Util.pp_list pp_term) c
     | Stmt_exit -> Fmt.string out "(exit)"
     | Stmt_data l ->
       Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data.pp) l

src/main/Dimacs_lexer.mll

@@ -0,0 +1,20 @@
+{
+  type token = EOF | P | CNF | ZERO | LIT of int
+}
+
+let number = ['1' - '9'] ['0' - '9']*
+
+rule token = parse
+  | eof                     { EOF }
+  | "c"                     { comment lexbuf }
+  | [' ' '\t' '\r']         { token lexbuf }
+  | 'p'                     { P }
+  | "cnf"                   { CNF }
+  | '\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/main/Dimacs_parser.ml

@@ -0,0 +1,54 @@
+module L = Dimacs_lexer
+
+type t = {
+  buf: Lexing.lexbuf;
+  mutable header: (int * int) option;
+}
+
+let create (ic:in_channel) : t =
+  let buf = Lexing.from_channel ic in
+  {buf; header=None}
+
+let parse_header self =
+  match self.header with
+  | Some tup -> tup
+  | None ->
+    let i, j =
+      try
+        (match L.token self.buf with
+         | L.P ->
+           (match L.token self.buf with
+            | L.CNF ->
+              (match L.token self.buf with
+               | L.LIT i ->
+                 (match L.token self.buf with
+                  | L.LIT j -> i,j
+                  | _ -> raise Exit)
+               | _ -> raise Exit)
+            | _ -> raise Exit)
+         | _ -> raise Exit
+        )
+      with Exit -> Error.errorf "expected file to start with header"
+    in
+    self.header <- Some (i,j);
+    i,j
+
+let next_clause self : _ option =
+  let rec loop acc = match L.token self.buf with
+    | L.EOF when acc=[] -> None
+    | L.EOF -> Error.errorf "unexpected EOF in a clause"
+    | L.ZERO -> Some (List.rev acc)
+    | L.LIT i -> loop (i::acc)
+    | _ -> Error.errorf "expected clause"
+  in
+  loop []
+
+let iter self k =
+  ignore (parse_header self : _*_);
+  let rec loop () =
+    match next_clause self with
+    | None -> ()
+    | Some c -> k c; loop ()
+  in
+  loop ()
+

src/main/Dimacs_parser.mli

@@ -0,0 +1,13 @@
+(** {1 DIMACS parser} *)
+
+type t
+
+val create : in_channel -> t
+
+val parse_header : t -> int*int
+
+val next_clause : t -> int list option
+
+val iter : t -> int list Iter.t
+
+

src/main/dune

@@ -7,3 +7,5 @@
  (libraries containers iter result msat sidekick.core sidekick.base-term
    sidekick.msat-solver sidekick-bin.smtlib)
  (flags :standard -safe-string -color always -open Sidekick_util))
+
+(ocamllex (modules Dimacs_lexer))

src/main/main.ml

@@ -82,6 +82,38 @@ let argspec = Arg.align [
     "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
   ] |> List.sort compare
 
+module Dimacs = struct
+  open Sidekick_base_term
+  module T = Term
+
+  let parse_file tst (file:string) : Statement.t list or_error =
+    let atoms = Util.Int_tbl.create 32 in
+    let get_lit i =
+      let v =
+        match Util.Int_tbl.find atoms (abs i) with
+        | x -> Term.const tst x
+        | exception Not_found ->
+          let f = Sidekick_base_term.Fun.mk_undef_const (ID.makef "%d" (abs i)) Ty.bool in
+          Util.Int_tbl.add atoms (abs i) f;
+          Term.const tst f
+      in
+      if i<0 then Term.not_ tst v else v
+    in
+    try
+      CCIO.with_in file
+        (fun ic ->
+           let p = Dimacs_parser.create ic in
+           let stmts = ref [] in
+           Dimacs_parser.iter p
+             (fun c ->
+                let lits = List.rev_map get_lit c in
+                stmts := Statement.Stmt_assert_clause lits :: !stmts);
+           stmts := Statement.Stmt_check_sat :: !stmts;
+           Ok (List.rev !stmts))
+    with e ->
+      E.of_exn_trace e
+end
+
 (* Limits alarm *)
 let check_limits () =
   let t = Sys.time () in
@@ -105,8 +137,10 @@ let main () =
   let al = Gc.create_alarm check_limits in
   Util.setup_gc();
   let tst = Term.create ~size:4_096 () in
+  let is_cnf = Filename.check_suffix !file ".cnf" in
   let solver =
-    let theories = [
+    let theories =
+      if is_cnf then [] else [
         Process.th_bool ;
         Process.th_cstor;
       ]
@@ -117,7 +151,11 @@ let main () =
     (* might have to check conflicts *)
     Solver.add_theory solver Process.Check_cc.theory;
   );
-  Sidekick_smtlib.parse tst !file >>= fun input ->
+  begin
+    if is_cnf then Dimacs.parse_file tst !file
+    else Sidekick_smtlib.parse tst !file
+  end
+  >>= fun input ->
   (* process statements *)
   let res =
     try

src/smtlib/Process.ml

@@ -244,6 +244,14 @@ let process_stmt
       CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
       Solver.add_clause solver (IArray.singleton atom);
       E.return()
+    | Statement.Stmt_assert_clause c ->
+      if pp_cnf then (
+        Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c
+      );
+      let c = List.map (Solver.mk_atom_t solver) c in
+      CCOpt.iter (fun h -> Vec.push h c) hyps;
+      Solver.add_clause solver (IArray.of_list c);
+      E.return()
     | Statement.Stmt_data _ ->
       E.return()
     | Statement.Stmt_define _ ->