Struct State 

pub struct State { /* private fields */ }

The State is the container of variables and propagators.

State implements Clone, and cloning the State will create a fresh copy of the State. If the State is large, this may be extremely expensive.

Implementations

impl State

Operations to create .

pub fn new_constraint_tag(&mut self) -> ConstraintTag

Create a new ConstraintTag.

pub fn new_literal(&mut self, name: Option<Arc<str>>) -> Literal

Creates a new Boolean (0-1) variable.

The name is used in solver traces to identify individual domains. They are required to be unique. If the state already contains a domain with the given name, then this function will panic.

Creation of new Literals is not influenced by the current checkpoint of the state. If a Literal is created at a non-zero checkpoint, then it will not ‘disappear’ when backtracking past the checkpoint where the domain was created.

pub fn new_interval_variable( &mut self, lower_bound: i32, upper_bound: i32, name: Option<Arc<str>>, ) -> DomainId

Creates a new interval variable with the given lower and upper bound.

The name is used in solver traces to identify individual domains. They are required to be unique. If the state already contains a domain with the given name, then this function will panic.

Creation of new domains is not influenced by the current checkpoint of the state. If a domain is created at a non-zero checkpoint, then it will not ‘disappear’ when backtracking past the checkpoint where the domain was created.)

pub fn new_sparse_variable( &mut self, values: Vec<i32>, name: Option<String>, ) -> DomainId

Creates a new sparse domain with the given values.

Note that this is implemented as an interval domain with explicit holes in the domain. For very sparse domains, this can result in a high memory overhead.

For more information on creation of domains, see State::new_interval_variable.

impl State

Operations to retrieve information about values

pub fn lower_bound<Var>(&self, variable: Var) -> i32

where Var: IntegerVariable,

Returns the lower-bound of the given variable.

pub fn upper_bound<Var>(&self, variable: Var) -> i32

where Var: IntegerVariable,

Returns the upper-bound of the given variable.

pub fn contains<Var>(&self, variable: Var, value: i32) -> bool

where Var: IntegerVariable,

Returns whether the given variable contains the provided value.

pub fn fixed_value<Var>(&self, variable: Var) -> Option<i32>

where Var: IntegerVariable,

If the given variable is fixed, then Some containing the assigned value is returned. Otherwise, None is returned.

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

Returns the truth value of the provided Predicate.

If the Predicate is assigned in the current State then Some containing whether the Predicate is satisfied or falsified is returned. Otherwise, None is returned.

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

If the provided Predicate is satisfied then it returns Some containing the checkpoint at which the Predicate became satisfied. Otherwise, None is returned.

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

Returns the truth value of the provided Literal.

If the Literal is assigned in the current State then Some containing whether the Literal is satisfied or falsified is returned. Otherwise, None is returned.

pub fn get_checkpoint(&self) -> usize

Returns the number of created checkpoints.

impl State

Operations for retrieving information about trail

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

Returns whether the provided Predicate is explicitly on the trail.

For example, if we post the Predicate [x >= v], then the predicate [x >= v - 1] is not explicity on the trail.

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

Returns whether the trail position of the provided Predicate.

impl State

Operations for adding constraints.

pub fn add_propagator<Constructor>( &mut self, constructor: Constructor, ) -> PropagatorHandle<<Constructor as PropagatorConstructor>::PropagatorImpl>

where Constructor: PropagatorConstructor, <Constructor as PropagatorConstructor>::PropagatorImpl: 'static,

Add a new propagator to the State. The constructor for that propagator should subscribe to the appropriate domain events so that the propagator is called when necessary.

While the propagator is added to the queue for propagation, this function does not trigger a round of propagation. An explicit call to State::propagate_to_fixed_point is necessary to run the new propagator for the first time.

pub fn add_inference_checker( &mut self, inference_code: InferenceCode, checker: Box<dyn InferenceChecker<Predicate>>, )

Add an inference checker to the state.

The inference checker will be used to check propagations performed during Self::propagate_to_fixed_point, if the check-propagations feature is enabled.

Multiple inference checkers may be added for the same inference code. In that case, if any checker accepts the inference, the inference is accepted.

impl State

Operations for retrieving propagators.

pub fn get_propagator<P>(&self, handle: PropagatorHandle<P>) -> Option<&P>

where P: Propagator,

Get a reference to the propagator identified by the given handle.

For an exclusive reference, use State::get_propagator_mut.

pub fn get_propagator_mut<P>( &mut self, handle: PropagatorHandle<P>, ) -> Option<&mut P>

where P: Propagator,

Get an exclusive reference to the propagator identified by the given handle.

impl State

Operations for modifying the state.

pub fn post(&mut self, predicate: Predicate) -> Result<bool, EmptyDomain>

Apply a Predicate to the State.

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.

This method does not perform any propagation. For that, an explicit call to State::propagate_to_fixed_point is required. This allows the posting of multiple predicates before the entire propagation engine is invoked.

A call to State::restore_to that goes past the checkpoint at which a Predicate was posted will undo the effect of that Predicate. See the documentation of State::new_checkpoint and State::restore_to for more information.

pub fn new_checkpoint(&mut self)

Create a checkpoint of the current State, that can be returned to with State::restore_to.

The current checkpoint can be retrieved using the method State::get_checkpoint.

If the state is not at fixed-point, then this method will panic.

Example

use pumpkin_core::predicate;
use pumpkin_core::state::State;

let mut state = State::default();
let variable = state.new_interval_variable(1, 10, Some("x1".into()));

assert_eq!(state.get_checkpoint(), 0);

state.new_checkpoint();

assert_eq!(state.get_checkpoint(), 1);

state
    .post(predicate![variable <= 5])
    .expect("The lower bound is 1 so no conflict");
assert_eq!(state.upper_bound(variable), 5);

state.restore_to(0);

assert_eq!(state.get_checkpoint(), 0);
assert_eq!(state.upper_bound(variable), 10);

pub fn restore_to(&mut self, checkpoint: usize) -> Vec<(DomainId, i32)>

Restore to the given checkpoint and return the DomainIds which were fixed before restoring, with their assigned values.

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 propagate_to_fixed_point(&mut self) -> Result<(), Conflict>

Performs fixed-point propagation using the propagators defined in the State.

The posted Predicates (using State::post) and added propagators (using State::add_propagator) cause propagators to be enqueued when the events that they have subscribed to are triggered. As propagation causes more changes to be made, more propagators are enqueued. This continues until applying all (enqueued) propagators leads to no more domain changes.

It could be that the current State implies a conflict by propagation. In that case, an error with Conflict is returned.

Once the State is conflicting, then the only operation that is defined is State::restore_to. All other operations and queries on the state are unspecified.

impl State

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

Get the reason for a predicate being true and store it in reason_buffer; additionally, if the provided Predicate is explicitly on the trail, this method will return the corresponding trail index.

The provided current_nogood can be used by the propagator to provide a different reason; use CurrentNogood::empty otherwise.

All the predicates in the returned slice will evaluate to true.

If the provided predicate is not true, then this method will panic.

impl State

pub fn get_domains(&mut self) -> Domains<'_>

pub fn get_propagation_context(&mut self) -> PropagationContext<'_>

Trait Implementations

impl Clone for State

fn clone(&self) -> State

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for State

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

Formats the value using the given formatter.

impl Default for State

fn default() -> State

Returns the “default value” for a type.