pcp/propagators/cmp/
x_eq_y_mul_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 propagation::*;
21use propagation::events::*;
22use gcollections::ops::*;
23use gcollections::*;
24use std::ops::*;
25use concept::*;
26
27/// TODO see K. Apt Section 6.5.4 for a better implementation.
28
29// x = y * z
30#[derive(Debug)]
31pub struct XEqYMulZ<VStore>
32{
33  x: Var<VStore>,
34  y: Var<VStore>,
35  z: Var<VStore>,
36}
37
38impl<VStore> XEqYMulZ<VStore> {
39  pub fn new(x: Var<VStore>, y: Var<VStore>, z: Var<VStore>) -> Self {
40    XEqYMulZ { x: x, y: y, z: z }
41  }
42}
43
44impl<VStore> Clone for XEqYMulZ<VStore>  where
45 VStore: Collection
46{
47  fn clone(&self) -> Self {
48    XEqYMulZ::new(self.x.bclone(), self.y.bclone(), self.z.bclone())
49  }
50}
51
52impl<VStore> DisplayStateful<Model> for XEqYMulZ<VStore>
53{
54  fn display(&self, model: &Model) {
55    self.x.display(model);
56    print!(" = ");
57    self.y.display(model);
58    print!(" * ");
59    self.z.display(model);
60  }
61}
62
63impl<VStore> NotFormula<VStore> for XEqYMulZ<VStore>
64{
65  fn not(&self) -> Formula<VStore> {
66    unimplemented!();
67  }
68}
69
70impl<VStore, Dom> Subsumption<VStore> for XEqYMulZ<VStore> where
71  VStore: Collection<Item=Dom>,
72  Dom: Bounded + IsSingleton + Mul<Output=Dom> + Overlap
73{
74  fn is_subsumed(&self, store: &VStore) -> SKleene {
75    // False: x and y*z do not overlap.
76    // True: x and y*z are singletons and equal.
77    // Unknown: x and y*z overlap but are not singletons.
78    let x = self.x.read(store);
79    let y = self.y.read(store);
80    let z = self.z.read(store);
81
82    let yz = y * z;
83    if yz.overlap(&x) {
84      if yz.is_singleton() && x.is_singleton() {
85        True
86      }
87      else { Unknown }
88    }
89    else { False }
90  }
91}
92
93impl<VStore, Dom> Propagator<VStore> for XEqYMulZ<VStore> where
94  VStore: Collection<Item=Dom>,
95  Dom: Bounded + Intersection<Output=Dom> + Mul<Output=Dom>
96{
97  fn propagate(&mut self, store: &mut VStore) -> bool {
98    let x = self.x.read(store);
99    let y = self.y.read(store);
100    let z = self.z.read(store);
101    let yz = y * z;
102    self.x.update(store, x.intersection(&yz))
103  }
104}
105
106impl<VStore> PropagatorDependencies<FDEvent> for XEqYMulZ<VStore>
107{
108  fn dependencies(&self) -> Vec<(usize, FDEvent)> {
109    let mut deps = self.x.dependencies(FDEvent::Bound);
110    deps.append(&mut self.y.dependencies(FDEvent::Bound));
111    deps.append(&mut self.z.dependencies(FDEvent::Bound));
112    deps
113  }
114}
115
116#[cfg(test)]
117mod test {
118  use super::*;
119  use propagation::events::FDEvent::*;
120  use interval::interval::*;
121  use propagators::test::*;
122
123  #[test]
124  fn x_eq_y_mul_z_test() {
125    let dom0_10 = (0,10).to_interval();
126    let dom10_20 = (10,20).to_interval();
127    let dom10_11 = (10,11).to_interval();
128    let dom5_15 = (5,15).to_interval();
129    let dom1_1 = (1,1).to_interval();
130    let dom1_2 = (1,2).to_interval();
131
132    x_eq_y_mul_z_test_one(1, dom0_10, dom0_10, dom0_10,
133      Unknown, Unknown, vec![], true);
134    x_eq_y_mul_z_test_one(2, dom10_11, dom5_15, dom5_15,
135      False, False, vec![], false);
136    x_eq_y_mul_z_test_one(3, dom10_20, dom1_1, dom1_1,
137      False, False, vec![], false);
138    x_eq_y_mul_z_test_one(4, dom1_1, dom1_1, dom1_1,
139      True, True, vec![], true);
140    x_eq_y_mul_z_test_one(5, dom1_2, dom1_1, dom1_1,
141      Unknown, True, vec![(0,Assignment)], true);
142  }
143
144  fn x_eq_y_mul_z_test_one(test_num: u32,
145    x: Interval<i32>, y: Interval<i32>, z: Interval<i32>,
146    before: SKleene, after: SKleene,
147    delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
148  {
149    trinary_propagator_test(test_num, XEqYMulZ::new, x, y, z, before, after, delta_expected, propagate_success);
150  }
151}
pcp/propagators/cmp/x_eq_y_mul_z.rs

pcp/propagators/cmp/
x_eq_y_mul_z.rs
