[−][src]Struct splr::propagator::AssignStack
A record of assignment. It's called 'trail' in Glucose.
Fields
trail: Vec<Lit>
assign: Vec<Lbool>
Trait Implementations
impl PropagatorIF for AssignStack
[src]
fn new(n: usize) -> AssignStack
[src]
fn len(&self) -> usize
[src]
fn is_empty(&self) -> bool
[src]
fn level(&self) -> usize
[src]
fn is_zero(&self) -> bool
[src]
fn num_at(&self, n: usize) -> usize
[src]
fn remains(&self) -> bool
[src]
fn assigned(&self, l: Lit) -> Lbool
[src]
fn enqueue(
&mut self,
v: &mut Var,
sig: Lbool,
cid: ClauseId,
dl: usize
) -> MaybeInconsistent
[src]
&mut self,
v: &mut Var,
sig: Lbool,
cid: ClauseId,
dl: usize
) -> MaybeInconsistent
fn enqueue_null(&mut self, v: &mut Var, sig: Lbool)
[src]
fn propagate(
&mut self,
cdb: &mut ClauseDB,
state: &mut State,
vars: &mut VarDB
) -> ClauseId
[src]
&mut self,
cdb: &mut ClauseDB,
state: &mut State,
vars: &mut VarDB
) -> ClauseId
propagate without checking dead clauses
Note: this function assumes there's no dead clause.
So Eliminator should call garbage_collect
before me.
fn cancel_until(&mut self, vars: &mut VarDB, lv: usize)
[src]
fn uncheck_enqueue(&mut self, vars: &mut VarDB, l: Lit, cid: ClauseId)
[src]
fn uncheck_assume(&mut self, vars: &mut VarDB, l: Lit)
[src]
fn select_var(&mut self, vars: &VarDB) -> VarId
[src]
fn update_order(&mut self, vec: &VarDB, v: VarId)
[src]
fn dump_cnf(&mut self, cdb: &ClauseDB, state: &State, vars: &VarDB, fname: &str)
[src]
impl Debug for AssignStack
[src]
impl Display for AssignStack
[src]
Auto Trait Implementations
impl Send for AssignStack
impl Unpin for AssignStack
impl Sync for AssignStack
impl UnwindSafe for AssignStack
impl RefUnwindSafe for AssignStack
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,