1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
use std::{collections::BTreeMap, io::Read, fs::File, path::Path, error::Error};
use crate::{
ContextHandle, Port, NodeID, PortID, LinkID, Polynomial,
spec::{CESSpec, spec_from_str},
node, sat,
};
/// A single c-e structure.
///
/// Internally, instances of this type own structural information (the
/// cause and effect polynomials), semantic properties (node
/// capacities for the carrier), the specification from which a c-e
/// structure originated (optionally), and some auxiliary recomputable
/// data. Other properties are available indirectly: `CES` instance
/// owns a [`ContextHandle`] which resolves to a shared [`Context`]
/// object.
///
/// [`Context`]: crate::Context
#[derive(Debug)]
pub struct CES {
context: ContextHandle,
spec: Option<Box<dyn CESSpec>>,
causes: BTreeMap<PortID, Polynomial<LinkID>>,
effects: BTreeMap<PortID, Polynomial<LinkID>>,
links: BTreeMap<LinkID, Option<node::Face>>,
carrier: BTreeMap<NodeID, node::Capacity>,
num_broken_links: u32,
}
impl CES {
/// Creates an empty c-e structure in a [`Context`] given by a
/// [`ContextHandle`].
///
/// [`Context`]: crate::Context
pub fn new(ctx: ContextHandle) -> Self {
Self {
context: ctx,
spec: Default::default(),
causes: Default::default(),
effects: Default::default(),
links: Default::default(),
carrier: Default::default(),
num_broken_links: 0,
}
}
fn add_cause_polynomial(&mut self, port_id: PortID, poly: Polynomial<LinkID>) {
for &lid in poly.get_atomics() {
if let Some(what_missing) = self.links.get_mut(&lid) {
if *what_missing == Some(node::Face::Rx) {
// Link occurs in causes and effects:
// nothing misses, link not broken.
*what_missing = None;
self.num_broken_links -= 1;
} else {
// Link reoccurrence in causes.
}
} else {
// Link occurs in causes, but its occurence
// in effects is missing: link is broken.
self.links.insert(lid, Some(node::Face::Tx));
self.num_broken_links += 1;
}
}
// FIXME add to old if any
self.causes.insert(port_id, poly);
}
fn add_effect_polynomial(&mut self, port_id: PortID, poly: Polynomial<LinkID>) {
for &lid in poly.get_atomics() {
if let Some(what_missing) = self.links.get_mut(&lid) {
if *what_missing == Some(node::Face::Tx) {
// Link occurs in causes and effects:
// nothing misses, link not broken.
*what_missing = None;
self.num_broken_links -= 1;
} else {
// Link reoccurrence in effects.
}
} else {
// Link occurs in effects, but its occurence
// in causes is missing: link is broken.
self.links.insert(lid, Some(node::Face::Rx));
self.num_broken_links += 1;
}
}
// FIXME add to old if any
self.effects.insert(port_id, poly);
}
/// Adds a [`Polynomial`] to this `CES` at a given `face` (cause
/// or effect) of a node.
///
/// The polynomial `poly` is added to another polynomial which is
/// already, explicitly or implicitly (as the default _θ_),
/// attached to a `node_id` at a given `face`.
pub fn add_polynomial(&mut self, node_id: NodeID, face: node::Face, poly: Polynomial<LinkID>) {
let mut port = Port::new(face, node_id);
let pid = self.context.lock().unwrap().share_port(&mut port);
match face {
node::Face::Rx => self.add_cause_polynomial(pid, poly),
node::Face::Tx => self.add_effect_polynomial(pid, poly),
}
self.carrier.entry(node_id).or_insert_with(Default::default);
}
/// Creates a new c-e structure from a specification string and in
/// a [`Context`] given by a [`ContextHandle`].
///
/// [`Context`]: crate::Context
pub fn from_str<S: AsRef<str>>(
ctx: ContextHandle,
raw_spec: S,
) -> Result<Self, Box<dyn Error>> {
let spec = spec_from_str(&ctx, raw_spec)?;
let mut ces = CES::new(ctx);
for id in spec.get_carrier_ids() {
let node_id = NodeID(id);
if let Some(ref spec_poly) = spec.get_causes_by_id(id) {
let mut port = Port::new(node::Face::Rx, node_id);
let pid = ces.context.lock().unwrap().share_port(&mut port);
let poly = Polynomial::from_spec(ces.context.clone(), &port, spec_poly);
ces.add_cause_polynomial(pid, poly);
ces.carrier.entry(node_id).or_insert_with(Default::default);
}
if let Some(ref spec_poly) = spec.get_effects_by_id(id) {
let mut port = Port::new(node::Face::Tx, node_id);
let pid = ces.context.lock().unwrap().share_port(&mut port);
let poly = Polynomial::from_spec(ces.context.clone(), &port, spec_poly);
ces.add_effect_polynomial(pid, poly);
ces.carrier.entry(node_id).or_insert_with(Default::default);
}
}
ces.spec = Some(spec);
Ok(ces)
}
/// Creates a new c-e structure from a specification file to be
/// found along the `path` and in a [`Context`] given by a
/// [`ContextHandle`].
///
/// [`Context`]: crate::Context
pub fn from_file<P: AsRef<Path>>(ctx: ContextHandle, path: P) -> Result<Self, Box<dyn Error>> {
let mut fp = File::open(path)?;
let mut raw_spec = String::new();
fp.read_to_string(&mut raw_spec)?;
Self::from_str(ctx, &raw_spec)
}
pub fn get_name(&self) -> Option<&str> {
if let Some(ref spec) = self.spec {
spec.get_name()
} else {
None
}
}
/// Returns link coherence status indicating whether this object
/// represents a proper c-e structure.
///
/// C-e structure is coherent iff it has no broken links, where a
/// link is broken iff it occurs either in causes or in effects,
/// but not in both. Internally, there is a broken links counter
/// associated with each `CES` object. This counter is updated
/// whenever a polynomial is added to the structure.
pub fn is_coherent(&self) -> bool {
self.num_broken_links == 0
}
pub fn get_formula(&self) -> sat::Formula {
let mut formula = sat::Formula::new(self.context.clone());
for (&pid, poly) in self.causes.iter() {
formula.add_polynomial(pid, poly);
formula.add_antiport(pid);
}
for (&pid, poly) in self.effects.iter() {
formula.add_polynomial(pid, poly);
}
for (&lid, _) in self.links.iter() {
formula.add_link_coherence(lid);
}
formula
}
}