conjure_cp_core/rule_engine/
rule.rs

1use std::collections::BTreeSet;
2use std::fmt::{self, Debug, Display, Formatter};
3use std::hash::Hash;
4use std::sync::Arc;
5
6use thiserror::Error;
7
8use crate::Model;
9use crate::ast::{
10    DeclarationKind, DeclarationPtr, Expression, Metadata, Name, SatEncodingDecision, SymbolTable,
11};
12
13#[derive(Debug, Error)]
14pub enum ApplicationError {
15    #[error("Rule is not applicable")]
16    RuleNotApplicable,
17
18    #[error("Could not calculate the expression domain")]
19    DomainError,
20}
21
22/// Represents the result of applying a rule to an expression within a model.
23///
24/// A `RuleEffect` encapsulates the changes made to a model during a rule application.
25/// It includes a new expression to replace the original one, an optional top-level constraint
26/// to be added to the model, and any updates to the model's symbol table.
27///
28/// This struct allows for representing side-effects of rule applications, ensuring that
29/// all modifications, including symbol table expansions and additional constraints, are
30/// accounted for and can be applied to the model consistently.
31///
32/// # Fields
33/// - `new_expression`: The updated [`Expression`] that replaces the original one after applying the rule.
34/// - `new_top`: An additional top-level [`Vec<Expression>`] constraint that should be added to the model. If no top-level
35///   constraint is needed, this field can be set to an empty vector [`Vec::new()`].
36/// - `symbols`: A [`SymbolTable`] containing any new symbol definitions or modifications to be added to the model's
37///   symbol table. If no symbols are modified, this field can be set to an empty symbol table.
38///
39/// # Usage
40/// A `RuleEffect` can be created using one of the provided constructors:
41/// - [`RuleEffect::new`]: Creates an effect with a new expression, top-level constraint, and symbol modifications.
42/// - [`RuleEffect::pure`]: Creates an effect with only a new expression and no side-effects on the symbol table or constraints.
43/// - [`RuleEffect::with_symbols`]: Creates an effect with a new expression and symbol table modifications, but no top-level constraint.
44/// - [`RuleEffect::with_top`]: Creates an effect with a new expression and a top-level constraint, but no symbol table modifications.
45/// - [`RuleEffect::sat`]: Creates an effect with a new expression, SAT encoding decisions and symbol modifications, but no top-level constraints.
46///
47/// The `apply` method allows for applying the changes represented by the `RuleEffect` to a [`Model`].
48///
49/// # Example
50/// ```
51/// // Need to add an example
52/// ```
53///
54/// # See Also
55/// - [`ApplicationResult`]: Represents the result of applying a rule, which may either be a `RuleEffect` or an `ApplicationError`.
56/// - [`Model`]: The structure to which the `RuleEffect` changes are applied.
57#[non_exhaustive]
58#[derive(Clone)]
59pub struct RuleEffect {
60    pub new_expression: Expression,
61    pub new_top: Vec<Expression>,
62    pub symbols: SymbolTable,
63    pub new_sat_decisions: Vec<SatEncodingDecision>,
64    /// Shared declarations to update if this effect is selected.
65    pub(crate) declaration_updates: Vec<DeclarationUpdate>,
66    materialise: Option<DeferredRuleEffect>,
67    pub(crate) uniform_choices: crate::representation::uniform::Choices,
68}
69
70/// An in-place update to a shared declaration, applied only after its rule is selected.
71#[derive(Clone, Debug)]
72pub(crate) struct DeclarationUpdate {
73    target: DeclarationPtr,
74    replacement_kind: DeclarationKind,
75}
76
77impl DeclarationUpdate {
78    /// Creates a deferred replacement for a shared declaration's kind.
79    fn new(target: DeclarationPtr, replacement_kind: DeclarationKind) -> Self {
80        Self {
81            target,
82            replacement_kind,
83        }
84    }
85
86    /// Returns the name of the declaration that will be updated.
87    pub(crate) fn name(&self) -> Name {
88        self.target.name().clone()
89    }
90
91    /// Commits the replacement while retaining the declaration's identity.
92    pub(crate) fn apply(mut self) {
93        let _ = self.target.replace_kind(self.replacement_kind);
94    }
95
96    /// Creates an unshared declaration containing the pending replacement.
97    fn preview(&self) -> DeclarationPtr {
98        DeclarationPtr::new(self.name(), self.replacement_kind.clone())
99    }
100}
101
102/// Deferred constructor for a concrete rule effect.
103type DeferredRuleEffect = Arc<dyn Fn(&SymbolTable) -> RuleEffect + Send + Sync>;
104
105/// The result of applying a rule to an expression.
106/// Contains either a set of rule effects or an error.
107pub type ApplicationResult = Result<RuleEffect, ApplicationError>;
108
109impl Debug for RuleEffect {
110    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
111        f.debug_struct("RuleEffect")
112            .field("new_expression", &self.new_expression)
113            .field("new_top", &self.new_top)
114            .field("symbols", &self.symbols)
115            .field("new_sat_decisions", &self.new_sat_decisions)
116            .field("declaration_updates", &self.declaration_updates)
117            .field("is_deferred", &self.materialise.is_some())
118            .finish()
119    }
120}
121
122impl RuleEffect {
123    pub fn new(new_expression: Expression, new_top: Vec<Expression>, symbols: SymbolTable) -> Self {
124        Self {
125            new_expression,
126            new_top,
127            symbols,
128            new_sat_decisions: Vec::new(),
129            declaration_updates: Vec::new(),
130            materialise: None,
131            uniform_choices: Default::default(),
132        }
133    }
134
135    /// Represents an effect with no side effects on the model.
136    pub fn pure(new_expression: Expression) -> Self {
137        Self {
138            new_expression,
139            new_top: Vec::new(),
140            symbols: SymbolTable::new(),
141            new_sat_decisions: Vec::new(),
142            declaration_updates: Vec::new(),
143            materialise: None,
144            uniform_choices: Default::default(),
145        }
146    }
147
148    /// Represents an effect that also modifies the symbol table.
149    pub fn with_symbols(new_expression: Expression, symbols: SymbolTable) -> Self {
150        Self {
151            new_expression,
152            new_top: Vec::new(),
153            symbols,
154            new_sat_decisions: Vec::new(),
155            declaration_updates: Vec::new(),
156            materialise: None,
157            uniform_choices: Default::default(),
158        }
159    }
160
161    /// Represents an effect that also adds a top-level constraint to the model.
162    pub fn with_top(new_expression: Expression, new_top: Vec<Expression>) -> Self {
163        Self {
164            new_expression,
165            new_top,
166            symbols: SymbolTable::new(),
167            new_sat_decisions: Vec::new(),
168            declaration_updates: Vec::new(),
169            materialise: None,
170            uniform_choices: Default::default(),
171        }
172    }
173
174    /// Represents an effect that adds semantic SAT encoding decisions.
175    pub fn sat(
176        new_expression: Expression,
177        new_sat_decisions: Vec<SatEncodingDecision>,
178        symbols: SymbolTable,
179    ) -> Self {
180        Self {
181            new_expression,
182            new_top: Vec::new(),
183            symbols,
184            new_sat_decisions,
185            declaration_updates: Vec::new(),
186            materialise: None,
187            uniform_choices: Default::default(),
188        }
189    }
190
191    /// Defers constructing a concrete effect until the rewriter chooses to apply this rule.
192    ///
193    /// This is intended for rule effects that allocate fresh names or otherwise depend on global
194    /// model state. Applicability checks can return a deferred effect without consuming those
195    /// effects; the rewriter calls [`RuleEffect::materialise`] only for the selected rule.
196    pub fn deferred(
197        materialise: impl Fn(&SymbolTable) -> RuleEffect + Send + Sync + 'static,
198    ) -> Self {
199        Self {
200            new_expression: Expression::Root(Metadata::new(), Vec::new()),
201            new_top: Vec::new(),
202            symbols: SymbolTable::new(),
203            new_sat_decisions: Vec::new(),
204            declaration_updates: Vec::new(),
205            materialise: Some(Arc::new(materialise)),
206            uniform_choices: Default::default(),
207        }
208    }
209
210    /// Returns the concrete effect for the current symbol table.
211    ///
212    /// This consumes the selected effect: cloning a concrete effect can duplicate its expression,
213    /// top-level constraints, SAT encoding decisions, and speculative symbol table. Before returning, the symbol
214    /// snapshot is reduced to the bindings that the effect actually changes.
215    pub fn materialise(mut self, symbols: &SymbolTable) -> Self {
216        crate::representation::uniform::commit(std::mem::take(&mut self.uniform_choices));
217        if let Some(materialise) = self.materialise.take() {
218            return materialise(symbols).materialise(symbols);
219        }
220
221        self.symbols.retain_local_changes_from(symbols);
222        self
223    }
224
225    pub(crate) fn is_deferred(&self) -> bool {
226        self.materialise.is_some()
227    }
228
229    /// Adds declaration replacements that are committed only if this effect is selected.
230    pub fn with_declaration_updates(
231        mut self,
232        updates: impl IntoIterator<Item = (DeclarationPtr, DeclarationKind)>,
233    ) -> Self {
234        self.declaration_updates.extend(
235            updates
236                .into_iter()
237                .map(|(target, kind)| DeclarationUpdate::new(target, kind)),
238        );
239        self
240    }
241
242    /// Iterates over the names changed by deferred declaration updates.
243    pub fn updated_declaration_names(&self) -> impl Iterator<Item = Name> + '_ {
244        self.declaration_updates.iter().map(DeclarationUpdate::name)
245    }
246
247    /// Applies pending declaration replacements to a detached symbol-table preview.
248    pub(crate) fn preview_declaration_updates(&self, symbols: &mut SymbolTable) {
249        for update in &self.declaration_updates {
250            symbols.update_insert(update.preview());
251        }
252    }
253
254    /// Applies side-effects (e.g. symbol table updates)
255    pub fn apply(mut self, model: &mut Model) {
256        crate::representation::uniform::commit(std::mem::take(&mut self.uniform_choices));
257        debug_assert!(
258            self.materialise.is_none(),
259            "deferred rule effects must be materialised before being applied"
260        );
261        for update in self.declaration_updates {
262            update.apply();
263        }
264        model.symbols_mut().extend(self.symbols); // Add new assignments to the symbol table
265        model.add_constraints(self.new_top);
266        model.add_sat_decisions(self.new_sat_decisions);
267    }
268
269    /// Gets symbols added by this effect.
270    ///
271    /// Walks this effect's own symbols rather than diffing two whole tables. The rewriter asks
272    /// this once per applied rule, and most effects are pure, so diffing made every rewrite cost
273    /// a clone and a sort of the entire model symbol table.
274    pub fn added_symbols(&self, initial_symbols: &SymbolTable) -> BTreeSet<Name> {
275        self.symbols
276            .iter_local()
277            .filter(|(name, _)| initial_symbols.lookup_local(name).is_none())
278            .map(|(name, _)| name.clone())
279            .collect()
280    }
281
282    /// Gets symbols changed by this effect.
283    ///
284    /// Returns a list of tuples of (name, domain before effect, domain after effect), ordered by
285    /// name.
286    ///
287    /// Walks this effect's symbols for the same reason as [`RuleEffect::added_symbols`]: a symbol
288    /// can only have changed if this effect carries its new value.
289    pub fn changed_symbols(
290        &self,
291        initial_symbols: &SymbolTable,
292    ) -> Vec<(Name, DeclarationPtr, DeclarationPtr)> {
293        let mut changes: Vec<(Name, DeclarationPtr, DeclarationPtr)> = self
294            .symbols
295            .iter_local()
296            .filter_map(|(name, new_value)| {
297                let initial_value = initial_symbols.lookup_local(name)?;
298                (!new_value.content_eq(&initial_value))
299                    .then(|| (name.clone(), initial_value.clone(), new_value.clone()))
300            })
301            .collect();
302        changes.sort_by(|(lhs, ..), (rhs, ..)| lhs.cmp(rhs));
303        changes
304    }
305}
306
307/// The function type used in a [`Rule`].
308pub type RuleFn = fn(&Expression, &SymbolTable) -> ApplicationResult;
309
310/// Atomic expression subvariants that can be used as rule prefilters.
311#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
312pub enum AtomKind {
313    /// An `Atomic` expression containing a literal.
314    Literal,
315    /// An `Atomic` expression containing a reference.
316    Reference,
317}
318
319/// A complete rule prefilter alternative.
320///
321/// A rule matches when any of its prefilter alternatives matches the focused expression. This keeps
322/// compound filters such as `And / Comprehension` paired instead of forming a cross product with
323/// other alternatives in the same rule declaration.
324#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
325pub enum RulePrefilter {
326    /// Focused expression must have this `Expression` variant.
327    Variant(usize),
328    /// Focused expression must have an immediate child with this `Expression` variant.
329    Child { child: usize },
330    /// Focused expression must have this variant and an immediate child with `child`'s variant.
331    VariantChild { variant: usize, child: usize },
332    /// Focused expression must be an `Atomic` expression with this atomic subvariant.
333    Atom(AtomKind),
334    /// Focused expression must have an immediate `Atomic` child with this atomic subvariant.
335    ChildAtom(AtomKind),
336}
337
338/// State changes that can invalidate a failed rule application.
339///
340/// Most rules may become applicable when either their focused expression or the symbol table
341/// changes. A small number of Root rules use the expression only as an entry point and decide
342/// applicability entirely from declarations. Remembering their failed applications until the
343/// symbol table changes avoids repeatedly scanning every declaration after unrelated expression
344/// rewrites.
345#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
346pub enum RuleFailureInvalidation {
347    /// Reconsider a failed application after any relevant expression or symbol-table change.
348    #[default]
349    ExpressionOrSymbols,
350    /// Reconsider a failed application only after the symbol table changes.
351    SymbolsOnly,
352}
353
354/**
355 * A rule with a name, application function, and rule sets.
356 *
357 * # Fields
358 * - `name` The name of the rule.
359 * - `application` The function to apply the rule.
360 * - `rule_sets` A list of rule set names and priorities that this rule is a part of. This is used to populate rulesets at runtime.
361 */
362#[derive(Clone, Debug)]
363pub struct Rule<'a> {
364    pub name: &'a str,
365    pub application: RuleFn,
366    pub rule_sets: &'a [(&'a str, u16)], // (name, priority). At runtime, we add the rule to rulesets
367    /// Complete prefilter alternatives this rule applies to, or `None` for universal rules.
368    pub prefilters: Option<&'static [RulePrefilter]>,
369    /// Which state changes can make a failed application become applicable.
370    pub failure_invalidation: RuleFailureInvalidation,
371}
372
373impl<'a> Rule<'a> {
374    pub const fn new(
375        name: &'a str,
376        application: RuleFn,
377        rule_sets: &'a [(&'static str, u16)],
378    ) -> Self {
379        Self {
380            name,
381            application,
382            rule_sets,
383            prefilters: None,
384            failure_invalidation: RuleFailureInvalidation::ExpressionOrSymbols,
385        }
386    }
387
388    pub fn apply(&self, expr: &Expression, symbols: &SymbolTable) -> ApplicationResult {
389        crate::representation::uniform::attempt(|| (self.application)(expr, symbols))
390    }
391}
392
393impl Display for Rule<'_> {
394    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
395        write!(f, "{}", self.name)
396    }
397}
398
399impl PartialEq for Rule<'_> {
400    fn eq(&self, other: &Self) -> bool {
401        self.name == other.name
402    }
403}
404
405impl Eq for Rule<'_> {}
406
407impl Hash for Rule<'_> {
408    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
409        self.name.hash(state);
410    }
411}
412
413#[cfg(test)]
414mod tests {
415    use super::*;
416    use crate::ast::{DecisionVariable, Domain, Range, Reference};
417    use crate::rule_engine::rewriter_common::{
418        snapshot_symbols_after_effect, snapshot_variable_declarations,
419    };
420
421    #[test]
422    fn declaration_updates_are_applied_only_when_effect_is_committed() {
423        let old_domain = Domain::int(vec![Range::Bounded(1, 3)]);
424        let new_domain = Domain::int(vec![Range::Bounded(1, 2)]);
425        let mut model = Model::new(Default::default());
426        let declaration = DeclarationPtr::new_find(Name::user("x"), old_domain.clone());
427        let reference = Reference::new(declaration.clone());
428        model.symbols_mut().insert(declaration.clone()).unwrap();
429
430        let effect = RuleEffect::pure(Expression::from(1)).with_declaration_updates([(
431            declaration,
432            DeclarationKind::Find(DecisionVariable::new(new_domain.clone())),
433        )]);
434
435        let before = snapshot_variable_declarations(&model.symbols());
436        let after = snapshot_symbols_after_effect(&model.symbols(), &effect);
437        assert_eq!(before.get(&Name::user("x")).unwrap(), "find x: int(1..3)");
438        assert_eq!(after.get(&Name::user("x")).unwrap(), "find x: int(1..2)");
439        assert_eq!(reference.domain(), Some(old_domain));
440        effect.apply(&mut model);
441        assert_eq!(reference.domain(), Some(new_domain));
442    }
443}
conjure_cp_core/rule_engine/rule.rs

conjure_cp_core/rule_engine/
rule.rs
