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

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

use std::ops::Not;

use pindakaas::Lit as RawLit;

use crate::{
	actions::BoolInspectionActions,
	solver::{
		Solver,
		decision::{Decision, DecisionReference, private},
		engine::State,
		trail::Trail,
	},
};

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

impl<Sat> BoolInspectionActions<Solver<Sat>> for Decision<bool> {
	fn val(&self, ctx: &Solver<Sat>) -> Option<bool> {
		self.val(&ctx.engine.borrow().state)
	}
}

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

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

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 {}