Added function to print unsat core in dimacs format

Thgis is meant to be used for debugging and/or benchmarking purposes.
For instance, when using msat in an application, all unsat cores can
be output this way to different files so that the results can be checked
and easily reproduced in case of errors.

sat/sat.ml

@@ -58,6 +58,7 @@ module Fsat = struct
       (if a < 0 then "~" else "")
       (if a mod 2 = 0 then "v" else "f")
       ((abs a) / 2)
+
 end
 
 module Tseitin = Tseitin.Make(Fsat)
@@ -78,4 +79,17 @@ module Make(Dummy : sig end) = struct
     in
     Dot.print out p
 
+  let print_dimacs_clause fmt l =
+    Format.fprintf fmt "%a0" (fun fmt l ->
+        List.iter (fun i -> Format.fprintf fmt "%d " i) l) l
+
+  let print_dimacs fmt l =
+    let l = List.map (fun c ->
+        List.map (fun a -> a.St.lit) @@ Proof.to_list c) l in
+    let n, m = List.fold_left (fun (n, m) c ->
+        let m' = List.fold_left (fun i j -> max i (abs j)) m c in
+        (n + 1, m')) (0, 0) l in
+    Format.fprintf fmt "p cnf %d %d@\n" n m;
+    List.iter (fun c -> Format.fprintf fmt "%a@\n" print_dimacs_clause c) l
+
 end

sat/sat.mli

@@ -55,5 +55,8 @@ module Make(Dummy : sig end) : sig
   val print_proof : Format.formatter -> Proof.proof -> unit
   (** Print the given proof in dot format. *)
 
+  val print_dimacs : Format.formatter -> St.clause list -> unit
+  (** Prints a cnf in dimacs format on the given formatter *)
+
 end