simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 03:35:38 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add used field to variables

Browse source
This commit is contained in:
Guillaume Bury 2017-01-17 12:26:18 +01:00
parent b5d816fbac
commit c77c997ab8
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/core/solver_types.ml
View file

@ -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.;

1
src/core/solver_types_intf.ml
View file

@ -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) *)