fixed problems with datatypes

removed stale contracts in stratified inlining
added test to datatypes

3 files changed, 19 insertions, 15 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d3448b5d..dab0807f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -206,13 +206,15 @@ namespace Microsoft.Boogie.SMTLib
           foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {

             datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";

             foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {

+              string quotedConstructorName = Namer.GetQuotedName(f, f.Name);

               if (f.InParams.Length == 0) {

-                datatypeString += Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += quotedConstructorName + " ";

               }

               else {

-                datatypeString += "(" + Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += "(" + quotedConstructorName + " ";

                 foreach (Variable v in f.InParams) {

-                  datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

+                  string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);

+                  datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

                 }

                 datatypeString += ") ";

               }

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 8d4a4256..635280d1 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -660,11 +660,14 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       private string ExtractDatatype(Function func) {

-        if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {

-          return func.Name.Remove(func.Name.IndexOf('#'));

-        }

-        else if (QKeyValue.FindBoolAttribute(func.Attributes, "membership")) {

-          return func.Name.Replace('#', '-');

+        if (func is DatatypeSelector) {

+          DatatypeSelector selector = (DatatypeSelector) func;

+          Variable v = selector.constructor.InParams[selector.index];

+          return ExprLineariser.Namer.GetQuotedName(v, v.Name + "#" + selector.constructor.Name);

+        }

+        else if (func is DatatypeMembership) {

+          DatatypeMembership membership = (DatatypeMembership)func;

+          return ExprLineariser.Namer.GetQuotedName(membership, "is-" + membership.constructor.Name);

         }

         else {

           return null;

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 0bc41c2a..4a4ecfb6 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -171,7 +171,7 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-        if (op != null && !IsDatatypeConstructor(op.Func) && !KnownFunctions.Contains(op.Func)) {

+        if (op != null && !IsDatatypeFunction(op.Func) && !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -264,12 +264,11 @@ void ObjectInvariant()
       return QKeyValue.FindBoolAttribute(ctorType.Decl.Attributes, "datatype");

     }

 

-    public static bool IsDatatypeConstructor(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "constructor");

-    }

-

-    public static bool IsDatatypeSelector(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "selector");

+    public static bool IsDatatypeFunction(Function f) {

+      return

+        QKeyValue.FindBoolAttribute(f.Attributes, "constructor") ||

+        f is DatatypeSelector ||

+        f is DatatypeMembership;

     }

 

     private void RegisterSelect(VCExprNAry node)