Some more doc + indentation

TODO.md

@@ -7,7 +7,6 @@
     * Allow theory propagation
 - Cleanup code
     * Simplify Solver.Make functor
-    * Clean Solver_types interface
 - Add proof output for smt/theories
     * Each theory brings its own proof output (tautologies), somehow
 - Allow to plug one's code into boolean propagation

sat/res.ml

@@ -260,13 +260,13 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
   (* Compute unsat-core *)
   let compare_cl c d =
     let rec aux = function
-    | [], [] -> 0
+      | [], [] -> 0
-    | a :: r, a' :: r' -> begin match compare_atoms a a' with
+      | a :: r, a' :: r' -> begin match compare_atoms a a' with
-      | 0 -> aux (r, r')
+          | 0 -> aux (r, r')
-      | x -> x
+          | x -> x
-    end
+        end
-    | _ :: _ , [] -> -1
+      | _ :: _ , [] -> -1
-    | [], _ :: _ -> 1
+      | [], _ :: _ -> 1
     in
     aux (to_list c, to_list d)
 
@@ -276,7 +276,7 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
       match p.step with
       | Hypothesis | Lemma _ -> [p.conclusion]
       | Resolution (proof1, proof2, _) ->
-              List.rev_append (aux proof1) (aux proof2)
+        List.rev_append (aux proof1) (aux proof2)
     in
     List.sort_uniq compare_cl (aux proof)
 

sat/res.mli

@@ -8,3 +8,4 @@ module type S = Res_intf.S
 
 module Make : functor (St : Solver_types.S)(Proof : sig type proof end)
   -> S with type atom= St.atom and type clause = St.clause and type lemma = Proof.proof
+(** Functor to create a module building proofs from a sat-solver unsat trace. *)

sat/res_intf.ml

@@ -1,10 +1,12 @@
 (* Copyright 2014 Guillaume Bury *)
 
 module type S = sig
+  (** Sinature for a module handling proof by resolution from sat solving traces *)
 
   type atom
   type clause
   type lemma
+  (** Abstract types for atoms, clauses and theoriy-specific lemmas *)
 
   val is_proven : clause -> bool
   (** Returns [true] if the clause has a derivation in the current proof graph, and [false] otherwise. *)

sat/sat.ml

@@ -13,11 +13,11 @@ module Fsat = struct
 
   let _make i =
     if i <> 0 && (abs i) < max_lit then begin
-        max_index := max !max_index (abs i);
+      max_index := max !max_index (abs i);
-        i
+      i
     end else
-        (Format.printf "Warning : %d/%d@." i max_lit;
+      (Format.printf "Warning : %d/%d@." i max_lit;
-        raise (Dummy i))
+       raise (Dummy i))
 
   let dummy = 0
 
@@ -35,8 +35,8 @@ module Fsat = struct
   let make i = _make (2 * i)
   let fresh, iter =
     let create () =
-        incr max_fresh;
+      incr max_fresh;
-        _make (2 * !max_fresh + 1)
+      _make (2 * !max_fresh + 1)
     in
     let iter: (t -> unit) -> unit = fun f ->
       for j = 1 to !max_index do

sat/solver_types.ml

@@ -162,15 +162,15 @@ module Make (F : Formula_intf.S) = struct
   let print_atom fmt a = F.print fmt a.lit
 
   let print_atoms fmt v =
-      print_atom fmt (Vec.get v 0);
+    print_atom fmt (Vec.get v 0);
-      if (Vec.size v) > 1 then begin
+    if (Vec.size v) > 1 then begin
-          for i = 1 to (Vec.size v) - 1 do
+      for i = 1 to (Vec.size v) - 1 do
-              Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
+        Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
-          done
+      done
-      end
+    end
 
   let print_clause fmt c =
-      Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
+    Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
 
   (* Complete debug printing *)
   let sign a = if a==a.var.pa then "" else "-"

sat/tseitin.ml

@@ -53,11 +53,11 @@ module Make (F : Formula_intf.S) = struct
   let f_false = make_atom atomic_false
 
   let rec flatten comb acc = function
-          | [] -> acc
+    | [] -> acc
-          | (Comb (c, l)) :: r when c = comb ->
+    | (Comb (c, l)) :: r when c = comb ->
-                  flatten comb (List.rev_append l acc) r
+      flatten comb (List.rev_append l acc) r
-          | a :: r ->
+    | a :: r ->
-                  flatten comb (a :: acc) r
+      flatten comb (a :: acc) r
 
   let make_not f = make Not [f]
   let make_and l = make And (flatten And [] l)
@@ -93,18 +93,18 @@ module Make (F : Formula_intf.S) = struct
     | Lit _ as f -> f
 
   let rec simplify_clause acc = function
-      | [] -> Some acc
+    | [] -> Some acc
-      | a :: r when F.equal atomic_true a -> None
+    | a :: r when F.equal atomic_true a -> None
-      | a :: r when F.equal atomic_false a ->
+    | a :: r when F.equal atomic_false a ->
-              simplify_clause acc r
+      simplify_clause acc r
-      | a :: r -> simplify_clause (a :: acc) r
+    | a :: r -> simplify_clause (a :: acc) r
 
   let rec rev_opt_map f acc = function
     | [] -> acc
     | a :: r -> begin match f a with
-      | None -> rev_opt_map f acc r
+        | None -> rev_opt_map f acc r
-      | Some b -> rev_opt_map f (b :: acc) r
+        | Some b -> rev_opt_map f (b :: acc) r
-    end
+      end
 
   let simplify_cnf = rev_opt_map (simplify_clause []) []
 

util/sat_solve.ml

@@ -43,20 +43,20 @@ let set_output s = set_io "Output" s output output_list
 
 (* Input Parsing *)
 let rec rev_flat_map f acc = function
-    | [] -> acc
+  | [] -> acc
-    | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
+  | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
 
 let format_of_filename s =
-    let last n =
+  let last n =
-        try String.sub s (String.length s - n) n
+    try String.sub s (String.length s - n) n
-        with Invalid_argument _ -> ""
+    with Invalid_argument _ -> ""
-    in
+  in
-    if last 4 = ".cnf" then
+  if last 4 = ".cnf" then
-        Dimacs
+    Dimacs
-    else if last 5 = ".smt2" then
+  else if last 5 = ".smt2" then
-        Smtlib
+    Smtlib
-    else (* Default choice *)
+  else (* Default choice *)
-        Dimacs
+    Dimacs
 
 let parse_with_input file = function
   | Auto -> assert false
@@ -64,9 +64,9 @@ let parse_with_input file = function
   | Smtlib -> Sat.Tseitin.simplify_cnf (rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file))
 
 let parse_input file =
-    parse_with_input file (match !input with
+  parse_with_input file (match !input with
-        | Auto -> format_of_filename file
+      | Auto -> format_of_filename file
-        | f -> f)
+      | f -> f)
 
 (* Printing wrappers *)
 let std = Format.std_formatter
@@ -85,15 +85,15 @@ let print_assign () = match !output with
   | Dot -> ()
 
 let rec print_cl fmt = function
-    | [] -> Format.fprintf fmt "[]"
+  | [] -> Format.fprintf fmt "[]"
-    | [a] -> Sat.Fsat.print fmt a
+  | [a] -> Sat.Fsat.print fmt a
-    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Sat.Fsat.print a print_cl r
+  | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Sat.Fsat.print a print_cl r
 
 let print_lcl l =
-    List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
+  List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
 
 let print_lclause l =
-    List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l
+  List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l
 
 (* Arguments parsing *)
 let file = ref ""
@@ -155,7 +155,7 @@ let argspec = Arg.align [
     "-time", Arg.String (int_arg time_limit),
     "<t>[smhd] Sets the time limit for the sat solver";
     "-u", Arg.Set p_unsat_core,
-    " Prints the unsat-core explanation of the unsat proof";
+    " Prints the unsat-core explanation of the unsat proof (if used with -check)";
     "-v", Arg.Int (fun i -> Log.set_debug i),
     "<lvl> Sets the debug verbose level";
   ]
@@ -185,7 +185,7 @@ let main () =
   (* Interesting stuff happening *)
   let cnf = get_cnf () in
   if !p_cnf then
-      print_lcl cnf;
+    print_lcl cnf;
   S.assume cnf;
   match S.solve () with
   | S.Sat ->
@@ -198,7 +198,7 @@ let main () =
       let p = S.get_proof () in
       print_proof p;
       if !p_unsat_core then
-          print_lclause (S.unsat_core p)
+        print_lclause (S.unsat_core p)
     end
 
 let () =