1use kernel::*;
16use trilean::SKleene;
17use model::*;
18use logic::*;
19use propagators::cmp::x_neq_y::*;
20use propagation::events::*;
21use propagation::*;
22use gcollections::*;
23use concept::*;
24
25pub 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 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}