Lines
95.45 %
Functions
66.67 %
//! Normalising rules for `Neq` and `Eq`.
use conjure_cp::ast::{Expression as Expr, SymbolTable, Typeable};
use conjure_cp::rule_engine::{
ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,
};
use conjure_cp::ast::ReturnType::{Matrix, Set};
use conjure_cp::essence_expr;
/// Converts a negated `Neq` to an `Eq`
///
/// ```text
/// not(neq(x)) ~> eq(x)
/// ```
#[register_rule(("Base", 8800))]
fn negated_neq_to_eq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
match expr {
Expr::Not(_, a) => match a.as_ref() {
Expr::Neq(_, b, c) if (b.is_safe() && c.is_safe()) => {
Ok(Reduction::pure(essence_expr!(&b = &c)))
}
_ => Err(RuleNotApplicable),
},
/// Converts a negated `Eq` to an `Neq`
/// not(eq(x)) ~> neq(x)
/// don't want this to apply to sets
/// Also can't apply to matrices, since undefinedness between two matrices with different domains
/// causes a != b to actually have a different meaning than !(a = b)
fn negated_eq_to_neq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
Expr::Eq(_, b, c) if (b.is_safe() && c.is_safe()) => {
if matches!(b.as_ref().return_type(), Set(_) | Matrix(_)) {
return Err(RuleNotApplicable);
if matches!(c.as_ref().return_type(), Set(_) | Matrix(_)) {
Ok(Reduction::pure(essence_expr!(&b != &c)))