New lexer/parser for dimacs format.

Makefile

@@ -1,7 +1,7 @@
 # copyright (c) 2014, guillaume bury
 
 LOG=build.log
-COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix -classic-display
+COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix,str -classic-display
 FLAGS=
 DIRS=-Is sat,smt,common,util
 DOC=msat.docdir/index.html

util/lexdimacs.mll

@@ -1,16 +0,0 @@
-(*  Copyright 2005 INRIA  *)
-{
-open Lexing;;
-open Parsedimacs;;
-}
-
-let number = ['0' - '9']+
-
-rule token = parse
-  | ' '                     { token lexbuf }
-  | 'p'                     { P }
-  | "cnf"                   { CNF }
-  | '\n'                    { EOL }
-  | "c " [^ '\n']* '\n'     { token lexbuf }
-  | ['-']? number           { LIT (int_of_string (Lexing.lexeme lexbuf)) }
-  | eof                     { EOF }

util/parsedimacs.mly

@@ -1,30 +0,0 @@
-/*  Copyright 2005 INRIA  */
-
-%{
-    exception Clause_ending of int
-%}
-
-%token <int> LIT
-%token P CNF EOL EOF
-
-%start file
-%type <int list list> file
-
-%%
-
-/* DIMACS syntax */
-
-file:
-  | EOF                             { [] }
-  | P CNF LIT LIT EOL clause_list   { $6 }
-;
-clause_list:
-  | EOF                 { [] }
-  | EOL clause_list     { $2 }
-  | clause clause_list  { $1 :: $2 }
-;
-clause:
-  /* clauses always ends with a '0' */
-  | LIT EOL         { if $1 = 0 then [] else raise (Clause_ending $1) }
-  | LIT clause      { $1 :: $2 }
-;

util/parser.ml

@@ -0,0 +1,53 @@
+(* Copyright 2014 Guillaume Bury *)
+
+exception Syntax_error of int
+
+type line =
+    | Empty
+    | Comment
+    | Pcnf of int * int
+    | Clause of int list
+
+let ssplit = Str.split (Str.regexp "[ \t]+")
+
+let of_input f =
+    match ssplit (input_line f) with
+    | [] -> Empty
+    | "c" :: _ -> Comment
+    | "p" :: "cnf" :: i :: j :: [] ->
+            begin try
+                Pcnf (int_of_string i, int_of_string j)
+            with Invalid_argument _ ->
+                raise (Syntax_error (-1))
+            end
+    | l ->
+            begin try begin match List.rev_map int_of_string l with
+            | 0 :: r -> Clause r
+            | _ -> raise (Syntax_error (-1))
+            end with
+            | Invalid_argument _ -> raise (Syntax_error (-1))
+            end
+
+let parse_with todo file =
+    let f = open_in file in
+    let line = ref 0 in
+    try
+        while true do
+            incr line;
+            todo (of_input f)
+        done
+    with
+    | Syntax_error _ ->
+        raise (Syntax_error !line)
+    | End_of_file ->
+        close_in f
+
+let cnf = ref []
+let parse_line = function
+    | Empty | Comment | Pcnf _ -> ()
+    | Clause l -> cnf := l :: !cnf
+
+let parse f =
+    cnf := [];
+    parse_with parse_line f;
+    !cnf

util/parser.mli

@@ -0,0 +1,5 @@
+(* Copyright 2014 Guillaume Bury *)
+
+exception Syntax_error of int
+
+val parse : string -> int list list

util/test.ml

@@ -59,10 +59,7 @@ let check () =
 
 (* Entry file parsing *)
 let get_cnf () =
-  let chan = open_in !file in
-  let lexbuf = Lexing.from_channel chan in
-  let l = Parsedimacs.file Lexdimacs.token lexbuf in
-  List.map (List.map S.make) l
+  List.map (List.map S.make) (Parser.parse !file)
 
 let print_cnf cnf =
   Format.printf "CNF :@\n";