pcp/logic/
disjunction.rs

1// Copyright 2017 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 trilean::SKleene;
16use kernel::*;
17use model::*;
18use logic::{NotFormula, Conjunction};
19use propagation::events::*;
20use propagation::*;
21use gcollections::kind::*;
22use std::fmt::{Debug, Formatter, Result};
23use concept::*;
24
25pub struct Disjunction<VStore> {
26  fs: Vec<Formula<VStore>>
27}
28
29impl<VStore> Disjunction<VStore>
30{
31  pub fn new(fs: Vec<Formula<VStore>>) -> Self {
32    Disjunction {
33      fs: fs
34    }
35  }
36}
37
38impl<VStore> Debug for Disjunction<VStore>
39{
40  fn fmt(&self, fmt: &mut Formatter) -> Result {
41    fmt.debug_struct("Disjunction")
42      .field("fs", &self.fs)
43      .finish()
44  }
45}
46
47impl<VStore> Clone for Disjunction<VStore> where
48 VStore: Collection
49{
50  fn clone(&self) -> Self {
51    Disjunction {
52      fs: self.fs.iter().map(|f| f.bclone()).collect()
53    }
54  }
55}
56
57impl<VStore> DisplayStateful<Model> for Disjunction<VStore>
58{
59  fn display(&self, model: &Model) {
60    let mut i = 0;
61    while i < self.fs.len() - 1 {
62      self.fs[i].display(model);
63      print!(" \\/ ");
64      i += 1;
65    }
66    self.fs[i].display(model);
67  }
68}
69
70impl<VStore> NotFormula<VStore> for Disjunction<VStore> where
71 VStore: Collection + 'static
72{
73  /// Apply De Morgan's laws.
74  fn not(&self) -> Formula<VStore> {
75    let fs = self.fs.iter().map(|f| f.not()).collect();
76    Box::new(Conjunction::new(fs))
77  }
78}
79
80impl<VStore> Subsumption<VStore> for Disjunction<VStore>
81{
82  fn is_subsumed(&self, vstore: &VStore) -> SKleene {
83    use trilean::SKleene::*;
84    let mut all_disentailed = true;
85    for f in &self.fs {
86      match f.is_subsumed(vstore) {
87        True => return True,
88        Unknown => all_disentailed = false,
89        _ => ()
90      }
91    }
92    if all_disentailed { False }
93    else { Unknown }
94  }
95}
96
97impl<VStore> Propagator<VStore> for Disjunction<VStore>
98{
99  fn propagate(&mut self, vstore: &mut VStore) -> bool {
100    use trilean::SKleene::*;
101    let mut num_disentailed = 0;
102    let mut unknown_formula = 0;
103    for (i, f) in self.fs.iter().enumerate() {
104      match f.is_subsumed(vstore) {
105        True => return true,
106        False => num_disentailed += 1,
107        Unknown => unknown_formula = i
108      }
109    }
110    if num_disentailed == self.fs.len() - 1 {
111      self.fs[unknown_formula].propagate(vstore)
112    }
113    else if num_disentailed == self.fs.len() {
114      false
115    }
116    else { true }
117  }
118}
119
120impl<VStore> PropagatorDependencies<FDEvent> for Disjunction<VStore>
121{
122  fn dependencies(&self) -> Vec<(usize, FDEvent)> {
123    let mut deps: Vec<_> = self.fs.iter()
124      .map(|f| f.dependencies())
125      .flat_map(|deps| deps.into_iter())
126      .collect();
127    deps.sort();
128    deps.dedup();
129    deps
130  }
131}
pcp/logic/disjunction.rs

pcp/logic/
disjunction.rs
