From eb702d50b002d07d40f94b1c8d2462ad0ec38838 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Sun, 18 Mar 2012 07:10:44 -0700
Subject: more type checking for datatypes

---
 Source/Provers/SMTLib/TypeDeclCollector.cs | 27 ++++++++++-----------------
 1 file changed, 10 insertions(+), 17 deletions(-)

(limited to 'Source/Provers')

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)
     {
-- 
cgit v1.2.3