From c77c997ab83529f0f208660287b52fb8ca59b355 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 17 Jan 2017 12:26:18 +0100
Subject: [PATCH] Add used field to variables

---
 src/core/solver_types.ml      | 3 +++
 src/core/solver_types_intf.ml | 1 +
 2 files changed, 4 insertions(+)

diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index 36fb949b..70b3ead6 100644
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
@@ -44,6 +44,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     vid : int;
     pa : atom;
     na : atom;
+    mutable used : int;
     mutable seen : bool;
     mutable v_level : int;
     mutable v_weight : float;
@@ -92,6 +93,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     { vid = -101;
       pa = dummy_atom;
       na = dummy_atom;
+      used = 0;
       seen = false;
       v_level = -1;
       v_weight = -1.;
@@ -159,6 +161,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
           { vid = !cpt_mk_var;
             pa = pa;
             na = na;
+            used = 0;
             seen = false;
             v_level = -1;
             v_weight = 0.;
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index 94f23b67..57b47e7c 100644
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
@@ -48,6 +48,7 @@ module type S = sig
     vid : int;  (** Unique identifier *)
     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 v_level : int;      (** Level of decision/propagation *)
     mutable v_weight : float;   (** Variable weight (for the heap) *)