diff --git a/src/backend/backend_intf.ml b/src/backend/Backend_intf.ml similarity index 100% rename from src/backend/backend_intf.ml rename to src/backend/Backend_intf.ml diff --git a/src/backend/coq.ml b/src/backend/Coq.ml similarity index 100% rename from src/backend/coq.ml rename to src/backend/Coq.ml diff --git a/src/backend/coq.mli b/src/backend/Coq.mli similarity index 100% rename from src/backend/coq.mli rename to src/backend/Coq.mli diff --git a/src/backend/dedukti.ml b/src/backend/Dedukti.ml similarity index 100% rename from src/backend/dedukti.ml rename to src/backend/Dedukti.ml diff --git a/src/backend/dedukti.mli b/src/backend/Dedukti.mli similarity index 100% rename from src/backend/dedukti.mli rename to src/backend/Dedukti.mli diff --git a/src/backend/dimacs.ml b/src/backend/Dimacs.ml similarity index 100% rename from src/backend/dimacs.ml rename to src/backend/Dimacs.ml diff --git a/src/backend/dimacs.mli b/src/backend/Dimacs.mli similarity index 100% rename from src/backend/dimacs.mli rename to src/backend/Dimacs.mli diff --git a/src/backend/dot.ml b/src/backend/Dot.ml similarity index 100% rename from src/backend/dot.ml rename to src/backend/Dot.ml diff --git a/src/backend/dot.mli b/src/backend/Dot.mli similarity index 100% rename from src/backend/dot.mli rename to src/backend/Dot.mli diff --git a/src/core/expr_intf.ml b/src/core/Expr_intf.ml similarity index 100% rename from src/core/expr_intf.ml rename to src/core/Expr_intf.ml diff --git a/src/core/external.ml b/src/core/External.ml similarity index 100% rename from src/core/external.ml rename to src/core/External.ml diff --git a/src/core/external.mli b/src/core/External.mli similarity index 100% rename from src/core/external.mli rename to src/core/External.mli diff --git a/src/core/formula_intf.ml b/src/core/Formula_intf.ml similarity index 100% rename from src/core/formula_intf.ml rename to src/core/Formula_intf.ml diff --git a/src/core/internal.ml b/src/core/Internal.ml similarity index 100% rename from src/core/internal.ml rename to src/core/Internal.ml diff --git a/src/core/internal.mli b/src/core/Internal.mli similarity index 100% rename from src/core/internal.mli rename to src/core/Internal.mli diff --git a/src/core/Log.ml b/src/core/Log.ml new file mode 100644 index 00000000..f60603ea --- /dev/null +++ b/src/core/Log.ml @@ -0,0 +1,33 @@ +(* +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 enabled = true (* NOTE: change here for 0-overhead *) + +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 + +(* does the printing, inconditionally *) +let debug_real_ l k = + k (fun fmt -> + Format.fprintf !debug_fmt_ "@[<2>@{[%d|%.3f]@}@ " + l (Sys.time()); + Format.kfprintf + (fun fmt -> Format.fprintf fmt "@]@.") + !debug_fmt_ fmt) + +let[@inline] debugf l k = + if enabled && l <= !debug_level_ then ( + debug_real_ l k; + ) + +let[@inline] debug l msg = debugf l (fun k->k "%s" msg) diff --git a/src/util/log.mli b/src/core/Log.mli similarity index 72% rename from src/util/log.mli rename to src/core/Log.mli index c60916bc..8923f8e3 100644 --- a/src/util/log.mli +++ b/src/core/Log.mli @@ -6,13 +6,14 @@ Copyright 2014 Simon Cruanes (** {1 Logging function, for debugging} *) -val set_debug : int -> unit (** Set debug level *) -val get_debug : unit -> int (** Current debug level *) +val enabled : bool + +val set_debug : int -> unit (** Set debug level *) +val get_debug : unit -> int (** Current debug level *) val debugf : int -> - ('a, Format.formatter, unit, unit) format4 -> - ('a -> unit) -> + ((('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 *) diff --git a/src/core/plugin_intf.ml b/src/core/Plugin_intf.ml similarity index 100% rename from src/core/plugin_intf.ml rename to src/core/Plugin_intf.ml diff --git a/src/core/res.ml b/src/core/Res.ml similarity index 100% rename from src/core/res.ml rename to src/core/Res.ml diff --git a/src/core/res.mli b/src/core/Res.mli similarity index 100% rename from src/core/res.mli rename to src/core/Res.mli diff --git a/src/core/res_intf.ml b/src/core/Res_intf.ml similarity index 100% rename from src/core/res_intf.ml rename to src/core/Res_intf.ml diff --git a/src/core/solver_intf.ml b/src/core/Solver_intf.ml similarity index 100% rename from src/core/solver_intf.ml rename to src/core/Solver_intf.ml diff --git a/src/core/solver_types.ml b/src/core/Solver_types.ml similarity index 100% rename from src/core/solver_types.ml rename to src/core/Solver_types.ml diff --git a/src/core/solver_types.mli b/src/core/Solver_types.mli similarity index 100% rename from src/core/solver_types.mli rename to src/core/Solver_types.mli diff --git a/src/core/solver_types_intf.ml b/src/core/Solver_types_intf.ml similarity index 100% rename from src/core/solver_types_intf.ml rename to src/core/Solver_types_intf.ml diff --git a/src/core/theory_intf.ml b/src/core/Theory_intf.ml similarity index 100% rename from src/core/theory_intf.ml rename to src/core/Theory_intf.ml diff --git a/src/core/jbuild b/src/core/jbuild new file mode 100644 index 00000000..777d98f1 --- /dev/null +++ b/src/core/jbuild @@ -0,0 +1,15 @@ +; vim:ft=lisp: + +(jbuild_version 1) + +; main binary +(library + ((name msat) + (public_name msat) + (synopsis "core data structures and algorithms for msat") + (libraries ()) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) + (ocamlopt_flags (:standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20)) + )) + diff --git a/src/util/log.ml b/src/util/log.ml deleted file mode 120000 index e4261c8e..00000000 --- a/src/util/log.ml +++ /dev/null @@ -1 +0,0 @@ -log_real.ml \ No newline at end of file diff --git a/src/util/log_dummy.ml b/src/util/log_dummy.ml deleted file mode 100644 index 554e3c2f..00000000 --- a/src/util/log_dummy.ml +++ /dev/null @@ -1,18 +0,0 @@ -(* -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 _ = () diff --git a/src/util/log_real.ml b/src/util/log_real.ml deleted file mode 100644 index 8ab71503..00000000 --- a/src/util/log_real.ml +++ /dev/null @@ -1,24 +0,0 @@ -(* -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)