Change the return type of StandardVisitor.VisitExistsExpr() from

ExistsExpr to Expr. Enforcing the return type be ExistsExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.

There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.

Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree

3 files changed, 4 insertions, 4 deletions

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 6164c23b..759077b5 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -204,7 +204,7 @@ namespace Microsoft.Boogie {
         Contract.Ensures(Contract.Result<List<Ensures>>() != null);

         return base.VisitEnsuresSeq(new List<Ensures>(ensuresSeq));

     }

-    public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public override Expr VisitExistsExpr(ExistsExpr node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<ExistsExpr>() != null);

       return base.VisitExistsExpr((ExistsExpr)node.Clone());

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index a19bf78b..963f3ec6 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -239,7 +239,7 @@ namespace Microsoft.Boogie {
       node.OutParams = this.VisitVariableSeq(node.OutParams);

       return node;

     }

-    public virtual ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public virtual Expr VisitExistsExpr(ExistsExpr node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<ExistsExpr>() != null);

       node = (ExistsExpr)this.VisitQuantifierExpr(node);

@@ -805,7 +805,7 @@ namespace Microsoft.Boogie {
           this.VisitVariableSeq(node.OutParams);

           return node;

       }

-      public override ExistsExpr VisitExistsExpr(ExistsExpr node)

+      public override Expr VisitExistsExpr(ExistsExpr node)

       {

           Contract.Ensures(Contract.Result<ExistsExpr>() == node);

           return (ExistsExpr)this.VisitQuantifierExpr(node);

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index f261553b..7cd3d240 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -454,7 +454,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;

     }

 

-    public override ExistsExpr VisitExistsExpr(ExistsExpr node) {

+    public override Expr VisitExistsExpr(ExistsExpr node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<ExistsExpr>() != null);

       node = (ExistsExpr)this.VisitQuantifierExpr(node);