[−][src]Struct varisat::assumptions::Assumptions

pub struct Assumptions {
    assumptions: Vec<Lit>,
    failed_core: Vec<Lit>,
    user_failed_core: Vec<Lit>,
    assumption_levels: usize,
    failed_propagation_hashes: Vec<ClauseHash>,
}

Incremental solving.

Fields

assumptions: Vec<Lit>failed_core: Vec<Lit>user_failed_core: Vec<Lit>assumption_levels: usizefailed_propagation_hashes: Vec<ClauseHash>

Methods

impl Assumptions[src]

pub fn assumption_levels(&self) -> usize[src]

Current number of decision levels used for assumptions.

pub fn full_restart(&mut self)[src]

Resets assumption_levels to zero on a full restart.

pub fn failed_core(&self) -> &[Lit][src]

Subset of assumptions that made the formula unsatisfiable.

pub fn user_failed_core(&self) -> &[Lit][src]

Subset of assumptions that made the formula unsatisfiable.

pub fn assumptions(&self) -> &[Lit][src]

Current assumptions.

Trait Implementations

impl Default for Assumptions[src]

Auto Trait Implementations

impl Send for Assumptions

impl Sync for Assumptions

Blanket Implementations

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T> From<T> for T[src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

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

The type returned in the event of a conversion error.

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

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

impl<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
    Inner: Part,
    Outer: Part<PartType = Field<OuterFieldType>>,
    OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
    Reference: HasPart<Outer> + ?Sized,