From 7a8a6d0de16ca9921d1aab03c6fa846fd0d9bfb1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 1 Nov 2014 16:31:19 +0100 Subject: [PATCH] Few fixes. Sat Solver is working. --- common/vec.ml | 5 ++ common/vec.mli | 1 + sat/.merlin | 1 + sat/explanation.ml | 2 +- sat/formula_intf.ml | 3 +- sat/sat.ml | 9 +-- sat/solver.ml | 37 +++++++++--- sat/solver_types.ml | 24 ++++---- sat/solver_types_intf.ml | 4 +- sat/theory_intf.ml | 3 + util/.merlin | 1 + util/log.ml | 124 +++++++++++++++++++++++++++++++++++++++ util/log.mli | 74 +++++++++++++++++++++++ util/test.ml | 6 +- 14 files changed, 264 insertions(+), 30 deletions(-) create mode 100644 util/log.ml create mode 100644 util/log.mli diff --git a/common/vec.ml b/common/vec.ml index a9522789..4cff679c 100644 --- a/common/vec.ml +++ b/common/vec.ml @@ -113,6 +113,11 @@ let sort t f = Array.fast_sort f sub_arr; t.data <- sub_arr +let iter f t = + for i = 0 to size t - 1 do + f (get t i) + done + (* template static inline void remove(V& ts, const T& t) diff --git a/common/vec.mli b/common/vec.mli index feb4d6cd..8c056b20 100644 --- a/common/vec.mli +++ b/common/vec.mli @@ -36,3 +36,4 @@ val move_to : 'a t -> 'a t -> unit val remove : 'a t -> 'a -> unit val fast_remove : 'a t -> 'a -> unit val sort : 'a t -> ('a -> 'a -> int) -> unit +val iter : ('a -> unit) -> 'a t -> unit diff --git a/sat/.merlin b/sat/.merlin index 167e6845..9350d683 100644 --- a/sat/.merlin +++ b/sat/.merlin @@ -3,4 +3,5 @@ S ../common/ B ../_build/ B ../_build/sat/ +B ../_build/util/ B ../_build/common/ diff --git a/sat/explanation.ml b/sat/explanation.ml index aec8b4f7..08171473 100644 --- a/sat/explanation.ml +++ b/sat/explanation.ml @@ -65,7 +65,7 @@ module Make(Stypes : Solver_types.S) = struct let print fmt ex = fprintf fmt "{"; S.iter (function - | Atom a -> fprintf fmt "%a, " Stypes.pp_atom a + | Atom a -> fprintf fmt "%s, " (Log.on_buffer Stypes.pp_atom a) | Fresh i -> fprintf fmt "Fresh%d " i) ex; fprintf fmt "}" diff --git a/sat/formula_intf.ml b/sat/formula_intf.ml index d0a9b329..0b83f305 100644 --- a/sat/formula_intf.ml +++ b/sat/formula_intf.ml @@ -28,7 +28,8 @@ module type S = sig val norm : t -> t * bool (** Returns a 'normalized' form of the formula, possibly negated (in which case return true). - Note : [fun a -> a, false] is a perfectly reasonnable implementation. *) + WARNING: for the solver to cork correctly, the normalisation function must be so that + [a] and [neg a] normalises to the same formula. *) val hash : t -> int val equal : t -> t -> bool diff --git a/sat/sat.ml b/sat/sat.ml index 57483417..7851bdf5 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -21,7 +21,7 @@ module Fsat = struct let make i = if i > 0 then unsafe_make i else dummy let neg a = { a with pos = not a.pos } - let norm a = a, false + let norm a = unsafe_make a.var, not a.pos let hash = Hashtbl.hash let equal = (=) @@ -57,14 +57,15 @@ module Tsat = struct (* We don't have anything to do since the SAT Solver already * does propagation and conflict detection *) - type t = unit + type t = int type formula = Fsat.t type explanation = Exp.t exception Inconsistent of explanation - let empty () = () - let assume ~cs:_ _ _ _ = () + let dummy = -1 + let empty () = 0 + let assume ~cs:_ _ _ _ = 0 end module Make(Dummy : sig end) = struct diff --git a/sat/solver.ml b/sat/solver.ml index 221d7d0a..4c5a74be 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -136,7 +136,7 @@ module Make (F : Formula_intf.S) nb_init_clauses = 0; model = Vec.make 0 dummy_var; tenv = Th.empty(); - tenv_queue = Vec.make 100 (Th.empty()); + tenv_queue = Vec.make 100 Th.dummy; tatoms_queue = Queue.create (); } @@ -187,11 +187,16 @@ module Make (F : Formula_intf.S) let new_decision_level() = Vec.push env.trail_lim (Vec.size env.trail); - Vec.push env.tenv_queue env.tenv (* save the current tenv *) + Vec.push env.tenv_queue env.tenv; (* save the current tenv *) + Log.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" + (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); + () let attach_clause c = Vec.push (Vec.get c.atoms 0).neg.watched c; Vec.push (Vec.get c.atoms 1).neg.watched c; + Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 0).neg St.pp_clause c; + Log.debug 8 "%a <-- %a" St.pp_atom (Vec.get c.atoms 1).neg St.pp_clause c; if c.learnt then env.learnts_literals <- env.learnts_literals + Vec.size c.atoms else @@ -220,6 +225,7 @@ module Make (F : Formula_intf.S) (* annule tout jusqu'a lvl *exclu* *) let cancel_until lvl = + Log.debug 5 "Bactracking to decision level %d (excluded)" lvl; if decision_level () > lvl then begin env.qhead <- Vec.get env.trail_lim lvl; for c = Vec.size env.trail - 1 downto env.qhead do @@ -232,6 +238,7 @@ module Make (F : Formula_intf.S) insert_var_order a.var done; Queue.clear env.tatoms_queue; + Log.debug 0 "Getting env : %d / %d" lvl (Vec.size env.tenv_queue); env.tenv <- Vec.get env.tenv_queue lvl; (* recover the right tenv *) Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); @@ -245,8 +252,8 @@ module Make (F : Formula_intf.S) if v.level>= 0 then begin assert (v.pa.is_true || v.na.is_true); pick_branch_lit () - end - else v + end else + v let enqueue a lvl reason = assert (not a.is_true && not a.neg.is_true && @@ -256,7 +263,7 @@ module Make (F : Formula_intf.S) a.is_true <- true; a.var.level <- lvl; a.var.reason <- reason; - (*eprintf "enqueue: %a@." Debug.atom a; *) + Log.debug 8 "Enqueue: %a" pp_atom a; Vec.push env.trail a let progress_estimate () = @@ -274,7 +281,7 @@ module Make (F : Formula_intf.S) let propagate_in_clause a c i watched new_sz = let atoms = c.atoms in let first = Vec.get atoms 0 in - if first == a.neg then begin (* le litiral false_ doit etre dans .(1) *) + if first == a.neg then begin (* le literal faux doit etre dans .(1) *) Vec.set atoms 0 (Vec.get atoms 1); Vec.set atoms 1 first end; @@ -293,6 +300,7 @@ module Make (F : Formula_intf.S) Vec.set atoms 1 ak; Vec.set atoms k a.neg; Vec.push ak.neg.watched c; + Log.debug 8 "New watcher (%a) for clause : %a" St.pp_atom ak.neg St.pp_clause c; raise Exit end done; @@ -304,18 +312,23 @@ module Make (F : Formula_intf.S) Vec.set watched !new_sz (Vec.get watched k); incr new_sz; done; + Log.debug 3 "Conflict found : %a" St.pp_clause c; raise (Conflict c) end else begin (* la clause est unitaire *) Vec.set watched !new_sz c; incr new_sz; + Log.debug 5 "Unit clause : %a" St.pp_clause c; enqueue first (decision_level ()) (Some c) end with Exit -> () let propagate_atom a res = + Log.debug 8 "Propagating %a" St.pp_atom a; let watched = a.watched in + Log.debug 10 "Watching %a :" St.pp_atom a; + Vec.iter (fun c -> Log.debug 10 " %a" St.pp_clause c) watched; let new_sz_w = ref 0 in begin try @@ -380,7 +393,6 @@ module Make (F : Formula_intf.S) env.simpDB_props <- env.simpDB_props - !num_props; !res - let analyze c_clause = let pathC = ref 0 in let learnt = ref [] in @@ -495,6 +507,7 @@ module Make (F : Formula_intf.S) l := List.rev_append v.vpremise !l; match v.reason with None -> () | Some c -> l := c :: !l done; + (* if false then begin eprintf "@.>>UNSAT Deduction made from:@."; List.iter @@ -502,6 +515,7 @@ module Make (F : Formula_intf.S) eprintf " %a@." pp_clause hc )!l; end; + *) let uc = HUC.create 17 in let rec roots todo = match todo with @@ -520,6 +534,7 @@ module Make (F : Formula_intf.S) | prems -> roots prems; roots r in roots !l; let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + (* if false then begin eprintf "@.>>UNSAT_CORE:@."; List.iter @@ -527,6 +542,7 @@ module Make (F : Formula_intf.S) eprintf " %a@." pp_clause hc )unsat_core; end; + *) env.is_unsat <- true; env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -540,6 +556,7 @@ module Make (F : Formula_intf.S) match v.reason with None -> l | Some c -> c :: l ) dep [] in + (* if false then begin eprintf "@.>>T-UNSAT Deduction made from:@."; List.iter @@ -547,6 +564,7 @@ module Make (F : Formula_intf.S) eprintf " %a@." pp_clause hc )l; end; + *) let uc = HUC.create 17 in let rec roots todo = match todo with @@ -565,6 +583,7 @@ module Make (F : Formula_intf.S) | prems -> roots prems; roots r in roots l; let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in + (* if false then begin eprintf "@.>>T-UNSAT_CORE:@."; List.iter @@ -572,6 +591,7 @@ module Make (F : Formula_intf.S) eprintf " %a@." pp_clause hc ) unsat_core; end; + *) env.is_unsat <- true; env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -739,7 +759,7 @@ module Make (F : Formula_intf.S) let next = pick_branch_lit () in let current_level = decision_level () in assert (next.level < 0); - (* eprintf "decide: %a@." Debug.atom next.pa; *) + Log.debug 5 "Deciding on %a" St.pp_atom next.pa; enqueue next.pa current_level None done @@ -825,7 +845,6 @@ module Make (F : Formula_intf.S) let clause = make_clause name atoms size false init in attach_clause clause; Vec.push env.clauses clause; - if a.neg.is_true then begin let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in cancel_until lvl; diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 84b09c77..d70e2f2f 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -11,7 +11,7 @@ (* *) (**************************************************************************) -open Format +open Printf let ale = Hstring.make "<=" let alt = Hstring.make "<" @@ -186,23 +186,23 @@ module Make (F : Formula_intf.S) = struct else if a.neg.is_true then sprintf ":0%s" (level a) else ":X" - let pp_premise fmt v = - List.iter (fun {name=name} -> fprintf fmt "%s," name) v + let pp_premise b v = + List.iter (fun {name=name} -> bprintf b "%s," name) v - let pp_atom fmt a = - fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" - (sign a) (a.var.vid+1) (value a) F.print a.lit + let pp_atom b a = + bprintf b "%s%d%s [lit:%s] vpremise={{%a}}" + (sign a) (a.var.vid+1) (value a) (Log.on_fmt F.print a.lit) pp_premise a.var.vpremise - let pp_atoms_list fmt l = List.iter (fprintf fmt "%a ; " pp_atom) l - let pp_atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " pp_atom) arr + let pp_atoms_list b l = List.iter (bprintf b "%a ; " pp_atom) l + let pp_atoms_array b arr = Array.iter (bprintf b "%a ; " pp_atom) arr - let pp_atoms_vec fmt vec = + let pp_atoms_vec b vec = for i = 0 to Vec.size vec - 1 do - fprintf fmt "%a ; " pp_atom (Vec.get vec i) + bprintf b "%a ; " pp_atom (Vec.get vec i) done - let pp_clause fmt {name=name; atoms=arr; cpremise=cp} = - fprintf fmt "%s:{ %a} cpremise={{%a}}" name pp_atoms_vec arr pp_premise cp + let pp_clause b {name=name; atoms=arr; cpremise=cp} = + bprintf b "%s:{ %a} cpremise={{%a}}" name pp_atoms_vec arr pp_premise cp end diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml index 80a9c0d3..274db2c6 100644 --- a/sat/solver_types_intf.ml +++ b/sat/solver_types_intf.ml @@ -73,7 +73,7 @@ module type S = sig val made_vars_info : unit -> int * var list val clear : unit -> unit - val pp_atom : Format.formatter -> atom -> unit - val pp_clause : Format.formatter -> clause -> unit + val pp_atom : Buffer.t -> atom -> unit + val pp_clause : Buffer.t -> clause -> unit end diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml index d3a0a040..5c59f1ed 100644 --- a/sat/theory_intf.ml +++ b/sat/theory_intf.ml @@ -19,7 +19,10 @@ module type S = sig exception Inconsistent of explanation + val dummy : t val empty : unit -> t val assume : cs:bool -> formula -> explanation -> t -> t + (** Any valid theory, either the empty one, or one returned by assume, should + be different from the dummy one. *) end diff --git a/util/.merlin b/util/.merlin index daa95b7d..9e3a669a 100644 --- a/util/.merlin +++ b/util/.merlin @@ -3,6 +3,7 @@ S ../sat/ S ../common/ B ../_build/ +B ../_build/util/ B ../_build/sat/ B ../_build/smt/ B ../_build/common/ diff --git a/util/log.ml b/util/log.ml new file mode 100644 index 00000000..f8f3018e --- /dev/null +++ b/util/log.ml @@ -0,0 +1,124 @@ +(* +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} *) + +(** {2 Time facilities} *) + +(** Time elapsed since initialization of the program, and time of start *) +let get_total_time, get_start_time = + let start = Unix.gettimeofday () in + (function () -> + let stop = Unix.gettimeofday () in + stop -. start), + (function () -> start) + +(** {2 Misc} *) + +let clear_line () = + output_string Pervasives.stdout + "\r \r"; + flush Pervasives.stdout + + +let debug_level_ = ref 0 +let set_debug l = debug_level_ := l +let get_debug () = !debug_level_ +let need_cleanup = ref false +let debug l format = + let b = Buffer.create 15 in + if l <= !debug_level_ + then ( + (if !need_cleanup then clear_line ()); + Printf.bprintf b "%% [%.3f] " (get_total_time ()); + Printf.kbprintf + (fun b -> print_endline (Buffer.contents b)) + b format) + else + Printf.ifprintf b format + +let pp_pos pos = + let open Lexing in + Printf.sprintf "line %d, column %d" pos.pos_lnum (pos.pos_cnum - pos.pos_bol) + +(** {2 Printing utils} *) + +let sprintf format = + let buffer = Buffer.create 64 in + Printf.kbprintf + (fun fmt -> Buffer.contents buffer) + buffer + format + +let fprintf oc format = + let buffer = Buffer.create 64 in + Printf.kbprintf + (fun fmt -> Buffer.output_buffer oc buffer) + buffer + format + +let printf format = fprintf stdout format +let eprintf format = fprintf stderr format + +let on_fmt pp x = + pp Format.str_formatter x; + Format.flush_str_formatter () + +let on_buffer pp x = + let buf = Buffer.create 24 in + pp buf x; + Buffer.contents buf + +let pp_pair ?(sep=" ") px py buf (x,y) = + px buf x; + Buffer.add_string buf sep; + py buf y + +let pp_opt pp buf x = match x with + | None -> Buffer.add_string buf "None" + | Some x -> Printf.bprintf buf "Some %a" pp x + +(** print a list of items using the printing function *) +let rec pp_list ?(sep=", ") pp_item buf = function + | x::((y::xs) as l) -> + pp_item buf x; + Buffer.add_string buf sep; + pp_list ~sep pp_item buf l + | x::[] -> pp_item buf x + | [] -> () + +(** print an array of items using the printing function *) +let pp_array ?(sep=", ") pp_item buf a = + for i = 0 to Array.length a - 1 do + (if i > 0 then Buffer.add_string buf sep); + pp_item buf a.(i) + done + +(** print an array of items using the printing function *) +let pp_arrayi ?(sep=", ") pp_item buf a = + for i = 0 to Array.length a - 1 do + (if i > 0 then Buffer.add_string buf sep); + pp_item buf i a.(i) + done diff --git a/util/log.mli b/util/log.mli new file mode 100644 index 00000000..80a0d4d8 --- /dev/null +++ b/util/log.mli @@ -0,0 +1,74 @@ +(* +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} *) + +(** {2 Time facilities} *) + +(** time elapsed since start of program *) +val get_total_time : unit -> float + +(** time at which the program started *) +val get_start_time : unit -> float + +(** {2 Misc} *) + +val set_debug : int -> unit (** Set debug level *) +val get_debug : unit -> int (** Current debug level *) +val need_cleanup : bool ref (** Cleanup line before printing? *) + +val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a + (** debug message *) + +val pp_pos : Lexing.position -> string + +(** {2 Printing utils} *) + +(** print into a string *) +val sprintf : ('a, Buffer.t, unit, string) format4 -> 'a + +val fprintf : out_channel -> ('a, Buffer.t, unit, unit) format4 -> 'a + +val printf : ('a, Buffer.t, unit, unit) format4 -> 'a +val eprintf : ('a, Buffer.t, unit, unit) format4 -> 'a +val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string +val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string + +val pp_pair: ?sep:string -> (Buffer.t -> 'a -> unit) -> + (Buffer.t -> 'b -> unit) -> Buffer.t -> ('a * 'b) -> unit + +val pp_opt : (Buffer.t -> 'a -> unit) -> Buffer.t -> 'a option -> unit + +(** print a list of items using the printing function *) +val pp_list: ?sep:string -> (Buffer.t -> 'a -> unit) + -> Buffer.t -> 'a list -> unit + +(** print an array of items with printing function *) +val pp_array: ?sep:string -> (Buffer.t -> 'a -> unit) + -> Buffer.t -> 'a array -> unit + +(** print an array, giving the printing function both index and item *) +val pp_arrayi: ?sep:string -> (Buffer.t -> int -> 'a -> unit) + -> Buffer.t -> 'a array -> unit diff --git a/util/test.ml b/util/test.ml index 4608e5e6..3a8f8dc1 100644 --- a/util/test.ml +++ b/util/test.ml @@ -7,10 +7,13 @@ let init () = [v.(0); v.(1)]; [S.neg v.(0); v.(2)]; [S.neg v.(1); v.(2)]; + ]; + [ [v.(3); v.(4)]; [S.neg v.(3); S.neg v.(2)]; [S.neg v.(4); S.neg v.(2)]; - ] ] + ] + ] let print_assign fmt () = S.iter_atoms (fun a -> @@ -20,6 +23,7 @@ let print_assign fmt () = ) let main () = + Log.set_debug 10; Format.printf "Hello World !@."; List.iter (fun l -> List.iter (fun c -> Format.printf "Adding : %a@."