Implemented the command line switch /useArrayTheory. This switch should be used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.

2 files changed, 19 insertions, 2 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index fc706e2c..00142344 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -429,6 +429,20 @@ namespace Microsoft.Boogie
       return true;

     }

 

+    public void AddAttribute(string! name, object! val)

+    {

+      QKeyValue kv;

+      for (kv = this.Attributes; kv != null; kv = kv.Next) {

+        if (kv.Key == name) {

+          kv.Params.Add(val);

+          break;

+        }

+      }

+      if (kv == null) {

+        Attributes = new QKeyValue(tok, name, new List<object!>(new object![] { val }), Attributes);

+      }

+    }                                   

+    

     public abstract void Emit(TokenTextWriter! stream, int level);

     public abstract void Register(ResolutionContext! rc);

 

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index d3eb2eba..5912220d 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -151,6 +151,8 @@ namespace Microsoft.Boogie
     public enum BvHandling { None, Z3Native, ToInt }

     public BvHandling Bitvectors = BvHandling.Z3Native;

     

+    public bool UseArrayTheory = false;

+    

     public bool UseAbstractInterpretation = true;          // true iff the user want to use abstract interpretation

     public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

     invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9;

@@ -788,7 +790,7 @@ namespace Microsoft.Boogie
               }

             }

             break;

-

+              

           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

@@ -1132,7 +1134,8 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||

               ps.CheckBooleanFlag("z3types", ref Z3types) ||

               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

-              ps.CheckBooleanFlag("monomorphize", ref Monomorphize)

+              ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

+              ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory)

               )

             {

               // one of the boolean flags matched