conjure_core/rules/
bubble.rs

1use conjure_core::ast::{Expression, ReturnType};
2use conjure_core::metadata::Metadata;
3use conjure_core::rule_engine::{
4    register_rule, register_rule_set, ApplicationError, ApplicationError::*, ApplicationResult,
5    Reduction,
6};
7use uniplate::Uniplate;
8
9use crate::ast::{Atom, Literal, SymbolTable};
10
11use super::utils::is_all_constant;
12
13register_rule_set!("Bubble", ("Base"));
14
15// Bubble reduction rules
16
17/*
18    Reduce bubbles with a boolean expression to a conjunction with their condition.
19
20    e.g. (a / b = c) @ (b != 0) => (a / b = c) & (b != 0)
21*/
22#[register_rule(("Bubble", 8900))]
23fn expand_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {
24    match expr {
25        Expression::Bubble(_, a, b) if a.return_type() == Some(ReturnType::Bool) => {
26            Ok(Reduction::pure(Expression::And(
27                Metadata::new(),
28                vec![*a.clone(), *b.clone()],
29            )))
30        }
31        _ => Err(ApplicationError::RuleNotApplicable),
32    }
33}
34
35/*
36    Bring bubbles with a non-boolean expression higher up the tree.
37
38    E.g. ((a / b) @ (b != 0)) = c => (a / b = c) @ (b != 0)
39*/
40#[register_rule(("Bubble", 8900))]
41fn bubble_up(expr: &Expression, _: &SymbolTable) -> ApplicationResult {
42    let mut sub = expr.children();
43    let mut bubbled_conditions = vec![];
44    for e in sub.iter_mut() {
45        if let Expression::Bubble(_, a, b) = e {
46            if a.return_type() != Some(ReturnType::Bool) {
47                bubbled_conditions.push(*b.clone());
48                *e = *a.clone();
49            }
50        }
51    }
52    if bubbled_conditions.is_empty() {
53        return Err(ApplicationError::RuleNotApplicable);
54    }
55    Ok(Reduction::pure(Expression::Bubble(
56        Metadata::new(),
57        Box::new(expr.with_children(sub)),
58        Box::new(Expression::And(Metadata::new(), bubbled_conditions)),
59    )))
60}
61
62// Bubble applications
63
64/// Converts an unsafe division to a safe division with a bubble condition.
65///
66/// ```text
67///     a / b => (a / b) @ (b != 0)
68/// ```
69///
70/// Division by zero is undefined and therefore not allowed, so we add a condition to check for it.
71/// This condition is brought up the tree and expanded into a conjunction with the first
72/// boolean-type expression it is paired with.
73
74#[register_rule(("Bubble", 6000))]
75fn div_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {
76    if is_all_constant(expr) {
77        return Err(RuleNotApplicable);
78    }
79    if let Expression::UnsafeDiv(_, a, b) = expr {
80        // bubble bottom up
81        if !a.is_safe() || !b.is_safe() {
82            return Err(RuleNotApplicable);
83        }
84
85        return Ok(Reduction::pure(Expression::Bubble(
86            Metadata::new(),
87            Box::new(Expression::SafeDiv(Metadata::new(), a.clone(), b.clone())),
88            Box::new(Expression::Neq(
89                Metadata::new(),
90                b.clone(),
91                Box::new(Expression::from(0)),
92            )),
93        )));
94    }
95    Err(ApplicationError::RuleNotApplicable)
96}
97
98/// Converts an unsafe mod to a safe mod with a bubble condition.
99///
100/// ```text
101/// a % b => (a % b) @ (b != 0)
102/// ```
103///
104/// Mod zero is undefined and therefore not allowed, so we add a condition to check for it.
105/// This condition is brought up the tree and expanded into a conjunction with the first
106/// boolean-type expression it is paired with.
107///
108#[register_rule(("Bubble", 6000))]
109fn mod_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {
110    if is_all_constant(expr) {
111        return Err(RuleNotApplicable);
112    }
113    if let Expression::UnsafeMod(_, a, b) = expr {
114        // bubble bottom up
115        if !a.is_safe() || !b.is_safe() {
116            return Err(RuleNotApplicable);
117        }
118
119        return Ok(Reduction::pure(Expression::Bubble(
120            Metadata::new(),
121            Box::new(Expression::SafeMod(Metadata::new(), a.clone(), b.clone())),
122            Box::new(Expression::Neq(
123                Metadata::new(),
124                b.clone(),
125                Box::new(Expression::from(0)),
126            )),
127        )));
128    }
129    Err(ApplicationError::RuleNotApplicable)
130}
131
132/// Converts an unsafe pow to a safe pow with a bubble condition.
133///
134/// ```text
135/// a**b => (a ** b) @ ((a!=0 \/ b!=0) /\ b>=0
136/// ```
137///
138/// Pow is only defined when `(a!=0 \/ b!=0) /\ b>=0`, so we add a condition to check for it.
139/// This condition is brought up the tree and expanded into a conjunction with the first
140/// boolean-type expression it is paired with.
141///
142#[register_rule(("Bubble", 6000))]
143fn pow_to_bubble(expr: &Expression, _: &SymbolTable) -> ApplicationResult {
144    if is_all_constant(expr) {
145        return Err(RuleNotApplicable);
146    }
147    if let Expression::UnsafePow(_, a, b) = expr.clone() {
148        // bubble bottom up
149        if !a.is_safe() || !b.is_safe() {
150            return Err(RuleNotApplicable);
151        }
152
153        return Ok(Reduction::pure(Expression::Bubble(
154            Metadata::new(),
155            Box::new(Expression::SafePow(Metadata::new(), a.clone(), b.clone())),
156            Box::new(Expression::And(
157                Metadata::new(),
158                vec![
159                    Expression::Or(
160                        Metadata::new(),
161                        vec![
162                            Expression::Neq(
163                                Metadata::new(),
164                                a,
165                                Box::new(Atom::Literal(Literal::Int(0)).into()),
166                            ),
167                            Expression::Neq(
168                                Metadata::new(),
169                                b.clone(),
170                                Box::new(Atom::Literal(Literal::Int(0)).into()),
171                            ),
172                        ],
173                    ),
174                    Expression::Geq(
175                        Metadata::new(),
176                        b,
177                        Box::new(Atom::Literal(Literal::Int(0)).into()),
178                    ),
179                ],
180            )),
181        )));
182    }
183    Err(ApplicationError::RuleNotApplicable)
184}
conjure_core/rules/bubble.rs

conjure_core/rules/
bubble.rs
