moved vec, iheap, etc. from common/ to util/;

removed dependency of util/ on unix,str

.merlin

@@ -0,0 +1,6 @@
+S sat
+S smt
+S util
+B _build/sat
+B _build/smt
+B _build/util

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

_tags

@@ -1,8 +1,8 @@
-<smt/*.cmx>: for-pack(Msat)
+<smt/*.cmx>: for-pack(Msat), package(zarith)
 <sat/*.cmx>: for-pack(Msat)
 
 # enable stronger inlining everywhere
-<common/**/*.cmx>: inline(15)
+<util/{vec,hashcons,hstring,iheap}.cmx>: inline(15)
 <sat/**/*.cmx>: inline(10)
 <smt/**/*.cmx>: inline(10)
 

common/.merlin

@@ -1,4 +0,0 @@
-S ./
-
-B ../_build/
-B ../_build/common/

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) =
+let on_fmt pp x =
-  px buf x;
+  pp Format.str_formatter x;
-  Buffer.add_string buf sep;
+  Format.flush_str_formatter ()
-  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

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 on_fmt : (Format.formatter -> 'a -> 'b) -> '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

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 =

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