[−][src]Trait splr::cdb::ClauseDBIF

pub trait ClauseDBIF: IndexMut<ClauseId, Output = Clause> {
    pub fn len(&self) -> usize;

    pub fn is_empty(&self) -> bool;

    pub fn iter(&self) -> Iter<'_, Clause>;

    pub fn iter_mut(&mut self) -> IterMut<'_, Clause>;

    pub fn bin_watcher_lists(&self) -> &[Vec<Watch>];

    pub fn watcher_list(&self, l: Lit) -> &[Watch];

    pub fn watcher_lists_mut(&mut self) -> &mut [Vec<Watch>];

    pub fn detach(&mut self, cid: ClauseId);

    pub fn check_and_reduce<A>(&mut self, asg: &A, nc: usize) -> bool
    where
        A: AssignIF;

    pub fn reset(&mut self);

    pub fn garbage_collect(&mut self);

    pub fn registered_bin_clause(&self, l0: Lit, l1: Lit) -> bool;

    pub fn new_clause<A>(
        &mut self, 
        asg: &mut A, 
        v: &mut Vec<Lit>, 
        learnt: bool, 
        level_sort: bool
    ) -> ClauseId
    where
        A: AssignIF;

    pub fn mark_clause_as_used<A>(&mut self, asg: &mut A, cid: ClauseId) -> bool
    where
        A: AssignIF;

    pub fn count(&self) -> usize;

    pub fn countf(&self, mask: Flag) -> usize;

    pub fn certificate_add(&mut self, vec: &[Lit]);

    pub fn certificate_delete(&mut self, vec: &[Lit]);

    pub fn touch_var(&mut self, vi: VarId);

    pub fn check_size(&self) -> Result<bool, SolverError>;

    pub fn validate(
        &self, 
        model: &[Option<bool>], 
        strict: bool
    ) -> Option<ClauseId>;

    pub fn strengthen(&mut self, cid: ClauseId, p: Lit) -> bool;

    pub fn minimize_with_biclauses<A>(&mut self, asg: &A, vec: &mut Vec<Lit>)
    where
        A: AssignIF;
}

API for clause management like check_and_reduce, new_clause, watcher_list, and so on.

Required methods

pub fn len(&self) -> usize[src]

return the length of clause.

pub fn is_empty(&self) -> bool[src]

return true if it's empty.

pub fn iter(&self) -> Iter<'_, Clause>[src]

return an iterator.

pub fn iter_mut(&mut self) -> IterMut<'_, Clause>[src]

return a mutable iterator.

pub fn bin_watcher_lists(&self) -> &[Vec<Watch>][src]

return the list of bin_watch lists

pub fn watcher_list(&self, l: Lit) -> &[Watch][src]

return a watcher list

pub fn watcher_lists_mut(&mut self) -> &mut [Vec<Watch>][src]

return the list of watch lists

pub fn detach(&mut self, cid: ClauseId)[src]

un-register a clause cid from clause database and make the clause dead.

pub fn check_and_reduce<A>(&mut self, asg: &A, nc: usize) -> bool where
    A: AssignIF, [src]

check a condition to reduce.

  • return true if reduction is done.
  • Otherwise return false.

CAVEAT

precondition: decision level == 0.

pub fn reset(&mut self)[src]

pub fn garbage_collect(&mut self)[src]

delete dead clauses from database, which are made by:

  • reduce
  • simplify
  • kill

pub fn registered_bin_clause(&self, l0: Lit, l1: Lit) -> bool[src]

return true if a literal pair (l0, l1) is registered.

pub fn new_clause<A>(
    &mut self,
    asg: &mut A,
    v: &mut Vec<Lit>,
    learnt: bool,
    level_sort: bool
) -> ClauseId where
    A: AssignIF, [src]

allocate a new clause and return its id.

  • If level_sort is on, register v as a learnt after sorting based on assign level.
  • Otherwise, register v as a permanent clause, which rank is zero.

pub fn mark_clause_as_used<A>(&mut self, asg: &mut A, cid: ClauseId) -> bool where
    A: AssignIF, [src]

update LBD then convert a learnt clause to permanent if needed.

pub fn count(&self) -> usize[src]

return the number of alive clauses in the database.

pub fn countf(&self, mask: Flag) -> usize[src]

return the number of clauses which satisfy given flags and aren't DEAD.

pub fn certificate_add(&mut self, vec: &[Lit])[src]

record a clause to unsat certification.

pub fn certificate_delete(&mut self, vec: &[Lit])[src]

record a deleted clause to unsat certification.

pub fn touch_var(&mut self, vi: VarId)[src]

flag positive and negative literals of a var as dirty

pub fn check_size(&self) -> Result<bool, SolverError>[src]

check the number of clauses

  • Err(SolverError::OutOfMemory) -- the db size is over the limit.
  • Ok(true) -- enough small
  • Ok(false) -- close to the limit

pub fn validate(&self, model: &[Option<bool>], strict: bool) -> Option<ClauseId>[src]

returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment. Clauses with an unassigned literal are treated as falsified in strict mode.

pub fn strengthen(&mut self, cid: ClauseId, p: Lit) -> bool[src]

removes Lit p from Clause self. This is an O(n) function! This returns true if the clause became a unit clause. And this is called only from Eliminator::strengthen_clause.

pub fn minimize_with_biclauses<A>(&mut self, asg: &A, vec: &mut Vec<Lit>) where
    A: AssignIF, [src]

minimize a clause.

Loading content...

Implementors

impl ClauseDBIF for ClauseDB[src]

pub fn detach(&mut self, cid: ClauseId)[src]

Warning

this function is the only function that turns Flag::DEAD on without calling garbage_collect which erases all the DEAD flags. So you must care about how and when garbage_collect is called.

Loading content...