implementing datatypes

1 files changed, 12 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 36df38e3..f008bb88 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -655,14 +655,26 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      private string ExtractDatatypeSelector(Function func) {

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

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

+        }

+        else {

+          return null;

+        }

+      }

+

       public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {

         VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

         Contract.Assert(op != null);

         string printedName;

 

         var builtin = ExtractBuiltin(op.Func);

+        var datatype = ExtractDatatypeSelector(op.Func);

         if (builtin != null)

           printedName = builtin;

+        else if (datatype != null)

+          printedName = datatype;

         else

           printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);

         Contract.Assert(printedName != null);