subst: Generate less shadow variables

src/opt/unfolder.rs

@@ -42,8 +42,6 @@ use crate::{
 use crate::smt::translate_exprs::TranslateExprs;
 
 pub struct Unfolder<'smt, 'ctx> {
-    limits_ref: LimitsRef,
-
     /// The expressions may contain substitutions. We keep track of those.
     subst: Subst<'smt>,
 
@@ -59,11 +57,15 @@ pub struct Unfolder<'smt, 'ctx> {
 
 impl<'smt, 'ctx> Unfolder<'smt, 'ctx> {
     pub fn new(limits_ref: LimitsRef, ctx: &'smt SmtCtx<'ctx>) -> Self {
+        // it's important that we use the native incremental mode here, because
+        // the performance benefit from the unfolder relies on many very fast
+        // SAT checks.
+        let prover = Prover::new(ctx.ctx(), IncrementalMode::Native);
+
         Unfolder {
-            limits_ref: limits_ref.clone(),
             subst: Subst::new(ctx.tcx(), &limits_ref),
             translate: TranslateExprs::new(ctx),
-            prover: Prover::new(ctx.ctx(), IncrementalMode::Native),
+            prover,
         }
     }
 
@@ -147,7 +149,7 @@ impl<'smt, 'ctx> VisitorMut for Unfolder<'smt, 'ctx> {
     type Err = LimitError;
 
     fn visit_expr(&mut self, e: &mut Expr) -> Result<(), Self::Err> {
-        self.limits_ref.check_limits()?;
+        self.subst.limits_ref.check_limits()?;
 
         let span = e.span;
         let ty = e.ty.clone().unwrap();

src/vc/subst.rs

@@ -19,64 +19,104 @@ use crate::{
     tyctx::TyCtx,
 };
 
+/// A stack frame of substitutions.
+///
+/// This structure uses immutable data structures, so it is cheap to clone.
 #[derive(Default, Clone)]
-struct SubstLevel {
+struct SubstFrame {
+    /// The substitutions in this frame.
     substs: im_rc::HashMap<Ident, Expr>,
-    free_vars: im_rc::HashSet<Ident>,
+    /// The number of right-hand sides of the substitutions in this frame that
+    /// the ident shows up in.
+    ///
+    /// This is used to compute whether a quantified variable needs to be
+    /// shadowed.
+    free_vars: im_rc::HashMap<Ident, usize>,
 }
 
+/// A structure to apply variable substitutions in expressions.
 pub struct Subst<'a> {
     tcx: &'a TyCtx,
-    cur: SubstLevel,
-    stack: Vec<SubstLevel>,
-    limits_ref: LimitsRef,
+    cur: SubstFrame,
+    stack: Vec<SubstFrame>,
+    pub limits_ref: LimitsRef,
 }
 
 impl<'a> Subst<'a> {
+    /// Create a new empty instance.
     pub fn new(tcx: &'a TyCtx, limits_ref: &LimitsRef) -> Self {
         Subst {
             tcx,
-            cur: SubstLevel::default(),
+            cur: SubstFrame::default(),
             stack: Vec::new(),
             limits_ref: limits_ref.clone(),
         }
     }
 
+    /// Push the stack and add a substitution.
     pub fn push_subst(&mut self, ident: Ident, mut expr: Expr) {
         self.stack.push(self.cur.clone());
         let mut free_var_collector = FreeVariableCollector::new();
         free_var_collector.visit_expr(&mut expr).unwrap();
-        self.cur.free_vars.extend(free_var_collector.variables);
+        for free_var in free_var_collector.variables {
+            *self.cur.free_vars.entry(free_var).or_insert(0) += 1;
+        }
         self.cur.substs.insert(ident, expr);
     }
 
+    /// Push the stack and handle quantified variables.
+    ///
+    /// This function removes all given variables from the substitutions. If a
+    /// variable is contained in the free variables of the current substitution,
+    /// then we create a "shadow" variable that is used instead of the original
+    /// variable to avoid name clashes.
     pub fn push_quant(&mut self, span: Span, vars: &mut [QuantVar], tcx: &TyCtx) {
         self.stack.push(self.cur.clone());
+
         for var in vars {
             let ident = var.name();
-            self.cur.substs.remove(&ident);
-            // TODO: if we removed a previous substitution, we should rebuild
-            // the set of free variables because it might contain variables that
-            // won't be inserted anymore.
-            //
-            // right now, we over-approximate the set of free variables which is
-            // sound, but might result in too many quantified variables being
-            // renamed.
-
-            if self.cur.free_vars.contains(&ident) {
-                let new_ident =
-                    tcx.clone_var(ident, span.variant(SpanVariant::Subst), VarKind::Subst);
-                *var = QuantVar::Shadow(new_ident);
+
+            // remove the substitution for the variable (if present)
+            let old_expr = self.cur.substs.remove(&ident);
+
+            // if we removed an expression from the substitution map, update the
+            // free variables counter.
+            if let Some(mut old_expr) = old_expr {
+                let mut free_var_collector = FreeVariableCollector::new();
+                free_var_collector.visit_expr(&mut old_expr).unwrap();
+
+                for free_var in free_var_collector.variables {
+                    let counter = self.cur.free_vars.get_mut(&free_var).unwrap();
+                    *counter -= 1;
+                }
+            }
+
+            // if the variable is contained in the free variables of this
+            // substitution, then shadow it: rename the variable and replace all
+            // occurrences of the original variable with the new one.
+            if self.cur.free_vars.get(&ident).unwrap_or(&0) > &0 {
+                tracing::trace!(ident=?ident, "shadowing quantified variable");
+
+                let new_span = span.variant(SpanVariant::Subst);
+                let new_ident = tcx.clone_var(ident, new_span, VarKind::Subst);
                 let builder = ExprBuilder::new(new_ident.span);
-                self.cur.substs.insert(ident, builder.var(new_ident, tcx));
+                let new_expr = builder.var(new_ident, tcx);
+
+                // shadow the variable
+                *var = QuantVar::Shadow(new_ident);
+
+                // substitute original variable with the shadow variable
+                self.cur.substs.insert(ident, new_expr);
             }
         }
     }
 
+    /// Pop the stack.
     pub fn pop(&mut self) {
         self.cur = self.stack.pop().expect("more calls to pop than push!");
     }
 
+    /// Lookup a variable in the current frame of substitutions.
     pub fn lookup_var(&self, ident: Ident) -> Option<&Expr> {
         self.cur.substs.get(&ident)
     }