Struct Cdcl 

pub struct Cdcl {
    pub kind: CdclKind,
    pub frame: StackIdx,
    pub propagates: Vec<LitIdx>,
    pub conflicts: bool,
}

Fields

kind: CdclKind

frame: StackIdx

propagates: Vec<LitIdx>

After an assignment some clauses may have only 1 unassigned literal left (with all others not satisfying the clause). Thus a decision propagates other assignments which are required.

conflicts: bool

Implementations

impl Cdcl

pub fn root(frame: StackIdx) -> Self

Creates the Root node of the CDCL tree. Should only be used once.

pub fn begin_check(parent: Option<CdclIdx>, frame: StackIdx) -> Self

Creates a BeginCheck node in the CDCL tree.

pub fn new_empty(parent: CdclIdx, frame: StackIdx) -> Self

Creates a Empty node in the CDCL tree.

pub fn new_decision(lit: LitIdx, frame: StackIdx) -> Self

pub fn new_conflict(conflict: Conflict, frame: StackIdx) -> Self

pub fn backlink(&self, cidx: CdclIdx) -> CdclBacklink

Return a pair of the previous node and the backtrack node. If the backtrack node is set then its the parent otherwise the previous node is

pub fn get_assignments(&self) -> impl Iterator<Item = LitIdx> + '_

Trait Implementations

impl Clone for Cdcl

fn clone(&self) -> Cdcl

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Cdcl

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.