From facfe336a1c03cf6255a224f21193979d9b27435 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 20 Jan 2016 20:06:56 +0100 Subject: [PATCH 1/4] add `eval_level` in the API of the SAT solver --- sat/sat.ml | 1 + sat/sat.mli | 6 ++++++ solver/internal.ml | 7 +++++-- solver/internal.mli | 6 ++++++ solver/solver.mli | 6 ++++++ 5 files changed, 24 insertions(+), 2 deletions(-) diff --git a/sat/sat.ml b/sat/sat.ml index 6348ffe4..c1c6b2a8 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -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..986d7682 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -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/solver/internal.ml b/solver/internal.ml index 194ec234..0e0c857b 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -941,11 +941,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 diff --git a/solver/internal.mli b/solver/internal.mli index 99bc6c0e..b391a343 100644 --- a/solver/internal.mli +++ b/solver/internal.mli @@ -31,6 +31,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/solver.mli b/solver/solver.mli index 629f5eba..12c6d2e8 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -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. *) From 6e5d737b42abf6dc7fe95dd4c959618e959b9837 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 20 Jan 2016 20:13:32 +0100 Subject: [PATCH 2/4] get rid of dependency on unix --- META | 2 +- _tags | 4 ++-- opam | 2 +- util/timer.ml | 35 ----------------------------------- util/timer.mli | 20 -------------------- 5 files changed, 4 insertions(+), 59 deletions(-) delete mode 100644 util/timer.ml delete mode 100644 util/timer.mli 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/_tags b/_tags index ee34cae3..05d4a2a6 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) 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/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 From 2fe5be8317d43593cb45f3a56adeb1d2da2e417b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 20 Jan 2016 21:03:34 +0100 Subject: [PATCH 3/4] update Log interface, with real/dummy implementation - `make disable_log` to use the dummy - `make enable_log` to use the real one (slower) --- .gitignore | 1 + Makefile | 8 +++++++- _tags | 1 + msat.mlpack | 1 - util/log.ml | 49 +---------------------------------------------- util/log.mli | 43 ++++++++++++++++------------------------- util/log_dummy.ml | 18 +++++++++++++++++ util/log_real.ml | 24 +++++++++++++++++++++++ 8 files changed, 68 insertions(+), 77 deletions(-) mode change 100644 => 120000 util/log.ml create mode 100644 util/log_dummy.ml create mode 100644 util/log_real.ml 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/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 05d4a2a6..26f4f35a 100644 --- a/_tags +++ b/_tags @@ -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/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) From 756363ffd6b669fef95c9185b9f9a647ef88ee4e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 20 Jan 2016 21:05:22 +0100 Subject: [PATCH 4/4] everwhere, use new Log interface and remove the functor on `Log_intf` --- sat/sat.ml | 4 +-- sat/sat.mli | 2 +- smt/mcsat.ml | 9 ++++--- smt/smt.ml | 9 ++++--- solver/internal.ml | 49 +++++++++++++++++++++---------------- solver/internal.mli | 1 - solver/log_intf.ml | 6 ----- solver/mcsolver.ml | 6 ++--- solver/mcsolver.mli | 2 +- solver/res.ml | 30 +++++++++++------------ solver/res.mli | 1 - solver/solver.ml | 6 ++--- solver/solver.mli | 2 +- solver/solver_types.ml | 39 ++++++++++++++--------------- solver/solver_types.mli | 2 -- solver/solver_types_intf.ml | 6 ++--- util/vec.ml | 8 ++++++ util/vec.mli | 4 +++ 18 files changed, 98 insertions(+), 88 deletions(-) delete mode 100644 solver/log_intf.ml diff --git a/sat/sat.ml b/sat/sat.ml index c1c6b2a8..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 diff --git a/sat/sat.mli b/sat/sat.mli index 986d7682..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 diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 6514ea08..3ffe265d 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 fc630713..a5310b3e 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 0e0c857b..18a9277a 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 @@ -268,7 +267,8 @@ module Make | Bcp (Some cl) -> atoms, false, max lvl cl.c_level | Semantic 0 -> atoms, init, 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, init, lvl @@ -334,7 +334,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; @@ -388,7 +388,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 @@ -397,7 +397,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 = @@ -450,7 +451,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 @@ -585,14 +586,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 init then init0 else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History [init0]) 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 @@ -605,10 +606,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 @@ -987,7 +989,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 @@ -1041,14 +1043,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 @@ -1072,7 +1079,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 b391a343..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 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 d6d7b504..417efc19 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 @@ -65,8 +65,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct (* 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 + | [a] -> St.pp_atom fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.pp_atom a print_cl r (* Compute resolution of 2 clauses *) let resolve l = @@ -101,7 +101,7 @@ 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 let print_clause fmt c = print_cl fmt (to_list c) @@ -122,9 +122,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let is_proven c = is_proved (c, to_list c) let add_res (c, cl_c) (d, cl_d) = - L.debug 7 " Resolving clauses :"; - L.debug 7 " %a" St.pp_clause c; - L.debug 7 " %a" St.pp_clause d; + Log.debugf 7 "@[ Resolving clauses : %a@,%a@]" + (fun k->k St.pp_clause c St.pp_clause d); assert (is_proved (c, cl_c)); assert (is_proved (d, cl_d)); let l = merge cl_c cl_d in @@ -135,7 +134,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct H.add !proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) (max c.St.c_level d.St.c_level) in - L.debug 5 "New clause : %a" St.pp_clause new_c; + Log.debugf 5 "@[<2>New clause :@ @[%a@]@]" (fun k->k St.pp_clause new_c); new_c, new_clause | _ -> raise (Resolution_error "Resolved to a tautology") @@ -165,9 +164,9 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *) match l with | a :: r -> - L.debug 5 "Resolving (with history) %a" St.pp_clause c; + Log.debugf 5 "Resolving (with history) %a" (fun k->k St.pp_clause c); let temp_c, temp_cl = List.fold_left add_res a r in - L.debug 10 " Switching to unit resolutions"; + Log.debug 10 " Switching to unit resolutions"; let new_c, new_cl = (ref temp_c, ref temp_cl) in while not (equal_cl cl !new_cl) do let unit_to_use = diff_learnt [] cl !new_cl in @@ -197,14 +196,14 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct end let prove c = - L.debug 3 "Proving : %a" St.pp_clause c; + Log.debugf 3 "Proving : %a" (fun k->k St.pp_clause c); do_clause [c]; - L.debug 3 "Proved : %a" St.pp_clause c + Log.debugf 3 "Proved : %a" (fun k->k St.pp_clause c) let rec prove_unsat_cl (c, cl) = match cl with | [] -> true | a :: r -> - L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; + Log.debugf 2 "Eliminating %a in %a" (fun k->k St.pp_atom a St.pp_clause c); let d = match St.(a.var.level, a.var.reason) with | 0, St.Bcp Some d -> d | _ -> raise Exit @@ -220,11 +219,12 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct false let learn v = - Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v; + Log.debugf 15 "@[<2>history : @[%a@]@]" + (fun k->k (Vec.print ~sep:"" St.pp_clause) v); Vec.iter prove v let assert_can_prove_unsat c = - L.debug 1 "=================== Proof ====================="; + Log.debug 1 "=================== Proof ====================="; prove c; if not (prove_unsat_cl (c, to_list c)) then raise Insuficient_hyps diff --git a/solver/res.mli b/solver/res.mli index 6fe8f9e9..ebfe5cfe 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -7,7 +7,6 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S module Make : - functor (L : Log_intf.S) -> functor (St : Solver_types.S) -> sig include S with module St = St val push : unit -> int 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 12c6d2e8..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. *) diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 3d0e5fd6..0462ad28 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 133a1ddc..bd7a09a8 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/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