Lines
84.91 %
Functions
25 %
use std::collections::HashSet;
use conjure_macros::register_rule;
use crate::ast::{Atom, Expression as Expr, Literal::*};
use crate::rule_engine::{ApplicationResult, Reduction};
use crate::Model;
#[register_rule(("Base",9000))]
fn partial_evaluator(expr: &Expr, _: &Model) -> ApplicationResult {
use conjure_core::rule_engine::ApplicationError::RuleNotApplicable;
use Expr::*;
// 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.clone() {
Bubble(_, _, _) => Err(RuleNotApplicable),
Atomic(_, _) => Err(RuleNotApplicable),
Sum(m, vec) => {
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(Int(x))) = expr {
acc += x;
n_consts += 1;
} else {
new_vec.push(expr);
}
if acc != 0 {
new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Int(acc))));
if n_consts <= 1 {
Err(RuleNotApplicable)
Ok(Reduction::pure(Sum(m, new_vec)))
Min(m, vec) => {
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(Int(i))));
Ok(Reduction::pure(Min(m, new_vec)))
Max(m, vec) => {
if i < x {
Ok(Reduction::pure(Max(m, new_vec)))
Not(_, _) => Err(RuleNotApplicable),
Or(m, vec) => {
let mut has_const: bool = false;
if let Expr::Atomic(_, Atom::Literal(Bool(x))) = expr {
has_const = true;
if x {
return Ok(Reduction::pure(Atomic(
Default::default(),
Atom::Literal(Bool(true)),
)));
if !has_const {
Ok(Reduction::pure(Or(m, new_vec)))
And(m, vec) => {
if !x {
Atom::Literal(Bool(false)),
Ok(Reduction::pure(And(m, new_vec)))
Eq(_, _, _) => Err(RuleNotApplicable),
Neq(_, _, _) => Err(RuleNotApplicable),
Geq(_, _, _) => Err(RuleNotApplicable),
Leq(_, _, _) => Err(RuleNotApplicable),
Gt(_, _, _) => Err(RuleNotApplicable),
Lt(_, _, _) => Err(RuleNotApplicable),
SafeDiv(_, _, _) => Err(RuleNotApplicable),
UnsafeDiv(_, _, _) => Err(RuleNotApplicable),
SumEq(m, vec, eq) => {
if let Expr::Atomic(_, Atom::Literal(Int(x))) = *eq {
// when rhs is a constant, move lhs constants to rhs
return Ok(Reduction::pure(SumEq(
m,
new_vec,
Box::new(Expr::Atomic(
Atom::Literal(Int(x - acc)),
)),
} else if acc != 0 {
Ok(Reduction::pure(SumEq(m, new_vec, eq)))
SumGeq(m, vec, geq) => {
if let Expr::Atomic(_, Atom::Literal(Int(x))) = *geq {
return Ok(Reduction::pure(SumGeq(
Ok(Reduction::pure(SumGeq(m, new_vec, geq)))
SumLeq(m, vec, leq) => {
if let Expr::Atomic(_, Atom::Literal(Int(x))) = *leq {
return Ok(Reduction::pure(SumLeq(
Ok(Reduction::pure(SumLeq(m, new_vec, leq)))
DivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),
Ineq(_, _, _, _) => Err(RuleNotApplicable),
AllDiff(m, vec) => {
let mut consts: HashSet<i32> = HashSet::new();
// check for duplicate constant values which would fail the constraint
for expr in &vec {
if !consts.insert(*x) {
return Ok(Reduction::pure(Expr::Atomic(m, Atom::Literal(Bool(false)))));
// nothing has changed
WatchedLiteral(_, _, _) => Err(RuleNotApplicable),
Reify(_, _, _) => Err(RuleNotApplicable),
AuxDeclaration(_, _, _) => Err(RuleNotApplicable),
UnsafeMod(_, _, _) => Err(RuleNotApplicable),
SafeMod(_, _, _) => Err(RuleNotApplicable),
ModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),