1use kernel::*;
16use trilean::SKleene;
17use trilean::SKleene::*;
18use model::*;
19use logic::*;
20use propagators::{x_leq_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 XGreaterYPlusZ<VStore>
30{
31 pub x: Var<VStore>,
32 pub y: Var<VStore>,
33 pub z: Var<VStore>,
34}
35
36impl<VStore> XGreaterYPlusZ<VStore> {
37 pub fn new(x: Var<VStore>, y: Var<VStore>, z: Var<VStore>) -> Self {
38 XGreaterYPlusZ { x: x, y: y, z: z }
39 }
40}
41
42impl<VStore> Clone for XGreaterYPlusZ<VStore> where
43 VStore: Collection
44{
45 fn clone(&self) -> Self {
46 XGreaterYPlusZ::new(self.x.bclone(), self.y.bclone(), self.z.bclone())
47 }
48}
49
50impl<VStore> DisplayStateful<Model> for XGreaterYPlusZ<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 XGreaterYPlusZ<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_leq_y_plus_z(self.x.bclone(), self.y.bclone(), self.z.bclone()))
68 }
69}
70
71impl<VStore, Dom, Bound> Subsumption<VStore> for XGreaterYPlusZ<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);
82 let y = self.y.read(store);
83 let z = self.z.read(store);
84
85 if x.upper() <= y.lower() + z.lower() {
86 False
87 }
88 else if x.lower() > y.upper() + z.upper() {
89 True
90 }
91 else {
92 Unknown
93 }
94 }
95}
96
97impl<VStore, Dom, Bound> Propagator<VStore> for XGreaterYPlusZ<VStore> where
98 VStore: Collection<Item=Dom>,
99 Dom: Bounded<Item=Bound> + StrictShrinkRight + StrictShrinkLeft,
100 Bound: PartialOrd + Num
101{
102 fn propagate(&mut self, store: &mut VStore) -> bool {
103 let x = self.x.read(store);
104 let y = self.y.read(store);
105 let z = self.z.read(store);
106 self.x.update(store, x.strict_shrink_left(y.lower() + z.lower())) &&
107 self.y.update(store, y.strict_shrink_right(x.upper() - z.lower())) &&
108 self.z.update(store, z.strict_shrink_right(x.upper() - y.lower()))
109 }
110}
111
112impl<VStore> PropagatorDependencies<FDEvent> for XGreaterYPlusZ<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_greater_y_plus_z_test() {
131 let dom0_10 = (0,10).to_interval();
132 let dom10_20 = (10,20).to_interval();
133 let dom10_11 = (10,11).to_interval();
134 let dom5_15 = (5,15).to_interval();
135 let dom1_10 = (1,10).to_interval();
136 let dom5_10 = (5,10).to_interval();
137 let dom6_10 = (6,10).to_interval();
138 let dom1_1 = (1,1).to_interval();
139 let dom2_2 = (2,2).to_interval();
140
141 x_greater_y_plus_z_test_one(1, dom0_10, dom0_10, dom0_10,
142 Unknown, Unknown, vec![(0, Bound), (1, Bound), (2, Bound)], true);
143 x_greater_y_plus_z_test_one(2, dom10_11, dom5_15, dom5_15,
144 Unknown, True, vec![(0, Assignment), (1, Assignment), (2, Assignment)], true);
145 x_greater_y_plus_z_test_one(3, dom10_20, dom1_1, dom1_1,
146 True, True, vec![], true);
147 x_greater_y_plus_z_test_one(4, dom1_1, dom1_1, dom1_1,
148 False, False, vec![], false);
149 x_greater_y_plus_z_test_one(5, dom2_2, dom1_1, dom1_1,
150 False, False, vec![], false);
151 x_greater_y_plus_z_test_one(6, dom6_10, dom5_10, dom1_10,
152 Unknown, Unknown, vec![(0, Bound), (1, Bound), (2, Bound)], true);
153 }
154
155 fn x_greater_y_plus_z_test_one(test_num: u32,
156 x: Interval<i32>, y: Interval<i32>, z: Interval<i32>,
157 before: SKleene, after: SKleene,
158 delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
159 {
160 trinary_propagator_test(test_num, XGreaterYPlusZ::new, x, y, z, before, after, delta_expected, propagate_success);
161 }
162}