pub struct Clause {
pub rank: u16,
pub rank_old: u16,
pub search_from: u16,
/* private fields */
}
Expand description
A representation of ‘clause’
Fields§
§rank: u16
A static clause evaluation criterion like LBD, NDD, or something.
rank_old: u16
A record of the rank at previos stage.
search_from: u16
the index from which propagate
starts searching an un-falsified literal.
Since it’s just a hint, we don’t need u32 or usize.
Implementations§
Trait Implementations§
source§impl ClauseIF for Clause
impl ClauseIF for Clause
source§fn is_empty(&self) -> bool
fn is_empty(&self) -> bool
return true if it contains no literals; a clause after unit propagation.
source§fn is_dead(&self) -> bool
fn is_dead(&self) -> bool
return true if it contains no literals; a clause after unit propagation.
source§fn is_satisfied_under(&self, asg: &impl AssignIF) -> bool
fn is_satisfied_under(&self, asg: &impl AssignIF) -> bool
check clause satisfiability
source§impl FlagIF for Clause
impl FlagIF for Clause
source§impl<'a> IntoIterator for &'a Clause
impl<'a> IntoIterator for &'a Clause
source§impl<'a> IntoIterator for &'a mut Clause
impl<'a> IntoIterator for &'a mut Clause
source§impl PartialEq for Clause
impl PartialEq for Clause
source§impl PartialOrd for Clause
impl PartialOrd for Clause
1.0.0 · source§fn le(&self, other: &Rhs) -> bool
fn le(&self, other: &Rhs) -> bool
This method tests less than or equal to (for
self
and other
) and is used by the <=
operator. Read moreimpl Eq for Clause
impl StructuralPartialEq for Clause
Auto Trait Implementations§
impl RefUnwindSafe for Clause
impl Send for Clause
impl Sync for Clause
impl Unpin for Clause
impl UnwindSafe for Clause
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