Struct ActivityTable 

pub struct ActivityTable {
    pq: KeyedPriorityQueue<usize, OrderedFloat<f64>>,
    activities: Vec<f64>,
    var_inc: f64,
    var_decay: f64,
}

VSIDS 的变量活跃度表。

启发式目标：

• 冲突相关变量会被 bump，分数上升；
• var_inc 随冲突递增并经衰减控制，强调近期冲突；
• 通过优先队列选取当前分数最高的未赋值变量。

例：设初始 var_inc = 1.0、var_decay = 0.8。

• 第 1 次冲突命中变量 v：activity[v] += 1.0
• 调用 decay_inc() 后：var_inc = 1.25
• 第 2 次冲突再次命中 v：activity[v] += 1.25

因而近期冲突对分数贡献更大，变量选择会更偏向“最近导致冲突”的区域。

Fields

pq: KeyedPriorityQueue<usize, OrderedFloat<f64>>

activities: Vec<f64>

var_inc: f64

var_decay: f64

Implementations

impl ActivityTable

pub fn new(max_vars: usize) -> Self

初始化活跃度表并把所有变量放入优先队列。

pub fn bump_var_score(&mut self, var_id: usize)

提升变量活跃度（通常在冲突分析中调用）。

若变量已在堆中，更新其优先级； 若暂不在堆中，按当前活跃度重新插入。

pub fn decay_inc(&mut self)

增大“本轮 bump 的权重”，体现 EVSIDS 的近期偏好。

pub fn bump_decay_factor(&mut self)

调整衰减系数，逐步降低历史冲突的影响。

pub fn next_variable<F>(&mut self, not_assigned: &F) -> Option<usize>

where F: Fn(usize) -> bool,

选取下一个未赋值变量。

not_assigned 由调用方提供，用于过滤当前已赋值变量。