simplification_bool_lowering.rs

use ast2::prelude::*;
use simplifier::prelude::*;

pub mod prelude {
    pub use super::BoolReducer;
}

/// This simplification procedure dissolves symbolic tautologies or contradictions
/// for boolean expressions.
/// 
/// This works best if used after an expression normalization transformation and
/// might be expensive for deeply nested expression trees that have many similarities.
#[derive(Debug, Default, Copy, Clone, PartialEq, Eq, Hash)]
pub struct BoolReducer;

impl AutoImplAnyTransformer for BoolReducer {}

impl Transformer for BoolReducer {
    fn transform_xor(&self, xor: expr::Xor) -> TransformOutcome {
        TransformOutcome::identity(xor)
    }

    fn transform_implies(&self, implies: expr::Implies) -> TransformOutcome {
        let (lhs, rhs) = implies.childs.into_childs_pair();
        return TransformOutcome::transformed(
            expr::Or::binary(unsafe{ expr::Not::new_unchecked(lhs) }, rhs)
                .expect("Since a and b are both childs expressions of an implies
                         expressions they are boolean expressions and thus creating
                         an or-expression of them cannot fail."))
    }
}

#[cfg(test)]
mod tests {
    // use super::*;
}