Trait splr::cdb::WatchDBIF

pub trait WatchDBIF {
    pub fn register(&mut self, blocker: Lit, c: ClauseId);
    pub fn detach(&mut self, n: usize);
    pub fn detach_with(&mut self, cid: ClauseId);
    pub fn update_blocker(&mut self, cid: ClauseId, l: Lit);
}

API for 'watcher list' like register, detach, update_blocker and so on.

Required methods

pub fn register(&mut self, blocker: Lit, c: ClauseId)

make a new 'watch', and add it to this watcher list.

pub fn detach(&mut self, n: usize)

remove n-th clause from the watcher list. O(1) operation.

pub fn detach_with(&mut self, cid: ClauseId)

remove a clause which id is cid from the watcher list. O(n) operation.

pub fn update_blocker(&mut self, cid: ClauseId, l: Lit)

update blocker of cid.

Loading content...

Implementations on Foreign Types

impl WatchDBIF for Vec<Watch>

pub fn register(&mut self, blocker: Lit, c: ClauseId)

pub fn detach(&mut self, n: usize)

pub fn detach_with(&mut self, cid: ClauseId)

pub fn update_blocker(&mut self, cid: ClauseId, l: Lit)

This O(n) function is used only in Eliminator. So the cost can be ignored.

Loading content...

Implementors

Loading content...