Added iCNF export to external

src/core/external.ml

@@ -118,12 +118,49 @@ module Make
 
   let get_tag cl = St.(cl.tag)
 
+  (* 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_dimacs fmt () =
-    (* Local assertions *)
-    let tmp = S.temp () in
-    assert (Vec.for_all (function
-        | { St.cpremise = St.Local; _} -> true | _ -> false
-      ) tmp);
     (* Problem hypothses *)
     let hyps = S.hyps () in
     assert (Vec.for_all (function
@@ -132,34 +169,47 @@ module Make
     (* Learnt clauses, then filtered to only keep only
        the theory lemmas; all other learnt clauses should be logical
        consequences of the rest. *)
-    let learnt = S.history () in
+    let lemmas = filter_vec (S.history ()) in
-    let lemmas = Vec.make (Vec.size learnt) St.dummy_clause in
+    (* Local assertions *)
-    Vec.iter (fun c ->
+    let tmp = S.temp () in
-        match c.St.cpremise with
+    assert (Vec.for_all (function
-        | St.Hyp | St.Local -> assert false
+        | { St.cpremise = St.Local; _} -> true | _ -> false
-        | St.Lemma _ -> Vec.push lemmas c
+      ) tmp);
-        | St.History l ->
-          begin match l with
-            | [] -> assert false
-            | d :: _ ->
-              begin match d.St.cpremise with
-                | St.Lemma _ -> Vec.push lemmas d
-                | St.Hyp | St.Local | St.History _ -> ()
-              end
-          end
-      ) learnt;
     (* Number of atoms and clauses *)
     let n = St.nb_elt () in
     let m = Vec.size tmp + Vec.size hyps + Vec.size lemmas in
-    (* Actual printing *)
-    let pp s fmt vec =
-      Format.fprintf fmt "c %s@,%a@," s (Vec.print ~sep:"" St.pp_dimacs) vec
-    in
     Format.fprintf fmt
-      "@[<v>p cnf %d %d@,%a%a%a@]@."
+      "@[<v>p cnf %d %d@,%a%a%a@]@." n m
-      n m
+      (export_vec "Local assumptions") tmp
-      (pp "Local assumptions") tmp
+      (export_vec "Hypotheses") hyps
-      (pp "Hypotheses") hyps
+      (export_vec "Lemmas") lemmas
-      (pp "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 () =
+    (* 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
 
 end

src/core/solver_intf.ml

@@ -76,5 +76,10 @@ module type S = sig
   (** Prints the entire set of clauses in the input problem
       (including hypothesis, lemmas and local assumptions),
       in the dimacs format. *)
+
+  val export_icnf : Format.formatter -> unit -> unit
+  (** Export the current problem contents to iCNF format.
+      This function is meant to be used icnrementally, i.e.
+      called for each return value of the solve function. *)
 end