more type checking for datatypes

1 files changed, 10 insertions, 17 deletions

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 40dc7cf6..05a6caf3 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -164,6 +164,7 @@ void ObjectInvariant()
       return TypeToString(t);

     }

 

+

     public override bool Visit(VCExprNAry node, bool arg) {

       Contract.Requires(node != null);

 

@@ -171,7 +172,9 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

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

+        if (op != null && 

+          !(op.Func is DatatypeConstructor) && !(op.Func is DatatypeMembership) && !(op.Func is DatatypeSelector) && 

+          !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -250,26 +253,16 @@ void ObjectInvariant()
       if (type.IsBool || type.IsInt || type.IsBv)

         return;

 

-      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic && !IsDatatype(type)) {

+      CtorType ctorType = type as CtorType;

+      if (ctorType != null && ctorType.IsDatatype())

+        return;

+

+      if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {

         AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");

         KnownTypes.Add(type);

         return;

       }

-    }

-

-    public static bool IsDatatype(Type t) {

-      CtorType ctorType = t.AsCtor;

-      if (t == null)

-        return false;

-      return QKeyValue.FindBoolAttribute(ctorType.Decl.Attributes, "datatype");

-    }

-

-    public static bool IsDatatypeFunction(Function f) {

-      return

-        f is DatatypeConstructor ||

-        f is DatatypeSelector ||

-        f is DatatypeMembership;

-    }

+    }  

 

     private void RegisterSelect(VCExprNAry node)

     {