Moved Dimacs problem export in its own module

src/backend/dimacs.ml

@@ -0,0 +1,121 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module type S = sig
+
+  type clause
+
+  val export :
+    Format.formatter ->
+    hyps:clause Vec.t ->
+    history:clause Vec.t ->
+    local:clause Vec.t ->
+    unit
+  (** Export the given clause vectors to the dimacs format.
+      The arguments should be transmitted directly from the corresponding
+      function of the {Internal} module. *)
+
+  val export_icnf :
+    Format.formatter ->
+    hyps:clause Vec.t ->
+    history:clause Vec.t ->
+    local:clause Vec.t ->
+    unit
+  (** Export the given clause vectors to the dimacs format.
+      The arguments should be transmitted directly from the corresponding
+      function of the {Internal} module. *)
+
+end
+
+module Make(St : Solver_types.S) = struct
+
+  (* Dimacs & iCNF export *)
+  let export_vec name fmt vec =
+    Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.pp_dimacs) vec
+
+  let export_assumption fmt vec =
+    Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec
+
+  let export_icnf r name map_filter fmt vec =
+    let aux fmt v =
+      for i = !r to (Vec.size vec) - 1 do
+        let x = Vec.get vec i in
+        match map_filter x with
+        | None -> ()
+        | Some y -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i)
+      done;
+      r := Vec.size vec
+    in
+    Format.fprintf fmt "c %s@,%a" name aux vec
+
+  let map_filter_learnt c =
+    match c.St.cpremise with
+    | St.Hyp | St.Local -> assert false
+    | St.Lemma _ -> Some c
+    | St.History l ->
+      begin match l with
+        | [] -> assert false
+        | d :: _ ->
+          begin match d.St.cpremise with
+            | St.Lemma _ -> Some d
+            | St.Hyp | St.Local | St.History _ -> None
+          end
+      end
+
+  let filter_vec learnt =
+    let lemmas = Vec.make (Vec.size learnt) St.dummy_clause in
+    Vec.iter (fun c ->
+        match map_filter_learnt c with
+        | None -> ()
+        | Some d -> Vec.push lemmas d
+      ) learnt;
+    lemmas
+
+  let export fmt ~hyps ~history ~local =
+    assert (Vec.for_all (function
+        | { St.cpremise = St.Hyp; _} -> true | _ -> false
+      ) hyps);
+    (* Learnt clauses, then filtered to only keep only
+       the theory lemmas; all other learnt clauses should be logical
+       consequences of the rest. *)
+    let lemmas = filter_vec history in
+    (* Local assertions *)
+    assert (Vec.for_all (function
+        | { St.cpremise = St.Local; _} -> true | _ -> false
+      ) local);
+    (* Number of atoms and clauses *)
+    let n = St.nb_elt () in
+    let m = Vec.size local + Vec.size hyps + Vec.size lemmas in
+    Format.fprintf fmt
+      "@[<v>p cnf %d %d@,%a%a%a@]@." n m
+      (export_vec "Local assumptions") local
+      (export_vec "Hypotheses") hyps
+      (export_vec "Lemmas") lemmas
+
+  (* Refs to remember what portion of a problem has been printed *)
+  let icnf_hyp = ref 0
+  let icnf_lemmas = ref 0
+
+  let export_icnf fmt ~hyps ~history ~local =
+    assert (Vec.for_all (function
+        | { St.cpremise = St.Hyp; _} -> true | _ -> false
+      ) hyps);
+    let lemmas = history in
+    (* Local assertions *)
+    let l = List.map (function
+        | {St.cpremise = St.Local; atoms = [| a |] } -> a
+        | _ -> assert false) (Vec.to_list local) in
+    let local = St.make_clause "local (tmp)" l St.Local in
+    (* Number of atoms and clauses *)
+    Format.fprintf fmt
+      "@[<v>%s@,%a%a%a@]@."
+      (if !icnf_hyp = 0 && !icnf_lemmas = 0 then "p inccnf" else "")
+      (export_icnf icnf_hyp "Hypotheses" (fun x -> Some x)) hyps
+      (export_icnf icnf_lemmas "Lemmas" map_filter_learnt) lemmas
+      export_assumption local
+
+end
+

src/backend/dimacs.mli

@@ -0,0 +1,45 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Dimacs backend for problems
+
+    This module provides functiosn to export problems to the dimacs and
+    iCNF formats.
+*)
+
+module type S = sig
+
+  type clause
+  (** The type of clauses *)
+
+  val export :
+    Format.formatter ->
+    hyps:clause Vec.t ->
+    history:clause Vec.t ->
+    local:clause Vec.t ->
+    unit
+  (** Export the given clause vectors to the dimacs format.
+      The arguments should be transmitted directly from the corresponding
+      function of the {Internal} module. *)
+
+  val export_icnf :
+    Format.formatter ->
+    hyps:clause Vec.t ->
+    history:clause Vec.t ->
+    local:clause Vec.t ->
+    unit
+  (** Export the given clause vectors to the dimacs format.
+      The arguments should be transmitted directly from the corresponding
+      function of the {Internal} module.
+      This function may be called multiple times in order to add
+      new clauses (and new local hyps) to the problem.
+  *)
+
+end
+
+module Make(St: Solver_types.S) : S with type clause := St.clause
+(** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *)
+

src/backend/dot.ml

@@ -4,17 +4,23 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Output interface for the backend *)
 module type S = Backend_intf.S
 
+(** Input module for the backend *)
 module type Arg = sig
 
   type atom
   type lemma
+  (** Types *)
 
   val print_atom : Format.formatter -> atom -> unit
   val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Printing functions for atoms and lemmas. *)
+
 end
 
+(** Functor to provide dot printing *)
 module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) = struct
 
   let node_id n = n.S.conclusion.S.St.name

src/backend/dot.mli

@@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
 
 (** Dot backend for proofs
 
-    This modules provides functions to export proofs into the dot graph format.
+    This module provides functions to export proofs into the dot graph format.
     Graphs in dot format can be used to generates images using the graphviz tool.
 *)
 

src/core/external.ml

@@ -120,97 +120,18 @@ module Make
   let new_atom = S.new_atom
 
   (* Dimacs & iCNF export *)
-  let export_vec name fmt vec =
-    Format.fprintf fmt "c %s@,%a@," name (Vec.print ~sep:"" St.pp_dimacs) vec
-
-  let export_assumption fmt vec =
-    Format.fprintf fmt "c Local assumptions@,a %a@," St.pp_dimacs vec
-
-  let export_icnf r name map_filter fmt vec =
-    let aux fmt v =
-      for i = !r to (Vec.size vec) - 1 do
-        let x = Vec.get vec i in
-        match map_filter x with
-        | None -> ()
-        | Some y -> Format.fprintf fmt "%a@," St.pp_dimacs (Vec.get vec i)
-      done;
-      r := Vec.size vec
-    in
-    Format.fprintf fmt "c %s@,%a" name aux vec
-
-  let map_filter_learnt c =
-    match c.St.cpremise with
-    | St.Hyp | St.Local -> assert false
-    | St.Lemma _ -> Some c
-    | St.History l ->
-      begin match l with
-        | [] -> assert false
-        | d :: _ ->
-          begin match d.St.cpremise with
-            | St.Lemma _ -> Some d
-            | St.Hyp | St.Local | St.History _ -> None
-          end
-      end
-
-  let filter_vec learnt =
-    let lemmas = Vec.make (Vec.size learnt) St.dummy_clause in
-    Vec.iter (fun c ->
-        match map_filter_learnt c with
-        | None -> ()
-        | Some d -> Vec.push lemmas d
-      ) learnt;
-    lemmas
+  module D = Dimacs.Make(St)
 
   let export_dimacs fmt () =
-    (* Problem hypothses *)
     let hyps = S.hyps () in
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Hyp; _} -> true | _ -> false
-      ) hyps);
-    (* Learnt clauses, then filtered to only keep only
-       the theory lemmas; all other learnt clauses should be logical
-       consequences of the rest. *)
-    let lemmas = filter_vec (S.history ()) in
-    (* Local assertions *)
-    let tmp = S.temp () in
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Local; _} -> true | _ -> false
-      ) tmp);
-    (* Number of atoms and clauses *)
-    let n = St.nb_elt () in
-    let m = Vec.size tmp + Vec.size hyps + Vec.size lemmas in
-    Format.fprintf fmt
-      "@[<v>p cnf %d %d@,%a%a%a@]@." n m
-      (export_vec "Local assumptions") tmp
-      (export_vec "Hypotheses") hyps
-      (export_vec "Lemmas") lemmas
-
-  (* Refs to remember what portion of a problem has been printed *)
-  let icnf_hyp = ref 0
-  let icnf_lemmas = ref 0
+    let history = S.history () in
+    let local = S.temp () in
+    D.export fmt ~hyps ~history ~local
 
   let export_icnf fmt () =
-    (* Problem hypothses *)
     let hyps = S.hyps () in
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Hyp; _} -> true | _ -> false
-      ) hyps);
-    (* Learnt clauses, then filtered to only keep only
-       the theory lemmas; all other learnt clauses should be logical
-       consequences of the rest. *)
-    let lemmas = S.history () in
-    (* Local assertions *)
-    let tmp = S.temp () in
-    let l = List.map (function
-        | {St.cpremise = St.Local; atoms = [| a |] } -> a
-        | _ -> assert false) (Vec.to_list tmp) in
-    let local = St.make_clause "local (tmp)" l St.Local in
-    (* Number of atoms and clauses *)
-    Format.fprintf fmt
-      "@[<v>%s@,%a%a%a@]@."
-      (if !icnf_hyp = 0 && !icnf_lemmas = 0 then "p inccnf" else "")
-      (export_icnf icnf_hyp "Hypotheses" (fun x -> Some x)) hyps
-      (export_icnf icnf_lemmas "Lemmas" map_filter_learnt) lemmas
-      export_assumption local
+    let history = S.history () in
+    let local = S.temp () in
+    D.export_icnf fmt ~hyps ~history ~local
 
 end

src/doc.txt

@@ -86,6 +86,7 @@ interfaces are not part of the main API and so are subject to a lot more breakin
 than the safe modules above.
 
 {!modules:
+Dimacs
 Internal
 External
 Solver_types

src/msat.mlpack

@@ -22,6 +22,7 @@ Solver_types
 Res
 Backend_intf
 Dot
+Dimacs
 Dedukti
 
 # Auxiliary modules