Struct LearnedClause

Source

pub struct LearnedClause {
    pub lits: Vec<Lit>,
    pub id: u64,
    pub hints: Vec<u64>,
}

Expand description

A learned clause logged for proof reconstruction. Each is a resolvent derivable from the formula by reverse unit propagation — the unit of a DRAT/LRAT proof. With proof tracing on (Solver::set_lrat) it carries its LRAT step: its id and the ids of the clauses that, in order, each become unit under its negation until the last conflicts.

Fields§

§lits: Vec<Lit>§id: u64§hints: Vec<u64>

LearnedClause

Struct LearnedClause Copy item path

Fields§

Trait Implementations§

impl Clone for LearnedClause

fn clone(&self) -> LearnedClause

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

impl Debug for LearnedClause

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

Auto Trait Implementations§

impl Freeze for LearnedClause

impl RefUnwindSafe for LearnedClause

impl Send for LearnedClause

impl Sync for LearnedClause

impl Unpin for LearnedClause

impl UnsafeUnpin for LearnedClause

impl UnwindSafe for LearnedClause

Blanket Implementations§

impl<T> Any for Twhere T: 'static + ?Sized,

fn type_id(&self) -> TypeId

impl<T> Borrow<T> for Twhere T: ?Sized,

fn borrow(&self) -> &T

impl<T> BorrowMut<T> for Twhere T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

impl<T> CloneToUninit for Twhere T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

impl<T> From<T> for T

fn from(t: T) -> T

impl<T, U> Into<U> for Twhere U: From<T>,

fn into(self) -> U

impl<T> ToOwned for Twhere T: Clone,

type Owned = T

fn to_owned(&self) -> T

fn clone_into(&self, target: &mut T)

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

type Error = Infallible

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Struct LearnedClause

impl<T> Any for T
where T: 'static + ?Sized,

impl<T> Borrow<T> for T
where T: ?Sized,

impl<T> BorrowMut<T> for T
where T: ?Sized,

impl<T> CloneToUninit for T
where T: Clone,

impl<T, U> Into<U> for T
where U: From<T>,

impl<T> ToOwned for T
where T: Clone,

impl<T, U> TryFrom<U> for T
where U: Into<T>,

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,