diff --git a/.gitignore b/.gitignore index 06560aa5..cb485aab 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,4 @@ tests/main .*.swp .session *.docdir +util/log.ml diff --git a/META b/META index 30e06fbb..f2ed910c 100644 --- a/META +++ b/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" diff --git a/Makefile b/Makefile index d0cde415..8f9cdbab 100644 --- a/Makefile +++ b/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 diff --git a/_tags b/_tags index ee34cae3..26f4f35a 100644 --- a/_tags +++ b/_tags @@ -1,5 +1,5 @@ -: for-pack(Msat), package(unix) -: package(unix) +: for-pack(Msat) +#: : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) @@ -10,6 +10,7 @@ #: inline(50) #: inline(100) #: inline(100) +: inline(30) # more warnings <**/*.ml>: warn_K, warn_Y, warn_X diff --git a/msat.mlpack b/msat.mlpack index ffd5248e..e53a1fc2 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -2,7 +2,6 @@ Log # Interface definitions -Log_intf Formula_intf Theory_intf Plugin_intf diff --git a/opam b/opam index eb0bf60a..d58df2f7 100644 --- a/opam +++ b/opam @@ -15,7 +15,7 @@ remove: [ ] depends: [ "ocamlfind" {build} - "base-unix" + "ocamlbuild" {build} ] available: [ ocaml-version >= "4.02.1" diff --git a/sat/sat.ml b/sat/sat.ml index 6348ffe4..6c806f22 100644 --- a/sat/sat.ml +++ b/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 ()); *) diff --git a/sat/sat.mli b/sat/sat.mli index c1adecf0..7f2f0a05 100644 --- a/sat/sat.mli +++ b/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. *) diff --git a/smt/mcsat.ml b/smt/mcsat.ml index ed2e53fc..911b4dba 100644 --- a/smt/mcsat.ml +++ b/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; - List.iter (fun s -> Log.debug 10 " |- %s" s) l; + Log.debugf 10 "@[<2>Expl : %s; %s@ %a@]" + (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", [] diff --git a/smt/smt.ml b/smt/smt.ml index ce92f16c..8658ceed 100644 --- a/smt/smt.ml +++ b/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; - List.iter (fun s -> Log.debug 10 " |- %s" s) l; + Log.debugf 10 "@[Expl : %s; %s@ %a@]" + (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 diff --git a/solver/internal.ml b/solver/internal.ml index 98d2ecf7..b6a81f6b 100644 --- a/solver/internal.ml +++ b/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:"; - L.debug 5 " %a" St.pp_clause confl; + Log.debugf 5 "@[Unsat conflict: %a@]" (fun k -> k 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:"; - for i = 0 to Vec.size env.elt_queue - 1 do - L.debug 99 "%s%s%d -- %a" - (if i = ul.ul_elt_lvl then "*" else " ") - (if i = ul.ul_th_lvl then "*" else " ") - i (fun fmt e -> - destruct e (St.pp_lit fmt) (St.pp_atom fmt)) (Vec.get env.elt_queue i) - done; + Log.debugf 99 "@[Current trail:@ %a@]" + (fun k-> + let pp out () = + for i = 0 to Vec.size env.elt_queue - 1 do + Format.fprintf out "%s%s%d -- %a@," + (if i = ul.ul_elt_lvl then "*" else " ") + (if i = ul.ul_th_lvl then "*" else " ") + 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 diff --git a/solver/internal.mli b/solver/internal.mli index 99bc6c0e..ec8c16a7 100644 --- a/solver/internal.mli +++ b/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. *) diff --git a/solver/log_intf.ml b/solver/log_intf.ml deleted file mode 100644 index 5636255b..00000000 --- a/solver/log_intf.ml +++ /dev/null @@ -1,6 +0,0 @@ - -module type S = sig - val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a - (** debug message *) -end - diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 9ebf753e..f50d6c7d 100644 --- a/solver/mcsolver.ml +++ b/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 diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 2a7bb2a0..26a0e92a 100644 --- a/solver/mcsolver.mli +++ b/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. *) diff --git a/solver/res.ml b/solver/res.ml index 89c9af0b..e4e951fa 100644 --- a/solver/res.ml +++ b/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 :"; - L.debug 10 " - %a" St.pp_clause c; - L.debug 10 " - %a" St.pp_clause d; + Log.debugf 7 "@[ Resolving clauses : %a@,%a@]" + (fun k -> k St.pp_clause c 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; } diff --git a/solver/res.mli b/solver/res.mli index 382e5291..5781ec3a 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -6,8 +6,5 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : - functor (L : Log_intf.S) -> - functor (St : Solver_types.S) -> - S with module St = St +module Make : functor (St : Solver_types.S) -> S with module St = St (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/solver.ml b/solver/solver.ml index b8f2bb5f..020ba371 100644 --- a/solver/solver.ml +++ b/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 diff --git a/solver/solver.mli b/solver/solver.mli index 629f5eba..a6ab67e5 100644 --- a/solver/solver.mli +++ b/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. *) diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 384ffc8a..aeb88a0b 100644 --- a/solver/solver_types.ml +++ b/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 - | History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v - | Lemma _ -> bprintf b "th_lemma" + let pp_premise out = function + | History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v + | 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 = - bprintf b "%d [lit:%s]%a" - (v.lid+1) (Log.on_fmt E.Term.print v.term) pp_assign v.assigned + let pp_lit out v = + Format.fprintf out "%d [lit:%a]%a" + (v.lid+1) E.Term.print v.term pp_assign v.assigned - let pp_atom b a = - bprintf b "%s%d%s[lit:%s]" - (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit) + let pp_atom out a = + Format.fprintf out "%s%d%s[lit:%a]" + (sign a) (a.var.vid+1) (value a) E.Formula.print a.lit - let pp_atoms_vec b vec = - for i = 0 to Vec.size vec - 1 do - bprintf b "%a ; " pp_atom (Vec.get vec i) - done + let pp_atoms_vec out vec = + Vec.print ~sep:"; " pp_atom out vec - let pp_clause b {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 + let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} = + 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 - include McMake(L)(struct +module SatMake (E : Formula_intf.S) = struct + include McMake(struct include E module Term = E module Formula = E diff --git a/solver/solver_types.mli b/solver/solver_types.mli index 9508254e..58b5efc3 100644 --- a/solver/solver_types.mli +++ b/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. *) diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml index fa056407..a3543d08 100644 --- a/solver/solver_types_intf.ml +++ b/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_atom : Buffer.t -> atom -> unit - val pp_clause : Buffer.t -> clause -> unit + val pp_lit : Format.formatter -> lit -> unit + val pp_atom : Format.formatter -> atom -> unit + val pp_clause : Format.formatter -> clause -> unit (** Debug function for atoms and clauses (very verbose) *) end diff --git a/util/log.ml b/util/log.ml deleted file mode 100644 index 6162952d..00000000 --- a/util/log.ml +++ /dev/null @@ -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 () diff --git a/util/log.ml b/util/log.ml new file mode 120000 index 00000000..58df3ad5 --- /dev/null +++ b/util/log.ml @@ -0,0 +1 @@ +log_dummy.ml \ No newline at end of file diff --git a/util/log.mli b/util/log.mli index 88da899f..6b96e256 100644 --- a/util/log.mli +++ b/util/log.mli @@ -1,35 +1,24 @@ (* -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. +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes *) -(** {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 -(** debug message *) +val debugf : + 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 on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string +val debug : int -> string -> unit +(** Simpler version of {!debug}, without formatting *) + +val set_debug_out : Format.formatter -> unit +(** Change the output formatter. *) diff --git a/util/log_dummy.ml b/util/log_dummy.ml new file mode 100644 index 00000000..554e3c2f --- /dev/null +++ b/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 _ = () diff --git a/util/log_real.ml b/util/log_real.ml new file mode 100644 index 00000000..3c0e4878 --- /dev/null +++ b/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) diff --git a/util/timer.ml b/util/timer.ml deleted file mode 100644 index 4122d1ba..00000000 --- a/util/timer.ml +++ /dev/null @@ -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 diff --git a/util/timer.mli b/util/timer.mli deleted file mode 100644 index 7e244b57..00000000 --- a/util/timer.mli +++ /dev/null @@ -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 diff --git a/util/vec.ml b/util/vec.ml index 6e2a83ca..78a16661 100644 --- a/util/vec.ml +++ b/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 static inline void remove(V& ts, const T& t) diff --git a/util/vec.mli b/util/vec.mli index 6ad3a3fb..3ac400e6 100644 --- a/util/vec.mli +++ b/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