diff --git a/src/opt/unfolder.rs b/src/opt/unfolder.rs index 9d67bb1d..7cc15b18 100644 --- a/src/opt/unfolder.rs +++ b/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(); diff --git a/src/vc/subst.rs b/src/vc/subst.rs index 583dd265..bb6bf9c2 100644 --- a/src/vc/subst.rs +++ b/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, - free_vars: im_rc::HashSet, + /// 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, } +/// A structure to apply variable substitutions in expressions. pub struct Subst<'a> { tcx: &'a TyCtx, - cur: SubstLevel, - stack: Vec, - limits_ref: LimitsRef, + cur: SubstFrame, + stack: Vec, + 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) }