Struct Watches 

pub struct Watches {
    pub clause_id: usize,
    pub blocker: Literal,
}

双观察文字（2WL）中的 watcher 条目。

其核心思想是：只跟踪每个子句中的少量关键文字，从而避免每次传播都整句扫描。

• clause_id 指向被监视的子句；
• blocker 通常存“另一个被监视文字”，若其已为真，则该子句已满足，可快速跳过。

flowchart LR C[子句 C 监视 l0 与 l1] --> W0[watch(-l0) 存 watcher] C --> W1[watch(-l1) 存 watcher] W0 --> P[当 l0 被赋假时触发检查] W1 --> Q[当 l1 被赋假时触发检查]

例：若子句监视 x3 与 -x8，则 watcher 分别放在 watch(-x3) 与 watch(x8)。

Fields

clause_id: usize

blocker: Literal

Trait Implementations

impl Clone for Watches

fn clone(&self) -> Watches

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Watches

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Watches

fn default() -> Watches

Returns the “default value” for a type.

impl Copy for Watches