Struct ImplicationGraph 

pub struct ImplicationGraph { /* private fields */ }

Implication graph for CDCL.

Implementations

impl ImplicationGraph

pub fn new() -> Self

Create new implication graph.

pub fn with_config(config: ImplicationGraphConfig) -> Self

Create with configuration.

pub fn stats(&self) -> &ImplicationGraphStats

Get statistics.

pub fn add_decision(&mut self, lit: Lit, level: Level)

Add decision literal.

pub fn add_propagation(&mut self, lit: Lit, level: Level, antecedents: Vec<Lit>)

Add propagated literal.

pub fn find_first_uip( &mut self, conflict_lits: &[Lit], decision_level: Level, ) -> Option<Lit>

Find first UIP (Unique Implication Point) for conflict.

Returns the literal that is the first UIP cut point.

pub fn get_level(&self, lit: Lit) -> Option<Level>

Get decision level of literal.

pub fn get_antecedents(&self, lit: Lit) -> Option<&[Lit]>

Get antecedents of literal.

pub fn compute_backjump_level(&self, clause: &[Lit]) -> Level

Compute backjump level for learned clause.

Returns the second-highest decision level in the clause.

pub fn backtrack(&mut self, level: Level)

Backtrack to decision level.

pub fn clear(&mut self)

Clear graph.

pub fn num_nodes(&self) -> usize

Get number of nodes.

pub fn current_level(&self) -> Level

Get current decision level.

Trait Implementations

impl Default for ImplicationGraph

fn default() -> Self

Returns the “default value” for a type.