conjure_core/rules/
base.rs

1use std::rc::Rc;
2
3use conjure_core::ast::{Atom, Expression as Expr, Literal as Lit, SymbolTable};
4use conjure_core::metadata::Metadata;
5use conjure_core::rule_engine::{
6    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,
7};
8use uniplate::Uniplate;
9
10use Atom::*;
11use Expr::*;
12use Lit::*;
13
14use crate::ast::Declaration;
15
16register_rule_set!("Base", ());
17
18/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.
19///
20/// For example:
21/// - `or([])` simplifies to `false` since no disjunction exists.
22///
23/// **Applicable examples:**
24/// ```text
25/// or([])  ~> false
26/// X([]) ~> Nothing
27/// ```
28#[register_rule(("Base", 8800))]
29fn remove_empty_expression(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
30    // excluded expressions
31    if matches!(
32        expr,
33        Atomic(_, _)
34            | Root(_, _)
35            | FlatIneq(_, _, _, _)
36            | FlatMinusEq(_, _, _)
37            | FlatSumGeq(_, _, _)
38            | FlatSumLeq(_, _, _)
39            | FlatProductEq(_, _, _, _)
40            | FlatWatchedLiteral(_, _, _)
41            | FlatWeightedSumGeq(_, _, _, _)
42            | FlatWeightedSumLeq(_, _, _, _)
43            | MinionDivEqUndefZero(_, _, _, _)
44            | MinionModuloEqUndefZero(_, _, _, _)
45            | MinionPow(_, _, _, _)
46            | MinionReify(_, _, _)
47            | MinionReifyImply(_, _, _)
48            | FlatAbsEq(_, _, _)
49    ) {
50        return Err(ApplicationError::RuleNotApplicable);
51    }
52
53    if !expr.children().is_empty() {
54        return Err(ApplicationError::RuleNotApplicable);
55    }
56
57    let new_expr = match expr {
58        Or(_, _) => Atomic(Metadata::new(), Literal(Bool(false))),
59        _ => And(Metadata::new(), vec![]), // TODO: (yb33) Change it to a simple vector after we refactor our model,
60    };
61
62    Ok(Reduction::pure(new_expr))
63}
64
65/**
66 * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum.
67 * ```text
68 * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b)
69 * ```
70 */
71#[register_rule(("Base", 6000))]
72fn min_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
73    match expr {
74        Min(_, exprs) => {
75            let mut symbols = symbols.clone();
76            let new_name = symbols.gensym();
77
78            let mut new_top = Vec::new(); // the new variable must be less than or equal to all the other variables
79            let mut disjunction = Vec::new(); // the new variable must be equal to one of the variables
80            for e in exprs {
81                new_top.push(Leq(
82                    Metadata::new(),
83                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
84                    Box::new(e.clone()),
85                ));
86                disjunction.push(Eq(
87                    Metadata::new(),
88                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
89                    Box::new(e.clone()),
90                ));
91            }
92            new_top.push(Or(Metadata::new(), disjunction));
93
94            let domain = expr
95                .domain_of(&symbols)
96                .ok_or(ApplicationError::DomainError)?;
97            symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));
98
99            Ok(Reduction::new(
100                Atomic(Metadata::new(), Reference(new_name)),
101                new_top,
102                symbols,
103            ))
104        }
105        _ => Err(ApplicationError::RuleNotApplicable),
106    }
107}
108
109/**
110 * Turn a Max into a new variable and post a top level constraint to ensure the new variable is the maximum.
111 * ```text
112 * max([a, b]) ~> c ; c >= a & c >= b & (c = a | c = b)
113 * ```
114 */
115#[register_rule(("Base", 6000))]
116fn max_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {
117    match expr {
118        Max(_, exprs) => {
119            let mut symbols = symbols.clone();
120            let new_name = symbols.gensym();
121
122            let mut new_top = Vec::new(); // the new variable must be more than or equal to all the other variables
123            let mut disjunction = Vec::new(); // the new variable must more than or equal to one of the variables
124            for e in exprs {
125                new_top.push(Geq(
126                    Metadata::new(),
127                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
128                    Box::new(e.clone()),
129                ));
130                disjunction.push(Eq(
131                    Metadata::new(),
132                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),
133                    Box::new(e.clone()),
134                ));
135            }
136            new_top.push(Or(Metadata::new(), disjunction));
137
138            let domain = expr
139                .domain_of(&symbols)
140                .ok_or(ApplicationError::DomainError)?;
141            symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));
142
143            Ok(Reduction::new(
144                Atomic(Metadata::new(), Reference(new_name)),
145                new_top,
146                symbols,
147            ))
148        }
149        _ => Err(ApplicationError::RuleNotApplicable),
150    }
151}
conjure_core/rules/base.rs

conjure_core/rules/
base.rs
