Lines
80.26 %
Functions
15 %
use std::collections::HashSet;
use crate::ast::Typeable;
use crate::{
ast::{Atom, Expression as Expr, Literal as Lit, Metadata, Moo, ReturnType},
into_matrix_expr,
rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, Reduction},
};
use itertools::iproduct;
pub fn run_partial_evaluator(expr: &Expr) -> ApplicationResult {
// NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this
// rule infinitely!
// This is why we always check whether we found a constant or not.
match expr {
Expr::Union(_, _, _) => Err(RuleNotApplicable),
Expr::In(_, _, _) => Err(RuleNotApplicable),
Expr::Intersect(_, _, _) => Err(RuleNotApplicable),
Expr::Supset(_, _, _) => Err(RuleNotApplicable),
Expr::SupsetEq(_, _, _) => Err(RuleNotApplicable),
Expr::Subset(_, _, _) => Err(RuleNotApplicable),
Expr::SubsetEq(_, _, _) => Err(RuleNotApplicable),
Expr::AbstractLiteral(_, _) => Err(RuleNotApplicable),
Expr::Comprehension(_, _) => Err(RuleNotApplicable),
Expr::AbstractComprehension(_, _) => Err(RuleNotApplicable),
Expr::DominanceRelation(_, _) => Err(RuleNotApplicable),
Expr::FromSolution(_, _) => Err(RuleNotApplicable),
Expr::Metavar(_, _) => Err(RuleNotApplicable),
Expr::UnsafeIndex(_, _, _) => Err(RuleNotApplicable),
Expr::UnsafeSlice(_, _, _) => Err(RuleNotApplicable),
Expr::Table(_, _, _) => Err(RuleNotApplicable),
Expr::SafeIndex(_, subject, indices) => {
// partially evaluate matrix literals indexed by a constant.
// subject must be a matrix literal
let (es, index_domain) = Moo::unwrap_or_clone(subject.clone())
.unwrap_matrix_unchecked()
.ok_or(RuleNotApplicable)?;
// must be indexing a 1d matrix.
//
// for n-d matrices, wait for the `remove_dimension_from_matrix_indexing` rule to run
// first. This reduces n-d indexing operations to 1d.
if indices.len() != 1 {
return Err(RuleNotApplicable);
}
// the index must be a number
let index: i32 = (&indices[0]).try_into().map_err(|_| RuleNotApplicable)?;
// index domain must be a single integer range with a lower bound
if let Some(ranges) = index_domain.as_int_ground()
&& ranges.len() == 1
&& let Some(from) = ranges[0].low()
{
let zero_indexed_index = index - from;
Ok(Reduction::pure(es[zero_indexed_index as usize].clone()))
} else {
Err(RuleNotApplicable)
Expr::SafeSlice(_, _, _) => Err(RuleNotApplicable),
Expr::InDomain(_, x, domain) => {
if let Expr::Atomic(_, Atom::Reference(decl)) = x.as_ref() {
let decl_domain = decl
.domain()
.ok_or(RuleNotApplicable)?
.resolve()
let domain = domain.resolve().ok_or(RuleNotApplicable)?;
let intersection = decl_domain
.intersect(&domain)
.map_err(|_| RuleNotApplicable)?;
// if the declaration's domain is a subset of domain, expr is always true.
if &intersection == decl_domain.as_ref() {
Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())))
// if no elements of declaration's domain are in the domain (i.e. they have no
// intersection), expr is always false.
// Only check this when the intersection is a finite integer domain, as we
// currently don't have a way to check whether other domain kinds are empty or not.
// we should expand this to cover more domain types in the future.
else if let Ok(values_in_domain) = intersection.values_i32()
&& values_in_domain.is_empty()
Ok(Reduction::pure(Expr::Atomic(Metadata::new(), false.into())))
} else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref() {
if domain
.contains(lit)
.ok()
Expr::Bubble(_, expr, cond) => {
// definition of bubble is "expr is valid as long as cond is true"
// check if cond is true and pop the bubble!
if let Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) = cond.as_ref() {
Ok(Reduction::pure(Moo::unwrap_or_clone(expr.clone())))
Expr::Atomic(_, _) => Err(RuleNotApplicable),
Expr::ToInt(_, expression) => {
if expression.return_type() == ReturnType::Int {
Ok(Reduction::pure(Moo::unwrap_or_clone(expression.clone())))
Expr::Abs(m, e) => match e.as_ref() {
Expr::Neg(_, inner) => Ok(Reduction::pure(Expr::Abs(m.clone(), inner.clone()))),
_ => Err(RuleNotApplicable),
},
Expr::Sum(m, vec) => {
let vec = Moo::unwrap_or_clone(vec.clone())
.unwrap_list()
let mut acc = 0;
let mut n_consts = 0;
let mut new_vec: Vec<Expr> = Vec::new();
for expr in vec {
if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {
acc += x;
n_consts += 1;
new_vec.push(expr);
if acc != 0 {
new_vec.push(Expr::Atomic(
Default::default(),
Atom::Literal(Lit::Int(acc)),
));
if n_consts <= 1 {
Ok(Reduction::pure(Expr::Sum(
m.clone(),
Moo::new(into_matrix_expr![new_vec]),
)))
Expr::Product(m, vec) => {
let mut acc = 1;
acc *= x;
if n_consts == 0 {
let new_product = Expr::Product(m.clone(), Moo::new(into_matrix_expr![new_vec]));
if acc == 0 {
// if safe, 0 * exprs ~> 0
// otherwise, just return 0* exprs
if new_product.is_safe() {
Ok(Reduction::pure(Expr::Atomic(
Atom::Literal(Lit::Int(0)),
Ok(Reduction::pure(new_product))
} else if n_consts == 1 {
// acc !=0, only one constant
// acc !=0, multiple constants found
Expr::Min(m, e) => {
let Some(vec) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
let mut acc: Option<i32> = None;
acc = match acc {
Some(i) => {
if i > x {
Some(x)
Some(i)
None => Some(x),
if let Some(i) = acc {
new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));
Ok(Reduction::pure(Expr::Min(
Expr::Max(m, e) => {
if i < x {
Ok(Reduction::pure(Expr::Max(
Expr::Not(_, _) => Err(RuleNotApplicable),
Expr::Or(m, e) => {
let Some(terms) = Moo::unwrap_or_clone(e.clone()).unwrap_list() else {
let mut has_changed = false;
// 2. boolean literals
let mut new_terms = vec![];
for expr in terms {
if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {
has_changed = true;
// true ~~> entire or is true
// false ~~> remove false from the or
if x {
return Ok(Reduction::pure(true.into()));
new_terms.push(expr);
// 2. check pairwise tautologies.
if check_pairwise_or_tautologies(&new_terms) {
// 3. empty or ~~> false
if new_terms.is_empty() {
return Ok(Reduction::pure(false.into()));
if !has_changed {
Ok(Reduction::pure(Expr::Or(
Moo::new(into_matrix_expr![new_terms]),
Expr::And(_, e) => {
let mut has_const: bool = false;
has_const = true;
if !x {
return Ok(Reduction::pure(Expr::Atomic(
Atom::Literal(Lit::Bool(false)),
)));
if !has_const {
Ok(Reduction::pure(Expr::And(
Metadata::new(),
// similar to And, but booleans are returned wrapped in Root.
Expr::Root(_, es) => {
match es.as_slice() {
[] => Err(RuleNotApplicable),
// want to unwrap nested ands
[Expr::And(_, _)] => Ok(()),
// root([true]) / root([false]) are already evaluated
[_] => Err(RuleNotApplicable),
[_, _, ..] => Ok(()),
}?;
let mut has_changed: bool = false;
for expr in es {
Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) => {
// false
return Ok(Reduction::pure(Expr::Root(
vec![Expr::Atomic(
)],
// remove trues
// flatten ands in root
Expr::And(_, vecs) => match Moo::unwrap_or_clone(vecs.clone()).unwrap_list() {
Some(mut list) => {
new_vec.append(&mut list);
None => new_vec.push(expr.clone()),
_ => new_vec.push(expr.clone()),
if new_vec.is_empty() {
new_vec.push(true.into());
Ok(Reduction::pure(Expr::Root(Metadata::new(), new_vec)))
Expr::Imply(_m, x, y) => {
if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {
if *x {
// (true) -> y ~~> y
return Ok(Reduction::pure(Moo::unwrap_or_clone(y.clone())));
// (false) -> y ~~> true
return Ok(Reduction::pure(Expr::Atomic(Metadata::new(), true.into())));
// reflexivity: p -> p ~> true
// instead of checking syntactic equivalence of a possibly deep expression,
// let identical-CSE turn them into identical variables first. Then, check if they are
// identical variables.
if x.identical_atom_to(y.as_ref()) {
Expr::Iff(_m, x, y) => {
// (true) <-> y ~~> y
// (false) <-> y ~~> !y
return Ok(Reduction::pure(Expr::Not(Metadata::new(), y.clone())));
if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {
if *y {
// x <-> (true) ~~> x
return Ok(Reduction::pure(Moo::unwrap_or_clone(x.clone())));
// x <-> (false) ~~> !x
return Ok(Reduction::pure(Expr::Not(Metadata::new(), x.clone())));
// reflexivity: p <-> p ~> true
Expr::Eq(_, _, _) => Err(RuleNotApplicable),
Expr::Neq(_, _, _) => Err(RuleNotApplicable),
Expr::Geq(_, _, _) => Err(RuleNotApplicable),
Expr::Leq(_, _, _) => Err(RuleNotApplicable),
Expr::Gt(_, _, _) => Err(RuleNotApplicable),
Expr::Lt(_, _, _) => Err(RuleNotApplicable),
Expr::SafeDiv(_, _, _) => Err(RuleNotApplicable),
Expr::UnsafeDiv(_, _, _) => Err(RuleNotApplicable),
Expr::Flatten(_, _, _) => Err(RuleNotApplicable), // TODO: check if anything can be done here
Expr::AllDiff(m, e) => {
let mut consts: HashSet<i32> = HashSet::new();
// check for duplicate constant values which would fail the constraint
if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr
&& !consts.insert(x)
// nothing has changed
Expr::Neg(_, _) => Err(RuleNotApplicable),
Expr::AuxDeclaration(_, _, _) => Err(RuleNotApplicable),
Expr::UnsafeMod(_, _, _) => Err(RuleNotApplicable),
Expr::SafeMod(_, _, _) => Err(RuleNotApplicable),
Expr::UnsafePow(_, _, _) => Err(RuleNotApplicable),
Expr::SafePow(_, _, _) => Err(RuleNotApplicable),
Expr::Minus(_, _, _) => Err(RuleNotApplicable),
// As these are in a low level solver form, I'm assuming that these have already been
// simplified and partially evaluated.
Expr::FlatAllDiff(_, _) => Err(RuleNotApplicable),
Expr::FlatAbsEq(_, _, _) => Err(RuleNotApplicable),
Expr::FlatIneq(_, _, _, _) => Err(RuleNotApplicable),
Expr::FlatMinusEq(_, _, _) => Err(RuleNotApplicable),
Expr::FlatProductEq(_, _, _, _) => Err(RuleNotApplicable),
Expr::FlatSumLeq(_, _, _) => Err(RuleNotApplicable),
Expr::FlatSumGeq(_, _, _) => Err(RuleNotApplicable),
Expr::FlatWatchedLiteral(_, _, _) => Err(RuleNotApplicable),
Expr::FlatWeightedSumLeq(_, _, _, _) => Err(RuleNotApplicable),
Expr::FlatWeightedSumGeq(_, _, _, _) => Err(RuleNotApplicable),
Expr::MinionDivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),
Expr::MinionModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),
Expr::MinionPow(_, _, _, _) => Err(RuleNotApplicable),
Expr::MinionReify(_, _, _) => Err(RuleNotApplicable),
Expr::MinionReifyImply(_, _, _) => Err(RuleNotApplicable),
Expr::MinionWInIntervalSet(_, _, _) => Err(RuleNotApplicable),
Expr::MinionWInSet(_, _, _) => Err(RuleNotApplicable),
Expr::MinionElementOne(_, _, _, _) => Err(RuleNotApplicable),
Expr::SATInt(_, _, _, _) => Err(RuleNotApplicable),
Expr::PairwiseSum(_, _, _) => Err(RuleNotApplicable),
Expr::PairwiseProduct(_, _, _) => Err(RuleNotApplicable),
Expr::Defined(_, _) => todo!(),
Expr::Range(_, _) => todo!(),
Expr::Image(_, _, _) => todo!(),
Expr::ImageSet(_, _, _) => todo!(),
Expr::PreImage(_, _, _) => todo!(),
Expr::Inverse(_, _, _) => todo!(),
Expr::Restrict(_, _, _) => todo!(),
Expr::LexLt(_, _, _) => Err(RuleNotApplicable),
Expr::LexLeq(_, _, _) => Err(RuleNotApplicable),
Expr::LexGt(_, _, _) => Err(RuleNotApplicable),
Expr::LexGeq(_, _, _) => Err(RuleNotApplicable),
Expr::FlatLexLt(_, _, _) => Err(RuleNotApplicable),
Expr::FlatLexLeq(_, _, _) => Err(RuleNotApplicable),
/// Checks for tautologies involving pairs of terms inside an or, returning true if one is found.
///
/// This applies the following rules:
/// ```text
/// (p->q) \/ (q->p) ~> true [totality of implication]
/// (p->q) \/ (p-> !q) ~> true [conditional excluded middle]
/// ```
fn check_pairwise_or_tautologies(or_terms: &[Expr]) -> bool {
// Collect terms that are structurally identical to the rule input.
// Then, try the rules on these terms, also checking the other conditions of the rules.
// stores (p,q) in p -> q
let mut p_implies_q: Vec<(&Expr, &Expr)> = vec![];
// stores (p,q) in p -> !q
let mut p_implies_not_q: Vec<(&Expr, &Expr)> = vec![];
for term in or_terms.iter() {
if let Expr::Imply(_, p, q) = term {
// we use identical_atom_to for equality later on, so these sets are mutually exclusive.
// in general however, p -> !q would be in p_implies_q as (p,!q)
if let Expr::Not(_, q_1) = q.as_ref() {
p_implies_not_q.push((p.as_ref(), q_1.as_ref()));
p_implies_q.push((p.as_ref(), q.as_ref()));
// `(p->q) \/ (q->p) ~> true [totality of implication]`
for ((p1, q1), (q2, p2)) in iproduct!(p_implies_q.iter(), p_implies_q.iter()) {
if p1.identical_atom_to(p2) && q1.identical_atom_to(q2) {
return true;
// `(p->q) \/ (p-> !q) ~> true` [conditional excluded middle]
for ((p1, q1), (p2, q2)) in iproduct!(p_implies_q.iter(), p_implies_not_q.iter()) {
false