pcp/propagators/cmp/
x_less_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_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    // False: min(X) >= max(Y) + max(Z)
78    // True: max(X) < min(Y) + min(Z)
79    // Unknown: Everything else.
80    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}