1use 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}