Change the return type of StandardVisitor.VisitBvExtractExpr() from

BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr 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

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 4c167953..a50acdba 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -245,7 +245,7 @@ namespace Microsoft.Boogie {
       node = (ExistsExpr)this.VisitQuantifierExpr(node);

       return node;

     }

-    public virtual BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {

+    public virtual Expr VisitBvExtractExpr(BvExtractExpr node) {

       Contract.Requires(node != null);

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

       node.Bitvector = this.VisitExpr(node.Bitvector);

@@ -810,7 +810,7 @@ namespace Microsoft.Boogie {
           Contract.Ensures(Contract.Result<ExistsExpr>() == node);

           return (ExistsExpr)this.VisitQuantifierExpr(node);

       }

-      public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node)

+      public override Expr VisitBvExtractExpr(BvExtractExpr node)

       {

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

           this.VisitExpr(node.Bitvector);