pcp/propagators/cmp/
x_eq_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 model::*;
18use logic::*;
19use propagators::cmp::{XGreaterEqYPlusZ, XLessEqYPlusZ, x_geq_y_plus_z, x_leq_y_plus_z};
20use propagation::*;
21use propagation::events::*;
22use gcollections::*;
23use concept::*;
24
25#[derive(Clone, Debug)]
26pub struct XEqYPlusZ<VStore: Collection>
27{
28  geq: XGreaterEqYPlusZ<VStore>,
29  leq: XLessEqYPlusZ<VStore>
30}
31
32impl<VStore, Domain, Bound> XEqYPlusZ<VStore> where
33 VStore: VStoreConcept<Item=Domain> + 'static,
34 Domain: Collection<Item=Bound> + IntDomain,
35 Bound: IntBound
36{
37  pub fn new(x: Var<VStore>, y: Var<VStore>, z: Var<VStore>) -> Self {
38    XEqYPlusZ {
39      geq: x_geq_y_plus_z(x.bclone(), y.bclone(), z.bclone()),
40      leq: x_leq_y_plus_z(x, y, z)
41    }
42  }
43}
44
45impl<VStore> DisplayStateful<Model> for XEqYPlusZ<VStore> where
46  VStore: Collection
47{
48  fn display(&self, model: &Model) {
49    self.geq.x.display(model);
50    print!(" = ");
51    self.geq.y.display(model);
52    print!(" + ");
53    self.geq.z.display(model);
54    print!(" (decomposed)");
55  }
56}
57
58impl<VStore> Subsumption<VStore> for XEqYPlusZ<VStore> where
59  VStore: Collection,
60  XGreaterEqYPlusZ<VStore>: Subsumption<VStore>,
61  XLessEqYPlusZ<VStore>: Subsumption<VStore>,
62{
63  fn is_subsumed(&self, store: &VStore) -> SKleene {
64    self.geq.is_subsumed(store).and(self.leq.is_subsumed(store))
65  }
66}
67
68impl<VStore> NotFormula<VStore> for XEqYPlusZ<VStore> where
69  VStore: Collection
70{
71  fn not(&self) -> Formula<VStore> {
72    unimplemented!()
73  }
74}
75
76impl<VStore> Propagator<VStore> for XEqYPlusZ<VStore> where
77  VStore: Collection,
78  XGreaterEqYPlusZ<VStore>: Propagator<VStore>,
79  XLessEqYPlusZ<VStore>: Propagator<VStore>
80{
81  fn propagate(&mut self, store: &mut VStore) -> bool {
82    self.geq.propagate(store) &&
83    self.leq.propagate(store)
84  }
85}
86
87impl<VStore> PropagatorDependencies<FDEvent> for XEqYPlusZ<VStore> where
88  VStore: Collection,
89  XGreaterEqYPlusZ<VStore>: PropagatorDependencies<FDEvent>,
90  XLessEqYPlusZ<VStore>: PropagatorDependencies<FDEvent>
91{
92  fn dependencies(&self) -> Vec<(usize, FDEvent)> {
93    let geq_deps = self.geq.dependencies();
94    let leq_deps = self.leq.dependencies();
95    assert_eq!(geq_deps, leq_deps,
96      "This function assumed both dependencies of X >= Y + Z and X <= Y + Z are equals.");
97    geq_deps
98  }
99}
100
101#[cfg(test)]
102mod test {
103  use super::*;
104  use trilean::SKleene::*;
105  use propagation::events::FDEvent::*;
106  use interval::interval::*;
107  use propagators::test::*;
108
109  #[test]
110  fn x_eq_y_plus_z_test() {
111    let dom0_10 = (0,10).to_interval();
112    let dom10_20 = (10,20).to_interval();
113    let dom12_12 = (12,12).to_interval();
114    let dom0_6 = (0,6).to_interval();
115    let dom0_5 = (0,5).to_interval();
116    let dom0_1 = (0,1).to_interval();
117    let dom1_1 = (1,1).to_interval();
118    let dom2_2 = (2,2).to_interval();
119
120    x_eq_y_plus_z_test_one(1, dom0_10, dom0_10, dom0_10, Unknown, Unknown, vec![], true);
121    x_eq_y_plus_z_test_one(2, dom12_12, dom0_6, dom0_6, Unknown, True, vec![(1, Assignment), (2, Assignment)], true);
122    x_eq_y_plus_z_test_one(3, dom10_20, dom1_1, dom1_1, False, False, vec![], false);
123    x_eq_y_plus_z_test_one(4, dom2_2, dom1_1, dom1_1, True, True, vec![], true);
124    x_eq_y_plus_z_test_one(5, dom1_1, dom2_2, dom2_2, False, False, vec![], false);
125    x_eq_y_plus_z_test_one(6, dom0_6, dom0_5, dom0_1, Unknown, Unknown, vec![], true);
126  }
127
128  fn x_eq_y_plus_z_test_one(test_num: u32,
129    x: Interval<i32>, y: Interval<i32>, z: Interval<i32>,
130    before: SKleene, after: SKleene,
131    delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
132  {
133    trinary_propagator_test(test_num, XEqYPlusZ::new, x, y, z, before, after, delta_expected, propagate_success);
134  }
135}