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

pub trait ClauseDBIF: ActivityIF<ClauseId> + IndexMut<ClauseId, Output = Clause> + Instantiate + PropertyDereference<Tusize, usize> + PropertyDereference<Tf64, f64> {
    fn len(&self) -> usize;

    fn is_empty(&self) -> bool;

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

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

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

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

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

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

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

    fn reset(&mut self);

    fn garbage_collect(&mut self);

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

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

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

    fn count(&self) -> usize;

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

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

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

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

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

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

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

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

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

Required methods

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

return the length of clause.

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

return true if it’s empty.

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

return an iterator.

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

return a mutable iterator.

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

return the list of bin_watch lists

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

return a watcher list

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

return the list of watch lists

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

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

fn reduce<A>(&mut self, asg: &mut 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.

fn reset(&mut self)[src]

fn garbage_collect(&mut self)[src]

delete dead clauses from database, which are made by:

  • reduce
  • simplify
  • kill

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

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

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.

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.

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

return the number of alive clauses in the database.

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

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

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

record a clause to unsat certification.

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

record a deleted clause to unsat certification.

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

flag positive and negative literals of a var as dirty

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

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.

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.

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]

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