simplifier: fix wrong de morgan rewrite

Author: ekiwi

patronus-sca/src/lib.rs

@@ -506,7 +506,7 @@ impl<'a, 'b> Display for PrettyPoly<'a, 'b> {
 mod tests {
     use super::*;
     use patronus::expr::{eval_bv_expr, find_symbols};
-    use patronus::smt::{SmtCommand, read_command};
+    use patronus::smt::{BITWUZLA, Logic, SmtCommand, Solver, SolverContext, read_command};
     use rustc_hash::FxHashMap;
     use std::io::BufReader;
 
@@ -630,33 +630,6 @@ mod tests {
         true
     }
 
-    #[test]
-    fn test_coward_three_add_with_rewrite_based_simplifier() {
-        // there might be a bug in our rewrite rules
-        let filename = "../inputs/coward/add_three.4_bit.smt2";
-        let mut ctx = Context::default();
-        let e = read_first_assert_expr(&mut ctx, filename).unwrap();
-        let p = find_sca_simplification_candidates(&ctx, e)[0];
-        // assert!(is_eq_exhaustive(&ctx, p));
-
-        let mut simplifier = Simplifier::new(DenseExprMetaData::default());
-        let simplified_gate = simplifier.simplify(&mut ctx, p.gate_level);
-        println!(
-            "gate[2] = {}",
-            extract_bit(&mut ctx, p.gate_level, 2).serialize_to_str(&ctx)
-        );
-        println!(
-            "gate[2] = {}",
-            extract_bit(&mut ctx, simplified_gate, 2).serialize_to_str(&ctx)
-        );
-        let simplified_p = ScaEqualityProblem {
-            equality: p.equality,
-            gate_level: simplified_gate,
-            word_level: p.word_level,
-        };
-        assert!(is_eq_exhaustive(&ctx, simplified_p));
-    }
-
     #[test]
     fn test_full_adder() {
         let mut ctx = Context::default();

patronus/src/expr/context.rs

@@ -244,6 +244,11 @@ impl Context {
     pub fn ones(&mut self, width: WidthInt) -> ExprRef {
         self.bv_lit(&BitVecValue::ones(width))
     }
+
+    pub fn distinct(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
+        let is_eq = self.equal(a, b);
+        self.not(is_eq)
+    }
     pub fn equal(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
         debug_assert_eq!(a.get_type(self), b.get_type(self));
         if a.get_type(self).is_bit_vector() {

patronus/src/expr/simplify.rs

@@ -4,11 +4,12 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use super::{
-    BVLitValue, Context, Expr, ExprMap, ExprRef, SparseExprMap, TypeCheck, WidthInt,
-    do_transform_expr,
+    BVLitValue, Context, Expr, ExprMap, ExprRef, SerializableIrNode, SparseExprMap, TypeCheck,
+    WidthInt, do_transform_expr, find_symbols,
 };
 use crate::expr::meta::get_fixed_point;
 use crate::expr::transform::ExprTransformMode;
+use crate::smt::{CheckSatResponse, SolverContext};
 use baa::BitVecOps;
 use smallvec::{SmallVec, smallvec};
 
@@ -38,6 +39,68 @@ impl<T: ExprMap<Option<ExprRef>>> Simplifier<T> {
         );
         get_fixed_point(&mut self.cache, e).unwrap()
     }
+
+    /// Uses an SMT solver to check all simplification steps that have been made with this Simplifier.
+    /// Returns the number of incorrect simplifications.
+    pub fn verify_simplification(
+        &self,
+        ctx: &mut Context,
+        solver: &mut impl SolverContext,
+    ) -> crate::smt::Result<usize> {
+        let mut incorrect = 0;
+        let mut correct = 0;
+        for (key, &value) in self.cache.iter() {
+            if let Some(simplified) = value {
+                let key_symbols = find_symbols(ctx, key);
+                let simpl_symbols = find_symbols(ctx, simplified);
+                let symbols: Vec<_> = key_symbols.union(&simpl_symbols).cloned().collect();
+                solver.push()?;
+                for &sym in symbols.iter() {
+                    solver.declare_const(ctx, sym)?;
+                }
+                let not_eq = ctx.distinct(key, simplified);
+                solver.assert(ctx, not_eq)?;
+                match solver.check_sat()? {
+                    CheckSatResponse::Sat => {
+                        let key_value = solver.get_value(ctx, key)?;
+                        let simplified_value = solver.get_value(ctx, simplified)?;
+                        println!(
+                            "{} ({}) =/= ({}) {}",
+                            key.serialize_to_str(ctx),
+                            key_value.serialize_to_str(ctx),
+                            simplified_value.serialize_to_str(ctx),
+                            simplified.serialize_to_str(ctx)
+                        );
+                        let mut syms = vec![];
+                        for &sym in symbols.iter() {
+                            let value = solver.get_value(ctx, sym)?;
+                            syms.push(format!(
+                                "{}={}",
+                                sym.serialize_to_str(ctx),
+                                value.serialize_to_str(ctx)
+                            ));
+                        }
+                        println!(" w/ {}", syms.join(", "));
+                        incorrect += 1;
+                    }
+                    CheckSatResponse::Unsat => {
+                        correct += 1;
+                    } // OK
+                    CheckSatResponse::Unknown => {} // OK
+                }
+
+                solver.pop()?;
+            }
+        }
+        if incorrect > 0 {
+            println!(
+                "{incorrect} / {} simplifications were incorrect. See log.",
+                incorrect + correct
+            );
+        }
+
+        Ok(incorrect)
+    }
 }
 
 /// Simplifies one expression (not its children)
@@ -254,8 +317,11 @@ fn simplify_bv_and(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef>
                 // a & !a -> 0
                 (Expr::BVNot(inner, w), _) if *inner == b => Some(ctx.zero(*w)),
                 (_, Expr::BVNot(inner, w)) if *inner == a => Some(ctx.zero(*w)),
-                // !a & !b -> a | b
-                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => Some(ctx.or(*a, *b)),
+                // !a & !b -> !(a | b)
+                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => {
+                    let or = ctx.or(*a, *b);
+                    Some(ctx.not(or))
+                }
                 _ => None,
             }
         }
@@ -290,8 +356,11 @@ fn simplify_bv_or(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef>
                 // a | !a -> 1
                 (Expr::BVNot(inner, w), _) if *inner == b => Some(ctx.ones(*w)),
                 (_, Expr::BVNot(inner, w)) if *inner == a => Some(ctx.ones(*w)),
-                // !a | !b -> a & b
-                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => Some(ctx.and(*a, *b)),
+                // !a | !b -> !(a & b)
+                (Expr::BVNot(a, _), Expr::BVNot(b, _)) => {
+                    let and = ctx.and(*a, *b);
+                    Some(ctx.not(and))
+                }
                 _ => None,
             }
         }

patronus/tests/simplify.rs

@@ -34,7 +34,10 @@ fn test_simplify_and() {
     ts("and(not(a : bv<1>), a)", "false");
 
     // de morgan
-    ts("and(not(a:bv<3>), not(b:bv<3>))", "or(a:bv<3>, b:bv<3>)")
+    ts(
+        "and(not(a:bv<3>), not(b:bv<3>))",
+        "not(or(a:bv<3>, b:bv<3>))",
+    )
 }
 
 #[test]
@@ -49,7 +52,10 @@ fn test_simplify_or() {
     ts("or(not(a : bv<1>), a)", "true");
 
     // de morgan
-    ts("or(not(a:bv<3>), not(b:bv<3>))", "and(a:bv<3>, b:bv<3>)")
+    ts(
+        "or(not(a:bv<3>), not(b:bv<3>))",
+        "not(and(a:bv<3>, b:bv<3>))",
+    )
 }
 
 #[test]