Few fixes. Sat Solver is working.

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<class V, class T>
 static inline void remove(V& ts, const T& t)

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

sat/.merlin

@@ -3,4 +3,5 @@ S ../common/
 
 B ../_build/
 B ../_build/sat/
+B ../_build/util/
 B ../_build/common/

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 "}"
 

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

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 dummy = -1
-    let assume ~cs:_ _ _ _ = ()
+    let empty () = 0
+    let assume ~cs:_ _ _ _ = 0
 end
 
 module Make(Dummy : sig end) = struct

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
+    end else
-    else v
+        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;

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 =
+  let pp_premise b v =
-    List.iter (fun {name=name} -> fprintf fmt "%s," name) v
+    List.iter (fun {name=name} -> bprintf b "%s," name) v
 
-  let pp_atom fmt a =
+  let pp_atom b a =
-    fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}"
+    bprintf b "%s%d%s [lit:%s] vpremise={{%a}}"
-      (sign a) (a.var.vid+1) (value a) F.print a.lit
+      (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_list b l = List.iter (bprintf b "%a ; " pp_atom) l
-  let pp_atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " pp_atom) arr
+  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} =
+  let pp_clause b {name=name; atoms=arr; cpremise=cp} =
-    fprintf fmt "%s:{ %a} cpremise={{%a}}" name pp_atoms_vec arr pp_premise cp
+    bprintf b "%s:{ %a} cpremise={{%a}}" name pp_atoms_vec arr pp_premise cp
 
 end

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_atom : Buffer.t -> atom -> unit
-  val pp_clause : Format.formatter -> clause -> unit
+  val pp_clause : Buffer.t -> clause -> unit
 end
 

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
 

util/.merlin

@@ -3,6 +3,7 @@ S ../sat/
 S ../common/
 
 B ../_build/
+B ../_build/util/
 B ../_build/sat/
 B ../_build/smt/
 B ../_build/common/

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

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

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@."