sca: remove Deque since the order should not matter anymore (for correctness)

Author: ekiwi

patronus-sca/src/lib.rs

@@ -3,12 +3,8 @@
 // author: Kevin Laeufer <laeufer@cornell.edu>
 
 use baa::{BitVecOps, BitVecValue, BitVecValueRef};
-use patronus::expr::{
-    Context, DenseExprMetaData, Expr, ExprRef, ForEachChild, SerializableIrNode, Simplifier,
-    TypeCheck, WidthInt, count_expr_uses, traversal,
-};
+use patronus::expr::*;
 use polysub::{Coef, Term, VarIndex};
-use std::collections::VecDeque;
 use std::fmt::{Display, Formatter};
 
 /// Returns a new expressions reference if simplification was possible
@@ -50,6 +46,8 @@ pub fn simplify_word_level_equality(ctx: &mut Context, p: ScaEqualityProblem) ->
     }
 }
 
+/// Extracts a bit from a concatenation. We use this to avoid having to call the full blown
+/// simplifier.
 fn extract_bit(ctx: &mut Context, e: ExprRef, bit: WidthInt) -> ExprRef {
     match ctx[e].clone() {
         Expr::BVConcat(a, b, _) => {
@@ -90,7 +88,7 @@ fn is_gate(expr: &Expr) -> bool {
     )
 }
 
-fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spec: Poly) -> Poly {
+fn backwards_sub(ctx: &Context, mut todo: Vec<(VarIndex, ExprRef)>, mut spec: Poly) -> Poly {
     let mut var_roots: Vec<_> = todo.iter().map(|(v, _)| *v).collect();
     var_roots.sort();
 
@@ -103,7 +101,7 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
     let mut uses = count_expr_uses(ctx, roots);
     let mut replaced = vec![];
 
-    while let Some((output_var, gate)) = todo.pop_back() {
+    while let Some((output_var, gate)) = todo.pop() {
         replaced.push(output_var);
 
         let add_children = match ctx[gate].clone() {
@@ -168,7 +166,7 @@ fn backwards_sub(ctx: &Context, mut todo: VecDeque<(VarIndex, ExprRef)>, mut spe
                 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));
+                    todo.push((expr_to_var(e), e));
                 }
             });
         }