First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.

3 files changed, 72 insertions, 1 deletions

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index 44d450c0..eb09576b 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -441,6 +441,34 @@ namespace Microsoft.Boogie.Z3
       } else if (s[j] == 'v') {

         // -> val!..., i.e. no value

         partitionToValue.Add(null);

+      } else if (s[j] == '{') {

+        // array

+        List<List<int>!> arrayModel = new List<List<int>!>();

+        string array = s.Substring(j);

+        int index1, index2;

+        string from, to;

+        List<int> tuple = new List<int>();

+        while (0 <= array.IndexOf(';')) {

+          index1 = array.IndexOf('*') + 1;

+          index2 = array.IndexOf(' ');

+          from = array.Substring(index1, index2-index1);

+          tuple.Add(int.Parse(from));

+          array = array.Substring(index2);

+          index1 = array.IndexOf('*') + 1;

+          index2 = array.IndexOf(';');

+          to = array.Substring(index1, index2-index1);

+          array = array.Substring(index2+2);

+          tuple.Add(int.Parse(to));

+          arrayModel.Add(tuple);

+          tuple = new List<int>();

+        }

+        assert array.StartsWith("else ->");

+        index1 = array.IndexOf('*') + 1;

+        index2 = array.IndexOf('}');

+        to = array.Substring(index1, index2-index1);

+        tuple.Add(int.Parse(to));

+        arrayModel.Add(tuple);

+        partitionToValue.Add(arrayModel);

       } else {

         string numberOrBv = s.Substring(j);

         // make number an int, then store it:

@@ -494,8 +522,10 @@ namespace Microsoft.Boogie.Z3
       ensures 0 <= result && result <= s.Length;

     {

       List<string!> identifiers = new List<string!>();

+      int arrowIndex = s.IndexOf('>');

+      assert 0 < arrowIndex;

       int j = s.IndexOf('{', 0) + 1;  // skip the '{', if present, and set j to 0 otherwise

-      if (1 <= j) {

+      if (1 <= j && j < arrowIndex) {

         // There is a list of ID's.

         assume j < s.Length;  // there should be more characters; the ending '}', for one

         //ID*

@@ -516,6 +546,8 @@ namespace Microsoft.Boogie.Z3
           }

           assume j < s.Length;  // there should be more characters; the ending '}', for one

         }//end ID*

+      } else {

+        j = 0;

       }

       Owner.AssignSame(identifiers, Owner.ElementProxy(partitionToIdentifiers));

       partitionToIdentifiers.Add(identifiers);

diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc
index 9a28eb42..cc788033 100644
--- a/Source/Provers/Z3/ProverInterface.ssc
+++ b/Source/Provers/Z3/ProverInterface.ssc
@@ -223,6 +223,11 @@ namespace Microsoft.Boogie.Z3
     private readonly UniqueNamer! Namer;

     private readonly TypeDeclCollector! DeclCollector;

 

+    public override string! Lookup(VCExprVar! var)

+    {

+      return Namer.Lookup(var);

+    }

+    

     public override string! translate(VCExpr! expr, int polarity) {

       DateTime start = DateTime.Now;

       if (CommandLineOptions.Clo.Trace)

diff --git a/Source/Provers/Z3/TypeDeclCollector.ssc b/Source/Provers/Z3/TypeDeclCollector.ssc
index 21aebabe..a45ca206 100644
--- a/Source/Provers/Z3/TypeDeclCollector.ssc
+++ b/Source/Provers/Z3/TypeDeclCollector.ssc
@@ -35,6 +35,9 @@ namespace Microsoft.Boogie.Z3
       KnownVariables = new Dictionary<VCExprVar!, bool> ();

       KnownTypes = new Dictionary<Type!, bool> ();

       KnownBvOps = new Dictionary<string!, bool> ();

+      

+      KnownStoreFunctions = new Dictionary<string!, bool> ();

+      KnownSelectFunctions = new Dictionary<string!, bool> ();

     }

 

     internal TypeDeclCollector(UniqueNamer! namer, TypeDeclCollector! coll) {

@@ -46,6 +49,9 @@ namespace Microsoft.Boogie.Z3
       KnownVariables = new Dictionary<VCExprVar!, bool> (coll.KnownVariables);

       KnownTypes = new Dictionary<Type!, bool> (coll.KnownTypes);

       KnownBvOps = new Dictionary<string!, bool> (coll.KnownBvOps);

+      

+      KnownStoreFunctions = new Dictionary<string!, bool> (coll.KnownStoreFunctions);

+      KnownSelectFunctions = new Dictionary<string!, bool> (coll.KnownSelectFunctions);

     }

 

     // not used

@@ -65,6 +71,9 @@ namespace Microsoft.Boogie.Z3
     // the names of registered BvConcatOps and BvExtractOps

     private readonly IDictionary<string!, bool>! KnownBvOps;

 

+    private readonly IDictionary<string!, bool>! KnownStoreFunctions;

+    private readonly IDictionary<string!, bool>! KnownSelectFunctions;

+

     public List<string!>! AllDeclarations { get {

       List<string!>! res = new List<string!> ();

       res.AddRange(AllDecls);

@@ -171,6 +180,31 @@ namespace Microsoft.Boogie.Z3
           }

         }

         //

+      } else if (node.Op is VCExprStoreOp) {

+        //

+        string name = SimplifyLikeExprLineariser.StoreOpName(node);

+        if (!KnownStoreFunctions.ContainsKey(name)) {

+          AddDeclaration("(DEFOP " + name + 

+                         " " + TypeToString(node[0].Type) + 

+                         " " + TypeToString(node[1].Type) +

+                         " " + TypeToString(node[2].Type) + 

+                         " " + TypeToString(node.Type) + 

+                         " :BUILTIN store)");

+          KnownStoreFunctions.Add(name, true);

+        }

+        //

+      } else if (node.Op is VCExprSelectOp) {

+        //

+        string name = SimplifyLikeExprLineariser.SelectOpName(node);

+        if (!KnownSelectFunctions.ContainsKey(name)) {

+          AddDeclaration("(DEFOP " + name + 

+                         " " + TypeToString(node[0].Type) + 

+                         " " + TypeToString(node[1].Type) +

+                         " " + TypeToString(node.Type) + 

+                         " :BUILTIN select)");

+          KnownSelectFunctions.Add(name, true);

+        }

+        //

       } else {

         //

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;