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

pub trait ClauseDBIF {
    fn new(config: &Config, nv: usize, nc: usize) -> Self;

    fn len(&self) -> usize;

    fn is_empty(&self) -> bool;

    fn attach(
        &mut self, 
        state: &mut State, 
        vars: &mut VarDB, 
        lbd: usize
    ) -> ClauseId;

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

    fn reduce(&mut self, state: &mut State, vars: &mut VarDB);

    fn simplify(
        &mut self, 
        asgs: &mut AssignStack, 
        elim: &mut Eliminator, 
        state: &mut State, 
        vars: &mut VarDB
    ) -> MaybeInconsistent;

    fn reset(&mut self);

    fn garbage_collect(&mut self);

    fn new_clause(&mut self, v: &[Lit], rank: usize, learnt: bool) -> ClauseId;

    fn reset_lbd(&mut self, vars: &VarDB, temp: &mut [usize]);

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

    fn scale_activity(&mut self);

    fn count(&self, alive: bool) -> usize;

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

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

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

    fn eliminate_satisfied_clauses(
        &mut self, 
        elim: &mut Eliminator, 
        vars: &mut VarDB, 
        occur: bool
    );

    fn check_size(&self) -> MaybeInconsistent;

    fn make_permanent(&mut self, reinit: bool);
}

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

Required methods

fn new(config: &Config, nv: usize, nc: usize) -> Self

return a new instance.

fn len(&self) -> usize

return the length of clause.

fn is_empty(&self) -> bool

return true if it's empty.

fn attach(
    &mut self,
    state: &mut State,
    vars: &mut VarDB,
    lbd: usize
) -> ClauseId

make a new clause from state.new_learnt and register it to clause database.

fn detach(&mut self, cid: ClauseId)

unregister a clause cid from clause database and make the clause dead.

fn reduce(&mut self, state: &mut State, vars: &mut VarDB)

halve the number of 'learnt' or removable clauses.

fn simplify(
    &mut self,
    asgs: &mut AssignStack,
    elim: &mut Eliminator,
    state: &mut State,
    vars: &mut VarDB
) -> MaybeInconsistent

simplify database by:

  • removing satisfiable clauses
  • calling exhaustive simplifier that tries clause subsumption and variable elimination.

Errors

if solver becomes inconsistent.

fn reset(&mut self)

fn garbage_collect(&mut self)

delete dead clauses from database, which are made by:

  • reduce
  • simplify
  • kill

fn new_clause(&mut self, v: &[Lit], rank: usize, learnt: bool) -> ClauseId

allocate a new clause and return its id.

fn reset_lbd(&mut self, vars: &VarDB, temp: &mut [usize])

re-calculate the lbd values of all (learnt) clauses.

fn bump_activity(&mut self, cid: ClauseId)

update clause activity.

fn scale_activity(&mut self)

increment activity step.

fn count(&self, alive: bool) -> usize

return the number of alive clauses in the database. Or return the database size if active is false.

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

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

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

record a clause to unsat certification.

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

record a deleted clause to unsat certification.

fn eliminate_satisfied_clauses(
    &mut self,
    elim: &mut Eliminator,
    vars: &mut VarDB,
    occur: bool
)

delete satisfied clauses at decision level zero.

fn check_size(&self) -> MaybeInconsistent

emit an error if the db size (the number of clauses) is over the limit.

fn make_permanent(&mut self, reinit: bool)

change good learnt clauses to permanent one.

Loading content...

Implementors

impl ClauseDBIF for ClauseDB[src]

Loading content...