Merge branch 'master' of github.com:Gbury/mSAT

_tags

@@ -11,5 +11,5 @@
 
 # more warnings
 <**/*.ml>: warn_K, warn_Y, warn_X
-
 <**/*.cm*>: debug
+

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

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)
+module Make :
-  -> S with type atom = St.atom and type clause = St.clause and type lemma = St.proof
+  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. *)

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. growing heap...";
     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;

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 f_map = MF.create 4096
-  let t_map = MT.create 1007
+  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 =

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
+module Make :
-    type term = E.Term.t and type formula = E.Formula.t)
+  functor (L : Log_intf.S) ->
-  -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
+  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. *)

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

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)
+module Make :
-  -> S with type atom= St.atom and type clause = St.clause and type lemma = St.proof
+  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. *)

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)
+module Make :
-  -> S with type formula = F.t and type proof = Th.proof
+  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. *)

util/vec.ml

@@ -82,17 +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";
-  t.sz <- max t.sz (i+1);  (* can set first empty slot *)
+  if i = t.sz then
-  Array.unsafe_set t.data i v
+    push t v
-
+  else
-let set_unsafe t i v =
+    Array.set t.data i v
-  if i < 0 || i >= Array.length t.data then invalid_arg "vec.set_unsafe";
-  t.sz <- max t.sz (i+1);
-  Array.unsafe_set t.data i v
 
 let copy t =
   let data = Array.copy t.data in
@@ -102,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;
@@ -134,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
 
@@ -143,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
@@ -151,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

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 *)