From d6cfd27f32f6a81f5afbd1d45f7c3295a8670623 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 7 Nov 2014 17:46:32 +0100
Subject: [PATCH] Fixed a bug in proof dot printer (+ indent)

---
 sat/res.ml        | 19 +++++++++----------
 util/sat_solve.ml | 26 +++++++++++++-------------
 2 files changed, 22 insertions(+), 23 deletions(-)

diff --git a/sat/res.ml b/sat/res.ml
index 94e2912f..30f32667 100644
--- a/sat/res.ml
+++ b/sat/res.ml
@@ -208,8 +208,8 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
       let d = match St.(a.var.level, a.var.reason) with
         | 0, Some d -> d
         | 0, None ->
-                let d, cl_d = unit_hyp a in
-                if is_proved (d, cl_d) then d else raise Exit
+          let d, cl_d = unit_hyp a in
+          if is_proved (d, cl_d) then d else raise Exit
         | _ -> raise Exit
       in
       prove d;
@@ -274,16 +274,15 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
     Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
 
   let is_drawn c =
-    try
-      fst (Hashtbl.find ids c)
-    with Not_found ->
-      false
+    ignore (c_id c);
+    fst (Hashtbl.find ids c)
 
   let has_drawn c =
-    assert (Hashtbl.mem ids c);
-    let b, id = Hashtbl.find ids c in
-    assert (not b);
-    Hashtbl.replace ids c (true, id)
+    if not (is_drawn c) then
+      let b, id = Hashtbl.find ids c in
+      Hashtbl.replace ids c (true, id)
+    else
+      ()
 
   let print_clause fmt c = print_cl fmt (to_list c)
 
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index 9c2bc2af..1a049353 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -7,32 +7,32 @@ exception Out_of_space
 (* IO wrappers *)
 (* Types for input/output languages *)
 type sat_input =
-    | Dimacs
+  | Dimacs
 
 type sat_output =
-    | Standard (* Only output problem status *)
-    | Dot
+  | Standard (* Only output problem status *)
+  | Dot
 
 let input = ref Dimacs
 let output = ref Standard
 
 let input_list = [
-    "dimacs", Dimacs;
+  "dimacs", Dimacs;
 ]
 let output_list = [
-    "dot", Dot;
+  "dot", Dot;
 ]
 
 let error_msg opt arg l =
-    Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
+  Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
     arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
-    Format.flush_str_formatter ()
+  Format.flush_str_formatter ()
 
 let set_io opt arg flag l =
-    try
-        flag := List.assoc arg l
-    with Not_found ->
-        invalid_arg (error_msg opt arg l)
+  try
+    flag := List.assoc arg l
+  with Not_found ->
+    invalid_arg (error_msg opt arg l)
 
 let set_input s = set_io "Input" s input input_list
 let set_output s = set_io "Output" s output output_list
@@ -149,8 +149,8 @@ let main () =
   | S.Unsat ->
     print "Unsat";
     if !p_proof_check then begin
-        let p = S.get_proof () in
-        print_proof p
+      let p = S.get_proof () in
+      print_proof p
     end
 
 let () =