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()?;
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(),
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::SafeIndex(_, subject, indices) => {
228            // partially evaluate matrix literals indexed by a constant.
229
230            // subject must be a matrix literal
231            let (es, index_domain) = resolve_matrix_subject(subject).ok_or(RuleNotApplicable)?;
232
233            if indices.is_empty() {
234                return Err(RuleNotApplicable);
235            }
236
237            // the leading index must be fixed to a single value
238            let index = singleton_int_value(&indices[0]).ok_or(RuleNotApplicable)?;
239
240            // index domain must be a single integer range with a lower bound
241            if let Some(ranges) = index_domain.as_int_ground()
242                && ranges.len() == 1
243                && let Some(from) = ranges[0].low()
244            {
245                let zero_indexed_index = index - from;
246                let selected = es
247                    .get(zero_indexed_index as usize)
248                    .ok_or(RuleNotApplicable)?
249                    .clone();
250
251                if indices.len() == 1 {
252                    Ok(Reduction::pure(selected))
253                } else {
254                    Ok(Reduction::pure(Expr::SafeIndex(
255                        Metadata::new(),
256                        Moo::new(selected),
257                        indices[1..].to_vec(),
258                    )))
259                }
260            } else {
261                Err(RuleNotApplicable)
262            }
263        }
264        Expr::SafeSlice(_, _, _) => Err(RuleNotApplicable),
265        Expr::InDomain(_, x, domain) => {
266            if let Some(result) = simplify_in_domain(x, domain) {
267                Ok(Reduction::pure(Expr::Atomic(
268                    Metadata::new(),
269                    result.into(),
270                )))
271            } else if let Expr::Atomic(_, Atom::Reference(decl)) = x.as_ref() {
272                let decl_domain = decl
273                    .domain()
274                    .ok_or(RuleNotApplicable)?
275                    .resolve()
276                    .ok_or(RuleNotApplicable)?;
277                let domain = domain.resolve().ok_or(RuleNotApplicable)?;
278
279                let intersection = decl_domain
280                    .intersect(&domain)
281                    .map_err(|_| RuleNotApplicable)?;
282
283                // if the declaration's domain is a subset of domain, expr is always true.
284                if &intersection == decl_domain.as_ref() {
285                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
286                }
287                // if no elements of declaration's domain are in the domain (i.e. they have no
288                // intersection), expr is always false.
289                //
290                // Only check this when the intersection is a finite integer domain, as we
291                // currently don't have a way to check whether other domain kinds are empty or not.
292                //
293                // we should expand this to cover more domain types in the future.
294                else if let Ok(values_in_domain) = intersection.values_i32()
295                    && values_in_domain.is_empty()
296                {
297                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))
298                } else {
299                    Err(RuleNotApplicable)
300                }
301            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref() {
302                if domain
303                    .resolve()
304                    .ok_or(RuleNotApplicable)?
305                    .contains(lit)
306                    .ok()
307                    .ok_or(RuleNotApplicable)?
308                {
309                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
310                } else {
311                    Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))
312                }
313            } else {
314                Err(RuleNotApplicable)
315            }
316        }
317        Expr::Bubble(_, expr, cond) => {
318            // definition of bubble is "expr is valid as long as cond is true"
319            //
320            // check if cond is true and pop the bubble!
321            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) = cond.as_ref() {
322                Ok(Reduction::pure(Moo::unwrap_or_clone(expr.clone())))
323            } else {
324                Err(RuleNotApplicable)
325            }
326        }
327        Expr::Atomic(_, _) => Err(RuleNotApplicable),
328        Expr::ToInt(_, expression) => {
329            if expression.return_type() == ReturnType::Int {
330                Ok(Reduction::pure(Moo::unwrap_or_clone(expression.clone())))
331            } else {
332                Err(RuleNotApplicable)
333            }
334        }
335        Expr::Abs(m, e) => match e.as_ref() {
336            Expr::Neg(_, inner) => Ok(Reduction::pure(Expr::Abs(m.clone(), inner.clone()))),
337            _ => Err(RuleNotApplicable),
338        },
339        Expr::Sum(m, vec) => {
340            let vec = Moo::unwrap_or_clone(vec.clone())
341                .unwrap_list()
342                .ok_or(RuleNotApplicable)?;
343            let mut acc = 0;
344            let mut n_consts = 0;
345            let mut new_vec: Vec<Expr> = Vec::new();
346            for expr in vec {
347                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
348                    acc += x;
349                    n_consts += 1;
350                } else {
351                    new_vec.push(expr);
352                }
353            }
354            if acc != 0 {
355                new_vec.push(Expr::Atomic(
356                    Default::default(),
357                    Atom::Literal(Lit::Int(acc)),
358                ));
359            }
360
361            if n_consts <= 1 {
362                Err(RuleNotApplicable)
363            } else {
364                Ok(Reduction::pure(Expr::Sum(
365                    m.clone(),
366                    Moo::new(into_matrix_expr![new_vec]),
367                )))
368            }
369        }
370
371        Expr::Product(m, vec) => {
372            let mut acc = 1;
373            let mut n_consts = 0;
374            let mut new_vec: Vec<Expr> = Vec::new();
375            let vec = Moo::unwrap_or_clone(vec.clone())
376                .unwrap_list()
377                .ok_or(RuleNotApplicable)?;
378            for expr in vec {
379                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
380                    acc *= x;
381                    n_consts += 1;
382                } else {
383                    new_vec.push(expr);
384                }
385            }
386
387            if n_consts == 0 {
388                return Err(RuleNotApplicable);
389            }
390
391            new_vec.push(Expr::Atomic(
392                Default::default(),
393                Atom::Literal(Lit::Int(acc)),
394            ));
395            let new_product = Expr::Product(m.clone(), Moo::new(into_matrix_expr![new_vec]));
396
397            if acc == 0 {
398                // if safe, 0 * exprs ~> 0
399                // otherwise, just return 0* exprs
400                if is_semantically_safe(&new_product) {
401                    Ok(Reduction::pure(Expr::Atomic(
402                        Default::default(),
403                        Atom::Literal(Lit::Int(0)),
404                    )))
405                } else {
406                    Ok(Reduction::pure(new_product))
407                }
408            } else if n_consts == 1 {
409                // acc !=0, only one constant
410                Err(RuleNotApplicable)
411            } else {
412                // acc !=0, multiple constants found
413                Ok(Reduction::pure(new_product))
414            }
415        }
416
417        Expr::Min(m, e) => {
418            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
419                return Err(RuleNotApplicable);
420            };
421            let mut acc: Option<i32> = None;
422            let mut n_consts = 0;
423            let mut new_vec: Vec<Expr> = Vec::new();
424            for expr in vec {
425                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
426                    n_consts += 1;
427                    acc = match acc {
428                        Some(i) => {
429                            if i > x {
430                                Some(x)
431                            } else {
432                                Some(i)
433                            }
434                        }
435                        None => Some(x),
436                    };
437                } else {
438                    new_vec.push(expr);
439                }
440            }
441
442            if let Some(i) = acc {
443                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));
444            }
445
446            if n_consts <= 1 {
447                Err(RuleNotApplicable)
448            } else {
449                Ok(Reduction::pure(Expr::Min(
450                    m.clone(),
451                    Moo::new(into_matrix_expr![new_vec]),
452                )))
453            }
454        }
455
456        Expr::Max(m, e) => {
457            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
458                return Err(RuleNotApplicable);
459            };
460
461            let mut acc: Option<i32> = None;
462            let mut n_consts = 0;
463            let mut new_vec: Vec<Expr> = Vec::new();
464            for expr in vec {
465                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
466                    n_consts += 1;
467                    acc = match acc {
468                        Some(i) => {
469                            if i < x {
470                                Some(x)
471                            } else {
472                                Some(i)
473                            }
474                        }
475                        None => Some(x),
476                    };
477                } else {
478                    new_vec.push(expr);
479                }
480            }
481
482            if let Some(i) = acc {
483                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));
484            }
485
486            if n_consts <= 1 {
487                Err(RuleNotApplicable)
488            } else {
489                Ok(Reduction::pure(Expr::Max(
490                    m.clone(),
491                    Moo::new(into_matrix_expr![new_vec]),
492                )))
493            }
494        }
495        Expr::Not(_, e1) => {
496            let Expr::Imply(_, p, q) = e1.as_ref() else {
497                return Err(RuleNotApplicable);
498            };
499
500            if !is_semantically_safe(e1) {
501                return Err(RuleNotApplicable);
502            }
503
504            match (p.as_ref(), q.as_ref()) {
505                (_, Expr::Atomic(_, Atom::Literal(Lit::Bool(true)))) => {
506                    Ok(Reduction::pure(Expr::from(false)))
507                }
508                (_, Expr::Atomic(_, Atom::Literal(Lit::Bool(false)))) => {
509                    Ok(Reduction::pure(Moo::unwrap_or_clone(p.clone())))
510                }
511                (Expr::Atomic(_, Atom::Literal(Lit::Bool(true))), _) => {
512                    Ok(Reduction::pure(Expr::Not(Metadata::new(), q.clone())))
513                }
514                (Expr::Atomic(_, Atom::Literal(Lit::Bool(false))), _) => {
515                    Ok(Reduction::pure(Expr::from(false)))
516                }
517                _ => Err(RuleNotApplicable),
518            }
519        }
520        Expr::Or(m, e) => {
521            let Some(terms) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
522                return Err(RuleNotApplicable);
523            };
524
525            let mut has_changed = false;
526
527            // 2. boolean literals
528            let mut new_terms = vec![];
529            for expr in terms {
530                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {
531                    has_changed = true;
532
533                    // true ~~> entire or is true
534                    // false ~~> remove false from the or
535                    if x {
536                        return Ok(Reduction::pure(true.into()));
537                    }
538                } else {
539                    new_terms.push(expr);
540                }
541            }
542
543            // 2. check pairwise tautologies.
544            if check_pairwise_or_tautologies(&new_terms) {
545                return Ok(Reduction::pure(true.into()));
546            }
547
548            // 3. empty or ~~> false
549            if new_terms.is_empty() {
550                return Ok(Reduction::pure(false.into()));
551            }
552
553            if !has_changed {
554                return Err(RuleNotApplicable);
555            }
556
557            Ok(Reduction::pure(Expr::Or(
558                m.clone(),
559                Moo::new(into_matrix_expr![new_terms]),
560            )))
561        }
562        Expr::And(_, e) => {
563            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
564                return Err(RuleNotApplicable);
565            };
566            let mut new_vec: Vec<Expr> = Vec::new();
567            let mut has_const: bool = false;
568            for expr in vec {
569                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {
570                    has_const = true;
571                    if !x {
572                        return Ok(Reduction::pure(Expr::Atomic(
573                            Default::default(),
574                            Atom::Literal(Lit::Bool(false)),
575                        )));
576                    }
577                } else {
578                    new_vec.push(expr);
579                }
580            }
581
582            if !has_const {
583                Err(RuleNotApplicable)
584            } else {
585                Ok(Reduction::pure(Expr::And(
586                    Metadata::new(),
587                    Moo::new(into_matrix_expr![new_vec]),
588                )))
589            }
590        }
591
592        // similar to And, but booleans are returned wrapped in Root.
593        Expr::Root(_, es) => {
594            match es.as_slice() {
595                [] => Err(RuleNotApplicable),
596                // want to unwrap nested ands
597                [Expr::And(_, _)] => Ok(()),
598                // root([true]) / root([false]) are already evaluated
599                [_] => Err(RuleNotApplicable),
600                [_, _, ..] => Ok(()),
601            }?;
602
603            let mut new_vec: Vec<Expr> = Vec::new();
604            let mut has_changed: bool = false;
605            for expr in es {
606                match expr {
607                    Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) => {
608                        has_changed = true;
609                        if !x {
610                            // false
611                            return Ok(Reduction::pure(Expr::Root(
612                                Metadata::new(),
613                                vec![Expr::Atomic(
614                                    Default::default(),
615                                    Atom::Literal(Lit::Bool(false)),
616                                )],
617                            )));
618                        }
619                        // remove trues
620                    }
621
622                    // flatten ands in root
623                    Expr::And(_, vecs) => match Moo::unwrap_or_clone(vecs.clone()).unwrap_list() {
624                        Some(mut list) => {
625                            has_changed = true;
626                            new_vec.append(&mut list);
627                        }
628                        None => new_vec.push(expr.clone()),
629                    },
630                    _ => new_vec.push(expr.clone()),
631                }
632            }
633
634            if !has_changed {
635                Err(RuleNotApplicable)
636            } else {
637                if new_vec.is_empty() {
638                    new_vec.push(true.into());
639                }
640                Ok(Reduction::pure(Expr::Root(Metadata::new(), new_vec)))
641            }
642        }
643        Expr::Imply(_m, x, y) => {
644            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {
645                if *x {
646                    // (true) -> y ~~> y
647                    return Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())));
648                } else {
649                    // (false) -> y ~~> true
650                    return Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())));
651                }
652            };
653
654            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {
655                if *y {
656                    // x -> (true) ~~> true
657                    return Ok(Reduction::pure(Expr::from(true)));
658                } else {
659                    // x -> (false) ~~> !x
660                    return Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())));
661                }
662            };
663
664            // reflexivity: p -> p ~> true
665
666            // instead of checking syntactic equivalence of a possibly deep expression,
667            // let identical-CSE turn them into identical variables first. Then, check if they are
668            // identical variables.
669
670            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)
671            {
672                return Ok(Reduction::pure(true.into()));
673            }
674
675            Err(RuleNotApplicable)
676        }
677        Expr::Iff(_m, x, y) => {
678            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {
679                if *x {
680                    // (true) <-> y ~~> y
681                    return Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())));
682                } else {
683                    // (false) <-> y ~~> !y
684                    return Ok(Reduction::pure(Expr::Not(Metadata::new(), y.clone())));
685                }
686            };
687            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {
688                if *y {
689                    // x <-> (true) ~~> x
690                    return Ok(Reduction::pure(Moo::unwrap_or_clone(x.clone())));
691                } else {
692                    // x <-> (false) ~~> !x
693                    return Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())));
694                }
695            };
696
697            // reflexivity: p <-> p ~> true
698
699            // instead of checking syntactic equivalence of a possibly deep expression,
700            // let identical-CSE turn them into identical variables first. Then, check if they are
701            // identical variables.
702
703            if x.identical_atom_to(y.as_ref()) && is_semantically_safe(x) && is_semantically_safe(y)
704            {
705                return Ok(Reduction::pure(true.into()));
706            }
707
708            Err(RuleNotApplicable)
709        }
710        Expr::Eq(_, x, y) => {
711            if let Some((eq_result, _)) = simplify_reflexive_comparison(x, y) {
712                Ok(Reduction::pure(Expr::Atomic(
713                    Metadata::new(),
714                    Atom::Literal(Lit::Bool(eq_result)),
715                )))
716            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()
717                && let Some((eq_result, _)) = simplify_comparison_with_literal(y, lit)
718            {
719                Ok(Reduction::pure(Expr::Atomic(
720                    Metadata::new(),
721                    Atom::Literal(Lit::Bool(eq_result)),
722                )))
723            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()
724                && let Some((eq_result, _)) = simplify_comparison_with_literal(x, lit)
725            {
726                Ok(Reduction::pure(Expr::Atomic(
727                    Metadata::new(),
728                    Atom::Literal(Lit::Bool(eq_result)),
729                )))
730            } else {
731                Err(RuleNotApplicable)
732            }
733        }
734        Expr::Neq(_, x, y) => {
735            if let Some((_, neq_result)) = simplify_reflexive_comparison(x, y) {
736                Ok(Reduction::pure(Expr::Atomic(
737                    Metadata::new(),
738                    Atom::Literal(Lit::Bool(neq_result)),
739                )))
740            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()
741                && let Some((_, neq_result)) = simplify_comparison_with_literal(y, lit)
742            {
743                Ok(Reduction::pure(Expr::Atomic(
744                    Metadata::new(),
745                    Atom::Literal(Lit::Bool(neq_result)),
746                )))
747            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()
748                && let Some((_, neq_result)) = simplify_comparison_with_literal(x, lit)
749            {
750                Ok(Reduction::pure(Expr::Atomic(
751                    Metadata::new(),
752                    Atom::Literal(Lit::Bool(neq_result)),
753                )))
754            } else {
755                Err(RuleNotApplicable)
756            }
757        }
758        Expr::Geq(_, _, _) => Err(RuleNotApplicable),
759        Expr::Leq(_, _, _) => Err(RuleNotApplicable),
760        Expr::Gt(_, _, _) => Err(RuleNotApplicable),
761        Expr::Lt(_, _, _) => Err(RuleNotApplicable),
762        Expr::SafeDiv(_, _, _) => Err(RuleNotApplicable),
763        Expr::UnsafeDiv(_, _, _) => Err(RuleNotApplicable),
764        Expr::Flatten(_, _, _) => Err(RuleNotApplicable), // TODO: check if anything can be done here
765        Expr::AllDiff(m, e) => {
766            let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
767                return Err(RuleNotApplicable);
768            };
769
770            let mut consts: HashSet<i32> = HashSet::new();
771
772            // check for duplicate constant values which would fail the constraint
773            for expr in vec {
774                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr
775                    && !consts.insert(x)
776                {
777                    return Ok(Reduction::pure(Expr::Atomic(
778                        m.clone(),
779                        Atom::Literal(Lit::Bool(false)),
780                    )));
781                }
782            }
783
784            // nothing has changed
785            Err(RuleNotApplicable)
786        }
787        Expr::Neg(_, _) => Err(RuleNotApplicable),
788        Expr::Factorial(_, _) => Err(RuleNotApplicable),
789        Expr::AuxDeclaration(_, _, _) => Err(RuleNotApplicable),
790        Expr::UnsafeMod(_, _, _) => Err(RuleNotApplicable),
791        Expr::SafeMod(_, _, _) => Err(RuleNotApplicable),
792        Expr::UnsafePow(_, _, _) => Err(RuleNotApplicable),
793        Expr::SafePow(_, _, _) => Err(RuleNotApplicable),
794        Expr::Minus(_, _, _) => Err(RuleNotApplicable),
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::Defined(_, _) => todo!(),
820        Expr::Range(_, _) => todo!(),
821        Expr::Image(_, _, _) => todo!(),
822        Expr::ImageSet(_, _, _) => todo!(),
823        Expr::PreImage(_, _, _) => todo!(),
824        Expr::Inverse(_, _, _) => todo!(),
825        Expr::Restrict(_, _, _) => todo!(),
826        Expr::LexLt(_, _, _) => Err(RuleNotApplicable),
827        Expr::LexLeq(_, _, _) => Err(RuleNotApplicable),
828        Expr::LexGt(_, _, _) => Err(RuleNotApplicable),
829        Expr::LexGeq(_, _, _) => Err(RuleNotApplicable),
830        Expr::FlatLexLt(_, _, _) => Err(RuleNotApplicable),
831        Expr::FlatLexLeq(_, _, _) => Err(RuleNotApplicable),
832    }
833}
834
835/// Checks for tautologies involving pairs of terms inside an or, returning true if one is found.
836///
837/// This applies the following rules:
838///
839/// ```text
840/// (p->q) \/ (q->p) ~> true    [totality of implication]
841/// (p->q) \/ (p-> !q) ~> true  [conditional excluded middle]
842/// ```
843///
844fn check_pairwise_or_tautologies(or_terms: &[Expr]) -> bool {
845    // Collect terms that are structurally identical to the rule input.
846    // Then, try the rules on these terms, also checking the other conditions of the rules.
847
848    // stores (p,q) in p -> q
849    let mut p_implies_q: Vec<(&Expr, &Expr)> = vec![];
850
851    // stores (p,q) in p -> !q
852    let mut p_implies_not_q: Vec<(&Expr, &Expr)> = vec![];
853
854    for term in or_terms.iter() {
855        if let Expr::Imply(_, p, q) = term {
856            // we use identical_atom_to for equality later on, so these sets are mutually exclusive.
857            //
858            // in general however, p -> !q would be in p_implies_q as (p,!q)
859            if let Expr::Not(_, q_1) = q.as_ref() {
860                p_implies_not_q.push((p.as_ref(), q_1.as_ref()));
861            } else {
862                p_implies_q.push((p.as_ref(), q.as_ref()));
863            }
864        }
865    }
866
867    // `(p->q) \/ (q->p) ~> true    [totality of implication]`
868    for ((p1, q1), (q2, p2)) in iproduct!(p_implies_q.iter(), p_implies_q.iter()) {
869        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {
870            return true;
871        }
872    }
873
874    // `(p->q) \/ (p-> !q) ~> true`    [conditional excluded middle]
875    for ((p1, q1), (p2, q2)) in iproduct!(p_implies_q.iter(), p_implies_not_q.iter()) {
876        if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {
877            return true;
878        }
879    }
880
881    false
882}
conjure_cp_core/ast/partial_eval.rs

conjure_cp_core/ast/
partial_eval.rs
