Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other bitvector operations

6 files changed, 19 insertions, 19 deletions

diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc
index 82854412..78a796c2 100644
--- a/Source/Core/AbsyExpr.ssc
+++ b/Source/Core/AbsyExpr.ssc
@@ -2990,12 +2990,12 @@ namespace Microsoft.Boogie
 

 

 

-  public class ExtractExpr : Expr, AI.IFunApp

+  public class BvExtractExpr : Expr, AI.IFunApp

   {

     public /*readonly--except in StandardVisitor*/ Expr! Bitvector;

     public readonly int Start, End;

     

-    public ExtractExpr(IToken! tok, Expr! bv, int end, int start)

+    public BvExtractExpr(IToken! tok, Expr! bv, int end, int start)

       : base(tok)

     {

       Bitvector = bv;

@@ -3008,9 +3008,9 @@ namespace Microsoft.Boogie
     public override bool Equals(object obj)

     {

       if (obj == null) return false;

-      if (!(obj is ExtractExpr)) return false;

+      if (!(obj is BvExtractExpr)) return false;

 

-      ExtractExpr other = (ExtractExpr)obj;

+      BvExtractExpr other = (BvExtractExpr)obj;

       return object.Equals(this.Bitvector, other.Bitvector) &&

         this.Start.Equals(other.Start) && this.End.Equals(other.End);

     }

@@ -3100,10 +3100,10 @@ namespace Microsoft.Boogie
     

       if(args.Count == 3)

       {      

-        retFun = new ExtractExpr(this.tok,

-                               BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),

-                               ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,

-                               ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);

+        retFun = new BvExtractExpr(this.tok,

+                                 BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),

+                                 ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,

+                                 ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);

       } 

       else

       {

@@ -3120,7 +3120,7 @@ namespace Microsoft.Boogie
 

     public override Absy! StdDispatch(StandardVisitor! visitor)

     {

-      return visitor.VisitExtractExpr(this);

+      return visitor.VisitBvExtractExpr(this);

     }

   }

 

diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc
index e91eaf7c..8ae741ab 100644
--- a/Source/Core/Parser.ssc
+++ b/Source/Core/Parser.ssc
@@ -1617,9 +1617,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
 			if (store)

 			 e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);

 			else if (bvExtract)

-			  e = new ExtractExpr(x, e,

-			                      ((BvBounds)index0).Upper.ToIntSafe,

-			                      ((BvBounds)index0).Lower.ToIntSafe);

+			  e = new BvExtractExpr(x, e,

+			                        ((BvBounds)index0).Upper.ToIntSafe,

+			                        ((BvBounds)index0).Lower.ToIntSafe);

 			else

 			  e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); 

 			

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index a6068426..1e0ceb8f 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -211,7 +211,7 @@ namespace Microsoft.Boogie
       node = (ExistsExpr) this.VisitQuantifierExpr(node);

       return node; 

     }

-    public virtual ExtractExpr! VisitExtractExpr(ExtractExpr! node)

+    public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)

     {

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

       return node; 

diff --git a/Source/Core/Util.ssc b/Source/Core/Util.ssc
index 914ccf09..e90358ac 100644
--- a/Source/Core/Util.ssc
+++ b/Source/Core/Util.ssc
@@ -266,7 +266,7 @@ namespace Microsoft.Boogie
       }

       public static string! PrettyPrintBplExpr (Expr! e) {

         // anything that is unknown will just be printed via ToString

-        // OldExpr and QuantifierExpr, ExtractExpr, BvConcatExpr are ignored for now

+        // OldExpr and QuantifierExpr, BvExtractExpr, BvConcatExpr are ignored for now

         // LiteralExpr is printed as itself by ToString

         if (e is IdentifierExpr) {

           string s = e.ToString();

diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc
index b344c03d..f9f76465 100644
--- a/Source/VCExpr/Boogie2VCExpr.ssc
+++ b/Source/VCExpr/Boogie2VCExpr.ssc
@@ -416,13 +416,13 @@ namespace Microsoft.Boogie.VCExprAST
 

     ///////////////////////////////////////////////////////////////////////////////////

 

-    public override ExtractExpr! VisitExtractExpr(ExtractExpr! node)

+    public override BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)

     {

-      Push(TranslateExtractExpr(node));

+      Push(TranslateBvExtractExpr(node));

       return node;

     }

 

-    private VCExpr! TranslateExtractExpr(ExtractExpr! node)

+    private VCExpr! TranslateBvExtractExpr(BvExtractExpr! node)

       requires node.Start <= node.End; {

       VCExpr! bv = Translate(node.Bitvector);

       return Gen.BvExtract(bv, ((!)node.Bitvector.Type).BvBits, node.Start, node.End);

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index eb54d1b9..bfdcf6c6 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -2686,8 +2686,8 @@ namespace VC
         // expression, thus just return -1

         return -1;

       } 

-      else if (expr is Bpl.ExtractExpr) {

-        Bpl.ExtractExpr ex = (Bpl.ExtractExpr) expr;

+      else if (expr is Bpl.BvExtractExpr) {

+        Bpl.BvExtractExpr ex = (Bpl.BvExtractExpr) expr;

         Bpl.Expr e0 = ex.Bitvector;

         Bpl.Expr e1 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.Start));

         Bpl.Expr e2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(ex.End));