Commit 32daf68c authored by François Bobot's avatar François Bobot

[Plugins] parser for cnf dimacs format

parent d625cbbd
......@@ -257,12 +257,12 @@ install-all: install install-lib
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
PLUG_PARSER = genequlin
PLUG_PARSER = genequlin dimacs
PLUG_PRINTER =
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUGINS = genequlin tptp
PLUGINS = genequlin dimacs tptp
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2013 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
{
open Why3
open Stdlib
type vars = Term.term array
let get_indice i =
if i > 0 then (i-1)*2
else if i < 0 then (-i-1)*2+1
else assert false
let init_vars th_uc nb_var =
let a = Array.create (nb_var*2) Term.t_true in
let th = ref th_uc in
for i = nb_var downto -nb_var do
if i <> 0 then
if i > 0 then
let id = Ident.id_fresh (Printf.sprintf "x%i" i) in
let ls = Term.create_psymbol id [] in
th := Theory.add_param_decl !th ls;
a.(get_indice i) <- (Term.ps_app ls [])
else if i < 0 then
a.(get_indice i) <- Term.t_not a.(get_indice (-i))
done;
!th,a
let get_lit vars i =
let i = int_of_string i in
vars.(get_indice i)
exception SyntaxError of string
let syntax_error s = raise (SyntaxError s)
let () = Exn_printer.register (fun fmt e -> match e with
| SyntaxError s -> Format.pp_print_string fmt s
| _ -> raise e)
}
let newline = '\n'
let space = [' ' '\t' '\r']+
let digit = ['0'-'9']
let sign = '-' | '+'
let integer = sign? digit+
rule find_header = parse
| newline { Lexing.new_line lexbuf; find_header lexbuf }
| space { find_header lexbuf }
| 'p'
space+ "cnf"
space+ (digit+ as nb_var)
space+ (digit+ as nb_cls) { int_of_string nb_var,
int_of_string nb_cls }
| 'c' [^'\n']* '\n' { Lexing.new_line lexbuf; find_header lexbuf }
| _
{ syntax_error "Can't find header" }
and clause vars acc = parse
| newline { Lexing.new_line lexbuf; clause vars acc lexbuf }
| space { clause vars acc lexbuf }
| '0' { List.rev acc }
| integer as i { clause vars ((get_lit vars i)::acc) lexbuf }
| _ { syntax_error "Bad clause" }
and file th_uc vars n = parse
| newline { Lexing.new_line lexbuf; file th_uc vars n lexbuf }
| space { file th_uc vars n lexbuf }
| '0' { file th_uc vars n lexbuf }
| integer as i { let l = clause vars [get_lit vars i] lexbuf in
let t = List.fold_left (fun acc t ->
Term.t_or acc t
) Term.t_false l in
let pr = Decl.create_prsymbol
(Ident.id_fresh ("Cl"^(string_of_int n))) in
let th_uc = Theory.add_prop_decl th_uc Decl.Paxiom pr t in
file th_uc vars (n+1) lexbuf
}
| 'c' [^'\n']* ('\n' | eof) { Lexing.new_line lexbuf;
file th_uc vars n lexbuf }
| eof { th_uc }
| _ { syntax_error "Bad clauses" }
{
let parse th_uc filename cin =
let lb = Lexing.from_channel cin in
Loc.set_file filename lb;
Loc.with_location (fun lexbuf ->
let nb_vars, _ = find_header lexbuf in
let th_uc, vars = init_vars th_uc nb_vars in
file th_uc vars 0 lexbuf) lb
let parse _env _path filename cin =
let th_uc = Theory.create_theory (Ident.id_fresh "Cnf") in
let th_uc = parse th_uc filename cin in
let pr = Decl.create_prsymbol (Ident.id_fresh "false") in
let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal pr Term.t_false in
(), Mstr.singleton "Cnf" (Theory.close_theory th_uc)
let library_of_env = Env.register_format "Dimacs" ["cnf"] parse
~desc:"@[<hov>Parser for dimacs format.@]"
}
(*
Local Variables:
compile-command: "unset LANG; make -C ../.."
End:
*)
......@@ -238,16 +238,10 @@ and comment_line = parse
{
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ast = with_location (tptp_file token) lb in
let ast = Loc.with_location (tptp_file token) lb in
(), Tptp_typing.typecheck env path ast
let _library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
......
......@@ -107,10 +107,6 @@ rule token = parse
{ raise (IllegalCharacter c) }
{
let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb)
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
let parse_file_gen parse input_lexbuf lexbuf =
let s = Stack.create () in
......@@ -130,7 +126,7 @@ rule token = parse
| _ -> tok in
let lex_dumb = Lexing.from_function (fun _ _ -> assert false) in
Loc.transfer_loc lexbuf lex_dumb;
with_location (parse multifile) lex_dumb
Loc.with_location (parse multifile) lex_dumb
let parse_file = parse_file_gen Driver_parser.file
let parse_file_extract = parse_file_gen Driver_parser.file_extract
......
......@@ -30,5 +30,3 @@ val comment : Lexing.lexbuf -> unit
val string : Lexing.lexbuf -> string
val remove_leading_plus : string -> string
val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a
......@@ -302,20 +302,15 @@ and string = parse
{ Buffer.add_char string_buf c; string lexbuf }
{
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let parse_logic_file env path lb =
open_file token (Lexing.from_string "") (Typing.open_file env path);
with_location (logic_file token) lb;
Loc.with_location (logic_file token) lb;
Typing.close_file ()
let parse_program_file inc lb =
open_file token (Lexing.from_string "") inc;
with_location (program_file token) lb
Loc.with_location (program_file token) lb
let token_counter lb =
let rec loop in_annot a p =
......
......@@ -117,3 +117,10 @@ let () = Exn_printer.register
| _ ->
raise exn)
let loc lb = extract (Lexing.lexeme_start_p lb, Lexing.lexeme_end_p lb)
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
| Located _ as e -> raise e
| e -> raise (Located (loc lb, e))
......@@ -56,3 +56,5 @@ val error: ?loc:position -> exn -> 'a
exception Message of string
val errorm: ?loc:position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val with_location: (Lexing.lexbuf -> 'a) -> (Lexing.lexbuf -> 'a)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment