pcp/propagators/
distinct.rs

1// Copyright 2015 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::x_neq_y::*;
20use propagation::events::*;
21use propagation::*;
22use gcollections::*;
23use concept::*;
24
25/// Precondition: `vars.len() > 1`.
26pub fn join_distinct<VStore, CStore, Domain, Bound>(
27  _vstore: &mut VStore, cstore: &mut CStore, vars: Vec<Var<VStore>>) where
28 VStore: VStoreConcept<Item=Domain> + 'static,
29 Domain: IntDomain<Item=Bound> + 'static,
30 Bound: IntBound + 'static,
31 CStore: IntCStore<VStore> + 'static
32{
33  assert!(vars.len() > 0,
34    "Variable array in `Distinct` must be non-empty.");
35  for i in 0..vars.len()-1 {
36    for j in i+1..vars.len() {
37      cstore.alloc(Box::new(XNeqY::new(vars[i].bclone(), vars[j].bclone())));
38    }
39  }
40}
41
42#[derive(Debug)]
43pub struct Distinct<VStore>
44{
45  conj: Conjunction<VStore>,
46  vars: Vec<Var<VStore>>
47}
48
49impl<VStore> NotFormula<VStore> for Distinct<VStore> where
50 VStore: Collection + 'static
51{
52  fn not(&self) -> Formula<VStore> {
53    self.conj.not()
54  }
55}
56
57impl<VStore, Domain, Bound> Distinct<VStore> where
58  VStore: VStoreConcept<Item=Domain> + 'static,
59  Domain: IntDomain<Item=Bound> + 'static,
60  Bound: IntBound + 'static,
61{
62  /// Precondition: `vars.len() > 1`.
63  pub fn new(vars: Vec<Var<VStore>>) -> Self {
64    assert!(vars.len() > 0,
65      "Variable array in `Distinct` must be non-empty.");
66    let mut props = vec![];
67    for i in 0..vars.len()-1 {
68      for j in i+1..vars.len() {
69        let i_neq_j = Box::new(XNeqY::new(vars[i].bclone(), vars[j].bclone())) as Formula<VStore>;
70        props.push(i_neq_j);
71      }
72    }
73    Distinct {
74      conj: Conjunction::new(props),
75      vars: vars
76    }
77  }
78}
79
80impl<VStore> Clone for Distinct<VStore> where
81 VStore: Collection
82{
83  fn clone(&self) -> Self {
84    Distinct {
85      conj: self.conj.clone(),
86      vars: self.vars.iter().map(|v| v.bclone()).collect()
87    }
88  }
89}
90
91impl<VStore> DisplayStateful<Model> for Distinct<VStore>
92{
93  fn display(&self, model: &Model) {
94    model.display_global("distinct", &self.vars);
95  }
96}
97
98impl<VStore> Subsumption<VStore> for Distinct<VStore>
99{
100  fn is_subsumed(&self, vstore: &VStore) -> SKleene {
101    self.conj.is_subsumed(vstore)
102  }
103}
104
105impl<VStore> Propagator<VStore> for Distinct<VStore>
106{
107  fn propagate(&mut self, vstore: &mut VStore) -> bool {
108    self.conj.propagate(vstore)
109  }
110}
111
112impl<VStore> PropagatorDependencies<FDEvent> for Distinct<VStore>
113{
114  fn dependencies(&self) -> Vec<(usize, FDEvent)> {
115    self.vars.iter().flat_map(|v| v.dependencies(FDEvent::Inner)).collect()
116  }
117}
118
119#[cfg(test)]
120mod test {
121  use super::*;
122  use trilean::SKleene::*;
123  use propagation::events::FDEvent::*;
124  use interval::interval::*;
125  use propagators::test::*;
126
127  #[test]
128  fn distinct_test() {
129    let zero = (0,0).to_interval();
130    let one = (1,1).to_interval();
131    let two = (2,2).to_interval();
132    let dom0_1 = (0,1).to_interval();
133    let dom0_2 = (0,2).to_interval();
134    let dom0_3 = (0,3).to_interval();
135
136    distinct_test_one(1, vec![zero,one,two], True, True, vec![], true);
137    distinct_test_one(2, vec![zero,zero,two], False, False, vec![], false);
138    distinct_test_one(3, vec![zero,one,dom0_3], Unknown, True, vec![(2, Bound)], true);
139    distinct_test_one(4, vec![zero,one,dom0_2], Unknown, True, vec![(2, Assignment)], true);
140    distinct_test_one(5, vec![zero,one,dom0_1], Unknown, False, vec![], false);
141    distinct_test_one(6, vec![zero,dom0_3,dom0_3], Unknown, Unknown, vec![(1, Bound),(2, Bound)], true);
142    distinct_test_one(7, vec![dom0_3], True, True, vec![], true);
143  }
144
145  fn distinct_test_one(test_num: u32, doms: Vec<Interval<i32>>,
146    before: SKleene, after: SKleene,
147    delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
148  {
149    nary_propagator_test(test_num, Distinct::new, doms, before, after, delta_expected, propagate_success);
150  }
151}