pcp/propagators/cmp/
x_greater_y_plus_z.rs

1// Copyright 2016 Pierre Talbot (IRCAM)
2
3// Licensed under the Apache License, Version 2.0 (the "License");
4// you may not use this file except in compliance with the License.
5// You may obtain a copy of the License at
6
7//     http://www.apache.org/licenses/LICENSE-2.0
8
9// Unless required by applicable law or agreed to in writing, software
10// distributed under the License is distributed on an "AS IS" BASIS,
11// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12// See the License for the specific language governing permissions and
13// limitations under the License.
14
15use 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    // False: max(X) <= min(Y) + min(Z)
78    // True: min(X) > max(Y) + max(Z)
79    // Unknown: Everything else.
80
81    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}