Parse else-> clauses in the model

Disable MODEL_PARTIAL in SMTLib

3 files changed, 61 insertions, 10 deletions

diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 355a277f..7dcd3dd8 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -120,6 +120,7 @@ namespace Microsoft.Boogie
       internal readonly List<FuncTuple> apps = new List<FuncTuple>();

       public IEnumerable<FuncTuple> Apps { get { return apps; } }

       public int AppCount { get { return apps.Count; } }

+      private Element @else;

 

       internal Func(Model p, string n, int a) { Model = p;  Name = n; Arity = a; }

 

@@ -128,6 +129,20 @@ namespace Microsoft.Boogie
         return string.Format("{0}/{1}", Name, Arity);

       }

 

+      public Element Else

+      {

+        get

+        {

+          return @else;

+        }

+        set

+        {

+          if (@else != null)

+            throw new ArgumentException();

+          @else = value;

+        }

+      }

+

       public void SetConstant(Element res)

       {

         if (Arity != 0 || apps.Count > 0)

@@ -512,6 +527,8 @@ namespace Microsoft.Boogie
               wr.Write("{0} ", a);

             wr.WriteLine("-> {0}", app.Result);

           }

+          if (f.Else != null)

+            wr.WriteLine("  else -> {0}", f.Else);

           wr.WriteLine("}");

         }

       foreach (var s in States) {

@@ -663,19 +680,42 @@ namespace Microsoft.Boogie
                 if (tuple == null) BadModel("EOF in function table");

                 if (tuple.Length == 0) continue;

                 if (tuple.Length == 1 && tuple[0] == "}") break;

-                if (tuple.Length < 3 || tuple[tuple.Length - 2] != "->") BadModel("invalid function tuple definition");

-                if (tuple[0] == "else") {

-                  if (tuple[tuple.Length - 1].EndsWith("}"))

+

+                var resultName = tuple[tuple.Length - 1];

+                var isElse = false;

+

+                if (tuple.Length == 1 && fn == null)

+                  isElse = true;

+

+                if (!isElse && (tuple.Length < 3 || tuple[tuple.Length - 2] != "->")) BadModel("invalid function tuple definition");

+

+                if (isElse || tuple[0] == "else") {

+                  var hasBrace = false;

+                  if (resultName.EndsWith("}")) {

+                    hasBrace = true;

+                    resultName = resultName.Substring(0, resultName.Length - 1);

+                  }

+                  if (!resultName.StartsWith("#unspec")) {

+                    if (fn == null)

+                      fn = currModel.TryGetFunc(funName);

+                    // if it's still null, we don't know the arity, so just skip it

+                    if (fn != null) {

+                      fn.Else = GetElt(resultName);

+                    }

+                  }

+

+                  if (hasBrace)                  

                     break;

                   else

                     continue;

                 }

+

                 if (fn == null)

                   fn = currModel.MkFunc(funName, tuple.Length - 2);

                 var args = new Element[fn.Arity];

                 for (int i = 0; i < fn.Arity; ++i)

                   args[i] = GetElt(tuple[i]);

-                fn.AddApp(GetElt(tuple[tuple.Length - 1]), args);

+                fn.AddApp(GetElt(resultName), args);

               }

             } else {

               fn = currModel.MkFunc(funName, 0);

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8b21861e..80a220cb 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -107,7 +107,7 @@ namespace Microsoft.Boogie.SMTLib
       // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

       options.AddWeakSmtOption("AUTO_CONFIG", "false");

 

-      options.AddWeakSmtOption("MODEL_PARTIAL", "true");

+      //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

       //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

       options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");

       options.AddWeakSmtOption("MODEL_V2", "true");

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da68aac0..e0c89603 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -417,7 +417,10 @@ namespace Microsoft.Boogie {
             tuples.Add(tpl);

           }

           var elseTpl = new List<int>();

-          elseTpl.Add(elseElt.Id);

+          if (f.Else != null)

+            elseTpl.Add(f.Else.Id);

+          else

+            elseTpl.Add(elseElt.Id);

           tuples.Add(elseTpl);

         }

       }

@@ -458,6 +461,11 @@ namespace Microsoft.Boogie {
         // get the Func ("it doesn't matter if you get the funk, just as long as the funk gets you", from Ulco Bed's "Get The Funk" on Candy Dulfer's 1990 album Saxuality)

         var name = t.Key;

         var arity = tuples[0].Count - 1;

+

+        // this may happen if the function only has the else clause; the 1 is just the best guess in such case

+        if (arity == 0)

+          arity = 1; 

+

         Model.Func f;

         if (Regex.IsMatch(name, "^MapType[0-9]*Select$")) {

           name = string.Format("[{0}]", arity);

@@ -477,10 +485,13 @@ namespace Microsoft.Boogie {
 

         var args = new Model.Element[arity];

         foreach (var l in tuples) {

-          if (l.Count == 1) continue;

-          for (int i = 0; i < f.Arity; ++i)

-            args[i] = elts[l[i]];

-          f.AddApp(elts[l[f.Arity]], args);

+          if (l.Count == 1) {

+            f.Else = elts[l[0]];

+          } else {

+            for (int i = 0; i < f.Arity; ++i)

+              args[i] = elts[l[i]];

+            f.AddApp(elts[l[f.Arity]], args);

+          }

         }

       }