From df524375a77239496bbd581b7d4e349dd6233d54 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 1 Nov 2014 21:43:58 +0100 Subject: [PATCH] Added small lexer/parser for dimacs (work in progress). --- Makefile | 2 +- sat/sat.ml | 18 ++++++++++++++- sat/sat.mli | 14 ++++++++--- util/lexdimacs.mll | 16 +++++++++++++ util/parsedimacs.mly | 29 +++++++++++++++++++++++ util/test.ml | 55 +++++++++++++++++++++++++------------------- 6 files changed, 105 insertions(+), 29 deletions(-) create mode 100644 util/lexdimacs.mll create mode 100644 util/parsedimacs.mly diff --git a/Makefile b/Makefile index 09f2eae7..cf05f91b 100644 --- a/Makefile +++ b/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) diff --git a/sat/sat.ml b/sat/sat.ml index e53a3fc4..c8149483 100644 --- a/sat/sat.ml +++ b/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 diff --git a/sat/sat.mli b/sat/sat.mli index 132de97d..d3d98015 100644 --- a/sat/sat.mli +++ b/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]. *) diff --git a/util/lexdimacs.mll b/util/lexdimacs.mll new file mode 100644 index 00000000..9cc1507a --- /dev/null +++ b/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 } diff --git a/util/parsedimacs.mly b/util/parsedimacs.mly new file mode 100644 index 00000000..147ff6ab --- /dev/null +++ b/util/parsedimacs.mly @@ -0,0 +1,29 @@ +/* Copyright 2005 INRIA */ + +%{ + exception Clause_ending of int +%} + +%token LIT +%token P CNF EOL EOF + +%start file +%type 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 } +; diff --git a/util/test.ml b/util/test.ml index cc1d70fd..60a69823 100644 --- a/util/test.ml +++ b/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] " +let argspec = Arg.align [ "-v", Arg.Int (fun i -> Log.set_debug i), - "Sets the debug verbose level"; + " 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 ()