Added small lexer/parser for dimacs (work in progress).

Makefile

@@ -20,7 +20,7 @@ doc:
 	$(COMP) $(FLAGS) $(DIRS) $(DOC)
 
 test: $(TEST)
-	./tests/main
+	./tests/main tests/test-0.d
 
 $(TEST): $(LIB)
 	$(COMP) $(FLAGS) $(DIRS) $(TEST)

sat/sat.ml

@@ -1,6 +1,7 @@
 (* Copyright 2014 Guillaume Bury *)
 
 module Fsat = struct
+  exception Dummy
   exception Out_of_int
 
   (* Until the constant true_ and false_ are not needed anymore,
@@ -10,6 +11,8 @@ module Fsat = struct
   let max_lit = min max_int (- min_int)
   let max_index = ref 0
 
+  let make i = if i <> 0 then i else raise Dummy
+
   let dummy = 0
 
   let neg a = - a
@@ -64,6 +67,8 @@ end
 module Make(Dummy : sig end) = struct
   module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat)
 
+  exception Bad_atom
+
   type res =
     | Sat
     | Unsat
@@ -73,8 +78,19 @@ module Make(Dummy : sig end) = struct
   type atom = Fsat.t
   type state = SatSolver.t
 
+  let new_atom () =
+      try
+          Fsat.create ()
+      with Fsat.Out_of_int ->
+          raise Bad_atom
+
+  let make i =
+      try
+          Fsat.make i
+      with Fsat.Dummy ->
+          raise Bad_atom
+
   let neg = Fsat.neg
-  let new_atom = Fsat.create
 
   let hash = Fsat.hash
   let equal = Fsat.equal

sat/sat.mli

@@ -3,14 +3,22 @@
 module Make(Dummy: sig end) : sig
   (** Fonctor to make a pure SAT Solver module with built-in literals. *)
 
-  type atom
-  (** Abstract type for atoms, i.e boolean literals. *)
+  exception Bad_atom
+  (** Exception raised when a problem with atomic formula encoding is detected. *)
+
+  type atom = private int
+  (** Type for atoms, i.e boolean literals. *)
 
   type res = Sat | Unsat
   (** Type of results returned by the solve function. *)
 
   val new_atom : unit -> atom
-  (** [new_atom ()] returns a fresh literal. *)
+  (** [new_atom ()] returns a fresh literal.
+      @raise Bad_atom if there are no more integer available to represent new atoms. *)
+
+  val make : int -> atom
+  (** Returns the literal corresponding to the integer.
+      @raise bad_atom if given [0] as argument.*)
 
   val neg : atom -> atom
   (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *)

util/lexdimacs.mll

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

util/parsedimacs.mly

@@ -0,0 +1,29 @@
+/*  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                 { [] }
+  | clause clause_list  { $1 :: $2 }
+;
+clause:
+  /* Clause always ends with a '0' */
+  | LIT EOL         { if $1 = 0 then [] else raise (Clause_ending $1) }
+  | LIT clause      { $1 :: $2 }
+;

util/test.ml

@@ -1,25 +1,32 @@
 
 module S = Sat.Make(struct end)
 
-let anon_fun = fun _ -> ()
-let usage = "Coming soon..."
-let argspec = [
+(* Arguments parsing *)
+let file = ref ""
+
+let input_file = fun s -> file := s
+let usage = "Usage : main [options] <file>"
+let argspec = Arg.align [
     "-v", Arg.Int (fun i -> Log.set_debug i),
-    "Sets the debug verbose level";
+    "<lvl> Sets the debug verbose level";
 ]
 
-(* Temp until lexer/parsezr is set up *)
-let init () =
-  let v = Array.init 5 (fun _ -> S.new_atom ()) in
-  [ [
-    [v.(0); v.(1)];
-    [S.neg v.(0); v.(2)];
-    [S.neg v.(1); v.(2)];
-    [v.(3); v.(4)];
-    [S.neg v.(3); S.neg v.(2)];
-    [S.neg v.(4); S.neg v.(2)];
-    ]
-  ]
+(* 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
+
+let print_cnf cnf =
+    Format.printf "CNF :@\n";
+    List.iter (fun c ->
+        Format.fprintf Format.std_formatter "%a;@\n"
+        (fun fmt -> List.iter (fun a ->
+            Format.fprintf fmt "%a@ " S.print_atom a
+            )
+        ) c
+    ) cnf
 
 (* Iterate over all variables created *)
 let print_assign fmt () =
@@ -30,14 +37,14 @@ let print_assign fmt () =
     )
 
 let main () =
-  Arg.parse argspec anon_fun usage;
-  List.iter (fun l ->
-      List.iter (fun c -> Format.printf "Adding : %a@."
-                    (fun _ -> List.iter (fun a -> Format.printf "%a " S.print_atom a)) c) l;
-      S.assume l;
-      match S.solve () with
-      | S.Sat -> Format.printf "Sat@\n%a@." print_assign ()
-      | S.Unsat -> Format.printf "Unsat@.") (init ());
+  Arg.parse argspec input_file usage;
+  if !file = "" then begin
+      Arg.usage argspec usage;
+      exit 2
+  end;
+  let cnf = get_cnf () in
+  print_cnf cnf;
+  ()
 ;;
 
 main ()