Merge branch 'master' of github.com:Gbury/mSAT

.gitignore

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

META

@@ -1,7 +1,7 @@
 name="msat"
 version="dev"
 description="MSAT is a modular SAT solver, plus extensions"
-requires="num unix"
+requires=""
 archive(byte) = "msat.cma"
 archive(byte, plugin) = "msat.cma"
 archive(native) = "msat.cmxa"

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

@@ -1,5 +1,5 @@
-<util/*.cmx>: for-pack(Msat), package(unix)
+<util/*.cmx>: for-pack(Msat)
-<util/*.native>: package(unix)
+#<util/*.native>: 
 <smt/*.cmx>: for-pack(Msat)
 <sat/*.cmx>: for-pack(Msat)
 <solver/*.cmx>: for-pack(Msat)
@@ -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

opam

@@ -15,7 +15,7 @@ remove: [
 ]
 depends: [
   "ocamlfind" {build}
-  "base-unix"
+  "ocamlbuild" {build}
 ]
 available: [
   ocaml-version >= "4.02.1"

sat/sat.ml

@@ -88,9 +88,9 @@ module Tsat = struct
 
 end
 
-module Make(Log : Log_intf.S) = struct
+module Make(Dummy : sig end) = struct
 
-  module SatSolver = Solver.Make(Log)(Fsat)(Tsat)
+  module SatSolver = Solver.Make(Fsat)(Tsat)
   module Dot = Dot.Make(SatSolver.Proof)(struct
       let clause_name c = SatSolver.St.(c.name)
       let print_atom = SatSolver.St.print_atom
@@ -146,6 +146,7 @@ module Make(Log : Log_intf.S) = struct
     with SatSolver.Unsat -> ()
 
   let eval = SatSolver.eval
+  let eval_level = SatSolver.eval_level
 
   let get_proof () =
     (* SatSolver.Proof.learn (SatSolver.history ()); *)

sat/sat.mli

@@ -8,7 +8,7 @@ module Fsat : Formula_intf.S with type t = private int
 
 module Tseitin : Tseitin.S with type atom = Fsat.t
 
-module Make(Log: Log_intf.S) : sig
+module Make(Dummy : sig end) : sig
   (** Fonctor to make a pure SAT Solver module with built-in literals. *)
 
   exception Bad_atom
@@ -57,6 +57,12 @@ module Make(Log: Log_intf.S) : sig
   val eval : atom -> bool
   (** Return the current assignement of the literals. *)
 
+  val eval_level : atom -> bool * int
+  (** Return the current assignement of the literals, as well as its
+      decision level. If the level is 0, then it is necessary for
+      the atom to have this value; otherwise it is due to choices
+      that can potentially be backtracked. *)
+
   val assume : ?tag:int -> atom list list -> unit
   (** Add a list of clauses to the set of assumptions. *)
 

smt/mcsat.ml

@@ -49,8 +49,9 @@ module Tsmt = struct
   let current_level () = !env
 
   let to_clause (a, b, l) =
-    Log.debug 10 "Expl : %s; %s" a b;
+    Log.debugf 10 "@[<2>Expl : %s; %s@ %a@]"
-    List.iter (fun s -> Log.debug 10 " |- %s" s) l;
+      (fun k->k a b
+        (fun out () -> List.iter (Format.fprintf out " |- %s@ ") l) ());
     let rec aux acc = function
       | [] | [_] -> acc
       | x :: ((y :: _) as r) ->
@@ -65,7 +66,7 @@ module Tsmt = struct
         | (Assign (x, v)), lvl ->
           env := { !env with assign = M.add x (v, lvl) !env.assign }
         | Lit f, _ ->
-          Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f);
+          Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print f);
           match f with
           | Fsmt.Prop _ -> ()
           | Fsmt.Equal (i, j) ->
@@ -110,7 +111,7 @@ end
 
 module Make(Dummy:sig end) = struct
 
-  module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
+  module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)
   module Dot = Dot.Make(SmtSolver.Proof)(struct
       let print_atom = SmtSolver.St.print_atom
       let lemma_info () = "Proof", Some "PURPLE", []

smt/smt.ml

@@ -31,8 +31,9 @@ module Tsmt = struct
   let current_level () = !env
 
   let to_clause (a, b, l) =
-    Log.debug 10 "Expl : %s; %s" a b;
+    Log.debugf 10 "@[Expl : %s; %s@ %a@]"
-    List.iter (fun s -> Log.debug 10 " |- %s" s) l;
+      (fun k->k a b
+        (fun out () -> List.iter (Format.fprintf out "|- %s@ ") l) ());
     let rec aux acc = function
       | [] | [_] -> acc
       | x :: ((y :: _) as r) ->
@@ -43,7 +44,7 @@ module Tsmt = struct
   let assume s =
     try
       for i = s.start to s.start + s.length - 1 do
-        Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i));
+        Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i));
         match s.get i with
         | Fsmt.Prop _ -> ()
         | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
@@ -60,7 +61,7 @@ end
 
 module Make(Dummy:sig end) = struct
 
-  module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt)
+  module SmtSolver = Solver.Make(Fsmt)(Tsmt)
   module Dot = Dot.Make(SmtSolver.Proof)(struct
       let clause_name c = SmtSolver.St.(c.name)
       let print_atom = SmtSolver.St.print_atom

solver/internal.ml

@@ -5,12 +5,11 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make
-    (L : Log_intf.S)
     (St : Solver_types.S)
     (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
 = struct
 
-  module Proof = Res.Make(L)(St)
+  module Proof = Res.Make(St)
 
   open St
 
@@ -266,7 +265,8 @@ module Make
         | Bcp (Some cl) -> atoms, cl :: history, max lvl cl.c_level
         | Semantic 0 -> atoms, history, lvl
         | _ ->
-          L.debug 0 "Unexpected semantic propagation at level 0: %a" St.pp_atom a;
+          Log.debugf 0 "Unexpected semantic propagation at level 0: %a"
+            (fun k->k St.pp_atom a);
           assert false
       end else
         a::atoms, history, lvl
@@ -332,7 +332,7 @@ module Make
       env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
 
   let detach_clause c =
-    L.debug 10 "Removing clause %a" St.pp_clause c;
+    Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
     c.removed <- true;
     (* Not necessary, cleanup is done during propagation
        Vec.remove (Vec.get c.atoms 0).neg.watched c;
@@ -381,8 +381,7 @@ module Make
     ()
 
   let report_unsat ({atoms=atoms} as confl) =
-    L.debug 5 "Unsat conflict:";
+    Log.debugf 5 "@[Unsat conflict: %a@]" (fun k -> k St.pp_clause confl);
-    L.debug 5 " %a" St.pp_clause confl;
     env.unsat_conflict <- Some confl;
     raise Unsat
 
@@ -401,7 +400,7 @@ module Make
 
   let enqueue_bool a lvl reason =
     if a.neg.is_true then begin
-      L.debug 0 "Trying to enqueue a false litteral: %a" St.pp_atom a;
+      Log.debugf 0 "Trying to enqueue a false litteral: %a" (fun k->k St.pp_atom a);
       assert false
     end;
     if not a.is_true then begin
@@ -414,7 +413,8 @@ module Make
       a.var.level <- lvl;
       a.var.reason <- reason;
       Vec.push env.elt_queue (of_atom a);
-      L.debug 20 "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_atom a
+      Log.debugf 20 "Enqueue (%d): %a"
+        (fun k->k (Vec.size env.elt_queue) pp_atom a)
     end
 
   let enqueue_assign v value lvl =
@@ -467,7 +467,7 @@ module Make
           raise Exit
         | _ ->
           decr tr_ind;
-          L.debug 20 "Looking at trail element %d" !tr_ind;
+          Log.debugf 20 "Looking at trail element %d" (fun k->k !tr_ind);
           destruct (Vec.get env.elt_queue !tr_ind)
             (fun _ -> ()) (* TODO remove *)
             (fun a -> match a.var.reason with
@@ -611,14 +611,14 @@ module Make
       let size = List.length atoms in
       match atoms with
       | [] ->
-        L.debug 1 "New clause (unsat) : %a" St.pp_clause init0;
+        Log.debugf 1 "New clause (unsat) :@ @[%a@]" (fun k->k St.pp_clause init0);
         report_unsat init0
       | a::b::_ ->
         let clause =
           if history = [] then init0
           else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History (init0 :: history)) level
         in
-        L.debug 4 "New clause: %a" St.pp_clause clause;
+        Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
         attach_clause clause;
         Vec.push vec clause;
         if a.neg.is_true then begin
@@ -631,10 +631,11 @@ module Make
           enqueue_bool a lvl (Bcp (Some clause))
         end
       | [a]   ->
-        L.debug 5 "New unit clause, propagating : %a" St.pp_atom a;
+        Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a);
         cancel_until 0;
         enqueue_bool a 0 (Bcp (Some init0))
-    with Trivial -> L.debug 5 "Trivial clause ignored : %a" St.pp_clause init0
+    with Trivial ->
+      Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0)
 
   let propagate_in_clause a c i watched new_sz =
     let atoms = c.atoms in
@@ -967,11 +968,14 @@ module Make
     let cnf = List.rev_map (List.rev_map atom) cnf in
     init_solver ?tag cnf
 
-  let eval lit =
+  let eval_level lit =
     let var, negated = make_boolean_var lit in
     assert (var.pa.is_true || var.na.is_true);
     let truth = var.pa.is_true in
-    if negated then not truth else truth
+    let value = if negated then not truth else truth in
+    value, var.level
+
+  let eval lit = fst (eval_level lit)
 
   let hyps () = env.clauses_hyps
 
@@ -1009,7 +1013,7 @@ module Make
 
   (* Backtrack to decision_level 0, with trail_lim && theory env specified *)
   let reset_until push_lvl elt_lvl th_lvl th_env =
-    L.debug 1 "Resetting to decision level 0 (pop/forced)";
+    Log.debug 1 "Resetting to decision level 0 (pop/forced)";
     env.th_head <- th_lvl;
     env.elt_head <- elt_lvl;
     for c = env.elt_head to Vec.size env.elt_queue - 1 do
@@ -1063,14 +1067,19 @@ module Make
       reset_until l ul.ul_elt_lvl ul.ul_th_lvl ul.ul_th_env;
 
       (* Log current assumptions for debugging purposes *)
-      L.debug 99 "Current trail:";
+      Log.debugf 99 "@[<v2>Current trail:@ %a@]"
-      for i = 0 to Vec.size env.elt_queue - 1 do
+        (fun k->
-        L.debug 99 "%s%s%d -- %a"
+          let pp out () =
-          (if i = ul.ul_elt_lvl then "*" else " ")
+            for i = 0 to Vec.size env.elt_queue - 1 do
-          (if i = ul.ul_th_lvl then "*" else " ")
+              Format.fprintf out "%s%s%d -- %a@,"
-          i (fun fmt e ->
+                (if i = ul.ul_elt_lvl then "*" else " ")
-              destruct e (St.pp_lit fmt) (St.pp_atom fmt)) (Vec.get env.elt_queue i)
+                (if i = ul.ul_th_lvl then "*" else " ")
-      done;
+                i (fun fmt e ->
+                  destruct e (St.pp_lit fmt) (St.pp_atom fmt))
+                (Vec.get env.elt_queue i)
+            done
+          in
+          k pp ());
 
       (* Clear hypothesis not valid anymore *)
       for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do
@@ -1091,7 +1100,7 @@ module Make
           | History [ { cpremise = Lemma _ } as c' ] -> Stack.push c' s
           | _ -> () (* Only simplified clauses can have a level > 0 *)
         end else begin
-          L.debug 15 "Keeping intact clause %a" St.pp_clause c;
+          Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c);
           Vec.set env.clauses_learnt !new_sz c;
           incr new_sz
         end

solver/internal.mli

@@ -5,7 +5,6 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make
-  (L : Log_intf.S)
   (St : Solver_types.S)
   (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
 : sig
@@ -31,6 +30,12 @@ module Make
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val eval_level : St.formula -> bool * int
+  (** Return the current assignement of the literals, as well as its
+      decision level. If the level is 0, then it is necessary for
+      the atom to have this value; otherwise it is due to choices
+      that can potentially be backtracked. *)
+
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses. *)

solver/log_intf.ml

@@ -1,6 +0,0 @@
-
-module type S = sig
-  val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a
-  (** debug message *)
-end
-

solver/mcsolver.ml

@@ -4,12 +4,12 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make (L : Log_intf.S)(E : Expr_intf.S)
+module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) = struct
 
-  module St = Solver_types.McMake(L)(E)
+  module St = Solver_types.McMake(E)
 
-  module M = Internal.Make(L)(St)(Th)
+  module M = Internal.Make(St)(Th)
 
   include St
 

solver/mcsolver.mli

@@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Make (L : Log_intf.S)(E : Expr_intf.S)
+module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) : sig
   (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
 

solver/res.ml

@@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
 
 module type S = Res_intf.S
 
-module Make(L : Log_intf.S)(St : Solver_types.S) = struct
+module Make(St : Solver_types.S) = struct
 
   module St = St
 
@@ -23,17 +23,13 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
   let equal_atoms a b = St.(a.aid) = St.(b.aid)
   let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
 
+  let print_clause = St.pp_clause
+
   let merge = List.merge compare_atoms
 
   let _c = ref 0
   let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
 
-  (* Printing functions *)
-  let rec print_cl fmt = function
-    | [] -> Format.fprintf fmt "[]"
-    | [a] -> St.print_atom fmt a
-    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r
-
   (* Compute resolution of 2 clauses *)
   let resolve l =
     let rec aux resolved acc = function
@@ -67,12 +63,9 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     let res = sort_uniq compare_atoms !l in
     let l, _ = resolve res in
     if l <> [] then
-      L.debug 3 "Input clause is a tautology";
+      Log.debug 3 "Input clause is a tautology";
     res
 
-  (* Printing *)
-  let print_clause fmt c = print_cl fmt (to_list c)
-
   (* Comparison of clauses *)
   let cmp_cl c d =
     let rec aux = function
@@ -116,9 +109,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
 
   let rec chain_res (c, cl) = function
     | d :: r ->
-      L.debug 10 " Resolving :";
+      Log.debugf 7 "@[<v4>  Resolving clauses : %a@,%a@]"
-      L.debug 10 "   - %a" St.pp_clause c;
+        (fun k -> k St.pp_clause c St.pp_clause d);
-      L.debug 10 "   - %a" St.pp_clause d;
       let dl = to_list d in
       begin match resolve (merge cl dl) with
       | [ a ], l ->
@@ -134,7 +126,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     | _ -> assert false
 
   let rec expand conclusion =
-    L.debug 5 "Expanding : %a" St.pp_clause conclusion;
+    Log.debugf 5 "@[Expanding : %a@]" (fun k -> k St.pp_clause conclusion);
     match conclusion.St.cpremise with
     | St.Lemma l ->
       {conclusion; step = Lemma l; }

solver/res.mli

@@ -6,8 +6,5 @@ Copyright 2014 Simon Cruanes
 
 module type S = Res_intf.S
 
-module Make :
+module Make : functor (St : Solver_types.S) -> S with module St = St
-  functor (L : Log_intf.S) ->
-  functor (St : Solver_types.S) ->
-    S with module St = St
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)

solver/solver.ml

@@ -10,7 +10,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (L : Log_intf.S)(E : Formula_intf.S)
+module Make (E : Formula_intf.S)
     (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
 
   module Plugin = struct
@@ -70,9 +70,9 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
     let proof_debug _ = assert false
   end
 
-  module St = Solver_types.SatMake(L)(E)
+  module St = Solver_types.SatMake(E)
 
-  module S = Internal.Make(L)(St)(Plugin)
+  module S = Internal.Make(St)(Plugin)
 
   include S
 

solver/solver.mli

@@ -11,7 +11,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (L : Log_intf.S)(F : Formula_intf.S)
+module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : sig
   (** Functor to create a SMT Solver parametrised by the atomic
       formulas and a theory. *)
@@ -38,6 +38,12 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val eval_level : F.t -> bool * int
+  (** Return the current assignement of the literals, as well as its
+      decision level. If the level is 0, then it is necessary for
+      the atom to have this value; otherwise it is due to choices
+      that can potentially be backtracked. *)
+
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses. *)

solver/solver_types.ml

@@ -18,7 +18,7 @@ module type S = Solver_types_intf.S
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
-module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
+module McMake (E : Expr_intf.S) = struct
 
   (* Flag for Mcsat v.s Pure Sat *)
   let mcsat = true
@@ -271,29 +271,28 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
     else if a.neg.is_true then sprintf "[F%s]" (level a)
     else "[]"
 
-  let pp_premise b = function
+  let pp_premise out = function
-    | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v
+    | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
-    | Lemma _ -> bprintf b "th_lemma"
+    | Lemma _ -> Format.fprintf out "th_lemma"
 
-  let pp_assign b = function
+  let pp_assign out = function
     | None -> ()
-    | Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t)
+    | Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t
 
-  let pp_lit b v =
+  let pp_lit out v =
-    bprintf b "%d [lit:%s]%a"
+    Format.fprintf out "%d [lit:%a]%a"
-      (v.lid+1) (Log.on_fmt E.Term.print v.term) pp_assign v.assigned
+      (v.lid+1) E.Term.print v.term pp_assign v.assigned
 
-  let pp_atom b a =
+  let pp_atom out a =
-    bprintf b "%s%d%s[lit:%s]"
+    Format.fprintf out "%s%d%s[lit:%a]"
-      (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)
+      (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
 
-  let pp_atoms_vec b vec =
+  let pp_atoms_vec out vec =
-    for i = 0 to Vec.size vec - 1 do
+    Vec.print ~sep:"; " pp_atom out vec
-      bprintf b "%a ; " pp_atom (Vec.get vec i)
-    done
 
-  let pp_clause b {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
+  let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
-    bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
+    Format.fprintf out "%s%s{ %a} cpremise={{%a}}"
+      name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
 
 end
 
@@ -301,8 +300,8 @@ end
 (* Solver types for pure SAT Solving *)
 (* ************************************************************************ *)
 
-module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
+module SatMake (E : Formula_intf.S) = struct
-  include McMake(L)(struct
+  include McMake(struct
       include E
       module Term = E
       module Formula = E

solver/solver_types.mli

@@ -14,13 +14,11 @@
 module type S = Solver_types_intf.S
 
 module McMake :
-  functor (L : Log_intf.S) ->
   functor (E : Expr_intf.S) ->
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
 module SatMake :
-  functor (L : Log_intf.S) ->
   functor (E : Formula_intf.S) ->
     S with type term = E.t and type formula = E.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)

solver/solver_types_intf.ml

@@ -134,9 +134,9 @@ module type S = sig
   val print_clause : Format.formatter -> clause -> unit
   (** Pretty printing functions for atoms and clauses *)
 
-  val pp_lit : Buffer.t -> lit -> unit
+  val pp_lit : Format.formatter -> lit -> unit
-  val pp_atom : Buffer.t -> atom -> unit
+  val pp_atom : Format.formatter -> atom -> unit
-  val pp_clause : Buffer.t -> clause -> unit
+  val pp_clause : Format.formatter -> clause -> unit
   (** Debug function for atoms and clauses (very verbose) *)
 
 end

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)

util/timer.ml

@@ -1,35 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type S = sig
-  val start : unit -> unit
-  val pause : unit -> unit
-  val get : unit -> float
-end
-
-module Make (X : sig end) = struct
-
-  open Unix
-
-  let u = ref 0.0
-
-  let cpt = ref 0.0
-
-  let start () = u:=(times()).tms_utime
-
-  let pause () = cpt := !cpt +. ((times()).tms_utime -. !u)
-
-  let get () =
-    !cpt
-
-end

util/timer.mli

@@ -1,20 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type S = sig
-  val start : unit -> unit
-  val pause : unit -> unit
-  val get : unit -> float
-end
-
-module Make (X : sig end) : S

util/vec.ml

@@ -161,6 +161,14 @@ let for_all p t =
     true
   with ExitVec -> false
 
+let print ?(sep=", ") pp out v =
+  let first = ref true in
+  iter
+    (fun x ->
+      if !first then first := false else Format.fprintf out "%s@," sep;
+      pp out x)
+    v
+
 (*
 template<class V, class T>
 static inline void remove(V& ts, const T& t)

util/vec.mli

@@ -100,3 +100,7 @@ val exists : ('a -> bool) -> 'a t -> bool
 val for_all : ('a -> bool) -> 'a t -> bool
 (** Do all elements satisfy the predicate? *)
 
+val print :
+  ?sep:string ->
+  (Format.formatter -> 'a -> unit) ->
+  Format.formatter -> 'a t -> unit