From e58cfe1c8f9d66818440e5ce8eb7c145885299b7 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 5 Feb 2016 14:30:47 +0100
Subject: [PATCH] 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  | 14 ++++++++++++++
 sat/sat.mli |  3 +++
 2 files changed, 17 insertions(+)

diff --git a/sat/sat.ml b/sat/sat.ml
index 9ef90445..5460fe8d 100644
--- a/sat/sat.ml
+++ b/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
diff --git a/sat/sat.mli b/sat/sat.mli
index d830b3cd..bcc87f68 100644
--- a/sat/sat.mli
+++ b/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