conjure_core/rules/
bubble.rs

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

conjure_core/rules/
bubble.rs
