From e641b8021a1649ca6d7b9ad13d1885925a6bc7d0 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 31 Jan 2025 16:31:12 +1100 Subject: [PATCH] More consistent naming of constraints and their propagators --- crates/huub/src/constraints.rs | 13 +- .../huub/src/constraints/array_int_element.rs | 61 -- ..._bool_element.rs => bool_array_element.rs} | 9 +- crates/huub/src/constraints/int_abs.rs | 4 +- ..._different_int.rs => int_all_different.rs} | 26 +- ...ar_int_element.rs => int_array_element.rs} | 88 ++- ...ay_int_minimum.rs => int_array_minimum.rs} | 31 +- crates/huub/src/constraints/int_div.rs | 8 +- .../{set_in_reif.rs => int_in_set.rs} | 8 +- crates/huub/src/constraints/int_linear.rs | 54 +- crates/huub/src/constraints/int_pow.rs | 8 +- .../{table_int.rs => int_table.rs} | 10 +- crates/huub/src/constraints/int_times.rs | 4 +- crates/huub/src/flatzinc.rs | 69 +- crates/huub/src/lib.rs | 590 ++++++++++-------- crates/huub/src/reformulate.rs | 165 ++--- crates/huub/src/solver.rs | 64 +- crates/huub/src/solver/solving_context.rs | 4 +- 18 files changed, 617 insertions(+), 599 deletions(-) delete mode 100644 crates/huub/src/constraints/array_int_element.rs rename crates/huub/src/constraints/{array_var_bool_element.rs => bool_array_element.rs} (87%) rename crates/huub/src/constraints/{all_different_int.rs => int_all_different.rs} (92%) rename crates/huub/src/constraints/{array_var_int_element.rs => int_array_element.rs} (82%) rename crates/huub/src/constraints/{array_int_minimum.rs => int_array_minimum.rs} (87%) rename crates/huub/src/constraints/{set_in_reif.rs => int_in_set.rs} (90%) rename crates/huub/src/constraints/{table_int.rs => int_table.rs} (95%) diff --git a/crates/huub/src/constraints.rs b/crates/huub/src/constraints.rs index f5dcaee..47ddd80 100644 --- a/crates/huub/src/constraints.rs +++ b/crates/huub/src/constraints.rs @@ -1,18 +1,17 @@ //! Module containing the definitions for propagators and their implementations. -pub mod all_different_int; -pub mod array_int_element; -pub mod array_int_minimum; -pub mod array_var_bool_element; -pub mod array_var_int_element; +pub mod bool_array_element; pub mod disjunctive_strict; pub mod int_abs; +pub mod int_all_different; +pub mod int_array_element; +pub mod int_array_minimum; pub mod int_div; +pub mod int_in_set; pub mod int_linear; pub mod int_pow; +pub mod int_table; pub mod int_times; -pub mod set_in_reif; -pub mod table_int; use std::{ error::Error, diff --git a/crates/huub/src/constraints/array_int_element.rs b/crates/huub/src/constraints/array_int_element.rs deleted file mode 100644 index 4abbfb7..0000000 --- a/crates/huub/src/constraints/array_int_element.rs +++ /dev/null @@ -1,61 +0,0 @@ -//! Structures and algorithms for the `array_int_element` constraint, which -//! enforces that a resulting variable equals an element of an array of integer -//! values, chosen by an index variable. - -use std::iter::once; - -use itertools::Itertools; -use pindakaas::ClauseDatabaseTools; - -use crate::{ - actions::{ReformulationActions, SimplificationActions}, - constraints::Constraint, - reformulate::ReformulationError, - solver::IntLitMeaning, - IntDecision, IntVal, -}; - -#[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `array_int_element` constraint within a model. -/// -/// This constraint enforces that a result integer decision variable takes the -/// value equal the element of the given array of integer values at the given -/// index decision variable. -pub struct ArrayIntElement { - /// The array of integer values - pub(crate) array: Vec, - /// The index variable - pub(crate) index: IntDecision, - /// The resulting variable - pub(crate) result: IntDecision, -} - -impl Constraint for ArrayIntElement { - fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { - let index = slv.get_solver_int(self.index); - let result = slv.get_solver_int(self.result); - - let idx_map = self - .array - .iter() - .enumerate() - .map(|(i, v)| (*v, i as IntVal)) - .into_group_map(); - - for (val, idxs) in idx_map { - let val_eq = slv.get_int_lit(result, IntLitMeaning::Eq(val)); - let idxs: Vec<_> = idxs - .into_iter() - .map(|i| slv.get_int_lit(index, IntLitMeaning::Eq(i))) - .collect(); - - for &i in idxs.iter() { - // (idx = i) -> (val = arr[i]) - slv.add_clause([!i, val_eq])?; - } - // (idx not in idxs) -> (val != arr[i]) - slv.add_clause(idxs.into_iter().chain(once(!val_eq)))?; - } - Ok(()) - } -} diff --git a/crates/huub/src/constraints/array_var_bool_element.rs b/crates/huub/src/constraints/bool_array_element.rs similarity index 87% rename from crates/huub/src/constraints/array_var_bool_element.rs rename to crates/huub/src/constraints/bool_array_element.rs index 9667607..6b20f23 100644 --- a/crates/huub/src/constraints/array_var_bool_element.rs +++ b/crates/huub/src/constraints/bool_array_element.rs @@ -1,4 +1,4 @@ -//! Structures and algorithms for the `array_var_bool_element` constraint, which +//! Structures and algorithms for the Boolean array element constraint, which //! enforces that a resulting variable equals an element of an array of Boolean //! decision variables, chosen by an index variable. @@ -15,12 +15,13 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `array_var_bool_element` constraint within a model. +/// Representation of the `array_element` constraint with an array of Boolean +/// decision variables within a model. /// /// This constraint enforces that a result Boolean decision variable takes the /// value equal the element of the given array of Boolean decision varaibles at /// the index given by the index integer decision variable. -pub struct ArrayVarBoolElement { +pub struct BoolDecisionArrayElement { /// The array of Boolean decision variables pub(crate) array: Vec, /// The index variable @@ -29,7 +30,7 @@ pub struct ArrayVarBoolElement { pub(crate) result: BoolDecision, } -impl Constraint for ArrayVarBoolElement { +impl Constraint for BoolDecisionArrayElement { fn simplify(&mut self, actions: &mut S) -> Result { if let Some(i) = actions.get_int_val(self.index) { actions.add_constraint(Formula::Equiv(vec![ diff --git a/crates/huub/src/constraints/int_abs.rs b/crates/huub/src/constraints/int_abs.rs index 5ef0711..50687ce 100644 --- a/crates/huub/src/constraints/int_abs.rs +++ b/crates/huub/src/constraints/int_abs.rs @@ -1,5 +1,5 @@ -//! Structures and algorithms for the `int_abs` constraint, which enforces that -//! one variable is takes absolute value of another. +//! Structures and algorithms for the integer absolute value constraint, which +//! enforces that one variable is takes absolute value of another. use std::iter::once; diff --git a/crates/huub/src/constraints/all_different_int.rs b/crates/huub/src/constraints/int_all_different.rs similarity index 92% rename from crates/huub/src/constraints/all_different_int.rs rename to crates/huub/src/constraints/int_all_different.rs index a56a3f9..8e51f0d 100644 --- a/crates/huub/src/constraints/all_different_int.rs +++ b/crates/huub/src/constraints/int_all_different.rs @@ -1,4 +1,4 @@ -//! Structure and algorithms for the `all_different_int` constraint, which +//! Structure and algorithms for the integer all different constraint, which //! enforces that a list of integer variables each take a different value. use itertools::{Either, Itertools}; @@ -21,19 +21,19 @@ use crate::{ /// /// This constraint enforces that all the given integer decisions take different /// values. -pub struct AllDifferentInt { +pub struct IntAllDifferent { /// List of integer decision variables that must take different values. pub(crate) vars: Vec, } #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Value consistent propagator for the `all_different_int` constraint. -pub struct AllDifferentIntValue { +pub struct IntAllDifferentValue { /// List of integer variables that must take different values. vars: Vec, } -impl Constraint for AllDifferentInt { +impl Constraint for IntAllDifferent { fn simplify(&mut self, actions: &mut S) -> Result { let (vals, vars): (Vec<_>, Vec<_>) = self.vars.iter().partition_map(|&var| { if let Some(val) = actions.get_int_val(var) { @@ -61,12 +61,12 @@ impl Constraint for AllDifferentInt { fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { let vars: Vec<_> = self.vars.iter().map(|v| slv.get_solver_int(*v)).collect(); - AllDifferentIntValue::new_in(slv, vars); + IntAllDifferentValue::new_in(slv, vars); Ok(()) } } -impl AllDifferentIntValue { +impl IntAllDifferentValue { /// Create a new [`AllDifferentIntValue`] propagator and post it in the /// solver. pub fn new_in(solver: &mut P, vars: Vec) { @@ -83,7 +83,7 @@ impl AllDifferentIntValue { } } -impl Propagator for AllDifferentIntValue +impl Propagator for IntAllDifferentValue where P: PropagationActions, E: ExplanationActions, @@ -113,7 +113,7 @@ mod tests { use tracing_test::traced_test; use crate::{ - constraints::all_different_int::AllDifferentIntValue, + constraints::int_all_different::IntAllDifferentValue, solver::{ int_var::{EncodingType, IntVar}, IntView, SolveResult, Solver, @@ -144,7 +144,7 @@ mod tests { EncodingType::Eager, ); - AllDifferentIntValue::new_in(&mut slv, vec![a, b, c]); + IntAllDifferentValue::new_in(&mut slv, vec![a, b, c]); slv.assert_all_solutions(&[a, b, c], |sol| sol.iter().all_unique()); } @@ -172,7 +172,7 @@ mod tests { EncodingType::Eager, ); - AllDifferentIntValue::new_in(&mut slv, vec![a, b, c]); + IntAllDifferentValue::new_in(&mut slv, vec![a, b, c]); slv.assert_unsatisfiable(); } @@ -197,7 +197,7 @@ mod tests { } } - AllDifferentIntValue::new_in(&mut slv, vars.clone()); + IntAllDifferentValue::new_in(&mut slv, vars.clone()); all_vars.push(vars); }); @@ -205,7 +205,7 @@ mod tests { for i in 0..9 { let col_vars: Vec = (0..9).map(|j| all_vars[j][i]).collect(); - AllDifferentIntValue::new_in(&mut slv, col_vars); + IntAllDifferentValue::new_in(&mut slv, col_vars); } // add all different propagator for each 3 by 3 grid for i in 0..3 { @@ -217,7 +217,7 @@ mod tests { } } - AllDifferentIntValue::new_in(&mut slv, block_vars); + IntAllDifferentValue::new_in(&mut slv, block_vars); } } assert_eq!( diff --git a/crates/huub/src/constraints/array_var_int_element.rs b/crates/huub/src/constraints/int_array_element.rs similarity index 82% rename from crates/huub/src/constraints/array_var_int_element.rs rename to crates/huub/src/constraints/int_array_element.rs index 9e30431..5df232f 100644 --- a/crates/huub/src/constraints/array_var_int_element.rs +++ b/crates/huub/src/constraints/int_array_element.rs @@ -1,16 +1,18 @@ -//! Structures and algorithms for the `array_var_int_element` constraint, which -//! enforces that a resulting variable equals an element of an array of -//! variables, chosen by an index variable. +//! Structures and algorithms for the integer array element constraint, which +//! enforces that a resulting variable equals an element of an array of integer +//! values or decision variables, chosen by an index variable. + +use std::iter::once; use itertools::Itertools; use pindakaas::ClauseDatabaseTools; use crate::{ actions::{ - ConstraintInitActions, ExplanationActions, PropagatorInitActions, ReformulationActions, - SimplificationActions, + ConstraintInitActions, ExplanationActions, PropagationActions, PropagatorInitActions, + ReformulationActions, SimplificationActions, }, - constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, + constraints::{Conflict, Constraint, Propagator, SimplificationStatus}, reformulate::ReformulationError, solver::{ activation_list::IntPropCond, queue::PriorityLevel, trail::TrailedInt, IntLitMeaning, @@ -20,12 +22,13 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `array_var_int_element` constraint within a model. +/// Representation of the `array_element` constraint with an array of integer +/// decision variables within a model. /// /// This constraint enforces that a result integer decision variable takes the /// value equal the element of the given array of integer decision variable at /// the given index decision variable. -pub struct ArrayVarIntElement { +pub struct IntDecisionArrayElement { /// The array of integer values pub(crate) array: Vec, /// The index variable @@ -35,8 +38,9 @@ pub struct ArrayVarIntElement { } #[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Bounds consistent propagator for the `array_var_int_element` constraint. -pub struct ArrayVarIntElementBounds { +/// Bounds consistent propagator for the `array_element` constraint with an +/// array of integer decision variables. +pub struct IntDecisionArrayElementBounds { /// Array of variables from which the element is selected vars: Vec, /// Variable that represent the result of the selection @@ -49,7 +53,23 @@ pub struct ArrayVarIntElementBounds { max_support: TrailedInt, } -impl Constraint for ArrayVarIntElement { +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `array_element` constraint with an array of integer +/// values within a model. +/// +/// This constraint enforces that a result integer decision variable takes the +/// value equal the element of the given array of integer values at the given +/// index decision variable. +pub struct IntValArrayElement { + /// The array of integer values + pub(crate) array: Vec, + /// The index variable + pub(crate) index: IntDecision, + /// The resulting variable + pub(crate) result: IntDecision, +} + +impl Constraint for IntDecisionArrayElement { fn initialize(&self, actions: &mut dyn ConstraintInitActions) { for &a in &self.array { actions.simplify_on_change_int(a); @@ -84,11 +104,11 @@ impl Constraint for ArrayVarIntElement { let array = self.array.iter().map(|&v| slv.get_solver_int(v)).collect(); let result = slv.get_solver_int(self.result); let index = slv.get_solver_int(self.index); - ArrayVarIntElementBounds::new_in(slv, array, result, index) + IntDecisionArrayElementBounds::new_in(slv, array, result, index) } } -impl ArrayVarIntElementBounds { +impl IntDecisionArrayElementBounds { /// Create a new [`ArrayVarIntElementBounds`] propagator and post it in the /// solver. pub fn new_in

( @@ -152,7 +172,7 @@ impl ArrayVarIntElementBounds { } } -impl Propagator for ArrayVarIntElementBounds +impl Propagator for IntDecisionArrayElementBounds where P: PropagationActions, E: ExplanationActions, @@ -298,6 +318,36 @@ where } } +impl Constraint for IntValArrayElement { + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let index = slv.get_solver_int(self.index); + let result = slv.get_solver_int(self.result); + + let idx_map = self + .array + .iter() + .enumerate() + .map(|(i, v)| (*v, i as IntVal)) + .into_group_map(); + + for (val, idxs) in idx_map { + let val_eq = slv.get_int_lit(result, IntLitMeaning::Eq(val)); + let idxs: Vec<_> = idxs + .into_iter() + .map(|i| slv.get_int_lit(index, IntLitMeaning::Eq(i))) + .collect(); + + for &i in idxs.iter() { + // (idx = i) -> (val = arr[i]) + slv.add_clause([!i, val_eq])?; + } + // (idx not in idxs) -> (val != arr[i]) + slv.add_clause(idxs.into_iter().chain(once(!val_eq)))?; + } + Ok(()) + } +} + #[cfg(test)] mod tests { use expect_test::expect; @@ -306,8 +356,8 @@ mod tests { use tracing_test::traced_test; use crate::{ - array_var_int_element, - constraints::array_var_int_element::ArrayVarIntElementBounds, + array_element, + constraints::int_array_element::IntDecisionArrayElementBounds, solver::{ int_var::{EncodingType, IntVar}, Solver, @@ -350,7 +400,7 @@ mod tests { EncodingType::Lazy, ); - ArrayVarIntElementBounds::new_in(&mut slv, vec![a, b, c], y, index).unwrap(); + IntDecisionArrayElementBounds::new_in(&mut slv, vec![a, b, c], y, index).unwrap(); slv.expect_solutions( &[index, y, a, b, c], @@ -403,7 +453,7 @@ mod tests { EncodingType::Lazy, ); - ArrayVarIntElementBounds::new_in(&mut slv, vec![a, b], y, index).unwrap(); + IntDecisionArrayElementBounds::new_in(&mut slv, vec![a, b], y, index).unwrap(); slv.expect_solutions( &[index, y, a, b], @@ -424,7 +474,7 @@ mod tests { let result = prb.new_int_var((1..=2).into()); let index = prb.new_int_var((0..=2).into()); - prb += array_var_int_element(index, vec![a, b, c], result); + prb += array_element(vec![a, b, c], index, result); prb.assert_unsatisfiable(); } } diff --git a/crates/huub/src/constraints/array_int_minimum.rs b/crates/huub/src/constraints/int_array_minimum.rs similarity index 87% rename from crates/huub/src/constraints/array_int_minimum.rs rename to crates/huub/src/constraints/int_array_minimum.rs index 8d09c90..1fbe6f0 100644 --- a/crates/huub/src/constraints/array_int_minimum.rs +++ b/crates/huub/src/constraints/int_array_minimum.rs @@ -1,5 +1,6 @@ -//! Structures and algorithms for the `array_int_minimum` constraint, which -//! enforces that a variable takes the minimum value of an array of variables. +//! Structures and algorithms for the integer array minimum constraint, which +//! enforces that a decision variable takes the minimum value of an array of +//! decision variables. use itertools::Itertools; @@ -15,11 +16,11 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `array_int_minimum` constraint within a model. +/// Representation of the `array_minimum_int` constraint within a model. /// /// This constraint enforces that an integer decision variable takes the minimum /// value of an array of integer decision variables. -pub struct ArrayIntMinimum { +pub struct IntArrayMinimum { /// Set of decision variables from which the mimimum must be taken pub(crate) vars: Vec, /// Decision variable that represents the minimum value @@ -27,15 +28,15 @@ pub struct ArrayIntMinimum { } #[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Bounds cosistent propagator for the `array_int_minimum` constraint. -pub struct ArrayIntMinimumBounds { +/// Bounds cosistent propagator for the `array_minimum_int` constraint. +pub struct IntArrayMinimumBounds { /// Set of decision variables from which the mimimum must be taken vars: Vec, /// Decision variable that represents the minimum value min: IntView, } -impl Constraint for ArrayIntMinimum { +impl Constraint for IntArrayMinimum { fn initialize(&self, actions: &mut dyn ConstraintInitActions) { for v in &self.vars { actions.simplify_on_change_int(*v); @@ -69,12 +70,12 @@ impl Constraint for ArrayIntMinimum { fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { let vars: Vec<_> = self.vars.iter().map(|v| slv.get_solver_int(*v)).collect(); let min = slv.get_solver_int(self.min); - ArrayIntMinimumBounds::new_in(slv, vars, min); + IntArrayMinimumBounds::new_in(slv, vars, min); Ok(()) } } -impl ArrayIntMinimumBounds { +impl IntArrayMinimumBounds { /// Create a new [`ArrayIntMinimumBounds`] propagator and post it in the /// solver. pub fn new_in

(solver: &mut P, vars: Vec, min: IntView) @@ -96,7 +97,7 @@ impl ArrayIntMinimumBounds { } } -impl Propagator for ArrayIntMinimumBounds +impl Propagator for IntArrayMinimumBounds where P: PropagationActions, E: ExplanationActions, @@ -149,7 +150,7 @@ mod tests { use itertools::Itertools; use tracing_test::traced_test; - use crate::{array_int_maximum, array_int_minimum, reformulate::InitConfig, Decision, Model}; + use crate::{array_maximum_int, array_minimum_int, reformulate::InitConfig, Decision, Model}; #[test] #[traced_test] @@ -160,7 +161,7 @@ mod tests { let c = prb.new_int_var((2..=5).into()); let y = prb.new_int_var((1..=3).into()); - prb += array_int_maximum(vec![a, b, c], y); + prb += array_maximum_int(vec![a, b, c], y); let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap(); let vars = vec![a, b, c, y] .into_iter() @@ -188,7 +189,7 @@ mod tests { let c = prb.new_int_var((4..=10).into()); let y = prb.new_int_var((13..=20).into()); - prb += array_int_maximum(vec![a, b, c], y); + prb += array_maximum_int(vec![a, b, c], y); prb.assert_unsatisfiable(); } @@ -201,7 +202,7 @@ mod tests { let c = prb.new_int_var((2..=3).into()); let y = prb.new_int_var((3..=4).into()); - prb += array_int_minimum(vec![a, b, c], y); + prb += array_minimum_int(vec![a, b, c], y); let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap(); let vars = vec![a, b, c, y] .into_iter() @@ -224,7 +225,7 @@ mod tests { let c = prb.new_int_var((4..=10).into()); let y = prb.new_int_var((1..=2).into()); - prb += array_int_minimum(vec![a, b, c], y); + prb += array_minimum_int(vec![a, b, c], y); prb.assert_unsatisfiable(); } } diff --git a/crates/huub/src/constraints/int_div.rs b/crates/huub/src/constraints/int_div.rs index 55817f1..583af99 100644 --- a/crates/huub/src/constraints/int_div.rs +++ b/crates/huub/src/constraints/int_div.rs @@ -1,6 +1,6 @@ -//! Structures and algorithms for the `int_div` constraint, which enforces that -//! a numerator, a denominator, and a result variable are correctly related by -//! integer division. +//! Structures and algorithms for the integer division constraint, which +//! enforces that a numerator, a denominator, and a result variable are +//! correctly related by integer division. use std::mem; @@ -18,7 +18,7 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `int_div` constraint within a model. +/// Representation of the `div_int` constraint within a model. /// /// This constraint enforces that a numerator decision integer variable divided /// by a denominator integer decision variable is equal to a result integer diff --git a/crates/huub/src/constraints/set_in_reif.rs b/crates/huub/src/constraints/int_in_set.rs similarity index 90% rename from crates/huub/src/constraints/set_in_reif.rs rename to crates/huub/src/constraints/int_in_set.rs index 216b0e7..3a9d766 100644 --- a/crates/huub/src/constraints/set_in_reif.rs +++ b/crates/huub/src/constraints/int_in_set.rs @@ -1,4 +1,4 @@ -//! Structures and algorithms for the `set_in_reif` constraint, which +//! Structures and algorithms for the integer in set constraint, which //! constraints that an integer decision variable is assigned to a member of a //! given set if-and-only-if a given Boolean decision variable is assigned to //! `true`. @@ -13,11 +13,11 @@ use crate::{ }; #[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Representation of the `set_in_reif` constraint within a model. +/// Representation of the `int_in_set_reif` constraint within a model. /// /// This constraint enforces that the given Boolean variable takes the value /// `true` if-and-only-if an integer variable is in a given set. -pub struct SetInReif { +pub struct IntInSetReif { /// The integer decision variable monitored. pub(crate) var: IntDecision, /// The set of considered values for the integer decision variable. @@ -27,7 +27,7 @@ pub struct SetInReif { pub(crate) reif: BoolDecision, } -impl Constraint for SetInReif { +impl Constraint for IntInSetReif { fn initialize(&self, actions: &mut dyn ConstraintInitActions) { actions.simplify_on_change_bool(self.reif); } diff --git a/crates/huub/src/constraints/int_linear.rs b/crates/huub/src/constraints/int_linear.rs index b145bb5..637749a 100644 --- a/crates/huub/src/constraints/int_linear.rs +++ b/crates/huub/src/constraints/int_linear.rs @@ -21,17 +21,6 @@ use crate::{ BoolDecision, Conjunction, IntDecision, IntVal, }; -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] -/// Possible operators that can be used for in a linear constraint. -pub(crate) enum LinOperator { - /// Sum is equal to the constant - Equal, - /// Sum is less than or equal to the constant - LessEq, - /// Sum is not equal to the constant - NotEqual, -} - #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Representation of an integer linear constraint within a model. /// @@ -95,6 +84,17 @@ pub struct IntLinearNotEqValueImpl { reification: OptField, } +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// Possible operators that can be used for in a linear constraint. +pub(crate) enum LinOperator { + /// Sum is equal to the constant + Equal, + /// Sum is less than or equal to the constant + LessEq, + /// Sum is not equal to the constant + NotEqual, +} + #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] /// Reification possibilities for a linear constraint. pub(crate) enum Reification { @@ -122,22 +122,6 @@ impl IntLinear { } } - /// Change the integer linear constraint to be reified by the given Boolean - /// decision variable. - /// - /// The integer linear constraint must hold if-and-only-if the given Boolean - /// decision variable is `true`. - pub fn reified_by(self, b: BoolDecision) -> Self { - assert!( - self.reif.is_none(), - "IntLinear is already implied or reified." - ); - Self { - reif: Some(Reification::ReifiedBy(b)), - ..self - } - } - /// Internal method to negate the linear constraint. fn negate(self) -> Self { match self.operator { @@ -156,6 +140,22 @@ impl IntLinear { }, } } + + /// Change the integer linear constraint to be reified by the given Boolean + /// decision variable. + /// + /// The integer linear constraint must hold if-and-only-if the given Boolean + /// decision variable is `true`. + pub fn reified_by(self, b: BoolDecision) -> Self { + assert!( + self.reif.is_none(), + "IntLinear is already implied or reified." + ); + Self { + reif: Some(Reification::ReifiedBy(b)), + ..self + } + } } impl Constraint for IntLinear { diff --git a/crates/huub/src/constraints/int_pow.rs b/crates/huub/src/constraints/int_pow.rs index b795569..a288612 100644 --- a/crates/huub/src/constraints/int_pow.rs +++ b/crates/huub/src/constraints/int_pow.rs @@ -1,6 +1,6 @@ -//! Structures and algorithms for the `int_pow` constraint, which enforces that -//! the result of exponentiation of two integer variables is equal to a third -//! integer variable. +//! Structures and algorithms for the integer power constraint, which enforces +//! that the result of exponentiation of two integer variables is equal to a +//! third integer variable. use pindakaas::ClauseDatabaseTools; @@ -15,7 +15,7 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `int_pow` constraint within a model. +/// Representation of the `pow_int` constraint within a model. /// /// This constraint enforces that a base integer decision variable /// exponentiated by an exponent integer decision variable is equal to a result diff --git a/crates/huub/src/constraints/table_int.rs b/crates/huub/src/constraints/int_table.rs similarity index 95% rename from crates/huub/src/constraints/table_int.rs rename to crates/huub/src/constraints/int_table.rs index 5f841ca..efe36a2 100644 --- a/crates/huub/src/constraints/table_int.rs +++ b/crates/huub/src/constraints/int_table.rs @@ -1,6 +1,6 @@ -//! Structures and algorithms for the `table_int` constraint, which constraints -//! a sequence of integer decision variable to be assigned to a set of possible -//! sequences of integer values. +//! Structures and algorithms for the integer table constraint, which +//! constraints a sequence of integer decision variable to be assigned to a set +//! of possible sequences of integer values. use itertools::Itertools; use pindakaas::ClauseDatabaseTools; @@ -18,14 +18,14 @@ use crate::{ /// /// This constraint enforces that the given list of integer views take their /// values according to one of the given lists of integer values. -pub struct TableInt { +pub struct IntTable { /// List of variables that must take the values of a row in the table. pub(crate) vars: Vec, /// The table of possible values for the variables. pub(crate) table: Vec>, } -impl Constraint for TableInt { +impl Constraint for IntTable { fn simplify(&mut self, actions: &mut S) -> Result { match self.vars.len() { 0 => return Ok(SimplificationStatus::Subsumed), diff --git a/crates/huub/src/constraints/int_times.rs b/crates/huub/src/constraints/int_times.rs index a57897d..8bc8601 100644 --- a/crates/huub/src/constraints/int_times.rs +++ b/crates/huub/src/constraints/int_times.rs @@ -1,4 +1,4 @@ -//! Structures and algorithms for the `int_times` constraint, which enforces +//! Structures and algorithms for the integer times constraint, which enforces //! that the product of two integer variables is equal to a third integer //! variable. @@ -16,7 +16,7 @@ use crate::{ }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] -/// Representation of the `int_times` constraint within a model. +/// Representation of the `times_int` constraint within a model. /// /// This constraint enforces that the product of the two integer decision /// variables is equal to a third. diff --git a/crates/huub/src/flatzinc.rs b/crates/huub/src/flatzinc.rs index 3cdd3f3..290d278 100644 --- a/crates/huub/src/flatzinc.rs +++ b/crates/huub/src/flatzinc.rs @@ -16,17 +16,16 @@ use flatzinc_serde::{ }; use itertools::Itertools; use pindakaas::propositional_logic::Formula; -use rangelist::{IntervalIterator, RangeList}; +use rangelist::IntervalIterator; use thiserror::Error; use tracing::warn; use crate::{ - actions::SimplificationActions, all_different_int, array_int_element, array_int_maximum, - array_int_minimum, array_var_bool_element, array_var_int_element, - constraints::table_int::TableInt, disjunctive_strict, int_abs, int_div, int_pow, int_times, - reformulate::ReformulationError, set_in_reif, table_int, BoolDecision, Branching, Decision, - IntDecision, IntDecisionInner, IntLinExpr, IntSetVal, IntVal, Model, NonZeroIntVal, - ValueSelection, VariableSelection, + abs_int, actions::SimplificationActions, all_different_int, array_element, array_maximum_int, + array_minimum_int, constraints::int_table::IntTable, disjunctive_strict, div_int, + int_in_set_reif, pow_int, reformulate::ReformulationError, table_int, times_int, BoolDecision, + Branching, Decision, IntDecision, IntDecisionInner, IntLinExpr, IntSetVal, IntVal, Model, + NonZeroIntVal, ValueSelection, VariableSelection, }; #[derive(Error, Debug)] @@ -455,7 +454,7 @@ where transitions: Vec>, init_state: IntVal, accept_states: HashSet, - ) -> Vec { + ) -> Vec { // TODO: Add the regular checking let mut table_constraints = Vec::new(); @@ -933,26 +932,7 @@ where let idx = self.arg_int(idx)?; let val = self.arg_bool(val)?; - // Convert array of boolean values to a set literals of the indices where - // the value is true - let mut ranges = Vec::new(); - let mut start = None; - for (i, b) in arr.iter().enumerate() { - match (b, start) { - (true, None) => start = Some((i + 1) as IntVal), - (false, Some(s)) => { - ranges.push(s..=i as IntVal); - start = None; - } - (false, None) | (true, Some(_)) => {} - } - } - if let Some(s) = start { - ranges.push(s..=arr.len() as IntVal); - } - assert_ne!(ranges.len(), 0, "unexpected empty range list"); - - self.prb += set_in_reif(idx, RangeList::from_iter(ranges), val); + self.prb += array_element(arr, idx - 1, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_bool_element", @@ -963,14 +943,14 @@ where } "array_int_element" => { if let [idx, arr, val] = c.args.as_slice() { - let arr: Result, _> = self + let arr: Vec<_> = self .arg_array(arr)? .iter() .map(|l| self.par_int(l)) - .collect(); + .try_collect()?; let idx = self.arg_int(idx)?; let val = self.arg_int(val)?; - self.prb += array_int_element(idx - 1, arr?, val); + self.prb += array_element(arr, idx - 1, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_int_element", @@ -989,7 +969,7 @@ where let idx = self.arg_int(idx)?; let val = self.arg_bool(val)?; - self.prb += array_var_bool_element(idx - 1, arr, val); + self.prb += array_element(arr, idx - 1, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_var_bool_element", @@ -1000,14 +980,15 @@ where } "array_var_int_element" => { if let [idx, arr, val] = c.args.as_slice() { - let arr: Result, _> = self + let arr: Vec<_> = self .arg_array(arr)? .iter() .map(|l| self.lit_int(l)) - .collect(); + .try_collect()?; let idx = self.arg_int(idx)?; let val = self.arg_int(val)?; - self.prb += array_var_int_element(idx - 1, arr?, val); + + self.prb += array_element(arr, idx - 1, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_var_int_element", @@ -1153,9 +1134,9 @@ where args.iter().map(|l| self.lit_int(l)).collect(); let m = self.arg_int(m)?; if is_maximum { - self.prb += array_int_maximum(args?, m); + self.prb += array_maximum_int(args?, m); } else { - self.prb += array_int_minimum(args?, m); + self.prb += array_minimum_int(args?, m); } } else { return Err(FlatZincError::InvalidNumArgs { @@ -1293,7 +1274,7 @@ where if let [origin, abs] = c.args.as_slice() { let origin = self.arg_int(origin)?; let abs = self.arg_int(abs)?; - self.prb += int_abs(origin, abs); + self.prb += abs_int(origin, abs); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_abs", @@ -1307,7 +1288,7 @@ where let num = self.arg_int(num)?; let denom = self.arg_int(denom)?; let res = self.arg_int(res)?; - self.prb += int_div(num, denom, res); + self.prb += div_int(num, denom, res); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_div", @@ -1470,9 +1451,9 @@ where let b = self.arg_int(b)?; let m = self.arg_int(m)?; if is_maximum { - self.prb += array_int_maximum(vec![a, b], m); + self.prb += array_maximum_int(vec![a, b], m); } else { - self.prb += array_int_minimum(vec![a, b], m); + self.prb += array_minimum_int(vec![a, b], m); } } else { return Err(FlatZincError::InvalidNumArgs { @@ -1487,7 +1468,7 @@ where let base = self.arg_int(base)?; let exponent = self.arg_int(exponent)?; let res = self.arg_int(res)?; - self.prb += int_pow(base, exponent, res); + self.prb += pow_int(base, exponent, res); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_pow", @@ -1501,7 +1482,7 @@ where let a = self.arg_int(x)?; let b = self.arg_int(y)?; let m = self.arg_int(z)?; - self.prb += int_times(a, b, m); + self.prb += times_int(a, b, m); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_times", @@ -1530,7 +1511,7 @@ where let s = self.arg_par_set(s)?; let r = self.arg_bool(r)?; - self.prb += set_in_reif(x, s, r); + self.prb += int_in_set_reif(x, s, r); } else { return Err(FlatZincError::InvalidNumArgs { name: "set_in_reif", diff --git a/crates/huub/src/lib.rs b/crates/huub/src/lib.rs index b515e2c..233c1d0 100644 --- a/crates/huub/src/lib.rs +++ b/crates/huub/src/lib.rs @@ -45,19 +45,18 @@ use crate::{ actions::{ConstraintInitActions, SimplificationActions}, branchers::{BoolBrancher, IntBrancher, WarmStartBrancher}, constraints::{ - all_different_int::AllDifferentInt, - array_int_element::ArrayIntElement, - array_int_minimum::ArrayIntMinimum, - array_var_bool_element::ArrayVarBoolElement, - array_var_int_element::ArrayVarIntElement, + bool_array_element::BoolDecisionArrayElement, disjunctive_strict::DisjunctiveStrict, int_abs::IntAbs, + int_all_different::IntAllDifferent, + int_array_element::{IntDecisionArrayElement, IntValArrayElement}, + int_array_minimum::IntArrayMinimum, int_div::IntDiv, + int_in_set::IntInSetReif, int_linear::{IntLinear, LinOperator}, int_pow::IntPow, + int_table::IntTable, int_times::IntTimes, - set_in_reif::SetInReif, - table_int::TableInt, BoxedConstraint, Constraint, SimplificationStatus, }, flatzinc::{FlatZincError, FlatZincStatistics, FznModelBuilder}, @@ -83,6 +82,10 @@ use crate::{ /// Note that decisions only represent where the decision is kept pub struct BoolDecision(BoolDecisionInner); +/// Type alias for the type used to represent propositional logic formulas that +/// can be used in [`Model`]. +pub type BoolFormula = Formula; + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Strategy for making a search decisions to be added to a [`Model`]. /// @@ -121,6 +124,23 @@ pub enum Decision { Int(IntDecision), } +/// Helper trait used to create array element constraints for on collections of +/// different types. +pub trait ElementConstraint: Sized { + /// The constraint type created and to be added to a [`Model`]. + type Constraint; + /// The decision variable type to contain the selected element. + type Result; + + /// Create a constraint that enforces that the `result` decision variables + /// takes the same value as `array[index]`. + fn element_constraint( + array: Vec, + index: IntDecision, + result: Self::Result, + ) -> Self::Constraint; +} + #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] /// A reference to an integer value or its transformation in a [`Model`]. pub struct IntDecision(IntDecisionInner); @@ -144,13 +164,6 @@ pub type IntSetVal = RangeList; /// Type alias for an parameter integer value. pub type IntVal = i64; -/// Type alias for the type used to represent logic formulas that can be used in -/// [`Model`]. -pub type LogicFormula = Formula; - -/// Type alias for a non-zero paremeter integer value. -pub type NonZeroIntVal = NonZeroI64; - #[derive(Clone, Debug, Default)] /// A formulation of a problem instance in terms of decisions and constraints. pub struct Model { @@ -169,6 +182,9 @@ pub struct Model { enqueued: Vec, } +/// Type alias for a non-zero paremeter integer value. +pub type NonZeroIntVal = NonZeroI64; + #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] /// Strategy for limiting the domain of a selected decision variable as part of /// a [`Branching`]. @@ -205,78 +221,61 @@ pub enum VariableSelection { Smallest, } -/// Create a `all_different_int` constraint that enforces that all the given -/// integer decisions take different values. -pub fn all_different_int(vars: Iter) -> AllDifferentInt +/// Create a constraint that enforces that the second integer decision variable +/// takes the absolute value of the first integer decision variable. +pub fn abs_int(origin: IntDecision, abs: IntDecision) -> IntAbs { + IntAbs { origin, abs } +} + +/// Create a constraint that enforces that all the given integer decisions take +/// different values. +pub fn all_different_int(vars: Iter) -> IntAllDifferent where Iter: IntoIterator, Iter::Item: Into, { - AllDifferentInt { + IntAllDifferent { vars: vars.into_iter().map_into().collect(), } } -/// Create an `array_int_element` constraint that enforces that a result integer -/// decision variable takes the value equal the element of the given array of -/// integer values at the given index decision variable. -pub fn array_int_element( +/// Create a constraint that enforces that a result decision variable takes the +/// value equal the element of the given array at the given index decision +/// variable. +pub fn array_element( + array: Vec, index: IntDecision, - array: Vec, - result: IntDecision, -) -> ArrayIntElement { - ArrayIntElement { - index, - array, - result, - } + result: ::Result, +) -> ::Constraint { + ::element_constraint(array, index, result) } -/// Create an `array_int_maximum` constraint that enforces that an integer -/// decision variable takes the minimum value of an array of integer decision -/// variables. -pub fn array_int_maximum(vars: Iter, max: IntDecision) -> ArrayIntMinimum +/// Create a constraint that enforces that an integer decision variable takes +/// the minimum value of an array of integer decision variables. +pub fn array_maximum_int(vars: Iter, max: IntDecision) -> IntArrayMinimum where Iter: IntoIterator, Iter::Item: Into, { - array_int_minimum(vars.into_iter().map(|v| -v.into()), -max) + array_minimum_int(vars.into_iter().map(|v| -v.into()), -max) } -/// Create an `array_int_minimum` constraint that enforces that an integer -/// decision variable takes the minimum value of an array of integer decision -/// variables. -pub fn array_int_minimum(vars: Iter, min: IntDecision) -> ArrayIntMinimum +/// Create a constraint that enforces that an integer decision variable takes +/// the minimum value of an array of integer decision variables. +pub fn array_minimum_int(vars: Iter, min: IntDecision) -> IntArrayMinimum where Iter: IntoIterator, Iter::Item: Into, { - ArrayIntMinimum { + IntArrayMinimum { vars: vars.into_iter().map_into().collect(), min, } } -/// Create an `array_var_bool_element` constraint that enforces that a result -/// Boolean decision variable takes the value equal the element of the given -/// array of Boolean decision varaibles at the index given by the index integer -/// decision variable. -pub fn array_var_bool_element( - index: IntDecision, - array: Vec, - result: BoolDecision, -) -> ArrayVarBoolElement { - ArrayVarBoolElement { - index, - array, - result, - } -} - -/// Create a `disjunctive_strict` constraint that enforces that the given a list -/// of integer decision variables representing the start times of tasks and a -/// list of integer values representing the durations of tasks, the tasks do not -/// overlap in time. +/// Create a constraint that enforces that the given a list of integer decision +/// variables representing the start times of tasks and a list of integer values +/// representing the durations of tasks, the tasks do not overlap in time. pub fn disjunctive_strict( start_times: Vec, durations: Vec, @@ -296,32 +295,10 @@ pub fn disjunctive_strict( } } -/// Create an `array_var_int_element` constraint that enforces that a result -/// integer decision variable takes the value equal the element of the given -/// array of integer decision variable at the given index decision variable. -pub fn array_var_int_element( - index: IntDecision, - array: Vec, - result: IntDecision, -) -> ArrayVarIntElement { - ArrayVarIntElement { - index, - array, - result, - } -} - -/// Create an `int_abs` constraint that enforces that the second integer -/// decision variable takes the absolute value of the first integer decision -/// variable. -pub fn int_abs(origin: IntDecision, abs: IntDecision) -> IntAbs { - IntAbs { origin, abs } -} - -/// Create an `int_div` constraint that enforces that a numerator decision -/// integer variable divided by a denominator integer decision variable is equal -/// to a result integer decision variable. -pub fn int_div(numerator: IntDecision, denominator: IntDecision, result: IntDecision) -> IntDiv { +/// Create a constraint that enforces that a numerator decision integer variable +/// divided by a denominator integer decision variable is equal to a result +/// integer decision variable. +pub fn div_int(numerator: IntDecision, denominator: IntDecision, result: IntDecision) -> IntDiv { IntDiv { numerator, denominator, @@ -329,10 +306,16 @@ pub fn int_div(numerator: IntDecision, denominator: IntDecision, result: IntDeci } } -/// Create an `int_pow` constraint that enforces that a base integer decision -/// variable exponentiated by an exponent integer decision variable is equal to -/// a result integer decision variable. -pub fn int_pow(base: IntDecision, exponent: IntDecision, result: IntDecision) -> IntPow { +/// Create constraint that enforces that the given Boolean variable takes the +/// value `true` if-and-only-if an integer variable is in a given set. +pub fn int_in_set_reif(var: IntDecision, set: IntSetVal, reif: BoolDecision) -> IntInSetReif { + IntInSetReif { var, set, reif } +} + +/// Create a constraint that enforces that a base integer decision variable +/// exponentiated by an exponent integer decision variable is equal to a result +/// integer decision variable. +pub fn pow_int(base: IntDecision, exponent: IntDecision, result: IntDecision) -> IntPow { IntPow { base, exponent, @@ -340,9 +323,17 @@ pub fn int_pow(base: IntDecision, exponent: IntDecision, result: IntDecision) -> } } -/// Create an `int_times` constraint that enforces that the product of the two -/// integer decision variables is equal to a third. -pub fn int_times(factor1: IntDecision, factor2: IntDecision, product: IntDecision) -> IntTimes { +/// Create a `table_int` constraint that enforces that given list of integer +/// views take their values according to one of the given lists of integer +/// values. +pub fn table_int(vars: Vec, table: Vec>) -> IntTable { + assert!(table.iter().all(|tup| tup.len() == vars.len()), "The number of values in each row of the table must be equal to the number of decision variables."); + IntTable { vars, table } +} + +/// Create a constraint that enforces that the product of the two integer +/// decision variables is equal to a third. +pub fn times_int(factor1: IntDecision, factor2: IntDecision, product: IntDecision) -> IntTimes { IntTimes { factor1, factor2, @@ -350,19 +341,21 @@ pub fn int_times(factor1: IntDecision, factor2: IntDecision, product: IntDecisio } } -/// Create a `set_in_reif` constraint that enforces that the given Boolean -/// variable takes the value `true` if-and-only-if an integer variable is in a -/// given set. -pub fn set_in_reif(var: IntDecision, set: IntSetVal, reif: BoolDecision) -> SetInReif { - SetInReif { var, set, reif } -} - -/// Create a `table_int` constraint that enforces that given list of integer -/// views take their values according to one of the given lists of integer -/// values. -pub fn table_int(vars: Vec, table: Vec>) -> TableInt { - assert!(table.iter().all(|tup| tup.len() == vars.len()), "The number of values in each row of the table must be equal to the number of decision variables."); - TableInt { vars, table } +impl ElementConstraint for BoolDecision { + type Constraint = BoolDecisionArrayElement; + type Result = BoolDecision; + + fn element_constraint( + array: Vec, + index: IntDecision, + result: Self::Result, + ) -> Self::Constraint { + Self::Constraint { + index, + array, + result, + } + } } impl From for BoolDecision { @@ -388,6 +381,12 @@ impl Not for BoolDecision { } } +impl From for BoolFormula { + fn from(v: BoolDecision) -> Self { + Self::Atom(v) + } +} + impl Branching { /// Add a [`Brancher`] implementation to the solver that matches the branching /// strategy of the [`Branching`]. @@ -457,16 +456,22 @@ impl IntDecision { } } + /// Get a Boolean view that represent whether the integer view is greater than + /// or equal to the given value. + pub fn geq(&self, v: IntVal) -> BoolDecision { + !self.lt(v) + } + /// Get a Boolean view that represent whether the integer view is greater than /// the given value. pub fn gt(&self, v: IntVal) -> BoolDecision { self.geq(v + 1) } - /// Get a Boolean view that represent whether the integer view is greater than - /// or equal to the given value. - pub fn geq(&self, v: IntVal) -> BoolDecision { - !self.lt(v) + /// Get a Boolean view that represent whether the integer view is less than or + /// equal to the given value. + pub fn leq(&self, v: IntVal) -> BoolDecision { + self.lt(v + 1) } /// Get a Boolean view that represent whether the integer view is less than @@ -496,12 +501,6 @@ impl IntDecision { } } - /// Get a Boolean view that represent whether the integer view is less than or - /// equal to the given value. - pub fn leq(&self, v: IntVal) -> BoolDecision { - self.lt(v + 1) - } - /// Get a Boolean view that represent whether the integer view is not equal to /// the given value. pub fn ne(&self, v: IntVal) -> BoolDecision { @@ -544,9 +543,20 @@ impl Add for IntDecision { } } -impl From for IntDecision { - fn from(value: i64) -> Self { - IntDecision(IntDecisionInner::Const(value)) +impl ElementConstraint for IntDecision { + type Constraint = IntDecisionArrayElement; + type Result = IntDecision; + + fn element_constraint( + array: Vec, + index: IntDecision, + result: Self::Result, + ) -> Self::Constraint { + Self::Constraint { + index, + array, + result, + } } } @@ -559,6 +569,12 @@ impl From for IntDecision { } } +impl From for IntDecision { + fn from(value: i64) -> Self { + IntDecision(IntDecisionInner::Const(value)) + } +} + impl Mul for IntDecision { type Output = Self; @@ -618,23 +634,6 @@ impl Sub for IntDecision { } impl IntLinExpr { - /// Create a new integer linear constraint that enforces that the sum of the - /// expressions in the object is less than or equal to the given value. - pub fn lt(self, rhs: IntVal) -> IntLinear { - self.leq(rhs - 1) - } - - /// Create a new integer linear constraint that enforces that the sum of the - /// expressions in the object is less than the given value. - pub fn leq(self, rhs: IntVal) -> IntLinear { - IntLinear { - terms: self.terms, - operator: LinOperator::LessEq, - rhs, - reif: None, - } - } - /// Create a new integer linear constraint that enforces that the sum of the /// expressions in the object is equal to the given value. pub fn eq(self, rhs: IntVal) -> IntLinear { @@ -658,6 +657,22 @@ impl IntLinExpr { pub fn gt(self, rhs: IntVal) -> IntLinear { self.geq(rhs + 1) } + + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is less than the given value. + pub fn leq(self, rhs: IntVal) -> IntLinear { + IntLinear { + terms: self.terms, + operator: LinOperator::LessEq, + rhs, + reif: None, + } + } + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is less than or equal to the given value. + pub fn lt(self, rhs: IntVal) -> IntLinear { + self.leq(rhs - 1) + } /// Create a new integer linear constraint that enforces that the sum of the /// expressions in the object is not equal to the given value. pub fn ne(self, rhs: IntVal) -> IntLinear { @@ -723,12 +738,22 @@ impl Sum for IntLinExpr { } } -impl From for LogicFormula { - fn from(v: BoolDecision) -> Self { - Self::Atom(v) +impl ElementConstraint for IntVal { + type Constraint = IntValArrayElement; + type Result = IntDecision; + + fn element_constraint( + array: Vec, + index: IntDecision, + result: Self::Result, + ) -> Self::Constraint { + Self::Constraint { + index, + array, + result, + } } } - impl Model { /// Internal method to add a constraint to the model. /// @@ -807,21 +832,21 @@ impl Model { }; let status = match &mut con_obj { - ConstraintStore::AllDifferentInt(c) => c.simplify(self), - ConstraintStore::ArrayIntElement(c) => c.simplify(self), - ConstraintStore::ArrayIntMinimum(c) => c.simplify(self), - ConstraintStore::ArrayVarBoolElement(c) => c.simplify(self), - ConstraintStore::ArrayVarIntElement(c) => c.simplify(self), + ConstraintStore::IntAllDifferent(c) => c.simplify(self), + ConstraintStore::IntValArrayElement(c) => c.simplify(self), + ConstraintStore::IntArrayMinimum(c) => c.simplify(self), + ConstraintStore::BoolDecisionArrayElement(c) => c.simplify(self), + ConstraintStore::IntDecisionArrayElement(c) => c.simplify(self), ConstraintStore::DisjunctiveStrict(c) => c.simplify(self), ConstraintStore::IntAbs(c) => c.simplify(self), ConstraintStore::IntDiv(c) => c.simplify(self), ConstraintStore::IntLinear(c) => c.simplify(self), ConstraintStore::IntPow(c) => c.simplify(self), ConstraintStore::IntTimes(c) => c.simplify(self), - ConstraintStore::PropLogic(exp) => exp.simplify(self), - ConstraintStore::SetInReif(c) => c.simplify(self), - ConstraintStore::TableInt(con) => con.simplify(self), - ConstraintStore::UserCustom(con) => con.simplify(self), + ConstraintStore::BoolFormula(exp) => exp.simplify(self), + ConstraintStore::IntInSetReif(c) => c.simplify(self), + ConstraintStore::IntTable(con) => con.simplify(self), + ConstraintStore::Other(con) => con.simplify(self), }?; match status { SimplificationStatus::Subsumed => { @@ -865,20 +890,20 @@ impl Model { let con_store = self.constraints[con].take().unwrap(); let mut ctx = ConstraintInitContext { con, model: self }; match &con_store { - ConstraintStore::AllDifferentInt(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntAllDifferent(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::ArrayIntElement(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntValArrayElement(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::ArrayIntMinimum(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntArrayMinimum(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::ArrayVarBoolElement(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::BoolDecisionArrayElement(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::ArrayVarIntElement(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntDecisionArrayElement(con) => { + >::initialize(con, &mut ctx); } ConstraintStore::DisjunctiveStrict(con) => { >::initialize(con, &mut ctx); @@ -898,16 +923,16 @@ impl Model { ConstraintStore::IntTimes(con) => { >::initialize(con, &mut ctx); } - ConstraintStore::PropLogic(exp) => { + ConstraintStore::BoolFormula(exp) => { as Constraint>::initialize(exp, &mut ctx); } - ConstraintStore::SetInReif(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntInSetReif(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::TableInt(con) => { - >::initialize(con, &mut ctx); + ConstraintStore::IntTable(con) => { + >::initialize(con, &mut ctx); } - ConstraintStore::UserCustom(con) => con.initialize(&mut ctx), + ConstraintStore::Other(con) => con.initialize(&mut ctx), } self.constraints[con] = Some(con_store); } @@ -957,7 +982,7 @@ impl Model { for c in self.constraints.iter().flatten() { match c { - ConstraintStore::AllDifferentInt(c) => { + ConstraintStore::IntAllDifferent(c) => { for v in &c.vars { if let IntDecisionInner::Var(iv) | IntDecisionInner::Linear(_, iv) = v.0 { if self.int_vars[iv].domain.card() <= (c.vars.len() * 100 / 80) { @@ -966,22 +991,22 @@ impl Model { } } } - ConstraintStore::ArrayIntElement(c) => { + ConstraintStore::IntValArrayElement(c) => { if let IntDecisionInner::Var(iv) | IntDecisionInner::Linear(_, iv) = c.index.0 { let _ = eager_direct.insert(iv); } } - ConstraintStore::ArrayVarBoolElement(c) => { + ConstraintStore::BoolDecisionArrayElement(c) => { if let IntDecisionInner::Var(iv) | IntDecisionInner::Linear(_, iv) = c.index.0 { let _ = eager_direct.insert(iv); } } - ConstraintStore::ArrayVarIntElement(c) => { + ConstraintStore::IntDecisionArrayElement(c) => { if let IntDecisionInner::Var(iv) | IntDecisionInner::Linear(_, iv) = c.index.0 { let _ = eager_direct.insert(iv); } } - ConstraintStore::TableInt(con) => { + ConstraintStore::IntTable(con) => { for &v in &con.vars { if let IntDecisionInner::Var(iv) | IntDecisionInner::Linear(_, iv) = v.0 { let _ = eager_direct.insert(iv); @@ -1014,25 +1039,6 @@ impl Model { }) .collect(); - // self.cnf.variables().map(|v| slv.new_lit()).collect(); - // for (i, var) in { - // let direct_enc = if eager_direct.contains(&i) { - // EncodingType::Eager - // } else { - // EncodingType::Lazy - // }; - // let order_enc = if eager_order.contains(&i) - // || eager_direct.contains(&i) - // || var.domain.card() <= config.int_eager_limit() - // { - // EncodingType::Eager - // } else { - // EncodingType::Lazy - // }; - // let view = SlvIntVar::new_in(&mut slv, var.domain.clone(), order_enc, direct_enc); - // map.insert_int(i, view); - // } - // let map = ReformulationMap { bool_map, int_map }; // Create constraint data structures within the solver @@ -1048,63 +1054,57 @@ impl Model { } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: AllDifferentInt) { - self.add_constraint(ConstraintStore::AllDifferentInt(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: BoolDecisionArrayElement) { + self.add_constraint(ConstraintStore::BoolDecisionArrayElement(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: ArrayIntElement) { - self.add_constraint(ConstraintStore::ArrayIntElement(constraint)); - } -} - -impl AddAssign for Model { - fn add_assign(&mut self, constraint: ArrayIntMinimum) { - self.add_constraint(ConstraintStore::ArrayIntMinimum(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: BoxedConstraint) { + self.add_constraint(ConstraintStore::Other(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: ArrayVarBoolElement) { - self.add_constraint(ConstraintStore::ArrayVarBoolElement(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, rhs: Branching) { + self.branchings.push(rhs); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: ArrayVarIntElement) { - self.add_constraint(ConstraintStore::ArrayVarIntElement(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: DisjunctiveStrict) { + self.add_constraint(ConstraintStore::DisjunctiveStrict(constraint)); } } impl AddAssign> for Model { fn add_assign(&mut self, constraint: Formula) { - self.add_constraint(ConstraintStore::PropLogic(constraint)); + self.add_constraint(ConstraintStore::BoolFormula(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, rhs: Branching) { - self.branchings.push(rhs); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntAbs) { + self.add_constraint(ConstraintStore::IntAbs(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: BoxedConstraint) { - self.add_constraint(ConstraintStore::UserCustom(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntAllDifferent) { + self.add_constraint(ConstraintStore::IntAllDifferent(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: DisjunctiveStrict) { - self.add_constraint(ConstraintStore::DisjunctiveStrict(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntArrayMinimum) { + self.add_constraint(ConstraintStore::IntArrayMinimum(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: IntAbs) { - self.add_constraint(ConstraintStore::IntAbs(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntDecisionArrayElement) { + self.add_constraint(ConstraintStore::IntDecisionArrayElement(constraint)); } } @@ -1114,6 +1114,12 @@ impl AddAssign for Model { } } +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntInSetReif) { + self.add_constraint(ConstraintStore::IntInSetReif(constraint)); + } +} + impl AddAssign for Model { fn add_assign(&mut self, constraint: IntLinear) { self.add_constraint(ConstraintStore::IntLinear(constraint)); @@ -1126,21 +1132,21 @@ impl AddAssign for Model { } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: IntTimes) { - self.add_constraint(ConstraintStore::IntTimes(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntTable) { + self.add_constraint(ConstraintStore::IntTable(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: SetInReif) { - self.add_constraint(ConstraintStore::SetInReif(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntTimes) { + self.add_constraint(ConstraintStore::IntTimes(constraint)); } } -impl AddAssign for Model { - fn add_assign(&mut self, constraint: TableInt) { - self.add_constraint(ConstraintStore::TableInt(constraint)); +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntValArrayElement) { + self.add_constraint(ConstraintStore::IntValArrayElement(constraint)); } } @@ -1361,6 +1367,56 @@ impl SimplificationActions for Model { } } + fn set_int_not_eq(&mut self, var: IntDecision, val: IntVal) -> Result<(), ReformulationError> { + self.set_int_in_set(var, &(val..=val).into()) + } + + fn set_int_not_in_set( + &mut self, + var: IntDecision, + values: &IntSetVal, + ) -> Result<(), ReformulationError> { + use IntDecisionInner::*; + + match var.0 { + Var(v) => { + let diff: RangeList<_> = self.int_vars[v].domain.diff(values); + if diff.is_empty() { + return Err(ReformulationError::TrivialUnsatisfiable); + } else if self.int_vars[v].domain == diff { + return Ok(()); + } + self.int_vars[v].domain = diff; + let constraints = self.int_vars[v].constraints.clone(); + for c in constraints { + self.enqueue(c); + } + Ok(()) + } + Const(v) => { + if values.contains(&v) { + Err(ReformulationError::TrivialUnsatisfiable) + } else { + Ok(()) + } + } + Linear(trans, iv) => { + let mask = trans.rev_transform_int_set(values); + self.set_int_not_in_set(IntDecision(Var(iv)), &mask) + } + Bool(trans, b) => { + let values = trans.rev_transform_int_set(values); + if values.contains(&0) { + self.set_bool(b)?; + } + if values.contains(&1) { + self.set_bool(!b)?; + } + Ok(()) + } + } + } + fn set_int_upper_bound( &mut self, var: IntDecision, @@ -1459,54 +1515,40 @@ impl SimplificationActions for Model { }, } } +} - fn set_int_not_eq(&mut self, var: IntDecision, val: IntVal) -> Result<(), ReformulationError> { - self.set_int_in_set(var, &(val..=val).into()) - } - - fn set_int_not_in_set( - &mut self, - var: IntDecision, - values: &IntSetVal, - ) -> Result<(), ReformulationError> { - use IntDecisionInner::*; - - match var.0 { - Var(v) => { - let diff: RangeList<_> = self.int_vars[v].domain.diff(values); - if diff.is_empty() { - return Err(ReformulationError::TrivialUnsatisfiable); - } else if self.int_vars[v].domain == diff { - return Ok(()); - } - self.int_vars[v].domain = diff; - let constraints = self.int_vars[v].constraints.clone(); - for c in constraints { - self.enqueue(c); - } - Ok(()) - } - Const(v) => { - if values.contains(&v) { - Err(ReformulationError::TrivialUnsatisfiable) - } else { - Ok(()) +impl ElementConstraint for bool { + type Constraint = IntInSetReif; + type Result = BoolDecision; + + fn element_constraint( + array: Vec, + index: IntDecision, + result: Self::Result, + ) -> Self::Constraint { + // Convert array of boolean values to a set literals of the indices where + // the value is true + let mut ranges = Vec::new(); + let mut start = None; + for (i, b) in array.iter().enumerate() { + match (b, start) { + (true, None) => start = Some(i as IntVal), + (false, Some(s)) => { + ranges.push(s..=i as IntVal); + start = None; } + (false, None) | (true, Some(_)) => {} } - Linear(trans, iv) => { - let mask = trans.rev_transform_int_set(values); - self.set_int_not_in_set(IntDecision(Var(iv)), &mask) - } - Bool(trans, b) => { - let values = trans.rev_transform_int_set(values); - if values.contains(&0) { - self.set_bool(b)?; - } - if values.contains(&1) { - self.set_bool(!b)?; - } - Ok(()) - } + } + if let Some(s) = start { + ranges.push(s..=array.len() as IntVal); + } + assert_ne!(ranges.len(), 0, "unexpected empty range list"); + + Self::Constraint { + var: index, + set: RangeList::from_iter(ranges), + reif: result, } } } diff --git a/crates/huub/src/reformulate.rs b/crates/huub/src/reformulate.rs index 30c1a6a..a5d1f9b 100644 --- a/crates/huub/src/reformulate.rs +++ b/crates/huub/src/reformulate.rs @@ -16,12 +16,19 @@ use crate::{ SimplificationActions, TrailingActions, }, constraints::{ - all_different_int::AllDifferentInt, array_int_element::ArrayIntElement, - array_int_minimum::ArrayIntMinimum, array_var_bool_element::ArrayVarBoolElement, - array_var_int_element::ArrayVarIntElement, disjunctive_strict::DisjunctiveStrict, - int_abs::IntAbs, int_div::IntDiv, int_linear::IntLinear, int_pow::IntPow, - int_times::IntTimes, set_in_reif::SetInReif, table_int::TableInt, BoxedConstraint, - BoxedPropagator, Constraint, SimplificationStatus, + bool_array_element::BoolDecisionArrayElement, + disjunctive_strict::DisjunctiveStrict, + int_abs::IntAbs, + int_all_different::IntAllDifferent, + int_array_element::{IntDecisionArrayElement, IntValArrayElement}, + int_array_minimum::IntArrayMinimum, + int_div::IntDiv, + int_in_set::IntInSetReif, + int_linear::IntLinear, + int_pow::IntPow, + int_table::IntTable, + int_times::IntTimes, + BoxedConstraint, BoxedPropagator, Constraint, SimplificationStatus, }, helpers::linear_transform::LinearTransform, solver::{ @@ -32,7 +39,7 @@ use crate::{ trail::TrailedInt, BoolView, BoolViewInner, IntView, IntViewInner, View, }, - BoolDecision, Decision, IntDecision, IntLitMeaning, IntSetVal, IntVal, LogicFormula, Model, + BoolDecision, BoolFormula, Decision, IntDecision, IntLitMeaning, IntSetVal, IntVal, Model, Solver, }; @@ -68,23 +75,21 @@ pub(crate) enum BoolDecisionInner { /// /// This enum type is used to store and analyze the constraints in a [`Model`]. pub(crate) enum ConstraintStore { - AllDifferentInt(AllDifferentInt), - ArrayIntElement(ArrayIntElement), - ArrayIntMinimum(ArrayIntMinimum), - ArrayVarBoolElement(ArrayVarBoolElement), - ArrayVarIntElement(ArrayVarIntElement), + BoolDecisionArrayElement(BoolDecisionArrayElement), + BoolFormula(BoolFormula), DisjunctiveStrict(DisjunctiveStrict), IntAbs(IntAbs), + IntAllDifferent(IntAllDifferent), + IntArrayMinimum(IntArrayMinimum), + IntDecisionArrayElement(IntDecisionArrayElement), IntDiv(IntDiv), + IntInSetReif(IntInSetReif), IntLinear(IntLinear), IntPow(IntPow), + IntTable(IntTable), IntTimes(IntTimes), - /// A constraint given as a propasitional logic formula, which is enforced to - /// be `true`. - PropLogic(Formula), - SetInReif(SetInReif), - TableInt(TableInt), - UserCustom(BoxedConstraint), + IntValArrayElement(IntValArrayElement), + Other(BoxedConstraint), } #[derive(Clone, Debug, Default, Hash, PartialEq, Eq)] @@ -100,9 +105,16 @@ pub struct InitConfig { vivification: bool, } -define_index_type! { - /// Reference type for integer decision variables in a [`Model`]. - pub(crate) struct IntDecisionIndex = u32; +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Definition of an integer decision variable in a [`Model`]. +pub(crate) struct IntDecisionDef { + /// The set of possible values that the variable can take. + pub(crate) domain: IntSetVal, + /// The list of (indexes of) constraints in which the variable appears. + /// + /// This list is used to enqueue the constraints for propagation when the + /// domain of the variable changes. + pub(crate) constraints: Vec, } #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] @@ -119,18 +131,6 @@ pub(crate) enum IntDecisionInner { Bool(LinearTransform, BoolDecision), } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Definition of an integer decision variable in a [`Model`]. -pub(crate) struct IntDecisionDef { - /// The set of possible values that the variable can take. - pub(crate) domain: IntSetVal, - /// The list of (indexes of) constraints in which the variable appears. - /// - /// This list is used to enqueue the constraints for propagation when the - /// domain of the variable changes. - pub(crate) constraints: Vec, -} - /// Context object used during the reformulation process that creates a /// [`Solver`] object from a [`crate::Model`]. pub(crate) struct ReformulationContext<'a> { @@ -161,6 +161,31 @@ pub struct ReformulationMap { pub(crate) bool_map: Vec, } +impl Constraint for BoolFormula { + fn simplify(&mut self, _: &mut S) -> Result { + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let mut resolver = |bv: BoolDecision| { + let inner = slv.get_solver_bool(bv); + match inner.0 { + BoolViewInner::Const(b) => Err(b), + BoolViewInner::Lit(l) => Ok(l), + } + }; + let result: Result, _> = self.clone().simplify_with(&mut resolver); + match result { + Err(false) => Err(ReformulationError::TrivialUnsatisfiable), + Err(true) => Ok(()), + Ok(f) => { + let mut wrapper = slv.with_conditions(vec![]); + Ok(TseitinEncoder.encode(&mut wrapper, &f)?) + } + } + } +} + impl ConstraintStore { /// Map the constraint into propagators and clauses to be added to the given /// solver, using the variable mapping provided. @@ -171,20 +196,11 @@ impl ConstraintStore { ) -> Result<(), ReformulationError> { let mut actions = ReformulationContext { slv, map }; match self { - ConstraintStore::AllDifferentInt(con) => { - >::to_solver(con, &mut actions) - } - ConstraintStore::ArrayIntElement(con) => { - >::to_solver(con, &mut actions) - } - ConstraintStore::ArrayIntMinimum(con) => { - >::to_solver(con, &mut actions) + ConstraintStore::BoolDecisionArrayElement(con) => { + >::to_solver(con, &mut actions) } - ConstraintStore::ArrayVarBoolElement(con) => { - >::to_solver(con, &mut actions) - } - ConstraintStore::ArrayVarIntElement(con) => { - >::to_solver(con, &mut actions) + ConstraintStore::BoolFormula(exp) => { + as Constraint>::to_solver(exp, &mut actions) } ConstraintStore::DisjunctiveStrict(con) => { >::to_solver(con, &mut actions) @@ -192,28 +208,37 @@ impl ConstraintStore { ConstraintStore::IntAbs(con) => { >::to_solver(con, &mut actions) } + ConstraintStore::IntAllDifferent(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntArrayMinimum(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntDecisionArrayElement(con) => { + >::to_solver(con, &mut actions) + } ConstraintStore::IntDiv(con) => { >::to_solver(con, &mut actions) } + ConstraintStore::IntInSetReif(con) => { + >::to_solver(con, &mut actions) + } ConstraintStore::IntLinear(con) => { >::to_solver(con, &mut actions) } ConstraintStore::IntPow(con) => { >::to_solver(con, &mut actions) } + ConstraintStore::IntTable(con) => { + >::to_solver(con, &mut actions) + } ConstraintStore::IntTimes(con) => { >::to_solver(con, &mut actions) } - ConstraintStore::PropLogic(exp) => { - as Constraint>::to_solver(exp, &mut actions) - } - ConstraintStore::SetInReif(con) => { - >::to_solver(con, &mut actions) + ConstraintStore::IntValArrayElement(con) => { + >::to_solver(con, &mut actions) } - ConstraintStore::TableInt(con) => { - >::to_solver(con, &mut actions) - } - ConstraintStore::UserCustom(con) => con.to_solver(&mut actions), + ConstraintStore::Other(con) => con.to_solver(&mut actions), } } } @@ -270,31 +295,6 @@ impl IntDecisionDef { } } -impl Constraint for LogicFormula { - fn simplify(&mut self, _: &mut S) -> Result { - Ok(SimplificationStatus::Fixpoint) - } - - fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { - let mut resolver = |bv: BoolDecision| { - let inner = slv.get_solver_bool(bv); - match inner.0 { - BoolViewInner::Const(b) => Err(b), - BoolViewInner::Lit(l) => Ok(l), - } - }; - let result: Result, _> = self.clone().simplify_with(&mut resolver); - match result { - Err(false) => Err(ReformulationError::TrivialUnsatisfiable), - Err(true) => Ok(()), - Ok(f) => { - let mut wrapper = slv.with_conditions(vec![]); - Ok(TseitinEncoder.encode(&mut wrapper, &f)?) - } - } - } -} - impl ClauseDatabase for ReformulationContext<'_> { delegate! { to self.slv { @@ -430,3 +430,8 @@ impl ReformulationMap { } } } + +define_index_type! { + /// Reference type for integer decision variables in a [`Model`]. + pub(crate) struct IntDecisionIndex = u32; +} diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index 7f72734..321003e 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -221,6 +221,15 @@ impl AssumptionChecker for A { } } +impl From for BoolVal { + fn from(val: BoolView) -> Self { + match val.0 { + BoolViewInner::Lit(l) => l.into(), + BoolViewInner::Const(b) => b.into(), + } + } +} + impl BoolView { /// Return an integers that can used to identify the literal, if there is one. pub fn reverse_map_info(&self) -> Option { @@ -237,15 +246,6 @@ impl From for BoolView { } } -impl From for BoolVal { - fn from(val: BoolView) -> Self { - match val.0 { - BoolViewInner::Lit(l) => l.into(), - BoolViewInner::Const(b) => b.into(), - } - } -} - impl Not for BoolView { type Output = Self; @@ -700,6 +700,16 @@ impl> Solver { } } + /// Access the inner [`Engine`] object. + pub(crate) fn engine(&self) -> &Engine { + self.oracle.propagator() + } + + /// Mutably access the inner [`Engine`] object. + pub(crate) fn engine_mut(&mut self) -> &mut Engine { + self.oracle.propagator_mut() + } + /// Create a new [`Solver`] instance from a [`FlatZinc`] instance. pub fn from_fzn>( fzn: &FlatZinc, @@ -719,16 +729,6 @@ impl> Solver { Ok((slv, map, fzn_stats)) } - /// Access the inner [`Engine`] object. - pub(crate) fn engine(&self) -> &Engine { - self.oracle.propagator() - } - - /// Mutably access the inner [`Engine`] object. - pub(crate) fn engine_mut(&mut self) -> &mut Engine { - self.oracle.propagator_mut() - } - /// Wrapper function for `all_solutions` that collects all solutions and returns them in a vector /// of solution values. /// @@ -884,6 +884,15 @@ impl ClauseDatabase for Solver { } } +impl> Debug for Solver { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + f.debug_struct("Solver") + .field("oracle", &self.oracle) + .field("engine", self.engine()) + .finish() + } +} + impl> DecisionActions for Solver { fn get_intref_lit(&mut self, iv: IntVarRef, meaning: IntLitMeaning) -> BoolView { let mut clauses = Vec::new(); @@ -977,10 +986,6 @@ impl> PropagatorInitActions for Solver p } - fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt { - self.engine_mut().state.trail.track_int(init) - } - fn enqueue_now(&mut self, prop: PropRef) { let state = &mut self.engine_mut().state; if !state.enqueued[prop] { @@ -1029,6 +1034,10 @@ impl> PropagatorInitActions for Solver }; self.engine_mut().state.int_activation[var].add(prop, cond); } + + fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt { + self.engine_mut().state.trail.track_int(init) + } } impl> TrailingActions for Solver { @@ -1043,15 +1052,6 @@ impl> TrailingActions for Solver { } } -impl> Debug for Solver { - fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - f.debug_struct("Solver") - .field("oracle", &self.oracle) - .field("engine", self.engine()) - .finish() - } -} - impl Value { /// If the `Value` is a Boolean, represent it as bool. Returns None otherwise. pub fn as_bool(&self) -> Option { diff --git a/crates/huub/src/solver/solving_context.rs b/crates/huub/src/solver/solving_context.rs index 4125218..7a6719e 100644 --- a/crates/huub/src/solver/solving_context.rs +++ b/crates/huub/src/solver/solving_context.rs @@ -2,7 +2,7 @@ //! during the progation and solution checking process. This structure contains //! the implementation of the actions that are exposed to the propagators. -use std::fmt::{self, Formatter}; +use std::fmt::{self, Debug, Formatter}; use delegate::delegate; use index_vec::IndexVec; @@ -161,7 +161,7 @@ impl<'a> SolvingContext<'a> { } } -impl fmt::Debug for SolvingContext<'_> { +impl Debug for SolvingContext<'_> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { f.debug_struct("SolvingContext") .field("state", &self.state)