pub struct DynamicLbdManager { /* private fields */ }Expand description
Dynamic LBD manager
Implementations§
Source§impl DynamicLbdManager
impl DynamicLbdManager
Sourcepub fn stats(&self) -> &DynamicLbdStats
pub fn stats(&self) -> &DynamicLbdStats
Get statistics
Sourcepub fn on_conflict(&mut self)
pub fn on_conflict(&mut self)
Increment conflict counter
Sourcepub fn should_update(&self) -> bool
pub fn should_update(&self) -> bool
Check if it’s time to update LBDs
Sourcepub fn update_clause_lbd(
&mut self,
clause_id: ClauseId,
clauses: &mut ClauseDatabase,
level: &[u32],
) -> bool
pub fn update_clause_lbd( &mut self, clause_id: ClauseId, clauses: &mut ClauseDatabase, level: &[u32], ) -> bool
Update LBD for a single clause
Returns true if the LBD was improved
Sourcepub fn update_all_lbds(
&mut self,
clauses: &mut ClauseDatabase,
level: &[u32],
) -> u64
pub fn update_all_lbds( &mut self, clauses: &mut ClauseDatabase, level: &[u32], ) -> u64
Update LBDs for all learned clauses
Returns the number of clauses with improved LBD
Sourcepub fn maybe_update(
&mut self,
clauses: &mut ClauseDatabase,
level: &[u32],
) -> u64
pub fn maybe_update( &mut self, clauses: &mut ClauseDatabase, level: &[u32], ) -> u64
Update LBDs if it’s time to do so
Returns the number of clauses with improved LBD, or 0 if not time to update
Sourcepub fn reset_conflicts(&mut self)
pub fn reset_conflicts(&mut self)
Reset conflict counter
Auto Trait Implementations§
impl Freeze for DynamicLbdManager
impl RefUnwindSafe for DynamicLbdManager
impl Send for DynamicLbdManager
impl Sync for DynamicLbdManager
impl Unpin for DynamicLbdManager
impl UnsafeUnpin for DynamicLbdManager
impl UnwindSafe for DynamicLbdManager
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more