update the simplifier

Author: ekiwi

patronus/src/expr/simplify.rs

@@ -401,9 +401,6 @@ fn simplify_sum_of_products(
         match (prods[0], prods[1]) {
             // !a & b | a & !b
             ((false, true), (true, false)) => Some(ctx.xor(a, b)),
-            // !a & !b | a & b
-            // TODO: this currently cannot be triggered, because !a & !b gets converted with demorgan first!
-            ((false, false), (true, true)) => Some(ctx.equal(a, b)),
             _ => None,
         }
     } else {

patronus/tests/simplify.rs

@@ -44,6 +44,14 @@ fn test_simplify_and() {
         "and(not(and(not(a:bv<3>), b:bv<3>)), not(and(not(b), a)))",
         "not(xor(a:bv<3>, b:bv<3>))",
     );
+    ts(
+        "not(and(not(and(not(a:bv<3>), b:bv<3>)), not(and(not(b), a))))",
+        "xor(a:bv<3>, b:bv<3>)",
+    );
+    ts(
+        "not(and(not(and(b:bv<3>, not(a:bv<3>))), not(and(not(b), a))))",
+        "xor(b:bv<3>, a:bv<3>)",
+    );
 }
 
 #[test]
@@ -68,9 +76,6 @@ fn test_simplify_or() {
         "or(and(not(a:bv<3>), b:bv<3>), and(not(b), a))",
         "xor(a:bv<3>, b:bv<3>)",
     );
-
-    // equality truth table (sum of products)
-    // ts("or(and(a:bv<3>, b:bv<3>), and(not(b), not(a)))", "eq(a:bv<3>, b:bv<3>)");
 }
 
 #[test]