[][src]Struct ascesis::Solver

pub struct Solver<'a> { /* fields omitted */ }

Methods

impl<'a> Solver<'a>[src]

Important traits for Solver<'_>
pub fn new(ctx: &Arc<Mutex<Context>>) -> Solver<'a>[src]

pub fn reset(&mut self) -> Result<(), SolverError>[src]

pub fn block_atom_id(&mut self, atom_id: NonZeroUsize)[src]

pub fn unblock_atom_id(&mut self, atom_id: NonZeroUsize) -> bool[src]

pub fn unblock_all_atoms(&mut self)[src]

pub fn add_formula(&mut self, formula: &Formula) -> Result<(), AcesError>[src]

pub fn inhibit_empty_solution(&mut self) -> Result<(), AcesError>[src]

Blocks empty solution models by adding a void inhibition clause.

A model represents an empty solution iff it contains only negative Port literals (hence no Port variable evaluates to true). Thus, the blocking clause is the disjunction of all Port variables known by the solver.

pub fn inhibit_model(&mut self, model: &[Lit]) -> Result<(), AcesError>[src]

Adds a model inhibition clause which will remove a specific model from solution space.

The blocking clause is constructed by negating the given model, i.e. by taking the disjunction of all explicit literals and reversing polarity of each. A literal is explicit iff its variable has been registered by occurring in a formula passed to a call to add_formula().

pub fn was_interrupted(&self) -> bool[src]

Returns true if last call to solve() was interrupted. Returns false if solve() either failed, or succeeded, or hasn't been called yet.

Note, that even if last call to solve() was indeed interrupted, a subsequent invocation of take_last_error() resets this to return false until next solve().

pub fn last_solution(&self) -> Option<Solution>[src]

Trait Implementations

impl<'_> Iterator for Solver<'_>[src]

type Item = Solution

The type of the elements being iterated over.

Auto Trait Implementations

impl<'a> !RefUnwindSafe for Solver<'a>

impl<'a> !Send for Solver<'a>

impl<'a> !Sync for Solver<'a>

impl<'a> Unpin for Solver<'a>

impl<'a> !UnwindSafe for Solver<'a>

Blanket Implementations

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

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

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

impl<T> From<T> for T[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

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

impl<I> IntoIterator for I where
    I: Iterator
[src]

type Item = <I as Iterator>::Item

The type of the elements being iterated over.

type IntoIter = I

Which kind of iterator are we turning this into?

impl<I> IteratorRandom for I where
    I: Iterator
[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<V, T> VZip<V> for T where
    V: MultiLane<T>,