Struct ResolutionNode 

pub struct ResolutionNode { /* private fields */ }

Node in the resolution graph

Implementations

impl ResolutionNode

pub fn new(id: usize, clause: Vec<Lit>, decision_level: usize) -> Self

Create a new resolution node

pub fn decision(id: usize, literal: Lit, decision_level: usize) -> Self

Create a decision node

pub fn add_resolution( &mut self, parent1: usize, parent2: usize, resolved_var: Var, )

Mark this node as a resolution of two parent clauses

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

Get the clause at this node

pub fn parents(&self) -> &[usize]

Get the parent node IDs

pub fn resolved_var(&self) -> Option<Var>

Get the variable this node resolved on

pub fn is_decision(&self) -> bool

Check if this is a decision node

pub fn decision_level(&self) -> usize

Get the decision level

Trait Implementations

impl Clone for ResolutionNode

fn clone(&self) -> ResolutionNode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolutionNode

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

Formats the value using the given formatter.