From 119f3a8566e6404864f9e480d9801ee2ac516268 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 18 Aug 2016 18:19:14 +0200
Subject: [PATCH] New function to export a problem to dimacs format

---
 src/core/external.ml          | 24 ++++++++++++++++++++++++
 src/core/internal.ml          | 19 +++++++++++++++++++
 src/core/internal.mli         |  5 +++++
 src/core/solver_intf.ml       |  4 ++++
 src/core/solver_types.ml      | 10 ++++++++++
 src/core/solver_types_intf.ml |  1 +
 6 files changed, 63 insertions(+)

diff --git a/src/core/external.ml b/src/core/external.ml
index 386e5f5d..20cc419a 100644
--- a/src/core/external.ml
+++ b/src/core/external.ml
@@ -93,4 +93,28 @@ module Make
 
   let get_tag cl = St.(cl.tag)
 
+  let export_dimacs fmt () =
+    let n = St.nb_elt () in
+    let tmp = S.temp () in
+    let hyps = S.hyps () in
+    let learnt = S.history () in
+    let m = Vec.size hyps + Vec.size learnt in
+    let aux fmt c =
+      let c' = match c.St.cpremise with
+        | St.Hyp | St.Lemma _ -> c
+        | St.History ( { St.cpremise = (St.Hyp | St.Lemma _) } as d :: _) -> d
+        | _ -> assert false
+      in
+      St.pp_dimacs fmt c'
+    in
+    let pp s fmt vec =
+      Format.fprintf fmt "c %s@\n%a" s (Vec.print ~sep:"\n" aux) vec
+    in
+    Format.fprintf fmt
+      "p cnf %d %d@\n%a%a%a"
+      n m
+      (pp "Local assumptions") tmp
+      (pp "Hypotheses") hyps
+      (pp "Learnt") learnt
+
 end
diff --git a/src/core/internal.ml b/src/core/internal.ml
index f13a3a63..50c81aeb 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -33,6 +33,9 @@ module Make
     (* clauses assumed (subject to user levels) *)
     clauses_learnt : clause Vec.t;
     (* learnt clauses (tautologies true at any time, whatever the user level) *)
+    clauses_temp : clause Vec.t;
+    (* Temp clauses, corresponding to the local assumptions. This vec is used
+       only to have an efficient way to access the list of local assumptions. *)
 
     clauses_to_add : clause Stack.t;
     (* Clauses either assumed or pushed by the theory, waiting to be added. *)
@@ -124,6 +127,8 @@ module Make
 
     clauses_hyps = Vec.make 0 dummy_clause;
     clauses_learnt = Vec.make 0 dummy_clause;
+    clauses_temp = Vec.make 0 dummy_clause;
+
     clauses_to_add = Stack.create ();
 
     th_head = 0;
@@ -1135,6 +1140,16 @@ module Make
       assert (env.base_level > 0);
       env.unsat_conflict <- None;
       env.base_level <- env.base_level - 1; (* before the [cancel_until]! *)
+      (* remove from env.clauses_temp the now invalid caluses. *)
+      let i = ref (Vec.size env.clauses_temp - 1) in
+      while !i >= 0 &&
+            (Vec.get env.clauses_temp !i).atoms.(0).var.v_level > env.base_level do
+        decr i
+      done;
+      Vec.shrink env.clauses_temp (Vec.size env.clauses_temp - !i - 1);
+      assert (Vec.for_all (fun c ->
+          Array.length c.atoms = 1 &&
+          c.atoms.(0).var.v_level <= env.base_level) env.clauses_temp);
       cancel_until env.base_level
     end
 
@@ -1147,6 +1162,7 @@ module Make
       if a.is_true then ()
       else
         let c = make_clause (fresh_hname ()) [a] Local in
+        Vec.push env.clauses_temp c;
         if a.neg.is_true then begin
           (* conflict between assumptions: UNSAT *)
           report_unsat c;
@@ -1166,5 +1182,8 @@ module Make
   let hyps () = env.clauses_hyps
 
   let history () = env.clauses_learnt
+
+  let temp () = env.clauses_temp
+
 end
 
diff --git a/src/core/internal.mli b/src/core/internal.mli
index 899a08d0..1f9a50ac 100644
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
@@ -56,6 +56,10 @@ module Make
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses. *)
 
+  val temp : unit -> St.clause Vec.t
+  (** Returns the clauses coreesponding to the local assumptions.
+      All clauses in this vec are assured to be unit clauses. *)
+
   val history : unit -> St.clause Vec.t
   (** Returns the history of learnt clauses, with no guarantees on order. *)
 
@@ -65,5 +69,6 @@ module Make
 
   val model : unit -> (St.term * St.term) list
   (** Returns the model found if the formula is satisfiable. *)
+
 end
 
diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml
index c70b1392..ad925cd2 100644
--- a/src/core/solver_intf.ml
+++ b/src/core/solver_intf.ml
@@ -69,5 +69,9 @@ module type S = sig
   val get_tag : St.clause -> int option
   (** Recover tag from a clause, if any *)
 
+  val export_dimacs : Format.formatter -> unit -> unit
+  (** Prints the entire set of clauses in the input problem
+      (including hypothesis, lemmas and local assumptions),
+      in the dimacs format. *)
 end
 
diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index d67aca27..db08a2bc 100644
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
@@ -301,6 +301,16 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
       name pp_atoms_vec arr pp_premise cp
 
+  let pp_dimacs fmt { atoms; } =
+    let aux fmt a =
+      Array.iter (fun p ->
+          Format.fprintf fmt "%s%d "
+            (if p == p.var.pa then "-" else "")
+            (p.var.vid+1)
+        ) a
+    in
+    Format.fprintf fmt "%a0" aux atoms
+
 end
 
 
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index 1d3e0dc4..5e42a169 100644
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
@@ -142,6 +142,7 @@ module type S = sig
   val pp_lit : Format.formatter -> lit -> unit
   val pp_atom : Format.formatter -> atom -> unit
   val pp_clause : Format.formatter -> clause -> unit
+  val pp_dimacs : Format.formatter -> clause -> unit
   (** Debug function for atoms and clauses (very verbose) *)
 
 end