conjure_cp_core/ast/
partial_eval.rs

1use std::collections::HashSet;
2
3use crate::ast::Typeable;
4use crate::{
5    ast::{
6        AbstractLiteral, Atom, DomainPtr, Expression as Expr, GroundDomain, Literal as Lit,
7        Metadata, Moo, Range, ReturnType,
8    },
9    into_matrix_expr,
10    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},
11};
12use itertools::iproduct;
13use uniplate::Uniplate;
14
15/// Normalises integer ranges so equivalent domains compare structurally equal.
16fn normalise_int_domain(domain: &GroundDomain) -> GroundDomain {
17    match domain {
18        GroundDomain::Int(ranges) => GroundDomain::Int(Range::squeeze(
19            &ranges
20                .iter()
21                .map(|range| Range::new(range.low().copied(), range.high().copied()))
22                .collect::<Vec<_>>(),
23        )),
24        _ => domain.clone(),
25    }
26}
27
28/// Returns whether `expr` is safe after resolving any referenced expressions.
29fn is_semantically_safe(expr: &Expr) -> bool {
30    fn helper(expr: &Expr, resolving: &mut HashSet<crate::ast::serde::ObjId>) -> bool {
31        if !expr.is_safe() {
32            return false;
33        }
34
35        for subexpr in expr.universe() {
36            let Expr::Atomic(_, Atom::Reference(reference)) = subexpr else {
37                continue;
38            };
39
40            let Some(resolved) = reference.resolve_expression() else {
41                continue;
42            };
43
44            let id = reference.id();
45            if !resolving.insert(id.clone()) {
46                return false;
47            }
48
49            let is_safe = helper(&resolved, resolving);
50            resolving.remove(&id);
51
52            if !is_safe {
53                return false;
54            }
55        }
56
57        true
58    }
59
60    helper(expr, &mut HashSet::new())
61}
62
63/// Tries to decide `expr in domain` from resolved domains alone.
64fn simplify_in_domain(expr: &Expr, domain: &DomainPtr) -> Option<bool> {
65    if !is_semantically_safe(expr) {
66        return None;
67    }
68
69    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;
70    let domain = domain.resolve().ok()?;
71    let intersection = expr_domain.intersect(&domain).ok()?;
72
73    if normalise_int_domain(&intersection) == normalise_int_domain(expr_domain.as_ref()) {
74        return Some(true);
75    }
76
77    if let Ok(values_in_domain) = intersection.values_i32()
78        && values_in_domain.is_empty()
79    {
80        return Some(false);
81    }
82
83    None
84}
85
86/// Extracts an integer when `expr` is known to be a singleton integer value.
87fn singleton_int_value(expr: &Expr) -> Option<i32> {
88    if let Ok(value) = expr.try_into() {
89        return Some(value);
90    }
91
92    let domain = resolved_ground_domain_of_for_partial_eval(expr)?;
93    let GroundDomain::Int(ranges) = domain.as_ref() else {
94        return None;
95    };
96    let [range] = ranges.as_slice() else {
97        return None;
98    };
99    let (Some(low), Some(high)) = (range.low(), range.high()) else {
100        return None;
101    };
102
103    if low == high { Some(*low) } else { None }
104}
105
106/// Resolves a matrix literal subject, including constant references to matrix literals.
107fn resolve_matrix_subject(subject: &Expr) -> Option<(Vec<Expr>, DomainPtr)> {
108    subject.clone().unwrap_matrix_unchecked().or_else(|| {
109        let Expr::Atomic(_, Atom::Reference(reference)) = subject else {
110            return None;
111        };
112
113        let Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, index_domain)) =
114            reference.resolve_constant()?
115        else {
116            return None;
117        };
118
119        Some((
120            elems
121                .into_iter()
122                .map(|elem| Expr::Atomic(Metadata::new(), Atom::Literal(elem)))
123                .collect(),
124            index_domain.into(),
125        ))
126    })
127}
128
129/// Resolves domains for partial evaluation while avoiding malformed indexing panics.
130fn resolved_ground_domain_of_for_partial_eval(expr: &Expr) -> Option<Moo<GroundDomain>> {
131    match expr {
132        Expr::SafeIndex(_, subject, _) => {
133            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;
134            let GroundDomain::Matrix(elem_domain, _) = subject_domain.as_ref() else {
135                return None;
136            };
137
138            Some(elem_domain.clone())
139        }
140        Expr::SafeSlice(_, subject, indices) => {
141            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;
142            let GroundDomain::Matrix(elem_domain, index_domains) = subject_domain.as_ref() else {
143                return None;
144            };
145            let sliced_dimension = indices.iter().position(Option::is_none);
146
147            match sliced_dimension {
148                Some(dimension) => Some(Moo::new(GroundDomain::Matrix(
149                    elem_domain.clone(),
150                    vec![index_domains[dimension].clone()],
151                ))),
152                None => Some(elem_domain.clone()),
153            }
154        }
155        Expr::UnsafeIndex(_, _, _) | Expr::UnsafeSlice(_, _, _) => None,
156        _ => expr.domain_of()?.resolve().ok(),
157    }
158}
159
160/// Tries to decide `expr = lit` and `expr != lit` from the resolved domain of `expr`.
161fn simplify_comparison_with_literal(expr: &Expr, lit: &Lit) -> Option<(bool, bool)> {
162    if !is_semantically_safe(expr) {
163        return None;
164    }
165
166    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;
167
168    if !expr_domain.contains(lit).ok()? {
169        return Some((false, true));
170    }
171
172    match (expr_domain.as_ref(), lit) {
173        (GroundDomain::Int(ranges), Lit::Int(value)) => {
174            let [range] = ranges.as_slice() else {
175                return None;
176            };
177            let (Some(low), Some(high)) = (range.low(), range.high()) else {
178                return None;
179            };
180
181            if low == high && low == value {
182                Some((true, false))
183            } else {
184                None
185            }
186        }
187        (GroundDomain::Bool, Lit::Bool(_)) => None,
188        _ => None,
189    }
190}
191
192/// Tries to decide reflexive equality and inequality when both sides are semantically safe.
193fn simplify_reflexive_comparison(x: &Expr, y: &Expr) -> Option<(bool, bool)> {
194    if x.identical_atom_to(y) && is_semantically_safe(x) && is_semantically_safe(y) {
195        return Some((true, false));
196    }
197
198    if is_semantically_safe(x) && is_semantically_safe(y) && x == y {
199        return Some((true, false));
200    }
201
202    None
203}
204
205pub fn run_partial_evaluator(expr: &Expr) -> ApplicationResult {
206    // NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this
207    // rule infinitely!
208    // This is why we always check whether we found a constant or not.
209    match expr {
210        Expr::Union(_, _, _) => Err(RuleNotApplicable),
211        Expr::In(_, _, _) => Err(RuleNotApplicable),
212        Expr::Intersect(_, _, _) => Err(RuleNotApplicable),
213        Expr::Supset(_, _, _) => Err(RuleNotApplicable),
214        Expr::SupsetEq(_, _, _) => Err(RuleNotApplicable),
215        Expr::Subset(_, _, _) => Err(RuleNotApplicable),
216        Expr::SubsetEq(_, _, _) => Err(RuleNotApplicable),
217        Expr::AbstractLiteral(_, _) => Err(RuleNotApplicable),
218        Expr::Comprehension(_, _) => Err(RuleNotApplicable),
219        Expr::AbstractComprehension(_, _) => Err(RuleNotApplicable),
220        Expr::DominanceRelation(_, _) => Err(RuleNotApplicable),
221        Expr::FromSolution(_, _) => Err(RuleNotApplicable),
222        Expr::Metavar(_, _) => Err(RuleNotApplicable),
223        Expr::UnsafeIndex(_, _, _) => Err(RuleNotApplicable),
224        Expr::UnsafeSlice(_, _, _) => Err(RuleNotApplicable),
225        Expr::Table(_, _, _) => Err(RuleNotApplicable),
226        Expr::NegativeTable(_, _, _) => Err(RuleNotApplicable),
227        Expr::RecordField(_, _, _) => Err(RuleNotApplicable),
228        Expr::SafeIndex(_, subject, indices) => {
229            // partially evaluate matrix literals indexed by a constant.
230
231            // subject must be a matrix literal
232            let (es, index_domain) = resolve_matrix_subject(subject).ok_or(RuleNotApplicable)?;
233
234            if indices.is_empty() {
235                return Err(RuleNotApplicable);
236            }
237
238            // the leading index must be fixed to a single value
239            let index = singleton_int_value(&indices[0]).ok_or(RuleNotApplicable)?;
240
241            // index domain must be a single integer range with a lower bound
242            if let Some(ranges) = index_domain.as_int_ground()
243                && ranges.len() == 1
244                && let Some(from) = ranges[0].low()
245            {
246                let zero_indexed_index = index - from;
247                let selected = es
248                    .get(zero_indexed_index as usize)
249                    .ok_or(RuleNotApplicable)?
250                    .clone();
251
252                if indices.len() == 1 {
253                    Ok(Reduction::pure(selected))
254                } else {
255                    Ok(Reduction::pure(Expr::SafeIndex(
256                        Metadata::new(),
257                        Moo::new(selected),
258                        indices[1..].to_vec(),
259                    )))
260                }
261            } else {
262                Err(RuleNotApplicable)
263            }
264        }
265        Expr::SafeSlice(_, _, _) => Err(RuleNotApplicable),
266        Expr::InDomain(_, x, domain) => {
267            if let Some(result) = simplify_in_domain(x, domain) {
268                Ok(Reduction::pure(Expr::Atomic(
269                    Metadata::new(),
270                    result.into(),
271                )))
272            } else if let Expr::Atomic(_, Atom::Reference(decl)) = x.as_ref() {
273                let decl_domain = decl
274                    .domain()
275                    .ok_or(RuleNotApplicable)?
276                    .resolve()
277                    .map_err(|_| RuleNotApplicable)?;
278                let domain = domain.resolve().map_err(|_| RuleNotApplicable)?;
279
280                let intersection = decl_domain
281                    .intersect(&domain)
282                    .map_err(|_| RuleNotApplicable)?;
283
284                // if the declaration's domain is a subset of domain, expr is always true.
285                if &intersection == decl_domain.as_ref() {
286                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
287                }
288                // if no elements of declaration's domain are in the domain (i.e. they have no
289                // intersection), expr is always false.
290                //
291                // Only check this when the intersection is a finite integer domain, as we
292                // currently don't have a way to check whether other domain kinds are empty or not.
293                //
294                // we should expand this to cover more domain types in the future.
295                else if let Ok(values_in_domain) = intersection.values_i32()
296                    && values_in_domain.is_empty()
297                {
298                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))
299                } else {
300                    Err(RuleNotApplicable)
301                }
302            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref() {
303                if domain
304                    .resolve()
305                    .and_then(|gd| gd.contains(lit))
306                    .map_err(|_| RuleNotApplicable)?
307                {
308                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
309                } else {
310                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))
311                }
312            } else {
313                Err(RuleNotApplicable)
314            }
315        }
316        Expr::Bubble(_, expr, cond) => {
317            // definition of bubble is "expr is valid as long as cond is true"
318            //
319            // check if cond is true and pop the bubble!
320            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) = cond.as_ref() {
321                Ok(Reduction::pure(Moo::unwrap_or_clone(expr.clone())))
322            } else {
323                Err(RuleNotApplicable)
324            }
325        }
326        Expr::Atomic(_, _) => Err(RuleNotApplicable),
327        Expr::ToInt(_, expression) => {
328            if expression.return_type() == ReturnType::Int {
329                Ok(Reduction::pure(Moo::unwrap_or_clone(expression.clone())))
330            } else {
331                Err(RuleNotApplicable)
332            }
333        }
334        Expr::Abs(m, e) => match e.as_ref() {
335            Expr::Neg(_, inner) => Ok(Reduction::pure(Expr::Abs(m.clone(), inner.clone()))),
336            _ => Err(RuleNotApplicable),
337        },
338        Expr::Sum(m, vec) => {
339            let vec = Moo::unwrap_or_clone(vec.clone())
340                .unwrap_list()
341                .ok_or(RuleNotApplicable)?;
342            let mut acc = 0;
343            let mut n_consts = 0;
344            let mut new_vec: Vec<Expr> = Vec::new();
345            for expr in vec {
346                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
347                    acc += x;
348                    n_consts += 1;
349                } else {
350                    new_vec.push(expr);
351                }
352            }
353            if acc != 0 {
354                new_vec.push(Expr::Atomic(
355                    Default::default(),
356                    Atom::Literal(Lit::Int(acc)),
357                ));
358            }
359
360            if n_consts <= 1 {
361                Err(RuleNotApplicable)
362            } else {
363                Ok(Reduction::pure(Expr::Sum(
364                    m.clone(),
365                    Moo::new(into_matrix_expr![new_vec]),
366                )))
367            }
368        }
369
370        Expr::Product(m, vec) => {
371            let mut acc = 1;
372            let mut n_consts = 0;
373            let mut new_vec: Vec<Expr> = Vec::new();
374            let vec = Moo::unwrap_or_clone(vec.clone())
375                .unwrap_list()
376                .ok_or(RuleNotApplicable)?;
377            for expr in vec {
378                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
379                    acc *= x;
380                    n_consts += 1;
381                } else {
382                    new_vec.push(expr);
383                }
384            }
385
386            if n_consts == 0 {
387                return Err(RuleNotApplicable);
388            }
389
390            new_vec.push(Expr::Atomic(
391                Default::default(),
392                Atom::Literal(Lit::Int(acc)),
393            ));
394            let new_product = Expr::Product(m.clone(), Moo::new(into_matrix_expr![new_vec]));
395
396            if acc == 0 {
397                // if safe, 0 * exprs ~> 0
398                // otherwise, just return 0* exprs
399                if is_semantically_safe(&new_product) {
400                    Ok(Reduction::pure(Expr::Atomic(
401                        Default::default(),
402                        Atom::Literal(Lit::Int(0)),
403                    )))
404                } else {
405                    Ok(Reduction::pure(new_product))
406                }
407            } else if n_consts == 1 {
408                // acc !=0, only one constant
409                Err(RuleNotApplicable)
410            } else {
411                // acc !=0, multiple constants found
412                Ok(Reduction::pure(new_product))
413            }
414        }
415
416        Expr::Min(m, e) => {
417            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
418                return Err(RuleNotApplicable);
419            };
420            let mut acc: Option<i32> = None;
421            let mut n_consts = 0;
422            let mut new_vec: Vec<Expr> = Vec::new();
423            for expr in vec {
424                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
425                    n_consts += 1;
426                    acc = match acc {
427                        Some(i) => {
428                            if i > x {
429                                Some(x)
430                            } else {
431                                Some(i)
432                            }
433                        }
434                        None => Some(x),
435                    };
436                } else {
437                    new_vec.push(expr);
438                }
439            }
440
441            if let Some(i) = acc {
442                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));
443            }
444
445            if n_consts <= 1 {
446                Err(RuleNotApplicable)
447            } else {
448                Ok(Reduction::pure(Expr::Min(
449                    m.clone(),
450                    Moo::new(into_matrix_expr![new_vec]),
451                )))
452            }
453        }
454
455        Expr::Max(m, e) => {
456            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
457                return Err(RuleNotApplicable);
458            };
459
460            let mut acc: Option<i32> = None;
461            let mut n_consts = 0;
462            let mut new_vec: Vec<Expr> = Vec::new();
463            for expr in vec {
464                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
465                    n_consts += 1;
466                    acc = match acc {
467                        Some(i) => {
468                            if i < x {
469                                Some(x)
470                            } else {
471                                Some(i)
472                            }
473                        }
474                        None => Some(x),
475                    };
476                } else {
477                    new_vec.push(expr);
478                }
479            }
480
481            if let Some(i) = acc {
482                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));
483            }
484
485            if n_consts <= 1 {
486                Err(RuleNotApplicable)
487            } else {
488                Ok(Reduction::pure(Expr::Max(
489                    m.clone(),
490                    Moo::new(into_matrix_expr![new_vec]),
491                )))
492            }
493        }
494        Expr::Not(_, e1) => {
495            let Expr::Imply(_, p, q) = e1.as_ref() else {
496                return Err(RuleNotApplicable);
497            };
498
499            if !is_semantically_safe(e1) {
500                return Err(RuleNotApplicable);
501            }
502
503            match (p.as_ref(), q.as_ref()) {
504                (_, Expr::Atomic(_, Atom::Literal(Lit::Bool(true)))) => {
505                    Ok(Reduction::pure(Expr::from(false)))
506                }
507                (_, Expr::Atomic(_, Atom::Literal(Lit::Bool(false)))) => {
508                    Ok(Reduction::pure(Moo::unwrap_or_clone(p.clone())))
509                }
510                (Expr::Atomic(_, Atom::Literal(Lit::Bool(true))), _) => {
511                    Ok(Reduction::pure(Expr::Not(Metadata::new(), q.clone())))
512                }
513                (Expr::Atomic(_, Atom::Literal(Lit::Bool(false))), _) => {
514                    Ok(Reduction::pure(Expr::from(false)))
515                }
516                _ => Err(RuleNotApplicable),
517            }
518        }
519        Expr::Or(m, e) => {
520            let Some(terms) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
521                return Err(RuleNotApplicable);
522            };
523
524            let mut has_changed = false;
525
526            // 2. boolean literals
527            let mut new_terms = vec![];
528            for expr in terms {
529                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {
530                    has_changed = true;
531
532                    // true ~~> entire or is true
533                    // false ~~> remove false from the or
534                    if x {
535                        return Ok(Reduction::pure(true.into()));
536                    }
537                } else {
538                    new_terms.push(expr);
539                }
540            }
541
542            // 2. check pairwise tautologies.
543            if check_pairwise_or_tautologies(&new_terms) {
544                return Ok(Reduction::pure(true.into()));
545            }
546
547            // 3. empty or ~~> false
548            if new_terms.is_empty() {
549                return Ok(Reduction::pure(false.into()));
550            }
551
552            if !has_changed {
553                return Err(RuleNotApplicable);
554            }
555
556            Ok(Reduction::pure(Expr::Or(
557                m.clone(),
558                Moo::new(into_matrix_expr![new_terms]),
559            )))
560        }
561        Expr::And(_, e) => {
562            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
563                return Err(RuleNotApplicable);
564            };
565            let mut new_vec: Vec<Expr> = Vec::new();
566            let mut has_const: bool = false;
567            for expr in vec {
568                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {
569                    has_const = true;
570                    if !x {
571                        return Ok(Reduction::pure(Expr::Atomic(
572                            Default::default(),
573                            Atom::Literal(Lit::Bool(false)),
574                        )));
575                    }
576                } else {
577                    new_vec.push(expr);
578                }
579            }
580
581            if !has_const {
582                Err(RuleNotApplicable)
583            } else {
584                Ok(Reduction::pure(Expr::And(
585                    Metadata::new(),
586                    Moo::new(into_matrix_expr![new_vec]),
587                )))
588            }
589        }
590
591        // similar to And, but booleans are returned wrapped in Root.
592        Expr::Root(_, es) => {
593            match es.as_slice() {
594                [] => Err(RuleNotApplicable),
595                // want to unwrap nested ands
596                [Expr::And(_, _)] => Ok(()),
597                // root([true]) / root([false]) are already evaluated
598                [_] => Err(RuleNotApplicable),
599                [_, _, ..] => Ok(()),
600            }?;
601
602            let mut new_vec: Vec<Expr> = Vec::new();
603            let mut has_changed: bool = false;
604            for expr in es {
605                match expr {
606                    Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) => {
607                        has_changed = true;
608                        if !x {
609                            // false
610                            return Ok(Reduction::pure(Expr::Root(
611                                Metadata::new(),
612                                vec![Expr::Atomic(
613                                    Default::default(),
614                                    Atom::Literal(Lit::Bool(false)),
615                                )],
616                            )));
617                        }
618                        // remove trues
619                    }
620
621                    // flatten ands in root
622                    Expr::And(_, vecs) => match Moo::unwrap_or_clone(vecs.clone()).unwrap_list() {
623                        Some(mut list) => {
624                            has_changed = true;
625                            new_vec.append(&mut list);
626                        }
627                        None => new_vec.push(expr.clone()),
628                    },
629                    _ => new_vec.push(expr.clone()),
630                }
631            }
632
633            if !has_changed {
634                Err(RuleNotApplicable)
635            } else {
636                if new_vec.is_empty() {
637                    new_vec.push(true.into());
638                }
639                Ok(Reduction::pure(Expr::Root(Metadata::new(), new_vec)))
640            }
641        }
642        Expr::Imply(_m, x, y) => {
643            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {
644                return if *x {
645                    // (true) -> y ~~> y
646                    Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())))
647                } else {
648                    // (false) -> y ~~> true
649                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
650                };
651            };
652
653            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {
654                return if *y {
655                    // x -> (true) ~~> true
656                    Ok(Reduction::pure(Expr::from(true)))
657                } else {
658                    // x -> (false) ~~> !x
659                    Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())))
660                };
661            };
662
663            // reflexivity: p -> p ~> true
664
665            // instead of checking syntactic equivalence of a possibly deep expression,
666            // let identical-CSE turn them into identical variables first. Then, check if they are
667            // identical variables.
668
669            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)
670            {
671                return Ok(Reduction::pure(true.into()));
672            }
673
674            Err(RuleNotApplicable)
675        }
676        Expr::Iff(_m, x, y) => {
677            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {
678                return if *x {
679                    // (true) <-> y ~~> y
680                    Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())))
681                } else {
682                    // (false) <-> y ~~> !y
683                    Ok(Reduction::pure(Expr::Not(Metadata::new(), y.clone())))
684                };
685            };
686            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {
687                return if *y {
688                    // x <-> (true) ~~> x
689                    Ok(Reduction::pure(Moo::unwrap_or_clone(x.clone())))
690                } else {
691                    // x <-> (false) ~~> !x
692                    Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())))
693                };
694            };
695
696            // reflexivity: p <-> p ~> true
697
698            // instead of checking syntactic equivalence of a possibly deep expression,
699            // let identical-CSE turn them into identical variables first. Then, check if they are
700            // identical variables.
701
702            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)
703            {
704                return Ok(Reduction::pure(true.into()));
705            }
706
707            Err(RuleNotApplicable)
708        }
709        Expr::Eq(_, x, y) => {
710            if let Some((eq_result, _)) = simplify_reflexive_comparison(x, y) {
711                Ok(Reduction::pure(Expr::Atomic(
712                    Metadata::new(),
713                    Atom::Literal(Lit::Bool(eq_result)),
714                )))
715            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()
716                && let Some((eq_result, _)) = simplify_comparison_with_literal(y, lit)
717            {
718                Ok(Reduction::pure(Expr::Atomic(
719                    Metadata::new(),
720                    Atom::Literal(Lit::Bool(eq_result)),
721                )))
722            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()
723                && let Some((eq_result, _)) = simplify_comparison_with_literal(x, lit)
724            {
725                Ok(Reduction::pure(Expr::Atomic(
726                    Metadata::new(),
727                    Atom::Literal(Lit::Bool(eq_result)),
728                )))
729            } else {
730                Err(RuleNotApplicable)
731            }
732        }
733        Expr::Neq(_, x, y) => {
734            if let Some((_, neq_result)) = simplify_reflexive_comparison(x, y) {
735                Ok(Reduction::pure(Expr::Atomic(
736                    Metadata::new(),
737                    Atom::Literal(Lit::Bool(neq_result)),
738                )))
739            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()
740                && let Some((_, neq_result)) = simplify_comparison_with_literal(y, lit)
741            {
742                Ok(Reduction::pure(Expr::Atomic(
743                    Metadata::new(),
744                    Atom::Literal(Lit::Bool(neq_result)),
745                )))
746            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()
747                && let Some((_, neq_result)) = simplify_comparison_with_literal(x, lit)
748            {
749                Ok(Reduction::pure(Expr::Atomic(
750                    Metadata::new(),
751                    Atom::Literal(Lit::Bool(neq_result)),
752                )))
753            } else {
754                Err(RuleNotApplicable)
755            }
756        }
757        Expr::Geq(_, _, _) => Err(RuleNotApplicable),
758        Expr::Leq(_, _, _) => Err(RuleNotApplicable),
759        Expr::Gt(_, _, _) => Err(RuleNotApplicable),
760        Expr::Lt(_, _, _) => Err(RuleNotApplicable),
761        Expr::SafeDiv(_, _, _) => Err(RuleNotApplicable),
762        Expr::UnsafeDiv(_, _, _) => Err(RuleNotApplicable),
763        Expr::Flatten(_, _, _) => Err(RuleNotApplicable), // TODO: check if anything can be done here
764        Expr::AllDiff(m, e) => {
765            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
766                return Err(RuleNotApplicable);
767            };
768
769            let mut consts: HashSet<i32> = HashSet::new();
770
771            // check for duplicate constant values which would fail the constraint
772            for expr in vec {
773                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr
774                    && !consts.insert(x)
775                {
776                    return Ok(Reduction::pure(Expr::Atomic(
777                        m.clone(),
778                        Atom::Literal(Lit::Bool(false)),
779                    )));
780                }
781            }
782
783            // nothing has changed
784            Err(RuleNotApplicable)
785        }
786        Expr::Neg(_, _) => Err(RuleNotApplicable),
787        Expr::Factorial(_, _) => Err(RuleNotApplicable),
788        Expr::AuxDeclaration(_, _, _) => Err(RuleNotApplicable),
789        Expr::UnsafeMod(_, _, _) => Err(RuleNotApplicable),
790        Expr::SafeMod(_, _, _) => Err(RuleNotApplicable),
791        Expr::UnsafePow(_, _, _) => Err(RuleNotApplicable),
792        Expr::SafePow(_, _, _) => Err(RuleNotApplicable),
793        Expr::Minus(_, _, _) => Err(RuleNotApplicable),
794        Expr::Card(_, _) => todo!(),
795
796        // As these are in a low level solver form, I'm assuming that these have already been
797        // simplified and partially evaluated.
798        Expr::FlatAllDiff(_, _) => Err(RuleNotApplicable),
799        Expr::FlatAbsEq(_, _, _) => Err(RuleNotApplicable),
800        Expr::FlatIneq(_, _, _, _) => Err(RuleNotApplicable),
801        Expr::FlatMinusEq(_, _, _) => Err(RuleNotApplicable),
802        Expr::FlatProductEq(_, _, _, _) => Err(RuleNotApplicable),
803        Expr::FlatSumLeq(_, _, _) => Err(RuleNotApplicable),
804        Expr::FlatSumGeq(_, _, _) => Err(RuleNotApplicable),
805        Expr::FlatWatchedLiteral(_, _, _) => Err(RuleNotApplicable),
806        Expr::FlatWeightedSumLeq(_, _, _, _) => Err(RuleNotApplicable),
807        Expr::FlatWeightedSumGeq(_, _, _, _) => Err(RuleNotApplicable),
808        Expr::MinionDivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),
809        Expr::MinionModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),
810        Expr::MinionPow(_, _, _, _) => Err(RuleNotApplicable),
811        Expr::MinionReify(_, _, _) => Err(RuleNotApplicable),
812        Expr::MinionReifyImply(_, _, _) => Err(RuleNotApplicable),
813        Expr::MinionWInIntervalSet(_, _, _) => Err(RuleNotApplicable),
814        Expr::MinionWInSet(_, _, _) => Err(RuleNotApplicable),
815        Expr::MinionElementOne(_, _, _, _) => Err(RuleNotApplicable),
816        Expr::SATInt(_, _, _, _) => Err(RuleNotApplicable),
817        Expr::PairwiseSum(_, _, _) => Err(RuleNotApplicable),
818        Expr::PairwiseProduct(_, _, _) => Err(RuleNotApplicable),
819        Expr::Active(_, _, _) => todo!(),
820        Expr::Defined(_, _) => todo!(),
821        Expr::Range(_, _) => todo!(),
822        Expr::Image(_, _, _) => todo!(),
823        Expr::ImageSet(_, _, _) => todo!(),
824        Expr::PreImage(_, _, _) => todo!(),
825        Expr::Inverse(_, _, _) => todo!(),
826        Expr::Restrict(_, _, _) => todo!(),
827        Expr::ToSet(_, _) => todo!(),
828        Expr::ToMSet(_, _) => todo!(),
829        Expr::ToRelation(_, _) => todo!(),
830        Expr::RelationProj(_, _, _) => todo!(),
831        Expr::Apart(_, _, _) => todo!(),
832        Expr::Together(_, _, _) => todo!(),
833        Expr::Participants(_, _) => todo!(),
834        Expr::Party(_, _, _) => todo!(),
835        Expr::Parts(_, _) => todo!(),
836        Expr::Subsequence(_, _, _) => todo!(),
837        Expr::Substring(_, _, _) => todo!(),
838        Expr::LexLt(_, _, _) => Err(RuleNotApplicable),
839        Expr::LexLeq(_, _, _) => Err(RuleNotApplicable),
840        Expr::LexGt(_, _, _) => Err(RuleNotApplicable),
841        Expr::LexGeq(_, _, _) => Err(RuleNotApplicable),
842        Expr::FlatLexLt(_, _, _) => Err(RuleNotApplicable),
843        Expr::FlatLexLeq(_, _, _) => Err(RuleNotApplicable),
844    }
845}
846
847/// Checks for tautologies involving pairs of terms inside an or, returning true if one is found.
848///
849/// This applies the following rules:
850///
851/// ```text
852/// (p->q) \/ (q->p) ~> true    [totality of implication]
853/// (p->q) \/ (p-> !q) ~> true  [conditional excluded middle]
854/// ```
855///
856fn check_pairwise_or_tautologies(or_terms: &[Expr]) -> bool {
857    // Collect terms that are structurally identical to the rule input.
858    // Then, try the rules on these terms, also checking the other conditions of the rules.
859
860    // stores (p,q) in p -> q
861    let mut p_implies_q: Vec<(&Expr, &Expr)> = vec![];
862
863    // stores (p,q) in p -> !q
864    let mut p_implies_not_q: Vec<(&Expr, &Expr)> = vec![];
865
866    for term in or_terms.iter() {
867        if let Expr::Imply(_, p, q) = term {
868            // we use identical_atom_to for equality later on, so these sets are mutually exclusive.
869            //
870            // in general however, p -> !q would be in p_implies_q as (p,!q)
871            if let Expr::Not(_, q_1) = q.as_ref() {
872                p_implies_not_q.push((p.as_ref(), q_1.as_ref()));
873            } else {
874                p_implies_q.push((p.as_ref(), q.as_ref()));
875            }
876        }
877    }
878
879    // `(p->q) \/ (q->p) ~> true    [totality of implication]`
880    for ((p1, q1), (q2, p2)) in iproduct!(p_implies_q.iter(), p_implies_q.iter()) {
881        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {
882            return true;
883        }
884    }
885
886    // `(p->q) \/ (p-> !q) ~> true`    [conditional excluded middle]
887    for ((p1, q1), (p2, q2)) in iproduct!(p_implies_q.iter(), p_implies_not_q.iter()) {
888        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {
889            return true;
890        }
891    }
892
893    false
894}
conjure_cp_core/ast/partial_eval.rs

conjure_cp_core/ast/
partial_eval.rs
