Struct ConstraintPoster 

pub struct ConstraintPoster<'solver, ConstraintImpl> { /* private fields */ }

A structure which is responsible for adding the created Constraints to the Solver. For an example on how to use this, see crate::constraints.

Implementations

impl<ConstraintImpl> ConstraintPoster<'_, ConstraintImpl>

where ConstraintImpl: Constraint,

pub fn post(self) -> Result<(), ConstraintOperationError>

Add the Constraint to the Solver.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

Examples found in repository

examples/nqueens.rs (line 65)

fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(SolverOptions {
        proof_log,
        ..Default::default()
    });

    // Create the constraint tags for the three all_different constraints.
    let c1_tag = solver.new_constraint_tag();
    let c2_tag = solver.new_constraint_tag();
    let c3_tag = solver.new_constraint_tag();

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone(), c1_tag))
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1, c2_tag))
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2, c3_tag))
        .post();

    let mut brancher = solver.default_brancher();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("Timeout.");
        }
    };
}

examples/bibd.rs (line 105)

fn main() {
    env_logger::init();

    let Some(bibd) = Bibd::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    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();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(
                row.clone(),
                bibd.row_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(
                row,
                bibd.column_sum as i32,
                constraint_tag,
            ))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                        constraint_tag,
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                    constraint_tag,
                ))
                .post();
        }
    }

    let mut brancher = solver.default_brancher();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let row_separator = format!("{}+", "+---".repeat(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable(_, _) => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown(_, _) => {
            println!("UNKNOWN")
        }
    };
}

pub fn implied_by( self, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

Add the half-reified version of the Constraint to the Solver; i.e. post the constraint r -> constraint where r is a reification literal.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

impl<ConstraintImpl> ConstraintPoster<'_, ConstraintImpl>

where ConstraintImpl: NegatableConstraint,

pub fn reify( self, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

Add the reified version of the Constraint to the Solver; i.e. post the constraint r <-> constraint where r is a reification literal.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

Trait Implementations

impl<'solver, ConstraintImpl> Debug for ConstraintPoster<'solver, ConstraintImpl>

where ConstraintImpl: Debug,

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

Formats the value using the given formatter.

impl<ConstraintImpl> Drop for ConstraintPoster<'_, ConstraintImpl>

fn drop(&mut self)

Executes the destructor for this type.