From 2ff1279f266b7814473090f9fb5d748a0bcb2c94 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 13 Jul 2016 17:44:04 +0200
Subject: [PATCH] Better perfs for unsat_core

---
 solver/res.ml               | 27 ++++++++++++++++++---------
 solver/solver_types.ml      |  3 +++
 solver/solver_types_intf.ml |  1 +
 3 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/solver/res.ml b/solver/res.ml
index 2663dcb5..2195ef0d 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -158,18 +158,27 @@ module Make(St : Solver_types.S) = struct
       { conclusion; step = Resolution (c', d', a); }
 
   (* Compute unsat-core
-     TODO: the uniq sort at the end may be costly, maybe remove it,
-           or compare the clauses faster ? *)
+     TODO: replace visited bool by a int unique to each call
+     of unsat_core, so that the cleanup can be removed ? *)
   let unsat_core proof =
-    let rec aux acc = function
-      | [] -> acc
+    let rec aux res acc = function
+      | [] -> res, acc
       | c :: r ->
-        begin match c.St.cpremise with
-          | St.Hyp _ | St.Lemma _ -> aux (c :: acc) r
-          | St.History l -> aux acc (l @ r)
-        end
+        if not c.St.visited then begin
+          c.St.visited <- true;
+          match c.St.cpremise with
+            | St.Hyp _ | St.Lemma _ -> aux (c :: res) acc r
+            | St.History h ->
+              let l = List.fold_left (fun acc c ->
+                  if not c.St.visited then c :: acc else acc) r h in
+              aux res (c :: acc) l
+        end else
+          aux res acc r
     in
-    sort_uniq cmp (aux [] [proof])
+    let res, tmp = aux [] [] [proof] in
+    List.iter (fun c -> c.St.visited <- false) res;
+    List.iter (fun c -> c.St.visited <- false) tmp;
+    res
 
   (* Iter on proofs *)
   module H = Hashtbl.Make(struct
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index f6cdaa37..414648ae 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -63,6 +63,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     mutable cpremise : premise;
     mutable activity : float;
     mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =
@@ -106,6 +107,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       attached = false;
       c_level = -1;
       learnt = false;
+      visited = false;
       cpremise = History [] }
 
   let () =
@@ -192,6 +194,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       tag = tag;
       atoms = atoms;
       attached = false;
+      visited = false;
       learnt = is_learnt;
       c_level = level;
       activity = 0.;
diff --git a/solver/solver_types_intf.ml b/solver/solver_types_intf.ml
index cb14fd89..740ee05d 100644
--- a/solver/solver_types_intf.ml
+++ b/solver/solver_types_intf.ml
@@ -58,6 +58,7 @@ module type S = sig
     mutable cpremise : premise;
     mutable activity : float;
     mutable attached : bool;
+    mutable visited : bool;
   }
 
   and reason =