conjure_core/rules/normalisers/
bool.rs

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

conjure_core/rules/normalisers/
bool.rs
