From e059441347dc5c334ea7b74e8c34212d125ab725 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 17 Mar 2015 14:20:11 +0100 Subject: [PATCH 1/3] Fixed potential bug in vec.set Removed some excessive logging messages --- solver/mcsolver.ml | 7 ------- solver/mcsolver_types.ml | 12 ++---------- util/vec.ml | 11 +++++------ util/vec.mli | 3 --- 4 files changed, 7 insertions(+), 26 deletions(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 2bece663..a6466df5 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -572,7 +572,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) done; (* no watch lit found *) if first.neg.is_true || (th_eval first = Some false) then begin - L.debug 100 "clause is false"; (* clause is false *) env.qhead <- Vec.size env.trail; for k = i to Vec.size watched - 1 do @@ -582,7 +581,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) L.debug 3 "Conflict found : %a" St.pp_clause c; raise (Conflict c) end else begin - L.debug 100 "clause is unit"; (* clause is unit *) Vec.set watched !new_sz c; incr new_sz; @@ -612,7 +610,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) (* Propagation (boolean and theory) *) let new_atom f = - L.debug 100 "New_atom"; let a = add_atom f in L.debug 10 "New atom : %a" St.pp_atom a; ignore (th_eval a); @@ -629,11 +626,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) add_clause (fresh_tname ()) atoms (Lemma lemma) let slice_propagate f lvl = - L.debug 100 "entering slice.propagate"; let a = add_atom f in - L.debug 100 "atom added"; Iheap.grow_to_by_double env.order (St.nb_vars ()); - L.debug 100 "heap grown"; enqueue_bool a lvl (Semantic lvl) let current_slice () = Th.({ @@ -792,7 +786,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) let conflictC = ref 0 in env.starts <- env.starts + 1; while (true) do - L.debug 100 "searching %d/%d (%d)" !conflictC n_of_conflicts n_of_learnts; match propagate () with | Some confl -> (* Conflict *) incr conflictC; diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml index d5d1942a..0d5765bd 100644 --- a/solver/mcsolver_types.ml +++ b/solver/mcsolver_types.ml @@ -102,8 +102,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with module MF = Hashtbl.Make(E.Formula) module MT = Hashtbl.Make(E.Term) - let f_map = MF.create 1007 - let t_map = MT.create 1007 + let f_map = MF.create 4096 + let t_map = MT.create 4096 let vars = Vec.make 107 (Either.mk_right dummy_var) let nb_vars () = Vec.size vars @@ -130,11 +130,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with let make_boolean_var = fun lit -> - L.debug 100 "normalizing lit"; let lit, negated = E.norm lit in try MF.find f_map lit, negated with Not_found -> - L.debug 100 "Lit not in table"; let cpt_fois_2 = !cpt_mk_var lsl 1 in let rec var = { vid = !cpt_mk_var; @@ -159,22 +157,16 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with neg = pa; is_true = false; aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in - L.debug 100 "adding lit to table..."; MF.add f_map lit var; - L.debug 100 "done"; incr cpt_mk_var; Vec.push vars (Either.mk_right var); - L.debug 100 "iterating on new lit..."; Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; - L.debug 100 "done"; var, negated let add_term t = make_semantic_var t let add_atom lit = - L.debug 100 "entering add_atom"; let var, negated = make_boolean_var lit in - L.debug 100 "found atom"; if negated then var.tag.na else var.tag.pa let make_clause name ali sz_ali is_learnt premise = diff --git a/util/vec.ml b/util/vec.ml index 57a6571c..54a9588a 100644 --- a/util/vec.ml +++ b/util/vec.ml @@ -48,6 +48,7 @@ let size t = t.sz let is_empty t = t.sz = 0 let grow_to t new_capa = + assert (new_capa >= Array.length t.data); let data = t.data in let capa = Array.length data in t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy) @@ -85,12 +86,10 @@ let get t i = let set t i v = if i < 0 || i > t.sz then invalid_arg "vec.set"; - t.sz <- max t.sz (i+1); (* can set first empty slot *) - Array.unsafe_set t.data i v - -let set_unsafe t i v = - if i < 0 || i >= Array.length t.data then invalid_arg "vec.set_unsafe"; - t.sz <- max t.sz (i+1); + if i = t.sz then begin + grow_to_double_size t; + t.sz <- i + 1 + end; Array.unsafe_set t.data i v let copy t = diff --git a/util/vec.mli b/util/vec.mli index f68fd877..f96041e2 100644 --- a/util/vec.mli +++ b/util/vec.mli @@ -69,9 +69,6 @@ val set : 'a t -> int -> 'a -> unit free slot if [not (is_full vec)], or @raise Invalid_argument if the index is not valid *) -val set_unsafe : 'a t -> int -> 'a -> unit -(* undocumented. TODO remove asap *) - val copy : 'a t -> 'a t (** Fresh copy *) From c1af34823c62ce7eced1c4d8a695384ef789d3b1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 17 Mar 2015 17:33:35 +0100 Subject: [PATCH 2/3] Fix for compilation on older ocaml compiler --- solver/mcproof.ml | 12 ++++++++++-- solver/mcproof.mli | 6 ++++-- solver/mcsolver_types.mli | 8 +++++--- solver/res.ml | 12 ++++++++++-- solver/res.mli | 6 ++++-- solver/solver_types.mli | 6 ++++-- 6 files changed, 37 insertions(+), 13 deletions(-) diff --git a/solver/mcproof.ml b/solver/mcproof.ml index a44f0601..10cd3380 100644 --- a/solver/mcproof.ml +++ b/solver/mcproof.ml @@ -71,13 +71,21 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct let resolved, new_clause = aux [] [] l in resolved, List.rev new_clause + (* List.sort_uniq is only since 4.02.0 *) + let sort_uniq compare l = + let rec aux = function + | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r + | l -> l + in + aux (List.sort compare l) + let to_list c = let v = St.(c.atoms) in let l = ref [] in for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - let res = List.sort_uniq compare_atoms !l in + let res = sort_uniq compare_atoms !l in let l, _ = resolve res in if l <> [] then L.debug 3 "Input clause is a tautology"; @@ -251,7 +259,7 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct | Resolution (proof1, proof2, _) -> aux (aux acc proof1) proof2 in - List.sort_uniq compare_cl (aux [] proof) + sort_uniq compare_cl (aux [] proof) (* Print proof graph *) let _i = ref 0 diff --git a/solver/mcproof.mli b/solver/mcproof.mli index d80cba71..cb7b2167 100644 --- a/solver/mcproof.mli +++ b/solver/mcproof.mli @@ -6,6 +6,8 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (L : Log_intf.S)(St : Mcsolver_types.S) - -> S with type atom = St.atom and type clause = St.clause and type lemma = St.proof +module Make : + functor (L : Log_intf.S) -> + functor (St : Mcsolver_types.S) -> + S with type atom = St.atom and type clause = St.clause and type lemma = St.proof (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/mcsolver_types.mli b/solver/mcsolver_types.mli index 85276113..a10ae5f5 100644 --- a/solver/mcsolver_types.mli +++ b/solver/mcsolver_types.mli @@ -13,7 +13,9 @@ module type S = Mcsolver_types_intf.S -module Make : functor (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with - type term = E.Term.t and type formula = E.Formula.t) - -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof +module Make : + functor (L : Log_intf.S) -> + functor (E : Expr_intf.S) -> + functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) -> + S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) diff --git a/solver/res.ml b/solver/res.ml index a068ba1a..f8615def 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -71,13 +71,21 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let resolved, new_clause = aux [] [] l in resolved, List.rev new_clause + (* List.sort_uniq is only since 4.02.0 *) + let sort_uniq compare l = + let rec aux = function + | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r + | l -> l + in + aux (List.sort compare l) + let to_list c = let v = St.(c.atoms) in let l = ref [] in for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - let l, res = resolve (List.sort_uniq compare_atoms !l) in + let l, res = resolve (sort_uniq compare_atoms !l) in if l <> [] then raise (Resolution_error "Input clause is a tautology"); res @@ -250,7 +258,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | Resolution (proof1, proof2, _) -> aux (aux acc proof1) proof2 in - List.sort_uniq compare_cl (aux [] proof) + sort_uniq compare_cl (aux [] proof) (* Print proof graph *) let _i = ref 0 diff --git a/solver/res.mli b/solver/res.mli index 33a44da8..306a724d 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -6,6 +6,8 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (L : Log_intf.S)(St : Solver_types.S) - -> S with type atom= St.atom and type clause = St.clause and type lemma = St.proof +module Make : + functor (L : Log_intf.S) -> + functor (St : Solver_types.S) -> + S with type atom= St.atom and type clause = St.clause and type lemma = St.proof (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/solver_types.mli b/solver/solver_types.mli index ecc41d8b..d4fa2200 100644 --- a/solver/solver_types.mli +++ b/solver/solver_types.mli @@ -13,6 +13,8 @@ module type S = Solver_types_intf.S -module Make : functor (F : Formula_intf.S)(Th : Theory_intf.S) - -> S with type formula = F.t and type proof = Th.proof +module Make : + functor (F : Formula_intf.S) -> + functor (Th : Theory_intf.S) -> + S with type formula = F.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) From e0ac6b31fdac8946b681543edeca4929b10507f8 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 18 Mar 2015 15:13:18 +0100 Subject: [PATCH 3/3] Fix for vector resizing in 'set' --- _tags | 2 +- util/vec.ml | 18 ++++++++---------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/_tags b/_tags index 491f9fe3..8b30136a 100644 --- a/_tags +++ b/_tags @@ -11,5 +11,5 @@ # more warnings <**/*.ml>: warn_K, warn_Y, warn_X - <**/*.cm*>: debug + diff --git a/util/vec.ml b/util/vec.ml index 54a9588a..26b1c393 100644 --- a/util/vec.ml +++ b/util/vec.ml @@ -82,15 +82,14 @@ let last t = let get t i = if i < 0 || i >= t.sz then invalid_arg "vec.get"; - Array.unsafe_get t.data i + Array.get t.data i let set t i v = if i < 0 || i > t.sz then invalid_arg "vec.set"; - if i = t.sz then begin - grow_to_double_size t; - t.sz <- i + 1 - end; - Array.unsafe_set t.data i v + if i = t.sz then + push t v + else + Array.set t.data i v let copy t = let data = Array.copy t.data in @@ -100,7 +99,6 @@ let move_to t t' = t'.data <- Array.copy t.data; t'.sz <- t.sz - let remove t e = let j = ref 0 in while (!j < t.sz && not (t.data.(!j) == e)) do incr j done; @@ -132,7 +130,7 @@ let fold f acc t = if i=t.sz then acc else - let acc' = f acc (Array.unsafe_get t.data i) in + let acc' = f acc (Array.get t.data i) in _fold f acc' t (i+1) in _fold f acc t 0 @@ -141,7 +139,7 @@ exception ExitVec let exists p t = try for i = 0 to t.sz - 1 do - if p (Array.unsafe_get t.data i) then raise ExitVec + if p (Array.get t.data i) then raise ExitVec done; false with ExitVec -> true @@ -149,7 +147,7 @@ let exists p t = let for_all p t = try for i = 0 to t.sz - 1 do - if not (p (Array.unsafe_get t.data i)) then raise ExitVec + if not (p (Array.get t.data i)) then raise ExitVec done; true with ExitVec -> false