Struct Literal 

pub struct Literal { /* private fields */ }

Implementations

impl Literal

pub fn get_integer_variable(&self) -> AffineView<DomainId>

pub fn get_true_predicate(&self) -> Predicate

Examples found in repository

examples/disjunctive_scheduling.rs (line 82)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_) => println!("Timeout."),
    };
}

pub fn get_false_predicate(&self) -> Predicate

Trait Implementations

impl Clone for Literal

fn clone(&self) -> Literal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Literal

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

Formats the value using the given formatter.

impl Hash for Literal

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl IntegerVariable for Literal

fn lower_bound(&self, assignment: &Assignments) -> i32

Returns the lower bound represented as a 0-1 value. Literals that evaluate to true have a lower bound of 1. Literal that evaluate to false have a lower bound of 0. Unassigned literals have a lower bound of 0.

fn upper_bound(&self, assignment: &Assignments) -> i32

Returns the upper bound represented as a 0-1 value. Literals that evaluate to true have an upper bound of 1. Literal that evaluate to false have a upper bound of 0. Unassigned literals have a upper bound of 1.

fn contains(&self, assignment: &Assignments, value: i32) -> bool

Returns whether the input value, when interpreted as a bool, can be considered for the literal. Literals that evaluate to true only contain value 1. Literals that evaluate to false only contain value 0. Unassigned literals contain both values 0 and 1.

type AffineView = AffineView<Literal>

fn lower_bound_at_trail_position( &self, assignment: &Assignments, trail_position: usize, ) -> i32

Get the lower bound of the variable at the given trail position.

fn upper_bound_at_trail_position( &self, assignment: &Assignments, trail_position: usize, ) -> i32

Get the upper bound of the variable at the given trail position.

fn contains_at_trail_position( &self, assignment: &Assignments, value: i32, trail_position: usize, ) -> bool

Determine whether the value is in the domain of this variable at the given trail position.

fn iterate_domain(&self, assignment: &Assignments) -> impl Iterator<Item = i32>

Iterate over the values of the domain.

fn watch_all(&self, watchers: &mut Watchers<'_>, events: EnumSet<DomainEvent>)

Register a watch for this variable on the given domain events.

fn unpack_event(&self, event: OpaqueDomainEvent) -> DomainEvent

Decode a domain event for this variable.

fn watch_all_backtrack( &self, watchers: &mut Watchers<'_>, events: EnumSet<DomainEvent>, )

fn get_holes_on_current_decision_level( &self, assignments: &Assignments, ) -> impl Iterator<Item = i32>

Returns all of the holes in the domain which were created at the current decision level

fn get_holes(&self, assignments: &Assignments) -> impl Iterator<Item = i32>

Returns all of the holes in the domain

impl Not for Literal

type Output = Literal

The resulting type after applying the ! operator.

fn not(self) -> <Literal as Not>::Output

Performs the unary ! operation.

impl PartialEq for Literal

fn eq(&self, other: &Literal) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PredicateConstructor for Literal

type Value = i32

The value used to represent a bound.

fn lower_bound_predicate( &self, bound: <Literal as PredicateConstructor>::Value, ) -> Predicate

Creates a lower-bound predicate (e.g. [x >= v]).

fn upper_bound_predicate( &self, bound: <Literal as PredicateConstructor>::Value, ) -> Predicate

Creates an upper-bound predicate (e.g. [x <= v]).

fn equality_predicate( &self, bound: <Literal as PredicateConstructor>::Value, ) -> Predicate

Creates an equality predicate (e.g. [x == v]).

fn disequality_predicate( &self, bound: <Literal as PredicateConstructor>::Value, ) -> Predicate

Creates a disequality predicate (e.g. [x != v]).

impl TransformableVariable<AffineView<Literal>> for Literal

fn scaled(&self, scale: i32) -> AffineView<Literal>

Get a variable which domain is scaled compared to the domain of self.

fn offset(&self, offset: i32) -> AffineView<Literal>

Get a variable which domain has a constant offset to the domain of self.

impl ValueSelector<Literal> for InDomainRandom

fn select_value( &mut self, context: &mut SelectionContext<'_>, decision_variable: Literal, ) -> Predicate

Determines which value in the domain of decision_variable to branch next on. The domain of the decision_variable variable should have at least 2 values in it (as it otherwise should not have been selected as decision_variable). Returns a Predicate specifying the required change in the domain.

fn is_restart_pointless(&mut self) -> bool

This method returns whether a restart is currently pointless for the ValueSelector.

fn subscribe_to_events(&self) -> Vec<BrancherEvent>

Indicates which BrancherEvent are relevant for this particular ValueSelector.

fn on_unassign_integer(&mut self, _variable: DomainId, _value: i32)

A function which is called after a DomainId is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides variable which is the DomainId which has been reset and value which is the value to which the variable was previously fixed. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_solution(&mut self, _solution: SolutionReference<'_>)

This method is called when a solution is found; either when iterating over all solutions in the case of a satisfiable problem or on solutions of increasing quality when solving an optimisation problem.

impl VariableSelector<Literal> for InputOrder<Literal>

fn select_variable( &mut self, context: &mut SelectionContext<'_>, ) -> Option<Literal>

Determines which variable to select next if there are any left to branch on. Should only return None when all variables which have been passed to the VariableSelector have been assigned. Otherwise it should return the variable to branch on next.

fn subscribe_to_events(&self) -> Vec<BrancherEvent>

Indicates which BrancherEvent are relevant for this particular VariableSelector.

fn on_conflict(&mut self)

A function which is called after a conflict has been found and processed but (currently) does not provide any additional information.

fn on_backtrack(&mut self)

A function which is called whenever a backtrack occurs in the solver.

fn on_unassign_integer(&mut self, _variable: DomainId, _value: i32)

A function which is called after a DomainId is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides variable which is the DomainId which has been reset. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_appearance_in_conflict_predicate(&mut self, _predicate: Predicate)

A function which is called when a Predicate appears in a conflict during conflict analysis.

fn is_restart_pointless(&mut self) -> bool

This method returns whether a restart is currently pointless for the VariableSelector.

impl Copy for Literal

impl Eq for Literal

impl StructuralPartialEq for Literal