[−][src]Struct ascesis::Solver
Methods
impl<'a> Solver<'a>
[src]
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.
fn next(&mut self) -> Option<<Solver<'_> as Iterator>::Item>
[src]
fn size_hint(&self) -> (usize, Option<usize>)
1.0.0[src]
fn count(self) -> usize
1.0.0[src]
fn last(self) -> Option<Self::Item>
1.0.0[src]
fn nth(&mut self, n: usize) -> Option<Self::Item>
1.0.0[src]
fn step_by(self, step: usize) -> StepBy<Self>
1.28.0[src]
fn chain<U>(self, other: U) -> Chain<Self, <U as IntoIterator>::IntoIter> where
U: IntoIterator<Item = Self::Item>,
1.0.0[src]
U: IntoIterator<Item = Self::Item>,
fn zip<U>(self, other: U) -> Zip<Self, <U as IntoIterator>::IntoIter> where
U: IntoIterator,
1.0.0[src]
U: IntoIterator,
fn map<B, F>(self, f: F) -> Map<Self, F> where
F: FnMut(Self::Item) -> B,
1.0.0[src]
F: FnMut(Self::Item) -> B,
fn for_each<F>(self, f: F) where
F: FnMut(Self::Item),
1.21.0[src]
F: FnMut(Self::Item),
fn filter<P>(self, predicate: P) -> Filter<Self, P> where
P: FnMut(&Self::Item) -> bool,
1.0.0[src]
P: FnMut(&Self::Item) -> bool,
fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F> where
F: FnMut(Self::Item) -> Option<B>,
1.0.0[src]
F: FnMut(Self::Item) -> Option<B>,
fn enumerate(self) -> Enumerate<Self>
1.0.0[src]
fn peekable(self) -> Peekable<Self>
1.0.0[src]
fn skip_while<P>(self, predicate: P) -> SkipWhile<Self, P> where
P: FnMut(&Self::Item) -> bool,
1.0.0[src]
P: FnMut(&Self::Item) -> bool,
fn take_while<P>(self, predicate: P) -> TakeWhile<Self, P> where
P: FnMut(&Self::Item) -> bool,
1.0.0[src]
P: FnMut(&Self::Item) -> bool,
fn map_while<B, P>(self, predicate: P) -> MapWhile<Self, P> where
P: FnMut(Self::Item) -> Option<B>,
[src]
P: FnMut(Self::Item) -> Option<B>,
fn skip(self, n: usize) -> Skip<Self>
1.0.0[src]
fn take(self, n: usize) -> Take<Self>
1.0.0[src]
fn scan<St, B, F>(self, initial_state: St, f: F) -> Scan<Self, St, F> where
F: FnMut(&mut St, Self::Item) -> Option<B>,
1.0.0[src]
F: FnMut(&mut St, Self::Item) -> Option<B>,
fn flat_map<U, F>(self, f: F) -> FlatMap<Self, U, F> where
F: FnMut(Self::Item) -> U,
U: IntoIterator,
1.0.0[src]
F: FnMut(Self::Item) -> U,
U: IntoIterator,
fn flatten(self) -> Flatten<Self> where
Self::Item: IntoIterator,
1.29.0[src]
Self::Item: IntoIterator,
fn fuse(self) -> Fuse<Self>
1.0.0[src]
fn inspect<F>(self, f: F) -> Inspect<Self, F> where
F: FnMut(&Self::Item),
1.0.0[src]
F: FnMut(&Self::Item),
fn by_ref(&mut self) -> &mut Self
1.0.0[src]
#[must_use =
"if you really need to exhaust the iterator, consider `.for_each(drop)` instead"]fn collect<B>(self) -> B where
B: FromIterator<Self::Item>,
1.0.0[src]
B: FromIterator<Self::Item>,
fn partition<B, F>(self, f: F) -> (B, B) where
B: Default + Extend<Self::Item>,
F: FnMut(&Self::Item) -> bool,
1.0.0[src]
B: Default + Extend<Self::Item>,
F: FnMut(&Self::Item) -> bool,
fn partition_in_place<'a, T, P>(self, predicate: P) -> usize where
P: FnMut(&T) -> bool,
Self: DoubleEndedIterator<Item = &'a mut T>,
T: 'a,
[src]
P: FnMut(&T) -> bool,
Self: DoubleEndedIterator<Item = &'a mut T>,
T: 'a,
fn is_partitioned<P>(self, predicate: P) -> bool where
P: FnMut(Self::Item) -> bool,
[src]
P: FnMut(Self::Item) -> bool,
fn try_fold<B, F, R>(&mut self, init: B, f: F) -> R where
F: FnMut(B, Self::Item) -> R,
R: Try<Ok = B>,
1.27.0[src]
F: FnMut(B, Self::Item) -> R,
R: Try<Ok = B>,
fn try_for_each<F, R>(&mut self, f: F) -> R where
F: FnMut(Self::Item) -> R,
R: Try<Ok = ()>,
1.27.0[src]
F: FnMut(Self::Item) -> R,
R: Try<Ok = ()>,
fn fold<B, F>(self, init: B, f: F) -> B where
F: FnMut(B, Self::Item) -> B,
1.0.0[src]
F: FnMut(B, Self::Item) -> B,
fn fold_first<F>(self, f: F) -> Option<Self::Item> where
F: FnMut(Self::Item, Self::Item) -> Self::Item,
[src]
F: FnMut(Self::Item, Self::Item) -> Self::Item,
fn all<F>(&mut self, f: F) -> bool where
F: FnMut(Self::Item) -> bool,
1.0.0[src]
F: FnMut(Self::Item) -> bool,
fn any<F>(&mut self, f: F) -> bool where
F: FnMut(Self::Item) -> bool,
1.0.0[src]
F: FnMut(Self::Item) -> bool,
fn find<P>(&mut self, predicate: P) -> Option<Self::Item> where
P: FnMut(&Self::Item) -> bool,
1.0.0[src]
P: FnMut(&Self::Item) -> bool,
fn find_map<B, F>(&mut self, f: F) -> Option<B> where
F: FnMut(Self::Item) -> Option<B>,
1.30.0[src]
F: FnMut(Self::Item) -> Option<B>,
fn try_find<F, E, R>(&mut self, f: F) -> Result<Option<Self::Item>, E> where
F: FnMut(&Self::Item) -> R,
R: Try<Ok = bool, Error = E>,
[src]
F: FnMut(&Self::Item) -> R,
R: Try<Ok = bool, Error = E>,
fn position<P>(&mut self, predicate: P) -> Option<usize> where
P: FnMut(Self::Item) -> bool,
1.0.0[src]
P: FnMut(Self::Item) -> bool,
fn rposition<P>(&mut self, predicate: P) -> Option<usize> where
P: FnMut(Self::Item) -> bool,
Self: ExactSizeIterator + DoubleEndedIterator,
1.0.0[src]
P: FnMut(Self::Item) -> bool,
Self: ExactSizeIterator + DoubleEndedIterator,
fn max(self) -> Option<Self::Item> where
Self::Item: Ord,
1.0.0[src]
Self::Item: Ord,
fn min(self) -> Option<Self::Item> where
Self::Item: Ord,
1.0.0[src]
Self::Item: Ord,
fn max_by_key<B, F>(self, f: F) -> Option<Self::Item> where
B: Ord,
F: FnMut(&Self::Item) -> B,
1.6.0[src]
B: Ord,
F: FnMut(&Self::Item) -> B,
fn max_by<F>(self, compare: F) -> Option<Self::Item> where
F: FnMut(&Self::Item, &Self::Item) -> Ordering,
1.15.0[src]
F: FnMut(&Self::Item, &Self::Item) -> Ordering,
fn min_by_key<B, F>(self, f: F) -> Option<Self::Item> where
B: Ord,
F: FnMut(&Self::Item) -> B,
1.6.0[src]
B: Ord,
F: FnMut(&Self::Item) -> B,
fn min_by<F>(self, compare: F) -> Option<Self::Item> where
F: FnMut(&Self::Item, &Self::Item) -> Ordering,
1.15.0[src]
F: FnMut(&Self::Item, &Self::Item) -> Ordering,
fn rev(self) -> Rev<Self> where
Self: DoubleEndedIterator,
1.0.0[src]
Self: DoubleEndedIterator,
fn unzip<A, B, FromA, FromB>(self) -> (FromA, FromB) where
FromA: Default + Extend<A>,
FromB: Default + Extend<B>,
Self: Iterator<Item = (A, B)>,
1.0.0[src]
FromA: Default + Extend<A>,
FromB: Default + Extend<B>,
Self: Iterator<Item = (A, B)>,
fn copied<'a, T>(self) -> Copied<Self> where
Self: Iterator<Item = &'a T>,
T: 'a + Copy,
1.36.0[src]
Self: Iterator<Item = &'a T>,
T: 'a + Copy,
fn cloned<'a, T>(self) -> Cloned<Self> where
Self: Iterator<Item = &'a T>,
T: 'a + Clone,
1.0.0[src]
Self: Iterator<Item = &'a T>,
T: 'a + Clone,
fn cycle(self) -> Cycle<Self> where
Self: Clone,
1.0.0[src]
Self: Clone,
fn sum<S>(self) -> S where
S: Sum<Self::Item>,
1.11.0[src]
S: Sum<Self::Item>,
fn product<P>(self) -> P where
P: Product<Self::Item>,
1.11.0[src]
P: Product<Self::Item>,
fn cmp<I>(self, other: I) -> Ordering where
I: IntoIterator<Item = Self::Item>,
Self::Item: Ord,
1.5.0[src]
I: IntoIterator<Item = Self::Item>,
Self::Item: Ord,
fn cmp_by<I, F>(self, other: I, cmp: F) -> Ordering where
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Ordering,
I: IntoIterator,
[src]
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Ordering,
I: IntoIterator,
fn partial_cmp<I>(self, other: I) -> Option<Ordering> where
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
fn partial_cmp_by<I, F>(self, other: I, partial_cmp: F) -> Option<Ordering> where
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Option<Ordering>,
I: IntoIterator,
[src]
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> Option<Ordering>,
I: IntoIterator,
fn eq<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialEq<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialEq<<I as IntoIterator>::Item>,
fn eq_by<I, F>(self, other: I, eq: F) -> bool where
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> bool,
I: IntoIterator,
[src]
F: FnMut(Self::Item, <I as IntoIterator>::Item) -> bool,
I: IntoIterator,
fn ne<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialEq<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialEq<<I as IntoIterator>::Item>,
fn lt<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
fn le<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
fn gt<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
fn ge<I>(self, other: I) -> bool where
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
1.5.0[src]
I: IntoIterator,
Self::Item: PartialOrd<<I as IntoIterator>::Item>,
fn is_sorted(self) -> bool where
Self::Item: PartialOrd<Self::Item>,
[src]
Self::Item: PartialOrd<Self::Item>,
fn is_sorted_by<F>(self, compare: F) -> bool where
F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
[src]
F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
fn is_sorted_by_key<F, K>(self, f: F) -> bool where
F: FnMut(Self::Item) -> K,
K: PartialOrd<K>,
[src]
F: FnMut(Self::Item) -> K,
K: PartialOrd<K>,
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]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[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,
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
unsafe fn part_ptr(
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
unsafe fn part_ptr_mut(
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<I> IntoIterator for I where
I: Iterator,
[src]
I: Iterator,
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?
fn into_iter(self) -> I
[src]
impl<I> IteratorRandom for I where
I: Iterator,
[src]
I: Iterator,
fn choose<R>(self, rng: &mut R) -> Option<Self::Item> where
R: Rng + ?Sized,
[src]
R: Rng + ?Sized,
fn choose_multiple_fill<R>(self, rng: &mut R, buf: &mut [Self::Item]) -> usize where
R: Rng + ?Sized,
[src]
R: Rng + ?Sized,
fn choose_multiple<R>(self, rng: &mut R, amount: usize) -> Vec<Self::Item> where
R: Rng + ?Sized,
[src]
R: Rng + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<V, T> VZip<V> for T where
V: MultiLane<T>,
V: MultiLane<T>,