huub 100.0.0

CP+SAT solver framework built to be reliable, performant, and extensible
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154

//! Helper trait that allows the definition of [`Model`] level array element
//! constraints in a more generic way.

use itertools::{Itertools, MinMaxResult};

use crate::{
	IntSet, IntVal,
	actions::IntInspectionActions,
	constraints::{
		Conflict,
		bool_array_element::BoolDecisionArrayElement,
		int_array_element::{IntArrayElementBounds, IntValArrayElement},
		int_set_contains::IntSetContainsReif,
	},
	model::{Model, view::View},
};

/// 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: Clone;

	/// Create a new decision variable that can contain the resulting element of
	/// the element constraint.
	fn define_result(prb: &mut Model, array: &[Self], index: View<IntVal>) -> Self::Result;

	/// Create and post a constraint that enforces that the `result` decision
	/// variables takes the same value as `array[index]`.
	fn element_constraint(
		prb: &mut Model,
		array: Vec<Self>,
		index: View<IntVal>,
		result: Self::Result,
	) -> Result<(), Conflict<View<bool>>>;
}

impl ElementConstraint for IntVal {
	type Constraint = IntValArrayElement<View<IntVal>, View<IntVal>>;
	type Result = View<IntVal>;

	fn define_result(prb: &mut Model, array: &[Self], _: View<IntVal>) -> Self::Result {
		let range = match array.iter().minmax() {
			MinMaxResult::NoElements => IntVal::MIN..=IntVal::MAX,
			MinMaxResult::OneElement(&v) => v..=v,
			MinMaxResult::MinMax(&min, &max) => min..=max,
		};
		prb.new_int_decision(range)
	}

	fn element_constraint(
		prb: &mut Model,
		array: Vec<Self>,
		index: View<IntVal>,
		result: Self::Result,
	) -> Result<(), Conflict<View<bool>>> {
		let con = IntValArrayElement(IntArrayElementBounds::new(prb, array, index, result));
		prb.post_constraint(con)
	}
}

impl ElementConstraint for View<IntVal> {
	type Constraint = IntArrayElementBounds<View<IntVal>, View<IntVal>, View<IntVal>>;
	type Result = View<IntVal>;

	fn define_result(prb: &mut Model, array: &[Self], _: View<IntVal>) -> Self::Result {
		let min = array
			.iter()
			.map(|v| v.min(prb))
			.min()
			.unwrap_or(IntVal::MIN);
		let max = array
			.iter()
			.map(|v| v.max(prb))
			.max()
			.unwrap_or(IntVal::MAX);
		prb.new_int_decision(min..=max)
	}

	fn element_constraint(
		prb: &mut Model,
		array: Vec<Self>,
		index: View<IntVal>,
		result: Self::Result,
	) -> Result<(), Conflict<View<bool>>> {
		let con = IntArrayElementBounds::new(prb, array, index, result);
		prb.post_constraint(con)
	}
}

impl ElementConstraint for View<bool> {
	type Constraint = BoolDecisionArrayElement;
	type Result = View<bool>;

	fn define_result(prb: &mut Model, _: &[Self], _: View<IntVal>) -> Self::Result {
		prb.new_bool_decision()
	}

	fn element_constraint(
		prb: &mut Model,
		array: Vec<Self>,
		index: View<IntVal>,
		result: Self::Result,
	) -> Result<(), Conflict<View<bool>>> {
		prb.post_constraint(Self::Constraint {
			index,
			array,
			result,
		})
	}
}

impl ElementConstraint for bool {
	type Constraint = IntSetContainsReif;
	type Result = View<bool>;

	fn define_result(prb: &mut Model, _: &[Self], _: View<IntVal>) -> Self::Result {
		prb.new_bool_decision()
	}

	fn element_constraint(
		prb: &mut Model,
		array: Vec<Self>,
		index: View<IntVal>,
		result: Self::Result,
	) -> Result<(), Conflict<View<bool>>> {
		// 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 - 1) as IntVal);
					start = None;
				}
				(false, None) | (true, Some(_)) => {}
			}
		}
		if let Some(s) = start {
			ranges.push(s..=array.len() as IntVal);
		}
		assert_ne!(ranges.len(), 0, "unexpected empty range list");

		prb.post_constraint(Self::Constraint {
			var: index,
			set: IntSet::from_iter(ranges),
			reif: result,
		})
	}
}