sca: exhaustive check for testing

ekiwi · ekiwi · commit 90fe8c9317cf · 2026-02-12T12:03:56.000-05:00
diff --git a/patronus-sca/src/lib.rs b/patronus-sca/src/lib.rs
@@ -5,10 +5,9 @@
 use baa::{BitVecOps, BitVecValue, BitVecValueRef};
 use patronus::expr::{
     Context, DenseExprMetaData, Expr, ExprRef, ForEachChild, SerializableIrNode, Simplifier,
-    TypeCheck, WidthInt, count_expr_uses, simplify_single_expression, traversal,
+    TypeCheck, WidthInt, count_expr_uses, traversal,
 };
 use polysub::{Coef, Term, VarIndex};
-use rustc_hash::FxHashMap;
 use std::collections::VecDeque;
 use std::fmt::{Display, Formatter};
 
@@ -85,24 +84,15 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
     var_roots.sort();
 
     let m = spec.get_mod();
-    println!("MOD={m:?} ({} bits)", m.bits());
     let one: DefaultCoef = Coef::from_i64(1, m);
-    println!("one = {one:?}");
     let minus_one: DefaultCoef = Coef::from_i64(-1, m);
-    println!("minus_one = {minus_one:?}");
     let minus_two: DefaultCoef = Coef::from_i64(-2, m);
     // first, we count how often expressions are used
     let roots: Vec<_> = todo.iter().map(|(_, e)| *e).collect();
     let mut uses = count_expr_uses(ctx, roots);
     let mut replaced = vec![];
 
     while let Some((output_var, gate)) = todo.pop_back() {
-        println!(
-            "{output_var}, {}, {:?} ({})",
-            expr_to_var(gate) == output_var,
-            &ctx[gate],
-            spec.size()
-        );
         replaced.push(output_var);
 
         let add_children = match ctx[gate].clone() {
@@ -171,7 +161,6 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
                 }
             });
         }
-        println!("{spec}");
     }
 
     println!("Roots: {var_roots:?}");
@@ -183,7 +172,7 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
     use patronus::expr::ExprMap;
     let mut still_used: Vec<_> = uses
         .iter()
-        .filter(|(k, v)| **v > 0)
+        .filter(|(_, v)| **v > 0)
         .map(|(k, _)| expr_to_var(k))
         .collect();
     still_used.sort();
@@ -274,7 +263,7 @@ fn build_bottom_up_poly(ctx: &mut Context, e: ExprRef) -> Poly {
     poly
 }
 
-#[derive(Debug, Clone, PartialEq)]
+#[derive(Debug, Clone, Copy, PartialEq)]
 pub struct ScaEqualityProblem {
     equality: ExprRef,
     gate_level: ExprRef,
@@ -486,11 +475,10 @@ impl<'a, 'b> Display for PrettyPoly<'a, 'b> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use patronus::expr::{eval_bv_expr, eval_expr, simplify_single_expression};
-    use patronus::smt::{SmtCommand, read_command, serialize_cmd};
+    use patronus::expr::{eval_bv_expr, find_symbols, simplify_single_expression};
+    use patronus::smt::{SmtCommand, read_command};
     use rustc_hash::FxHashMap;
-    use std::io::{BufReader, BufWriter};
-    use std::ptr::eq;
+    use std::io::BufReader;
 
     fn read_first_assert_expr(
         ctx: &mut Context,
@@ -516,7 +504,13 @@ mod tests {
         let candidates = find_sca_simplification_candidates(&ctx, e);
         let simplified: Vec<_> = candidates
             .into_iter()
-            .flat_map(|c| simplify_word_level_equality(&mut ctx, c))
+            .flat_map(|p| {
+                let exhaustive = is_eq_exhaustive(&ctx, p.clone());
+                let sca_based = simplify_word_level_equality(&mut ctx, p).unwrap();
+                let sca_based_bool = ctx[sca_based].is_true();
+                assert_eq!(exhaustive, sca_based_bool);
+                Some(sca_based)
+            })
             .collect();
         if simplified.is_empty() {
             None
@@ -551,7 +545,70 @@ mod tests {
 
     /// Performs an exhaustive check of all input values
     fn is_eq_exhaustive(ctx: &Context, p: ScaEqualityProblem) -> bool {
-        todo!()
+        let word_symbols = find_symbols(ctx, p.word_level);
+        let gate_symbols = find_symbols(ctx, p.word_level);
+        debug_assert_eq!(word_symbols, gate_symbols);
+        let inputs: Vec<_> = word_symbols
+            .iter()
+            .map(|&s| {
+                let width = s.get_bv_type(ctx).unwrap();
+                debug_assert!(width <= 16);
+                let max_value = (1u64 << width) - 1;
+                (
+                    ctx[s].get_symbol_name(ctx).unwrap().to_string(),
+                    s,
+                    width,
+                    max_value,
+                )
+            })
+            .collect();
+
+        let mut values = vec![0u64; inputs.len()];
+        let max_values: Vec<_> = inputs.iter().map(|(_, _, _, v)| *v).collect();
+
+        let mut count = 0;
+        while values != max_values {
+            count += 1;
+            // perform check
+            let symbols: Vec<_> = inputs
+                .iter()
+                .zip(values.iter())
+                .map(|((_, s, w, _), v)| (*s, BitVecValue::from_u64(*v, *w)))
+                .collect();
+
+            let word_value = eval_bv_expr(&ctx, symbols.as_slice(), p.word_level);
+            let gate_value = eval_bv_expr(&ctx, symbols.as_slice(), p.gate_level);
+            let is_equal = eval_bv_expr(&ctx, symbols.as_slice(), p.equality);
+
+            if !is_equal.is_true() {
+                let syms: Vec<_> = inputs
+                    .iter()
+                    .zip(values.iter())
+                    .map(|((n, _, _, _), v)| format!("{n}={v}"))
+                    .collect();
+                println!(
+                    "Not equal! GATE: {} =/= WORD: {} w/ {}",
+                    gate_value.to_dec_str(),
+                    word_value.to_dec_str(),
+                    syms.join(", ")
+                );
+                return false;
+            }
+
+            // increment
+            for (value, max_value) in values.iter_mut().zip(max_values.iter()) {
+                debug_assert!(*value <= *max_value);
+                if *value == *max_value {
+                    *value = 0;
+                    // set to zero and go to next "digit"
+                } else {
+                    *value += 1;
+                    break; // done
+                }
+            }
+        }
+        println!("expressions appear to be equivalent after {count} iterations");
+        true
     }
 
     #[test]
@@ -578,11 +635,10 @@ mod tests {
         let gate_level = ctx.concat(c0, s0);
         let equality = ctx.equal(word_level, gate_level);
 
-        let problem = ScaEqualityProblem {
-            equality,
-            gate_level,
-            word_level,
-        };
+        let problem = find_sca_simplification_candidates(&ctx, equality)[0];
+
+        // manually check that our problem is actually correct
+        assert!(is_eq_exhaustive(&ctx, problem));
 
         let result = simplify_word_level_equality(&mut ctx, problem).unwrap();
         assert_eq!(result, ctx.get_true());
@@ -604,30 +660,10 @@ mod tests {
         let gate_level = ctx.concat(gate_level_1, gate_level_0);
         let equality = ctx.equal(word_level, gate_level);
 
-        // manually check that our problem is actually correct
-        for a_value in 0..3 {
-            for b_value in 0..3 {
-                let symbols = [
-                    (a, BitVecValue::from_u64(a_value, 2)),
-                    (b, BitVecValue::from_u64(b_value, 2)),
-                ];
-                let word_value = eval_bv_expr(&ctx, symbols.as_slice(), word_level);
-                let gate_value = eval_bv_expr(&ctx, symbols.as_slice(), gate_level);
-                let is_equal = eval_bv_expr(&ctx, symbols.as_slice(), equality);
-                assert!(
-                    is_equal.is_true(),
-                    "a={a_value}, b={b_value}, gate={}, word={}",
-                    gate_value.to_dec_str(),
-                    word_value.to_dec_str()
-                );
-            }
-        }
+        let problem = find_sca_simplification_candidates(&ctx, equality)[0];
 
-        let problem = ScaEqualityProblem {
-            equality,
-            gate_level,
-            word_level,
-        };
+        // manually check that our problem is actually correct
+        assert!(is_eq_exhaustive(&ctx, problem));
 
         let result = simplify_word_level_equality(&mut ctx, problem).unwrap();
         assert_eq!(result, ctx.get_true());
diff --git a/patronus/src/expr.rs b/patronus/src/expr.rs
@@ -14,7 +14,7 @@ mod transform;
 pub mod traversal;
 mod types;
 
-pub use analysis::{UseCountInt, count_expr_uses, update_expr_child_uses};
+pub use analysis::{UseCountInt, count_expr_uses, find_symbols, update_expr_child_uses};
 pub use context::{Builder, Context, ExprRef, StringRef};
 pub use eval::{SymbolValueStore, eval_array_expr, eval_bv_expr, eval_expr};
 pub use foreach::ForEachChild;
diff --git a/patronus/src/expr/analysis.rs b/patronus/src/expr/analysis.rs
@@ -3,7 +3,8 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
-use crate::expr::{Context, ExprMap, ExprRef, ForEachChild, SparseExprMap};
+use crate::expr::{Context, ExprMap, ExprRef, ForEachChild, SparseExprMap, traversal};
+use rustc_hash::FxHashSet;
 
 pub type UseCountInt = u16;
 
@@ -24,6 +25,17 @@ pub fn count_expr_uses(ctx: &Context, roots: Vec<ExprRef>) -> impl ExprMap<UseCo
     use_count
 }
 
+/// Returns all symbols in the given expression.
+pub fn find_symbols(ctx: &Context, e: ExprRef) -> FxHashSet<ExprRef> {
+    let mut out = FxHashSet::default();
+    traversal::bottom_up(ctx, e, |ctx, e, _| {
+        if ctx[e].is_symbol() {
+            out.insert(e);
+        }
+    });
+    out
+}
+
 /// Increments the use counts for all children of the expression `expr` and
 /// adds any child encountered for the first time to the `todo` list.
 #[inline]
diff --git a/python/src/smt.rs b/python/src/smt.rs
@@ -38,16 +38,6 @@ impl SolverCtx {
     }
 }
 
-fn find_symbols(ctx: &Context, e: patronus::expr::ExprRef) -> FxHashSet<patronus::expr::ExprRef> {
-    let mut out = FxHashSet::default();
-    patronus::expr::traversal::bottom_up(ctx, e, |ctx, e, _| {
-        if ctx[e].is_symbol() {
-            out.insert(e);
-        }
-    });
-    out
-}
-
 #[pymethods]
 impl SolverCtx {
     #[pyo3(signature = (*assertions))]
@@ -86,7 +76,7 @@ impl SolverCtx {
         let ctx = ctx_guard.deref();
         let a = assertion.0;
         // scan the expression for any unknown symbols and declare them
-        let symbols = find_symbols(ctx, a);
+        let symbols = patronus::expr::find_symbols(ctx, a);
         for symbol in symbols.into_iter() {
             let tpe = ctx[symbol].get_type(ctx);
             let name = ctx[symbol].get_symbol_name(ctx).unwrap();
