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

//! Module containing structures for tracking the relationships between Boolean
//! variables and integer variables.

use pindakaas::{Var as RawVar, VarRange};
use rustc_hash::FxHashMap;

use crate::{
	IntVal,
	solver::{IntLitMeaning, decision::Decision},
};

/// A mapping of Boolean variables to integer variables of which they represent
/// conditions.
#[derive(Clone, Debug, Default, Eq, PartialEq)]
pub(crate) struct BoolToIntMap {
	/// The mapping of eagerly created Boolean variables to the integer
	/// variables.
	eager: Vec<(VarRange, Decision<IntVal>)>,
	/// The mapping of lazily created Boolean variables to the integer variables
	/// and their meanings.
	lazy: FxHashMap<RawVar, (Decision<IntVal>, IntLitMeaning)>,
}

impl BoolToIntMap {
	/// Return the integer variable the given Boolean variable represents a
	/// condition for, if any. If the Boolean variable was lazily created, then
	/// also return the [`LitMeaning`] of the literal.
	pub(crate) fn get(&self, var: RawVar) -> Option<(Decision<IntVal>, Option<IntLitMeaning>)> {
		let is_eager = self
			.eager
			.last()
			.map(|(last, _)| var <= last.end())
			.unwrap_or(false);
		if is_eager {
			self.eager
				.binary_search_by(|(range, _)| {
					if range.start() > var {
						std::cmp::Ordering::Greater
					} else if range.end() < var {
						std::cmp::Ordering::Less
					} else {
						std::cmp::Ordering::Equal
					}
				})
				.ok()
				.map(|i| (self.eager[i].1, None))
		} else {
			self.lazy
				.get(&var)
				.map(|(int_var, meaning)| (*int_var, Some(*meaning)))
		}
	}
	/// Insert a range of Boolean variables to map them to the integer variable
	/// for which they are eagerly created to represent conditions for.
	pub(crate) fn insert_eager(&mut self, range: VarRange, var: Decision<IntVal>) {
		if range.is_empty() {
			return;
		}
		if self.eager.is_empty() || self.eager.last().unwrap().0.end() < range.start() {
			self.eager.push((range, var));
			return;
		}
		panic!("Literal Mapping not added in the correct order")
	}

	/// Insert a mapping of a lazily created Boolean variable to the integer
	/// variable and the meaning of the literal on the integer variable.
	pub(crate) fn insert_lazy(&mut self, var: RawVar, iv: Decision<IntVal>, lit: IntLitMeaning) {
		let x = self.lazy.insert(var, (iv, lit));
		debug_assert_eq!(x, None, "lazy literal already exists");
	}
}