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

//! Boolean decision variable definitions for the model layer.

use std::ops::Not;

use pindakaas::Lit as RawLit;

use crate::{
	actions::{
		BoolInspectionActions, BoolPropagationActions, BoolSimplificationActions, ReasoningContext,
	},
	constraints::ReasonBuilder,
	model::{
		Model,
		decision::{Decision, DecisionReference, private},
		view::View,
	},
	solver::activation_list::ActivationActionS,
};

/// Definition of an Boolean decision variable in a [`Model`].
#[derive(Clone, Debug, Eq, Hash, PartialEq)]
pub(crate) struct BoolDecision {
	/// Whether the Boolean variable has already been assigned a value, or has
	/// been aliased to another variable.
	pub(crate) alias: Option<View<bool>>,
	/// 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<ActivationActionS>,
}

impl Decision<bool> {
	/// Return the index used to access this decision in model storage.
	pub(crate) fn idx(&self) -> usize {
		(i32::from(self.0.var()) - 1) as usize
	}

	/// Return whether this decision represents a negated literal.
	pub(crate) fn is_negated(&self) -> bool {
		self.0.is_negated()
	}

	/// Return the non-negated decision variable for this literal.
	pub(crate) fn var(&self) -> Self {
		Decision(self.0.var().into())
	}
}

impl BoolInspectionActions<Model> for Decision<bool> {
	fn val(&self, ctx: &Model) -> Option<bool> {
		self.resolve_alias(ctx).val(ctx)
	}
}

impl BoolPropagationActions<Model> for Decision<bool> {
	fn fix(
		&self,
		ctx: &mut Model,
		val: bool,
		reason: impl ReasonBuilder<Model>,
	) -> Result<(), <Model as ReasoningContext>::Conflict> {
		self.resolve_alias(ctx).fix(ctx, val, reason)
	}
}

impl BoolSimplificationActions<Model> for Decision<bool> {
	fn unify(
		&self,
		ctx: &mut Model,
		other: impl Into<View<bool>>,
	) -> Result<(), <Model as ReasoningContext>::Conflict> {
		let other = other.into().resolve_alias(ctx);
		self.resolve_alias(ctx).unify(ctx, other)
	}
}

impl Not for Decision<bool> {
	type Output = Self;

	fn not(self) -> Self::Output {
		Decision(!self.0)
	}
}

impl DecisionReference for bool {
	type Ref = RawLit;
}
impl private::Sealed for bool {}