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

//! 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.

use std::iter::once;

use crate::{
	IntVal,
	actions::{
		BoolInitActions, BoolSimplificationActions, IntDecisionActions, IntInitActions,
		IntInspectionActions, IntPropCond, IntPropagationActions, ReasoningEngine,
	},
	constraints::{
		BoolModelActions, Constraint, IntModelActions, Propagator, SimplificationStatus,
	},
	lower::{LoweringContext, LoweringError},
	model::view::View,
	solver::IntLitMeaning,
};

/// 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 variables at
/// the index given by the index integer decision variable.
#[derive(Clone, Debug, Eq, Hash, PartialEq)]
pub struct BoolDecisionArrayElement {
	/// The array of Boolean decision variables
	pub(crate) array: Vec<View<bool>>,
	/// The index variable
	pub(crate) index: View<IntVal>,
	/// The resulting variable
	pub(crate) result: View<bool>,
}

impl<E> Constraint<E> for BoolDecisionArrayElement
where
	E: ReasoningEngine,
	View<IntVal>: IntModelActions<E>,
	View<bool>: BoolModelActions<E>,
{
	fn simplify(
		&mut self,
		ctx: &mut E::PropagationContext<'_>,
	) -> Result<SimplificationStatus, E::Conflict> {
		Self::propagate(self, ctx)?;
		// Unify if the index is already fixed
		if let Some(i) = self.index.val(ctx) {
			self.array[i as usize].unify(ctx, self.result)?;
			return Ok(SimplificationStatus::Subsumed);
		}
		Ok(SimplificationStatus::NoFixpoint)
	}

	fn to_solver(&self, slv: &mut LoweringContext<'_>) -> Result<(), LoweringError> {
		let result = slv.solver_view(self.result);
		let index = slv.solver_view(self.index);

		// Evaluate result literal
		let arr: Vec<_> = self.array.iter().map(|&v| slv.solver_view(v)).collect();

		for (i, &l) in arr.iter().enumerate() {
			// Evaluate array literal
			let idx_eq = index.lit(slv, IntLitMeaning::Eq(i as IntVal));
			// add clause (idx = i + 1 /\ arr[i]) => val
			slv.add_clause([!idx_eq, !l, result])?;
			// add clause (idx = i + 1 /\ !arr[i]) => !val
			slv.add_clause([!idx_eq, l, !result])?;
		}

		// add clause (arr[1] /\ arr[2] /\ ... /\ arr[n]) => val
		slv.add_clause(arr.iter().map(|&l| !l).chain(once(result)))?;
		// add clause (!arr[1] /\ !arr[2] /\ ... /\ !arr[n]) => !val
		slv.add_clause(arr.into_iter().chain(once(!result)))?;
		Ok(())
	}
}

impl<E> Propagator<E> for BoolDecisionArrayElement
where
	E: ReasoningEngine,
	View<IntVal>: IntModelActions<E>,
	View<bool>: BoolModelActions<E>,
{
	fn initialize(&mut self, ctx: &mut E::InitializationContext<'_>) {
		for &b in &self.array {
			b.enqueue_when_fixed(ctx);
		}
		self.index.enqueue_when(ctx, IntPropCond::Fixed);
		self.result.enqueue_when_fixed(ctx);
	}

	fn propagate(&mut self, ctx: &mut E::PropagationContext<'_>) -> Result<(), E::Conflict> {
		// Restrict the index to the bounds of the array.
		self.index.tighten_min(ctx, 0, vec![])?;
		self.index
			.tighten_max(ctx, self.array.len() as IntVal - 1, vec![])?;

		// TODO: Do more propagation
		Ok(())
	}
}