simplify: detect xor

Author: ekiwi

patronus/src/expr.rs

@@ -28,6 +28,5 @@ pub use serialize::SerializableIrNode;
 pub(crate) use serialize::{serialize_expr, serialize_expr_ref};
 pub(crate) use simplify::simplify;
 pub use simplify::{Simplifier, simplify_single_expression};
-pub use transform::simple_transform_expr;
-pub(crate) use transform::{ExprTransformMode, do_transform_expr};
+pub use transform::{ExprTransformMode, do_transform_expr, simple_transform_expr};
 pub use types::{TypeCheck, TypeCheckError};

patronus/src/expr/simplify.rs

@@ -103,6 +103,14 @@ impl<T: ExprMap<Option<ExprRef>>> Simplifier<T> {
     }
 }
 
+impl<T: ExprMap<Option<ExprRef>> + Default> Default for Simplifier<T> {
+    fn default() -> Self {
+        Self {
+            cache: T::default(),
+        }
+    }
+}
+
 /// Simplifies one expression (not its children)
 pub(crate) fn simplify(ctx: &mut Context, expr: ExprRef, children: &[ExprRef]) -> Option<ExprRef> {
     match (ctx[expr].clone(), children) {
@@ -324,6 +332,17 @@ fn simplify_bv_and(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef>
                     let or = ctx.or(*a, *b);
                     Some(ctx.not(or))
                 }
+                // or(a, b) & !and(a,b) -> a xor b
+                (Expr::BVOr(a, b, _), Expr::BVNot(n, _))
+                | (Expr::BVNot(n, _), Expr::BVOr(a, b, _)) => {
+                    if let Expr::BVAnd(c, d, _) = &ctx[*n]
+                        && ((a == c && b == d) || (a == d && b == c))
+                    {
+                        Some(ctx.xor(*a, *b))
+                    } else {
+                        None
+                    }
+                }
                 _ => None,
             }
         }

patronus/src/expr/transform.rs

@@ -30,7 +30,7 @@ pub fn simple_transform_expr(
 }
 
 #[inline]
-pub(crate) fn do_transform_expr<T: ExprMap<Option<ExprRef>>>(
+pub fn do_transform_expr<T: ExprMap<Option<ExprRef>>>(
     ctx: &mut Context,
     mode: ExprTransformMode,
     transformed: &mut T,