1use kernel::*;
16use trilean::SKleene;
17use trilean::SKleene::*;
18use model::*;
19use logic::*;
20use propagators::{x_geq_y_plus_z};
21use propagation::*;
22use propagation::events::*;
23use gcollections::ops::*;
24use gcollections::*;
25use num::traits::Num;
26use concept::*;
27
28#[derive(Debug)]
29pub struct XLessYPlusZ<VStore>
30{
31 x: Var<VStore>,
32 y: Var<VStore>,
33 z: Var<VStore>,
34}
35
36impl<VStore> XLessYPlusZ<VStore> {
37 pub fn new(x: Var<VStore>, y: Var<VStore>, z: Var<VStore>) -> Self {
38 XLessYPlusZ { x: x, y: y, z: z }
39 }
40}
41
42impl<VStore> Clone for XLessYPlusZ<VStore> where
43 VStore: Collection
44{
45 fn clone(&self) -> Self {
46 XLessYPlusZ::new(self.x.bclone(), self.y.bclone(), self.z.bclone())
47 }
48}
49
50impl<VStore> DisplayStateful<Model> for XLessYPlusZ<VStore>
51{
52 fn display(&self, model: &Model) {
53 self.x.display(model);
54 print!(" < ");
55 self.y.display(model);
56 print!(" + ");
57 self.z.display(model);
58 }
59}
60
61impl<VStore, Domain, Bound> NotFormula<VStore> for XLessYPlusZ<VStore> where
62 VStore: VStoreConcept<Item=Domain> + 'static,
63 Domain: Collection<Item=Bound> + IntDomain,
64 Bound: IntBound
65{
66 fn not(&self) -> Formula<VStore> {
67 Box::new(x_geq_y_plus_z(self.x.bclone(), self.y.bclone(), self.z.bclone()))
68 }
69}
70
71impl<VStore, Dom, Bound> Subsumption<VStore> for XLessYPlusZ<VStore> where
72 VStore: Collection<Item=Dom>,
73 Dom: Bounded<Item=Bound>,
74 Bound: PartialOrd + Num
75{
76 fn is_subsumed(&self, store: &VStore) -> SKleene {
77 let x = self.x.read(store);
81 let y = self.y.read(store);
82 let z = self.z.read(store);
83
84 if x.lower() >= y.upper() + z.upper() {
85 False
86 }
87 else if x.upper() < y.lower() + z.lower() {
88 True
89 }
90 else {
91 Unknown
92 }
93 }
94}
95
96impl<VStore, Dom, Bound> Propagator<VStore> for XLessYPlusZ<VStore> where
97 VStore: Collection<Item=Dom>,
98 Dom: Bounded<Item=Bound> + StrictShrinkRight + StrictShrinkLeft,
99 Bound: PartialOrd + Num
100{
101 fn propagate(&mut self, store: &mut VStore) -> bool {
102 let x = self.x.read(store);
103 let y = self.y.read(store);
104 let z = self.z.read(store);
105
106 self.x.update(store, x.strict_shrink_right(y.upper() + z.upper())) &&
107 self.y.update(store, y.strict_shrink_left(x.lower() - z.upper())) &&
108 self.z.update(store, z.strict_shrink_left(x.lower() - y.upper()))
109 }
110}
111
112impl<VStore> PropagatorDependencies<FDEvent> for XLessYPlusZ<VStore>
113{
114 fn dependencies(&self) -> Vec<(usize, FDEvent)> {
115 let mut deps = self.x.dependencies(FDEvent::Bound);
116 deps.append(&mut self.y.dependencies(FDEvent::Bound));
117 deps.append(&mut self.z.dependencies(FDEvent::Bound));
118 deps
119 }
120}
121
122#[cfg(test)]
123mod test {
124 use super::*;
125 use propagation::events::FDEvent::*;
126 use interval::interval::*;
127 use propagators::test::*;
128
129 #[test]
130 fn x_less_y_test() {
131 let dom0_10 = (0,10).to_interval();
132 let dom10_20 = (10,20).to_interval();
133 let dom11_12 = (11,12).to_interval();
134 let dom0_6 = (0,6).to_interval();
135 let dom0_5 = (0,5).to_interval();
136 let dom0_1 = (0,1).to_interval();
137 let dom1_1 = (1,1).to_interval();
138 let dom2_2 = (2,2).to_interval();
139
140 x_less_y_plus_z_test_one(1, dom0_10, dom0_10, dom0_10, Unknown, Unknown, vec![], true);
141 x_less_y_plus_z_test_one(2, dom11_12, dom0_6, dom0_6, Unknown, True, vec![(0, Assignment), (1, Assignment), (2, Assignment)], true);
142 x_less_y_plus_z_test_one(3, dom10_20, dom1_1, dom1_1, False, False, vec![], false);
143 x_less_y_plus_z_test_one(4, dom2_2, dom1_1, dom1_1, False, False, vec![], false);
144 x_less_y_plus_z_test_one(5, dom1_1, dom2_2, dom2_2, True, True, vec![], true);
145 x_less_y_plus_z_test_one(6, dom0_6, dom0_5, dom0_1, Unknown, Unknown, vec![(0, Bound)], true);
146 }
147
148 fn x_less_y_plus_z_test_one(test_num: u32,
149 x: Interval<i32>, y: Interval<i32>, z: Interval<i32>,
150 before: SKleene, after: SKleene,
151 delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
152 {
153 trinary_propagator_test(test_num, XLessYPlusZ::new, x, y, z, before, after, delta_expected, propagate_success);
154 }
155}