conjure_core/rules/normalisers/
bool.rs

Help
1//! Normalising rules for boolean operations (not, and, or, ->).
2
3use conjure_core::ast::Expression as Expr;
4use conjure_core::metadata::Metadata;
5use conjure_core::rule_engine::{
6    register_rule, ApplicationError, ApplicationError::RuleNotApplicable, ApplicationResult,
7    Reduction,
8};
9use uniplate::Uniplate;
10
11use Expr::*;
12
13use crate::ast::{Atom, SymbolTable};
14use crate::{into_matrix_expr, matrix_expr};
15
16/// Removes double negations
17///
18/// ```text
19/// not(not(a)) = a
20/// ```
21#[register_rule(("Base", 8400))]
22fn remove_double_negation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
23    match expr {
24        Not(_, contents) => match contents.as_ref() {
25            Not(_, expr_box) => Ok(Reduction::pure(*expr_box.clone())),
26            _ => Err(ApplicationError::RuleNotApplicable),
27        },
28        _ => Err(ApplicationError::RuleNotApplicable),
29    }
30}
31
32/// Distributes `ands` contained in `ors`
33///
34/// ```text
35/// or(and(a, b), c) ~> and(or(a, c), or(b, c))
36/// ```
37#[register_rule(("Base", 8400))]
38fn distribute_or_over_and(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
39    fn find_and(exprs: &[Expr]) -> Option<usize> {
40        // ToDo: may be better to move this to some kind of utils module?
41        for (i, e) in exprs.iter().enumerate() {
42            if let And(_, _) = e {
43                return Some(i);
44            }
45        }
46        None
47    }
48
49    match expr {
50        Or(_, e) => {
51            let Some(exprs) = e.as_ref().clone().unwrap_list() else {
52                return Err(RuleNotApplicable);
53            };
54
55            match find_and(&exprs) {
56                Some(idx) => {
57                    let mut rest = exprs.clone();
58                    let and_expr = rest.remove(idx);
59
60                    match and_expr {
61                        And(metadata, e) => {
62                            let Some(and_exprs) = e.as_ref().clone().unwrap_list() else {
63                                return Err(RuleNotApplicable);
64                            };
65
66                            let mut new_and_contents = Vec::new();
67
68                            for e in and_exprs {
69                                // ToDo: Cloning everything may be a bit inefficient - discuss
70                                let mut new_or_contents = rest.clone();
71                                new_or_contents.push(e.clone());
72                                new_and_contents.push(Or(
73                                    metadata.clone_dirty(),
74                                    Box::new(into_matrix_expr![new_or_contents]),
75                                ))
76                            }
77
78                            Ok(Reduction::pure(And(
79                                metadata.clone_dirty(),
80                                Box::new(into_matrix_expr![new_and_contents]),
81                            )))
82                        }
83                        _ => Err(ApplicationError::RuleNotApplicable),
84                    }
85                }
86                None => Err(ApplicationError::RuleNotApplicable),
87            }
88        }
89        _ => Err(ApplicationError::RuleNotApplicable),
90    }
91}
92
93/// Distributes `not` over `and` by De Morgan's Law
94///
95/// ```text
96/// not(and(a, b)) ~> or(not(a), not(b))
97/// ```
98#[register_rule(("Base", 8400))]
99fn distribute_not_over_and(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
100    for child in expr.universe() {
101        if matches!(
102            child,
103            Expr::UnsafeDiv(_, _, _) | Expr::Bubble(_, _, _) | Expr::UnsafeMod(_, _, _)
104        ) {
105            return Err(RuleNotApplicable);
106        }
107    }
108    match expr {
109        Not(_, contents) => match contents.as_ref() {
110            And(metadata, e) => {
111                let Some(exprs) = e.as_ref().clone().unwrap_list() else {
112                    return Err(RuleNotApplicable);
113                };
114
115                if exprs.len() == 1 {
116                    let single_expr = exprs[0].clone();
117                    return Ok(Reduction::pure(Not(
118                        Metadata::new(),
119                        Box::new(single_expr.clone()),
120                    )));
121                }
122                let mut new_exprs = Vec::new();
123                for e in exprs {
124                    new_exprs.push(Not(metadata.clone(), Box::new(e.clone())));
125                }
126                Ok(Reduction::pure(Or(
127                    metadata.clone(),
128                    Box::new(into_matrix_expr![new_exprs]),
129                )))
130            }
131            _ => Err(ApplicationError::RuleNotApplicable),
132        },
133        _ => Err(ApplicationError::RuleNotApplicable),
134    }
135}
136
137/// Distributes `not` over `or` by De Morgan's Law
138///
139/// ```text
140/// not(or(a, b)) ~> and(not(a), not(b))
141/// ```
142#[register_rule(("Base", 8400))]
143fn distribute_not_over_or(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
144    match expr {
145        Not(_, contents) => match contents.as_ref() {
146            Or(metadata, e) => {
147                let Some(exprs) = e.as_ref().clone().unwrap_list() else {
148                    return Err(RuleNotApplicable);
149                };
150
151                if exprs.len() == 1 {
152                    let single_expr = exprs[0].clone();
153                    return Ok(Reduction::pure(Not(
154                        Metadata::new(),
155                        Box::new(single_expr.clone()),
156                    )));
157                }
158
159                let mut new_exprs = Vec::new();
160
161                for e in exprs {
162                    new_exprs.push(Not(metadata.clone(), Box::new(e.clone())));
163                }
164
165                Ok(Reduction::pure(And(
166                    metadata.clone(),
167                    Box::new(into_matrix_expr![new_exprs]),
168                )))
169            }
170            _ => Err(ApplicationError::RuleNotApplicable),
171        },
172        _ => Err(ApplicationError::RuleNotApplicable),
173    }
174}
175
176/// Removes ands with a single argument.
177///
178/// ```text
179/// or([a]) ~> a
180/// ```
181#[register_rule(("Base", 8800))]
182fn remove_unit_vector_and(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
183    match expr {
184        And(_, e) => {
185            let Some(exprs) = e.as_ref().clone().unwrap_list() else {
186                return Err(RuleNotApplicable);
187            };
188
189            if exprs.len() == 1 {
190                return Ok(Reduction::pure(exprs[0].clone()));
191            }
192
193            Err(ApplicationError::RuleNotApplicable)
194        }
195        _ => Err(ApplicationError::RuleNotApplicable),
196    }
197}
198
199/// Removes ors with a single argument.
200///
201/// ```text
202/// or([a]) ~> a
203/// ```
204#[register_rule(("Base", 8800))]
205fn remove_unit_vector_or(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
206    let Expr::Or(_, e) = expr else {
207        return Err(RuleNotApplicable);
208    };
209
210    let Some(exprs) = e.as_ref().clone().unwrap_list() else {
211        return Err(RuleNotApplicable);
212    };
213
214    // do not conflict with unwrap_nested_or rule.
215    if exprs.len() != 1 || matches!(exprs[0], Expr::Or(_, _)) {
216        return Err(RuleNotApplicable);
217    }
218
219    Ok(Reduction::pure(exprs[0].clone()))
220}
221
222/// Applies the contrapositive of implication.
223///
224/// ```text
225/// !p -> !q ~> q -> p
226/// ```
227/// where p,q are safe.
228#[register_rule(("Base", 8800))]
229fn normalise_implies_contrapositive(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
230    let Expr::Imply(_, e1, e2) = expr else {
231        return Err(RuleNotApplicable);
232    };
233
234    let Expr::Not(_, p) = e1.as_ref() else {
235        return Err(RuleNotApplicable);
236    };
237
238    let Expr::Not(_, q) = e2.as_ref() else {
239        return Err(RuleNotApplicable);
240    };
241
242    // we only negate e1, e2 if they are safe.
243    if !e1.is_safe() || !e2.is_safe() {
244        return Err(RuleNotApplicable);
245    }
246
247    Ok(Reduction::pure(Expr::Imply(
248        Metadata::new(),
249        q.clone(),
250        p.clone(),
251    )))
252}
253
254/// Simplifies the negation of implication.
255///
256/// ```text
257/// !(p->q) ~> p /\ !q
258/// ```,
259///
260/// where p->q is safe
261#[register_rule(("Base", 8800))]
262fn normalise_implies_negation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
263    let Expr::Not(_, e1) = expr else {
264        return Err(RuleNotApplicable);
265    };
266
267    let Expr::Imply(_, p, q) = e1.as_ref() else {
268        return Err(RuleNotApplicable);
269    };
270
271    // p->q must be safe to negate
272    if !e1.is_safe() {
273        return Err(RuleNotApplicable);
274    }
275
276    Ok(Reduction::pure(Expr::And(
277        Metadata::new(),
278        Box::new(matrix_expr![
279            *p.clone(),
280            Expr::Not(Metadata::new(), q.clone())
281        ]),
282    )))
283}
284
285/// Applies left distributivity to implication.
286///
287/// ```text
288/// ((r -> p) -> (r->q)) ~> (r -> (p -> q))
289/// ```
290///
291/// This rule relies on CSE to unify the two instances of `r` to a single atom; therefore, it might
292/// not work as well when optimisations are disabled.
293///
294/// Has a higher priority than `normalise_implies_uncurry` as this should apply first. See the
295/// docstring for `normalise_implies_uncurry`.
296#[register_rule(("Base", 8800))]
297fn normalise_implies_left_distributivity(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
298    let Expr::Imply(_, e1, e2) = expr else {
299        return Err(RuleNotApplicable);
300    };
301
302    let Expr::Imply(_, r1, p) = e1.as_ref() else {
303        return Err(RuleNotApplicable);
304    };
305
306    let Expr::Imply(_, r2, q) = e2.as_ref() else {
307        return Err(RuleNotApplicable);
308    };
309
310    // Instead of checking deep equality, let CSE unify them to a common variable and check for
311    // that.
312
313    let r1_atom: &Atom = r1.as_ref().try_into().or(Err(RuleNotApplicable))?;
314    let r2_atom: &Atom = r2.as_ref().try_into().or(Err(RuleNotApplicable))?;
315
316    if !(r1_atom == r2_atom) {
317        return Err(RuleNotApplicable);
318    }
319
320    Ok(Reduction::pure(Expr::Imply(
321        Metadata::new(),
322        r1.clone(),
323        Box::new(Expr::Imply(Metadata::new(), p.clone(), q.clone())),
324    )))
325}
326
327/// Applies import-export to implication, i.e. uncurrying.
328///
329/// ```text
330/// p -> (q -> r) ~> (p/\q) -> r
331/// ```
332///
333/// This rule has a lower priority of 8400 to allow distributivity, contraposition, etc. to
334/// apply first.
335///
336/// For example, we want to do:
337///
338/// ```text
339/// ((r -> p) -> (r -> q)) ~> (r -> (p -> q))  [left-distributivity]
340/// (r -> (p -> q)) ~> (r/\p) ~> q [uncurry]
341/// ```
342///
343/// not
344///
345/// ```text
346/// ((r->p) -> (r->q)) ~> ((r->p) /\ r) -> q) ~> [uncurry]
347/// ```
348///
349/// # Rationale
350///
351/// With this rule, I am assuming (without empirical evidence) that and is a cheaper constraint
352/// than implication (in particular, Minion's reifyimply constraint).
353#[register_rule(("Base", 8400))]
354fn normalise_implies_uncurry(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
355    let Expr::Imply(_, p, e1) = expr else {
356        return Err(RuleNotApplicable);
357    };
358
359    let Expr::Imply(_, q, r) = e1.as_ref() else {
360        return Err(RuleNotApplicable);
361    };
362
363    Ok(Reduction::pure(Expr::Imply(
364        Metadata::new(),
365        Box::new(Expr::And(
366            Metadata::new(),
367            Box::new(matrix_expr![*p.clone(), *q.clone()]),
368        )),
369        r.clone(),
370    )))
371}
conjure_core/rules/normalisers/bool.rs

conjure_core/rules/normalisers/
bool.rs
