Struct varisat::analyze_conflict::AnalyzeConflict

pub struct AnalyzeConflict {
    clause: Vec<Lit>,
    current_level_count: usize,
    var_flags: Vec<bool>,
    to_clean: Vec<Var>,
    involved: Vec<ClauseRef>,
    clause_hashes: Vec<ClauseHash>,
    unordered_clause_hashes: Vec<(LitIdx, ClauseHash)>,
    stack: Vec<Lit>,
}

Temporaries for conflict analysis

Fields

clause: Vec<Lit>

This is the learned clause after analysis finishes.

current_level_count: usize

Number of literals in the current clause at the current level.

var_flags: Vec<bool>

Variables in the current clause.

to_clean: Vec<Var>

Entries to clean in var_flags.

involved: Vec<ClauseRef>

Clauses to bump.

clause_hashes: Vec<ClauseHash>

Hashes of all involved clauses needed to proof the minimized clause.

unordered_clause_hashes: Vec<(LitIdx, ClauseHash)>

Clause hashes paired with the trail depth of the propagated lit.

stack: Vec<Lit>

Stack for recursive minimization.

Methods

impl AnalyzeConflict

pub fn set_var_count(&mut self, count: usize)

Update structures for a new variable count.

pub fn clause(&self) -> &[Lit]

The learned clause.

pub fn involved(&self) -> &[ClauseRef]

Long clauses involved in the conflict.

pub fn clause_hashes(&self) -> &[ClauseHash]

Hashes of clauses involved in the proof of the learned clause.

Hashes are in clause propagation order.

Trait Implementations

impl Default for AnalyzeConflict

fn default() -> AnalyzeConflict

Returns the "default value" for a type.