diff --git a/.merlin b/.merlin new file mode 100644 index 00000000..cc724db2 --- /dev/null +++ b/.merlin @@ -0,0 +1,6 @@ +S sat +S smt +S util +B _build/sat +B _build/smt +B _build/util diff --git a/Makefile b/Makefile index 8da6dccf..cd4a9a4a 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ # copyright (c) 2014, guillaume bury LOG=build.log -COMP=ocamlbuild -log $(LOG) -use-ocamlfind -package num,zarith,unix,str -classic-display +COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display FLAGS= DIRS=-Is sat,smt,common,util DOC=msat.docdir/index.html diff --git a/_tags b/_tags index c1b52373..8508f50a 100644 --- a/_tags +++ b/_tags @@ -1,8 +1,8 @@ -: for-pack(Msat) +: for-pack(Msat), package(zarith) : for-pack(Msat) # enable stronger inlining everywhere -: inline(15) +: inline(15) : inline(10) : inline(10) diff --git a/common/.merlin b/common/.merlin deleted file mode 100644 index db2b3820..00000000 --- a/common/.merlin +++ /dev/null @@ -1,4 +0,0 @@ -S ./ - -B ../_build/ -B ../_build/common/ diff --git a/common/hashcons.ml b/util/hashcons.ml similarity index 100% rename from common/hashcons.ml rename to util/hashcons.ml diff --git a/common/hashcons.mli b/util/hashcons.mli similarity index 100% rename from common/hashcons.mli rename to util/hashcons.mli diff --git a/common/hstring.ml b/util/hstring.ml similarity index 100% rename from common/hstring.ml rename to util/hstring.ml diff --git a/common/hstring.mli b/util/hstring.mli similarity index 100% rename from common/hstring.mli rename to util/hstring.mli diff --git a/common/iheap.ml b/util/iheap.ml similarity index 100% rename from common/iheap.ml rename to util/iheap.ml diff --git a/common/iheap.mli b/util/iheap.mli similarity index 100% rename from common/iheap.mli rename to util/iheap.mli diff --git a/util/log.ml b/util/log.ml index 151d17c8..07e41416 100644 --- a/util/log.ml +++ b/util/log.ml @@ -24,101 +24,24 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (** {1 Some helpers} *) - -(** {2 Time facilities} *) - -(** Time elapsed since initialization of the program, and time of start *) -let get_total_time, get_start_time = - let start = Unix.gettimeofday () in - (function () -> - let stop = Unix.gettimeofday () in - stop -. start), - (function () -> start) - -(** {2 Misc} *) - -let clear_line () = - output_string Pervasives.stdout - "\r \r"; - flush Pervasives.stdout - - let debug_level_ = ref 0 let set_debug l = debug_level_ := l let get_debug () = !debug_level_ -let need_cleanup = ref false let debug l format = let b = Buffer.create 15 in if l <= !debug_level_ then ( - (if !need_cleanup then clear_line ()); - Printf.bprintf b "%% [%.3f] " (get_total_time ()); Printf.kbprintf (fun b -> print_endline (Buffer.contents b)) b format) else Printf.ifprintf b format -let pp_pos pos = - let open Lexing in - Printf.sprintf "line %d, column %d" pos.pos_lnum (pos.pos_cnum - pos.pos_bol) - -(** {2 Printing utils} *) - -let sprintf format = - let buffer = Buffer.create 64 in - Printf.kbprintf - (fun fmt -> Buffer.contents buffer) - buffer - format - -let fprintf oc format = - let buffer = Buffer.create 64 in - Printf.kbprintf - (fun fmt -> Buffer.output_buffer oc buffer) - buffer - format - -let printf format = fprintf stdout format -let eprintf format = fprintf stderr format - -let on_fmt pp x = - pp Format.str_formatter x; - Format.flush_str_formatter () - let on_buffer pp x = let buf = Buffer.create 24 in pp buf x; Buffer.contents buf -let pp_pair ?(sep=" ") px py buf (x,y) = - px buf x; - Buffer.add_string buf sep; - py buf y - -let pp_opt pp buf x = match x with - | None -> Buffer.add_string buf "None" - | Some x -> Printf.bprintf buf "Some %a" pp x - -(** print a list of items using the printing function *) -let rec pp_list ?(sep=", ") pp_item buf = function - | x::((y::xs) as l) -> - pp_item buf x; - Buffer.add_string buf sep; - pp_list ~sep pp_item buf l - | x::[] -> pp_item buf x - | [] -> () - -(** print an array of items using the printing function *) -let pp_array ?(sep=", ") pp_item buf a = - for i = 0 to Array.length a - 1 do - (if i > 0 then Buffer.add_string buf sep); - pp_item buf a.(i) - done - -(** print an array of items using the printing function *) -let pp_arrayi ?(sep=", ") pp_item buf a = - for i = 0 to Array.length a - 1 do - (if i > 0 then Buffer.add_string buf sep); - pp_item buf i a.(i) - done +let on_fmt pp x = + pp Format.str_formatter x; + Format.flush_str_formatter () diff --git a/util/log.mli b/util/log.mli index 3a5c6b42..88da899f 100644 --- a/util/log.mli +++ b/util/log.mli @@ -25,50 +25,11 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. (** {1 Some helpers} *) -(** {2 Time facilities} *) - -(** time elapsed since start of program *) -val get_total_time : unit -> float - -(** time at which the program started *) -val get_start_time : unit -> float - -(** {2 Misc} *) - val set_debug : int -> unit (** Set debug level *) val get_debug : unit -> int (** Current debug level *) -val need_cleanup : bool ref (** Cleanup line before printing? *) val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a (** debug message *) -val pp_pos : Lexing.position -> string - -(** {2 Printing utils} *) - -(** print into a string *) -val sprintf : ('a, Buffer.t, unit, string) format4 -> 'a - -val fprintf : out_channel -> ('a, Buffer.t, unit, unit) format4 -> 'a - -val printf : ('a, Buffer.t, unit, unit) format4 -> 'a -val eprintf : ('a, Buffer.t, unit, unit) format4 -> 'a -val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string - -val pp_pair: ?sep:string -> (Buffer.t -> 'a -> unit) -> - (Buffer.t -> 'b -> unit) -> Buffer.t -> ('a * 'b) -> unit - -val pp_opt : (Buffer.t -> 'a -> unit) -> Buffer.t -> 'a option -> unit - -(** print a list of items using the printing function *) -val pp_list: ?sep:string -> (Buffer.t -> 'a -> unit) - -> Buffer.t -> 'a list -> unit - -(** print an array of items with printing function *) -val pp_array: ?sep:string -> (Buffer.t -> 'a -> unit) - -> Buffer.t -> 'a array -> unit - -(** print an array, giving the printing function both index and item *) -val pp_arrayi: ?sep:string -> (Buffer.t -> int -> 'a -> unit) - -> Buffer.t -> 'a array -> unit +val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string diff --git a/util/parser.ml b/util/parser.ml index 4863338d..0098703e 100644 --- a/util/parser.ml +++ b/util/parser.ml @@ -1,4 +1,8 @@ -(* Copyright 2014 Guillaume Bury *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) exception Syntax_error of int @@ -8,7 +12,23 @@ type line = | Pcnf of int * int | Clause of int list -let ssplit = Str.split (Str.regexp "[ \t]+") +let rec _read_word s acc i len = + assert (len>0); + if i+len=String.length s + then String.sub s i len :: acc + else match s.[i+len] with + | ' ' | '\t' -> + let acc = String.sub s i len :: acc in + _skip_space s acc (i+len+1) + | _ -> _read_word s acc i (len+1) +and _skip_space s acc i = + if i=String.length s + then acc + else match s.[i] with + | ' ' | '\t' -> _skip_space s acc (i+1) + | _ -> _read_word s acc i 1 + +let ssplit s = List.rev (_skip_space s [] 0) let of_input f = match ssplit (input_line f) with @@ -17,7 +37,7 @@ let of_input f = | "p" :: "cnf" :: i :: j :: [] -> begin try Pcnf (int_of_string i, int_of_string j) - with Invalid_argument _ -> + with Failure _ -> raise (Syntax_error (-1)) end | l -> @@ -26,7 +46,7 @@ let of_input f = | 0 :: r -> Clause r | _ -> raise (Syntax_error (-1)) end - with Invalid_argument _ -> raise (Syntax_error (-1)) + with Failure _ -> raise (Syntax_error (-1)) end let parse_with todo file = diff --git a/util/parser.mli b/util/parser.mli index 2847772b..84a7b222 100644 --- a/util/parser.mli +++ b/util/parser.mli @@ -1,4 +1,8 @@ -(* Copyright 2014 Guillaume Bury *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) exception Syntax_error of int diff --git a/common/timer.ml b/util/timer.ml similarity index 100% rename from common/timer.ml rename to util/timer.ml diff --git a/common/timer.mli b/util/timer.mli similarity index 100% rename from common/timer.mli rename to util/timer.mli diff --git a/common/vec.ml b/util/vec.ml similarity index 100% rename from common/vec.ml rename to util/vec.ml diff --git a/common/vec.mli b/util/vec.mli similarity index 100% rename from common/vec.mli rename to util/vec.mli