minor fixes as a result of review of Chris's getType() rewrite; also fix some macros...

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 28404005cc23751e0043b2698622693107cb15d2..280c552544bf3a962b1d6e403da9916ca108c6e9 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -423,9 +423,9 @@ TypeNode NodeManager::computeType(TNode n, bool check)
   }
 
   setAttribute(n, TypeAttr(), typeNode);
-  setAttribute(n, TypeCheckedAttr(), 
+  setAttribute(n, TypeCheckedAttr(),
                check || getAttribute(n, TypeCheckedAttr()));
-  
+
   return typeNode;
 }
 
@@ -449,8 +449,10 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
       bool readyToCompute = true;
 
-      for( TNode::iterator it = m.begin(), end = m.end() ; it != end; ++it ) {
-        if( !hasAttribute(*it, TypeAttr()) 
+      for( TNode::iterator it = m.begin(), end = m.end();
+           it != end;
+           ++it ) {
+        if( !hasAttribute(*it, TypeAttr())
             || (check && !getAttribute(*it, TypeCheckedAttr())) ) {
           readyToCompute = false;
           worklist.push(*it);
@@ -459,23 +461,23 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
       if( readyToCompute ) {
         /* All the children have types, time to compute */
-        typeNode = computeType(m,check);
+        typeNode = computeType(m, check);
         worklist.pop();
-      } 
+      }
     } // end while
 
     /* Last type computed in loop should be the type of n */
-    Assert( typeNode == getAttribute(n,TypeAttr()) );
+    Assert( typeNode == getAttribute(n, TypeAttr()) );
   } else if( !hasType || needsCheck ) {
     /* We can compute the type top-down, without worrying about
        deep recursion. */
-    typeNode = computeType(n,check);
+    typeNode = computeType(n, check);
   }
 
   /* The type should be have been computed and stored. */
   Assert( hasAttribute(n, TypeAttr()) );
   /* The check should have happened, if we asked for it. */
-  Assert( !check || hasAttribute(n, TypeCheckedAttr()) );
+  Assert( !check || getAttribute(n, TypeCheckedAttr()) );
 
   Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
   return typeNode;

diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index f2dbd3bce0567f348b105b75c0f1e583c221352c..2ac1facb01aef6f1a9a8a7f8430851da196b65ef 100644 (file)
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -49,15 +49,32 @@
 // copy constructors.  The advantage is that with CVC4_UNDEFINED,
 // if something _does_ try to call the function, you get an error
 // at the point of the call (rather than a link error later).
+
+// CVC4_UNUSED is to mark something (e.g. local variable, function)
+// as being _possibly_ unused, so that the compiler generates no
+// warning about it.  This might be the case for e.g. a variable
+// only used in DEBUG builds.
+
 #ifdef __GNUC__
-#  define CVC4_UNDEFINED __attribute__((error("this function intentionally undefined")))
+#  if __GNUC__ > 4 || ( __GNUC__ == 4 && __GNUC_MINOR__ >= 3 )
+     /* error function attribute only exists in GCC >= 4.3.0 */
+#    define CVC4_UNDEFINED __attribute__((error("this function intentionally undefined")))
+#  else /* GCC < 4.3.0 */
+#    define CVC4_UNDEFINED
+#  endif /* GCC >= 4.3.0 */
 #else /* ! __GNUC__ */
 #  define CVC4_UNDEFINED
 #endif /* __GNUC__ */
 
+#ifdef __GNUC__
+#  define CVC4_UNUSED __attribute__((unused))
+#else /* ! __GNUC__ */
+#  define CVC4_UNUSED
+#endif /* __GNUC__ */
+
 #define EXPECT_TRUE(x) __builtin_expect( (x), true )
 #define EXPECT_FALSE(x) __builtin_expect( (x), false )
-#define NORETURN __attribute__ ((noreturn))
+#define CVC4_NORETURN __attribute__ ((noreturn))
 
 #ifndef NULL
 #  define NULL ((void*) 0)

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 38c75f0d3960913722e243d342458414a98e47ab..fcd322e993362ed4f903564b0f329f805408dfc0 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -133,7 +133,7 @@ int runCvc4(int argc, char* argv[]) {
   cvc4_init();
 
   progPath = argv[0];
-  
+
   // Parse the options
   int firstArgIndex = options.parseOptions(argc, argv);
 
@@ -148,7 +148,7 @@ int runCvc4(int argc, char* argv[]) {
   } else if( options.version ) {
     *options.out << Configuration::about().c_str() << flush;
     exit(0);
-  } 
+  }
 
   segvNoSpin = options.segvNoSpin;