Removed true_ and false_ constants

Added some debug output in solver.ml
Added options to test utility

sat/formula_intf.ml

@@ -19,8 +19,6 @@ module type S = sig
   type t
   (** The type of atomic formulas. *)
 
-  val true_ : t
-  val false_ : t
   val dummy : t
   (** Formula constants. A valid formula should never be physically equal to [dummy] *)
 

sat/sat.ml

@@ -5,47 +5,40 @@ module Fsat = struct
 
   (* Until the constant true_ and false_ are not needed anymore,
    * wa can't simply use sigend integers to represent literals *)
-  type t = {
+  type t = int
-    (* Invariant : var >= 0 *)
-    var : int;
-    pos : bool;
-  }
 
+  let max_lit = min max_int (- min_int)
   let max_index = ref 0
 
-  let true_ = { var = 0; pos = true }
+  let dummy = 0
-  let false_ = { var = 0; pos = false }
-  let dummy = { var = -1; pos = true }
 
-  let unsafe_make i = { var = i; pos = true }
+  let neg a = - a
-  let make i = if i > 0 then unsafe_make i else dummy
+  let norm a = abs a, a < 0
-
-  let neg a = { a with pos = not a.pos }
-  let norm a = unsafe_make a.var, not a.pos
 
   let hash = Hashtbl.hash
   let equal = (=)
   let compare = Pervasives.compare
 
-  let label a = Hstring.make ""
+  let _str = Hstring.make ""
+  let label a = _str
   let add_label _ _ = ()
 
   let create, iter =
     let create () =
-      if !max_index <> max_int then
+      if !max_index <> max_lit then
-        (incr max_index; unsafe_make !max_index)
+          (incr max_index; !max_index)
       else
         raise Out_of_int
     in
     let iter: (t -> unit) -> unit = fun f ->
       for j = 1 to !max_index do
-        f (unsafe_make j)
+        f j
       done
     in
     create, iter
 
   let print fmt a =
-    Format.fprintf fmt "%s%d" (if not a.pos then "~" else "") a.var
+    Format.fprintf fmt "%s%d" (if a < 0 then "~" else "") (abs a)
 
 end
 

sat/solver.ml

@@ -238,7 +238,6 @@ 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);
@@ -620,18 +619,20 @@ module Make (F : Formula_intf.S)
       | [] -> assert false
       | [fuip] ->
         assert (blevel = 0);
+        Log.debug 2 "Unit clause learnt : %a" St.pp_atom fuip;
         fuip.var.vpremise <- history;
         enqueue fuip 0 None
       | fuip :: _ ->
         let name = fresh_lname () in
         let lclause = make_clause name learnt size true history in
+        Log.debug 2 "New clause learnt : %a" St.pp_clause lclause;
         Vec.push env.learnts lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
         enqueue fuip blevel (Some lclause)
     end;
     var_decay_activity ();
-    clause_decay_activity()
+    clause_decay_activity ()
 
   let check_inconsistence_of dep =
     try

util/test.ml

@@ -1,20 +1,27 @@
 
 module S = Sat.Make(struct end)
 
+let anon_fun = fun _ -> ()
+let usage = "Coming soon..."
+let argspec = [
+    "-v", Arg.Int (fun i -> Log.set_debug i),
+    "Sets the debug verbose level";
+]
+
+(* Temp until lexer/parsezr is set up *)
 let init () =
   let v = Array.init 5 (fun _ -> S.new_atom ()) in
   [ [
     [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)];
     ]
   ]
 
+(* Iterate over all variables created *)
 let print_assign fmt () =
   S.iter_atoms (fun a ->
       Format.fprintf fmt "%a -> %s,@ "
@@ -23,8 +30,7 @@ let print_assign fmt () =
     )
 
 let main () =
-  Log.set_debug 10;
+  Arg.parse argspec anon_fun usage;
-  Format.printf "Hello World !@.";
   List.iter (fun l ->
       List.iter (fun c -> Format.printf "Adding : %a@."
                     (fun _ -> List.iter (fun a -> Format.printf "%a " S.print_atom a)) c) l;