update Log interface, with real/dummy implementation

- `make disable_log` to use the dummy
- `make enable_log` to use the real one (slower)

.gitignore

@@ -7,3 +7,4 @@ tests/main
 .*.swp
 .session
 *.docdir
+util/log.ml

Makefile

@@ -27,6 +27,12 @@ test: build-test
 	@/usr/bin/time -f "%e" ./tests/run smt
 	@/usr/bin/time -f "%e" ./tests/run mcsat
 
+enable_log:
+	cd util; ln -sf log_real.ml log.ml
+
+disable_log:
+	cd util; ln -sf log_dummy.ml log.ml
+
 bench: build-test
 	cd bench && $(MAKE)
 
@@ -51,4 +57,4 @@ reinstall: all
 	ocamlfind remove msat || true
 	ocamlfind install msat $(TO_INSTALL)
 
-.PHONY: clean doc all bench install uninstall reinstall
+.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log

_tags

@@ -10,6 +10,7 @@
 #<solver/*.cmx>: inline(50)
 #<sat/**/*.cmx>: inline(100)
 #<smt/**/*.cmx>: inline(100)
+<util/log.cmx>: inline(30)
 
 # more warnings
 <**/*.ml>: warn_K, warn_Y, warn_X

msat.mlpack

@@ -2,7 +2,6 @@
 Log
 
 # Interface definitions
-Log_intf
 Formula_intf
 Theory_intf
 Plugin_intf

util/log.ml

@@ -1,48 +0,0 @@
-(*
-Copyright (c) 2013, Simon Cruanes
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-Redistributions of source code must retain the above copyright notice, this
-list of conditions and the following disclaimer.  Redistributions in binary
-form must reproduce the above copyright notice, this list of conditions and the
-following disclaimer in the documentation and/or other materials provided with
-the distribution.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
-ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
-FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
-SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
-OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-*)
-
-(** {1 Some helpers} *)
-let debug_level_ = ref 0
-let set_debug l = debug_level_ := l
-let get_debug () = !debug_level_
-let _dummy_buf = Buffer.create 0  (* dummy buffer, never used *)
-let debug l format =
-  if l <= !debug_level_
-  then (
-    let b = Buffer.create 64 in
-    Printf.kbprintf
-      (fun b -> print_endline (Buffer.contents b))
-      b format)
-  else
-    Printf.ifprintf _dummy_buf format
-
-let on_buffer pp x =
-  let buf = Buffer.create 24 in
-  pp buf x;
-  Buffer.contents buf
-
-let on_fmt pp x =
-  let _ = pp Format.str_formatter x in
-  Format.flush_str_formatter ()

util/log.ml

@@ -0,0 +1 @@
+log_dummy.ml

util/log.mli

@@ -1,35 +1,24 @@
 (*
-Copyright (c) 2013, Simon Cruanes
+MSAT is free software, using the Apache license, see file LICENSE
-All rights reserved.
+Copyright 2014 Guillaume Bury
-
+Copyright 2014 Simon Cruanes
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-Redistributions of source code must retain the above copyright notice, this
-list of conditions and the following disclaimer.  Redistributions in binary
-form must reproduce the above copyright notice, this list of conditions and the
-following disclaimer in the documentation and/or other materials provided with
-the distribution.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
-ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
-FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
-SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
-OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
-(** {1 Some helpers} *)
+(** {1 Logging function, for debugging} *)
 
 val set_debug : int -> unit     (** Set debug level *)
 val get_debug : unit -> int     (** Current debug level *)
 
-val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a
+val debugf :
-(** debug message *)
+  int ->
+  ('a, Format.formatter, unit, unit) format4 ->
+  ('a -> unit) ->
+  unit
+(** Emit a debug message at the given level. If the level is lower
+    than [get_debug ()], the message will indeed be emitted *)
 
-val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string
+val debug : int -> string -> unit
-val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string
+(** Simpler version of {!debug}, without formatting *)
+
+val set_debug_out : Format.formatter -> unit
+(** Change the output formatter. *)

util/log_dummy.ml

@@ -0,0 +1,18 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 Logging functions, dummy version}
+
+    This does nothing. *)
+
+let debug_level_ = ref 0
+let set_debug l = debug_level_ := l
+let get_debug () = !debug_level_
+
+let debugf _ _ _ = ()
+let debug _ _ = ()
+
+let set_debug_out _ = ()

util/log_real.ml

@@ -0,0 +1,24 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** {1 Logging functions, real version} *)
+
+let debug_level_ = ref 0
+let set_debug l = debug_level_ := l
+let get_debug () = !debug_level_
+
+let debug_fmt_ = ref Format.err_formatter
+
+let set_debug_out f = debug_fmt_ := f
+
+let debugf l format k =
+  if l <= !debug_level_
+  then
+    k (Format.kfprintf
+        (fun fmt -> Format.fprintf fmt "@]@.")
+        !debug_fmt_ format)
+
+let debug l msg = debugf l "%s" (fun k->k msg)