sca: backwards substitution terminates, but with unexpected result

Author: ekiwi

patronus-sca/Cargo.toml

@@ -13,4 +13,4 @@ rust-version.workspace = true
 patronus = { path = "../patronus" }
 baa = {version = "0.17.1", features = ["bigint"]}
 rustc-hash.workspace = true
-polysub = "0.1.7"
+polysub = "0.1.8"

patronus-sca/src/lib.rs

@@ -6,7 +6,7 @@ use baa::{BitVecOps, BitVecValue, BitVecValueRef};
 use patronus::expr::traversal::TraversalCmd;
 use patronus::expr::{
     Context, DenseExprMetaData, Expr, ExprRef, ForEachChild, SerializableIrNode, Simplifier,
-    SparseExprMap, TypeCheck, WidthInt, simplify_single_expression, traversal,
+    SparseExprMap, TypeCheck, WidthInt, count_expr_uses, simplify_single_expression, traversal,
 };
 use polysub::{Coef, Polynom, Term, VarIndex};
 use rustc_hash::{FxHashMap, FxHashSet};
@@ -44,9 +44,15 @@ pub fn simplify_word_level_equality(ctx: &mut Context, p: ScaEqualityProblem) ->
         .collect();
 
     // now we can perform backwards substitution
-    backwards_sub(ctx, gate_outputs.into(), spec);
+    let result = backwards_sub(ctx, gate_outputs.into(), spec);
 
-    todo!("check the result of backwards substitution")
+    if result.is_zero() {
+        println!("The SAME!")
+    } else {
+        println!("DIFFERENT: {result}")
+    }
+
+    None
 }
 
 type DefaultCoef = polysub::ArrayCoef<8>;
@@ -68,15 +74,32 @@ fn var_to_expr(v: polysub::VarIndex) -> ExprRef {
     usize::from(v).into()
 }
 
-fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spec: Poly) {
+fn is_gate(expr: &Expr) -> bool {
+    matches!(
+        expr,
+        Expr::BVNot(_, 1) | Expr::BVAnd(_, _, 1) | Expr::BVOr(_, _, 1) | Expr::BVXor(_, _, 1)
+    )
+}
+
+fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spec: Poly) -> Poly {
     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);
-    let mut on_todo = FxHashSet::default();
+    println!("minus_one = {minus_one:?}");
+    // 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);
 
     while let Some((output_var, gate)) = todo.pop_back() {
-        println!("{output_var}, {}", expr_to_var(gate) == output_var);
-        on_todo.remove(&gate);
+        println!(
+            "{output_var}, {}, {:?} ({})",
+            expr_to_var(gate) == output_var,
+            &ctx[gate],
+            spec.size()
+        );
+
         let add_children = match ctx[gate].clone() {
             Expr::BVOr(a, b, 1) => {
                 // a || b = !(!a && !b)
@@ -86,12 +109,16 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
                     (one.clone(), vec![x1].into()),
                     (minus_one.clone(), vec![x0, x1].into()),
                 ];
+                assert_ne!(gate, a);
+                assert_ne!(gate, b);
                 spec.replace_var(output_var, &monoms);
                 true
             }
             Expr::BVAnd(a, b, 1) => {
                 let (x0, x1) = exprs_to_vars_commutative(a, b);
                 let monoms = [(one.clone(), vec![x0, x1].into())];
+                assert_ne!(gate, a);
+                assert_ne!(gate, b);
                 spec.replace_var(output_var, &monoms);
                 true
             }
@@ -101,6 +128,7 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
                     (one.clone(), vec![].into()),
                     (minus_one.clone(), vec![x0].into()),
                 ];
+                assert_ne!(gate, a);
                 spec.replace_var(output_var, &monoms);
                 true
             }
@@ -113,13 +141,18 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
         };
         if add_children {
             ctx[gate].for_each_child(|&e| {
-                if !on_todo.contains(&e) {
-                    on_todo.insert(e);
+                // reduce the use by one
+                let prev_uses = uses[e];
+                assert!(prev_uses > 0);
+                uses[e] = prev_uses - 1;
+                // did the use count just go down to zero?
+                if prev_uses == 1 && is_gate(&ctx[e]) {
                     todo.push_front((expr_to_var(e), e));
                 }
             });
         }
     }
+    spec
 }
 
 fn poly_for_bv_expr(ctx: &mut Context, e: ExprRef) -> Poly {