Skip to content

Instantly share code, notes, and snippets.

@Robbepop
Created February 25, 2018 10:28
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Robbepop/d8a8b8d1b6a16b4747810bbdb33875dd to your computer and use it in GitHub Desktop.
Save Robbepop/d8a8b8d1b6a16b4747810bbdb33875dd to your computer and use it in GitHub Desktop.
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::*;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment