From f56e48c8fa05e45ec9a3a7ead5911e9e070fe33a Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 8 Mar 2025 23:53:49 -0800 Subject: [PATCH 1/2] first commit --- Source/VCExpr/VCExprAST.cs | 7 +++++- Source/VCExpr/VCExprASTVisitors.cs | 34 +++--------------------------- 2 files changed, 9 insertions(+), 32 deletions(-) diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 8249e0d9e..854684591 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -373,7 +373,7 @@ public abstract class VCExprNAry : VCExpr { public override string ToString() { - return $"${Op}(${String.Join(", ", Arguments)})"; + return $"{Op}({String.Join(", ", Arguments)})"; } [Pure] @@ -1765,6 +1765,11 @@ public override Result Accept( //Contract.Requires(expr != null); return visitor.VisitBoogieFunctionOp(expr, arg); } + + public override string ToString() + { + return Func.Name; + } } ///////////////////////////////////////////////////////////////////////////////// diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 47ad03bfc..3b19b49dc 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -1112,29 +1112,6 @@ public SubstitutingVCExprVisitor(VCExpressionGenerator gen) Contract.Requires(gen != null); } - // when descending across a binder, we have to check that no collisions - // or variable capture can occur. if this might happen, we replace the - // term and type variables bound by the binder with fresh variables - private bool CollisionPossible(IEnumerable /*!*/ typeParams, - IEnumerable /*!*/ boundVars, VCExprSubstitution /*!*/ substitution) - { - Contract.Requires(Cce.NonNullElements(typeParams)); - Contract.Requires(Cce.NonNullElements(boundVars)); - Contract.Requires(substitution != null); - // variables can be shadowed by a binder - if (typeParams.Any(var => substitution.ContainsKey(var)) || - boundVars.Any(var => substitution.ContainsKey(var))) - { - return true; - } - // compute the codomain of the substitution - FreeVariableCollector coll = substitution.Codomains; - Contract.Assert(coll != null); - // variables could be captured when applying the substitution - return typeParams.Any(var => coll.FreeTypeVars.Contains(var)) || - boundVars.Any(var => coll.FreeTermVars.Contains(var)); - } - // can be overwritten if names of bound variables are to be changed protected virtual string ChooseNewVariableName(string oldName) { @@ -1202,9 +1179,7 @@ protected virtual string ChooseNewVariableName(string oldName) List /*!*/ typeParams = node.TypeParameters; Contract.Assert(Cce.NonNullElements(typeParams)); - bool refreshAllVariables = refreshBoundVariables || - CollisionPossible(node.TypeParameters, node.BoundVars, substitution); - if (refreshAllVariables) + if (refreshBoundVariables) { // we introduce fresh type variables to ensure that none gets captured typeParams = new List(); @@ -1224,7 +1199,7 @@ protected virtual string ChooseNewVariableName(string oldName) List /*!*/ boundVars = node.BoundVars; Contract.Assert(Cce.NonNullElements(boundVars)); - if (refreshAllVariables || !substitution.TypeSubstIsEmpty) + if (refreshBoundVariables || !substitution.TypeSubstIsEmpty) { // collisions are possible, or we also substitute type variables. in this case // the bound term variables have to be replaced with fresh variables with the @@ -1301,10 +1276,7 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres substitution.PushScope(); try { - bool refreshAllVariables = - refreshBoundVariables || - !substitution.TypeSubstIsEmpty || - CollisionPossible(new List(), node.BoundVars, substitution); + bool refreshAllVariables = refreshBoundVariables || !substitution.TypeSubstIsEmpty; List /*!*/ newBoundVars = node.BoundVars; From 138624fd483538a8ac84acf773a4803f93a6d058 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 9 Mar 2025 09:44:37 -0700 Subject: [PATCH 2/2] second commit --- Source/VCExpr/VCExprASTVisitors.cs | 55 +++--------------------------- 1 file changed, 4 insertions(+), 51 deletions(-) diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 3b19b49dc..d125b696b 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -1161,49 +1161,18 @@ protected virtual string ChooseNewVariableName(string oldName) Contract.Requires(substitution != null); Contract.Ensures(Contract.Result() != null); - // the default is to refresh bound variables only if necessary - // because of collisions - return Visit(node, substitution, false); - } - - public VCExpr /*!*/ Visit(VCExprQuantifier /*!*/ node, VCExprSubstitution /*!*/ substitution, - bool refreshBoundVariables) - { - Contract.Requires(node != null); - Contract.Requires(substitution != null); - Contract.Ensures(Contract.Result() != null); - substitution.PushScope(); try { List /*!*/ typeParams = node.TypeParameters; Contract.Assert(Cce.NonNullElements(typeParams)); - if (refreshBoundVariables) - { - // we introduce fresh type variables to ensure that none gets captured - typeParams = new List(); - foreach (TypeVariable /*!*/ var in node.TypeParameters) - { - Contract.Assert(var != null); - TypeVariable /*!*/ - freshVar = - new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name)); - Contract.Assert(freshVar != null); - typeParams.Add(freshVar); - substitution[var] = freshVar; - // this might overwrite other elements of the substitution, deliberately - } - } - List /*!*/ boundVars = node.BoundVars; Contract.Assert(Cce.NonNullElements(boundVars)); - if (refreshBoundVariables || !substitution.TypeSubstIsEmpty) + if (!substitution.TypeSubstIsEmpty) { - // collisions are possible, or we also substitute type variables. in this case - // the bound term variables have to be replaced with fresh variables with the - // right types + // replace each bound term variable with a fresh variable of correct type boundVars = new List(); IDictionary /*!*/ typeSubst = substitution.ToTypeSubst; @@ -1218,7 +1187,6 @@ protected virtual string ChooseNewVariableName(string oldName) Contract.Assert(freshVar != null); boundVars.Add(freshVar); substitution[var] = freshVar; - // this might overwrite other elements of the substitution, deliberately } } @@ -1258,16 +1226,6 @@ public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) } public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) - { - Contract.Requires(substitution != null); - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - // the default is to refresh bound variables only if necessary - // because of collisions - return Visit(node, substitution, false); - } - - public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables) { Contract.Requires(substitution != null); Contract.Requires(node != null); @@ -1276,16 +1234,12 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres substitution.PushScope(); try { - bool refreshAllVariables = refreshBoundVariables || !substitution.TypeSubstIsEmpty; - List /*!*/ newBoundVars = node.BoundVars; Contract.Assert(Cce.NonNullElements(newBoundVars)); - if (refreshAllVariables) + if (!substitution.TypeSubstIsEmpty) { - // collisions are possible, or we also substitute type variables. in this case - // the bound term variables have to be replaced with fresh variables with the - // right types + // replace each bound term variable with a fresh variable of correct type newBoundVars = new List(); IDictionary /*!*/ typeSubst = substitution.ToTypeSubst; @@ -1300,7 +1254,6 @@ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refres Contract.Assert(freshVar != null); newBoundVars.Add(freshVar); substitution[var] = freshVar; - // this might overwrite other elements of the substitution, deliberately } }