From e059441347dc5c334ea7b74e8c34212d125ab725 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 17 Mar 2015 14:20:11 +0100
Subject: [PATCH] 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 *)