Struct AssumptionStack 

pub struct AssumptionStack { /* private fields */ }

Assumption stack with level management

Implementations

impl AssumptionStack

pub fn new() -> Self

Create a new assumption stack

pub fn push(&mut self, lit: Lit) -> Result<(), String>

Push an assumption at the current level

pub fn push_with_data(&mut self, lit: Lit, data: u64) -> Result<(), String>

Push an assumption with user data

pub fn new_level(&mut self)

Create a new assumption level

pub fn pop_level(&mut self)

Pop all assumptions at the current level and above

pub fn clear(&mut self)

Clear all assumptions

pub fn get_all(&self) -> &[Assumption]

Get all assumptions as a slice

pub fn get_literals(&self) -> Vec<Lit>

Get assumptions as literals

pub fn get_at_level(&self, level: AssumptionLevel) -> Vec<&Assumption>

Get assumptions at a specific level

pub fn is_assumed(&self, lit: Lit) -> bool

Check if a literal is assumed

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

Get the level of an assumption

pub fn set_conflict(&mut self, core: Vec<Lit>)

Set the conflict set from UNSAT core

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

Get the conflict set

pub fn current_level(&self) -> AssumptionLevel

Get the current level

pub fn len(&self) -> usize

Get number of assumptions

pub fn is_empty(&self) -> bool

Check if empty

Trait Implementations

impl Default for AssumptionStack

fn default() -> Self

Returns the “default value” for a type.