Struct Conflict Analysis Context &nbsp; Copy item path

Returns true if a change to a domain occured, and false if the given Predicate was already true.

If a domain becomes empty due to this operation, an EmptyDomain error is returned.

pub fn restore_to(&mut self, checkpoint: usize)

Restore to the given checkpoint.

If the provided checkpoint is equal to the current checkpoint, this is a no-op. If the provided checkpoint is larger than the current checkpoint, this method will panic.

See State::new_checkpoint for an example.

pub fn get_conflict_nogood(&mut self) -> Vec<Predicate>

Returns a nogood which led to the conflict, excluding predicates from the root decision level.

pub fn get_propagation_reason( &mut self, predicate: Predicate, current_nogood: CurrentNogood<'_>, reason_buffer: &mut (impl Extend<Predicate> + AsRef<[Predicate]>), )

Compute the reason for predicate being true. The reason will be stored in reason_buffer.

If predicate is not true, or it is a decision, then this function will panic.

pub fn find_last_decision(&mut self) -> Option<Predicate>

Returns the last decision which was made by the solver (if such a decision exists).

impl ConflictAnalysisContext<'_>

Methods used for proof logging

pub fn explain_root_assignment(&mut self, predicate: Predicate)

Explains the root assignment of predicate in the proof log.

pub fn log_deduction( &mut self, premises: impl IntoIterator<Item = Predicate>, ) -> ConstraintTag

Log a deduction (learned nogood) to the proof.

The inferences and marked propagations are assumed to be recorded in reverse-application order.

impl ConflictAnalysisContext<'_>

Methods used for keeping track of statistics.

pub fn predicate_appeared_in_conflict(&mut self, predicate: Predicate)

Informs the used Brancher that the provided predicate appeared during conflict analysis.

This is used by Branchers such as [AutonomousSearch] to guide the search.

impl ConflictAnalysisContext<'_>

pub fn process_learned_nogood( &mut self, learned_nogood_predicates: Vec<Predicate>, lbd: u32, ) -> usize

Backtracks the solver and adds the learned nogood to the database, returning the level to which the solver backtracked.

Trait Implementations§

impl Debug for ConflictAnalysisContext<'_>

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

Formats the value using the given formatter. Read more

Auto Trait Implementations§

impl<'a> Freeze for ConflictAnalysisContext<'a>

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

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

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

impl<'a> Unpin for ConflictAnalysisContext<'a>

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

Blanket Implementations§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

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

Mutably borrows from an owned value. Read more

impl<T> Downcast for T
where T: Any,

fn into_any(self: Box<T>) -> Box<dyn Any>

Convert Box<dyn Trait> (where Trait: Downcast) to Box<dyn Any>. Box<dyn Any> can then be further downcast into Box<ConcreteType> where ConcreteType implements Trait.

fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>

Convert Rc<Trait> (where Trait: Downcast) to Rc<Any>. Rc<Any> can then be further downcast into Rc<ConcreteType> where ConcreteType implements Trait.

fn as_any(&self) -> &(dyn Any + 'static)

Convert &Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot generate &Any’s vtable from &Trait’s.

fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)

Convert &mut Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot generate &mut Any’s vtable from &mut Trait’s.

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

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

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T> IntoEither for T

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

impl<T> ProblemSolution for T
where T: HasAssignments,

fn num_domains(&self) -> usize

Returns the number of defined DomainIds.

fn get_integer_value<Var>(&self, var: Var) -> i32
where Var: IntegerVariable,

fn get_literal_value(&self, literal: Literal) -> bool

impl<T> ReadDomains for T
where T: HasAssignments,

fn evaluate_predicate(&self, predicate: Predicate) -> Option<bool>

Returns whether the provided Predicate is assigned (either true or false) or is currently unassigned.

fn evaluate_literal(&self, literal: Literal) -> Option<bool>

Returns whether the provided Literal is assigned (either true or false) or is currently unassigned.

fn get_holes_at_current_checkpoint<Var>( &self, var: &Var, ) -> impl Iterator<Item = i32>
where Var: IntegerVariable,

Returns the holes in the domain which were created on the current checkpoint.

fn get_holes<Var>(&self, var: &Var) -> impl Iterator<Item = i32>
where Var: IntegerVariable,

Returns all of the holes (currently) in the domain of var (including ones which were created at previous decision levels).

fn is_fixed<Var>(&self, var: &Var) -> bool
where Var: IntegerVariable,

Returns true if the domain of the given variable is singleton (i.e., the variable is fixed).

fn lower_bound<Var>(&self, var: &Var) -> i32
where Var: IntegerVariable,

Returns the lowest value in the domain of var.

fn lower_bound_at_trail_position<Var>( &self, var: &Var, trail_position: usize, ) -> i32
where Var: IntegerVariable,

Returns the lowest value in the domain of var at the given trail_position. Read more

fn upper_bound<Var>(&self, var: &Var) -> i32
where Var: IntegerVariable,

Returns the highest value in the domain of var.

fn upper_bound_at_trail_position<Var>( &self, var: &Var, trail_position: usize, ) -> i32
where Var: IntegerVariable,

Returns the highest value in the domain of var at the given trail_position. Read more

fn contains<Var>(&self, var: &Var, value: i32) -> bool
where Var: IntegerVariable,

Returns whether the provided value is in the domain of var.

fn contains_at_trail_position<Var>( &self, var: &Var, value: i32, trail_position: usize, ) -> bool
where Var: IntegerVariable,

Returns whether the provided value is in the domain of var at the given trail_position. Read more

fn iterate_domain<Var>(&self, var: &Var) -> impl Iterator<Item = i32>
where Var: IntegerVariable,

Returns an Iterator over the values in the domain of the provided var (including the lower-bound and upper-bound values).

fn is_decision_predicate(&self, predicate: Predicate) -> bool

Returns whether the provided Predicate was posted as a decision (i.e., it was posted as a Predicate without a reason).

fn is_initial_bound(&self, predicate: Predicate) -> bool

Returns whether the provided Predicate is an initial bound of its domain.

fn get_checkpoint_for_predicate(&self, predicate: Predicate) -> Option<usize>

If the provided Predicate is true, then this method returns the checkpoint at which it first become true; otherwise, it returns None.

fn read_trailed_integer(&self, trailed_integer: TrailedInteger) -> i64

Returns the current value of the provided TrailedInteger.

fn new_trailed_integer(&mut self, initial_value: i64) -> TrailedInteger

Creates a new TrailedInteger assigned to the provided initial_value.

fn write_trailed_integer(&mut self, trailed_integer: TrailedInteger, value: i64)

Assigns the provided TrailedInteger to the provided value.

fn get_checkpoint(&self) -> usize

Returns the current checkpoint.

fn initial_lower_bound(&self, var: DomainId) -> i32

Returns the lowest value in the domain of var at the time of its creation.

fn initial_upper_bound(&self, var: DomainId) -> i32

Returns the highest value in the domain of var at the time of its creation.

fn initial_holes(&self, var: DomainId) -> Vec<i32>

Returns all of the holes present at the time of thecreation of var.

fn number_of_domains(&self) -> u32

Returns the number of currently defined domains.

impl<T, U> TryFrom for T
where 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>::Error>

Performs the conversion.

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

type Error = >::Error

The type returned in the event of a conversion error.

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

Performs the conversion.

impl<V, T> VZip<V> for T
where V: MultiLane<T>,