Extend the 'seen' field to store more information

src/core/internal.ml

@@ -320,14 +320,22 @@ module Make
 
   (* Eliminates atom doublons in clauses *)
   let eliminate_doublons clause : clause =
+    let trivial = ref false in
     let duplicates = ref [] in
     let res = ref [] in
     Array.iter (fun a ->
-        if a.var.seen then duplicates := a :: !duplicates
-        else (a.var.seen <- true; res := a :: !res)
+        if seen a then duplicates := a :: !duplicates
+        else (mark a; res := a :: !res)
       ) clause.atoms;
-    List.iter (fun a -> a.var.seen <- false) !res;
-    if !duplicates = [] then
+    List.iter (fun a ->
+        begin match a.var.seen with
+        | Both -> trivial := true
+        | _ -> ()
+        end;
+        clear a.var) !res;
+    if !trivial then
+      raise Trivial
+    else if !duplicates = [] then
       clause
     else
       make_clause (fresh_lname ()) !res (History [clause])
@@ -632,8 +640,8 @@ module Make
           | Some Bcp cl -> history := cl :: !history
           | _ -> assert false
         end;
-        if not q.var.seen then begin
-          q.var.seen <- true;
+        if not (q.var.seen = Both) then begin
+          q.var.seen <- Both;
           seen := q :: !seen;
           if q.var.v_level > 0 then begin
             var_bump_activity q.var;
@@ -650,7 +658,7 @@ module Make
       (* look for the next node to expand *)
       while
         let q = get_atom !tr_ind in
-        (not q.var.seen) ||
+        (not (q.var.seen = Both)) ||
         (q.var.v_level < conflict_level)
       do
         decr tr_ind;
@@ -671,7 +679,7 @@ module Make
         c := cl
       | n, _ -> assert false
     done;
-    List.iter (fun q -> q.var.seen <- false) !seen;
+    List.iter (fun q -> clear q.var) !seen;
     let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in
     let level, is_uip = backtrack_lvl l in
     { cr_backtrack_lvl = level;

src/core/solver_types.ml

@@ -30,6 +30,12 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   type formula = E.Formula.t
   type proof = E.proof
 
+  type seen =
+    | Nope
+    | Both
+    | Positive
+    | Negative
+
   type lit = {
     lid : int;
     term : term;
@@ -43,7 +49,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     pa : atom;
     na : atom;
     mutable used : int;
-    mutable seen : bool;
+    mutable seen : seen;
     mutable v_level : int;
     mutable v_weight : float;
     mutable v_assignable: lit list option;
@@ -92,7 +98,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
       pa = dummy_atom;
       na = dummy_atom;
       used = 0;
-      seen = false;
+      seen = Nope;
       v_level = -1;
       v_weight = -1.;
       v_assignable = None;
@@ -160,7 +166,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
             pa = pa;
             na = na;
             used = 0;
-            seen = false;
+            seen = Nope;
             v_level = -1;
             v_weight = 0.;
             v_assignable = None;
@@ -205,6 +211,30 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   let empty_clause = make_clause "Empty" [] (History [])
 
+  (* Marking helpers *)
+  let clear v = v.seen <- Nope
+
+  let seen a =
+    let pos = (a == a.var.pa) in
+    match a.var.seen, pos with
+    | Nope, _ -> false
+    | Both, _
+    | Positive, true
+    | Negative, false -> true
+    | Positive, false
+    | Negative, true -> false
+
+  let mark a =
+    let pos = (a == a.var.pa) in
+    match a.var.seen with
+    | Both -> ()
+    | Nope ->
+      a.var.seen <- (if pos then Positive else Negative)
+    | Positive ->
+      if pos then () else a.var.seen <- Both
+    | Negative ->
+      if pos then a.var.seen <- Both else ()
+
   (* Decisions & propagations *)
   type t =
     | Lit of lit

src/core/solver_types_intf.ml

@@ -35,6 +35,12 @@ module type S = sig
   type proof
   (** The types of terms, formulas and proofs. All of these are user-provided. *)
 
+  type seen =
+    | Nope
+    | Both
+    | Positive
+    | Negative
+
   type lit = {
     lid : int;                      (** Unique identifier *)
     term : term;                    (** Wrapped term *)
@@ -49,7 +55,7 @@ module type S = sig
     pa : atom;  (** Link for the positive atom *)
     na : atom;  (** Link for the negative atom *)
     mutable used : int;         (** Number of attached clause that contain the var *)
-    mutable seen : bool;        (** Boolean used during propagation *)
+    mutable seen : seen;        (** Boolean used during propagation *)
     mutable v_level : int;      (** Level of decision/propagation *)
     mutable v_weight : float;   (** Variable weight (for the heap) *)
     mutable v_assignable: lit list option;
@@ -163,6 +169,17 @@ module type S = sig
   val make_clause : ?tag:int -> string -> atom list -> premise -> clause
   (** [make_clause name atoms size premise] creates a clause with the given attributes. *)
 
+
+  (** {2 Helpers} *)
+
+  val mark : atom -> unit
+  (** Mark the atom as seen, using the 'seen' field in the variable. *)
+  val seen : atom -> bool
+  (** Returns wether the atom has been marked as seen. *)
+  val clear : var -> unit
+  (** Clear the 'seen' field of the variable. *)
+
+
   (** {2 Clause names} *)
 
   val fresh_name : unit -> string