* reviewed BooleanSimplification, added documentation & unit test

* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

6 files changed, 257 insertions, 48 deletions

diff --git a/src/util/Assert.h b/src/util/Assert.h
index ec942e00b..0ff89bedf 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -250,8 +250,8 @@ void debugAssertionFailed(const AssertionException& thisException,
       if(EXPECT_FALSE( ! (cond) )) {                                    \
         /* save the last assertion failure */                           \
         const char* lastException = s_debugLastException;               \
-        AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
-        debugAssertionFailed(exception, lastException);                 \
+        CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+        CVC4::debugAssertionFailed(exception, lastException);                 \
       }                                                                 \
     } while(0)
 
@@ -261,27 +261,27 @@ void debugAssertionFailed(const AssertionException& thisException,
 #  define AlwaysAssert(cond, msg...)                                    \
      do {                                                               \
        if(EXPECT_FALSE( ! (cond) )) {                                   \
-         throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+         throw CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
        }                                                                \
      } while(0)
 #endif /* CVC4_DEBUG */
 
 #define Unreachable(msg...) \
-  throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unhandled(msg...) \
-  throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unimplemented(msg...) \
-  throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define InternalError(msg...) \
-  throw InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
-  throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+  throw CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define CheckArgument(cond, arg, msg...)         \
   AlwaysAssertArgument(cond, arg, ## msg)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
   do { \
     if(EXPECT_FALSE( ! (cond) )) { \
-      throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+      throw CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index aaf9ca03b..e76858d80 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -46,9 +46,11 @@ libutil_la_SOURCES = \
 	dynamic_array.h \
 	language.h \
 	triple.h \
+	subrange_bound.h \
 	trans_closure.h \
 	trans_closure.cpp \
-	boolean_simplification.h
+	boolean_simplification.h \
+	boolean_simplification.cpp
 
 libutil_la_LIBADD = \
 	@builddir@/libutilcudd.la
diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp
new file mode 100644
index 000000000..a154f342f
--- /dev/null
+++ b/src/util/boolean_simplification.cpp
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file boolean_simplification.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Simple routines for Boolean simplification
+ **
+ ** Simple, commonly-used routines for Boolean simplification.
+ **/
+
+#include "util/boolean_simplification.h"
+
+namespace CVC4 {
+
+void
+BooleanSimplification::push_back_associative_commute_recursive
+    (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
+    throw(AssertionException) {
+  Node::iterator i = n.begin(), end = n.end();
+  for(; i != end; ++i){
+    Node child = *i;
+    if(child.getKind() == k){
+      push_back_associative_commute_recursive(child, buffer, k, notK, negateNode);
+    }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
+      push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode);
+    }else{
+      if(negateNode){
+        buffer.push_back(negate(child));
+      }else{
+        buffer.push_back(child);
+      }
+    }
+  }
+}/* BooleanSimplification::push_back_associative_commute_recursive() */
+
+}/* CVC4 namespace */
+
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index 95d5fb435..e938a2b38 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -11,10 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Simple routines for Boolean simplification
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Simple, commonly-used routines for Boolean simplification.
  **/
 
 #include "cvc4_private.h"
@@ -22,30 +21,62 @@
 #ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
 #define __CVC4__BOOLEAN_SIMPLIFICATION_H
 
-#include "expr/node.h"
-#include "util/Assert.h"
 #include <vector>
+#include <algorithm>
 
+#include "expr/node.h"
+#include "util/Assert.h"
 
 namespace CVC4 {
 
+/**
+ * A class to contain a number of useful functions for simple
+ * simplification of nodes.  One never uses it as an object (and
+ * it cannot be constructed).  It is used as a namespace.
+ */
 class BooleanSimplification {
+  // cannot construct one of these
+  BooleanSimplification() CVC4_UNUSED;
+  BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED;
+
+  static void push_back_associative_commute_recursive
+    (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
+    throw(AssertionException);
+
 public:
 
+  /**
+   * The threshold for removing duplicates.  (See removeDuplicates().)
+   */
   static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
 
-  static void removeDuplicates(std::vector<Node>& buffer){
-    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
+  /**
+   * Remove duplicate nodes from a vector, modifying it in-place.
+   * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this
+   * function is a no-op.
+   */
+  static void removeDuplicates(std::vector<Node>& buffer)
+      throw(AssertionException) {
+    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
       std::sort(buffer.begin(), buffer.end());
-      std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end());
+      std::vector<Node>::iterator new_end =
+        std::unique(buffer.begin(), buffer.end());
       buffer.erase(new_end, buffer.end());
     }
   }
 
-  static Node simplifyConflict(Node andNode){
-    Assert(andNode.getKind() == kind::AND);
+  /**
+   * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded
+   * children of it (as far as possible---see
+   * push_back_associative_commute()), removes duplicates, and returns
+   * the resulting Node.
+   */
+  static Node simplifyConflict(Node andNode) throw(AssertionException) {
+    AssertArgument(!andNode.isNull(), andNode);
+    AssertArgument(andNode.getKind() == kind::AND, andNode);
+
     std::vector<Node> buffer;
-    push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false);
+    push_back_associative_commute(andNode, buffer, kind::AND, kind::OR);
 
     removeDuplicates(buffer);
 
@@ -54,10 +85,18 @@ public:
     return nb;
   }
 
-  static Node simplifyClause(Node orNode){
-    Assert(orNode.getKind() == kind::OR);
+  /**
+   * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded
+   * children of it (as far as possible---see
+   * push_back_associative_commute()), removes duplicates, and returns
+   * the resulting Node.
+   */
+  static Node simplifyClause(Node orNode) throw(AssertionException) {
+    AssertArgument(!orNode.isNull(), orNode);
+    AssertArgument(orNode.getKind() == kind::OR, orNode);
+
     std::vector<Node> buffer;
-    push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false);
+    push_back_associative_commute(orNode, buffer, kind::OR, kind::AND);
 
     removeDuplicates(buffer);
 
@@ -66,34 +105,63 @@ public:
     return nb;
   }
 
-  static Node simplifyHornClause(Node implication){
-    Assert(implication.getKind() == kind::IMPLIES);
+  /**
+   * Takes a node with kind IMPLIES, converts it to an OR, then
+   * simplifies the result with simplifyClause().
+   *
+   * The input doesn't actually have to be Horn, it seems, but that's
+   * the common case(?), hence the name.
+   */
+  static Node simplifyHornClause(Node implication) throw(AssertionException) {
+    AssertArgument(implication.getKind() == kind::IMPLIES, implication);
+
     TNode left = implication[0];
     TNode right = implication[1];
-    Node notLeft = NodeBuilder<1>(kind::NOT)<<left;
-    Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
+
+    Node notLeft = negate(left);
+    Node clause = NodeBuilder<2>(kind::OR) << notLeft << right;
+
     return simplifyClause(clause);
   }
 
-  static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){
-    Node::iterator i = n.begin(), end = n.end();
-    for(; i != end; ++i){
-      Node child = *i;
-      if(child.getKind() == k){
-        push_back_associative_commute(child, buffer, k, notK, negateNode);
-      }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
-        push_back_associative_commute(child, buffer, notK, k, !negateNode);
-      }else{
-        if(negateNode){
-          buffer.push_back(negate(child));
-        }else{
-          buffer.push_back(child);
-        }
-      }
-    }
-  }
+  /**
+   * Aids in reforming a node.  Takes a node of (N-ary) kind k and
+   * copies its children into an output vector, collapsing its k-kinded
+   * children into it.  Also collapses negations of notK.  For example:
+   *
+   *   push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]],
+   *                                  buffer, kind::OR, kind::AND )
+   *   yields a "buffer" vector of [a b b c d e f]
+   *
+   * @param n the node to operate upon
+   * @param buffer the output vector (must be empty on entry)
+   * @param k the kind to collapse (should equal the kind of node n)
+   * @param notK the "negation" of kind k (e.g. OR's negation is AND),
+   * or kind::UNDEFINED_KIND if none.
+   */
+  static inline void
+  push_back_associative_commute(Node n, std::vector<Node>& buffer,
+                                Kind k, Kind notK)
+      throw(AssertionException) {
+    AssertArgument(buffer.empty(), buffer);
+    AssertArgument(!n.isNull(), n);
+    AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k);
+    AssertArgument(notK != kind::NULL_EXPR, notK);
+    AssertArgument(n.getKind() == k, n,
+                   "expected node to have kind %s", kindToString(k).c_str());
+
+    push_back_associative_commute_recursive(n, buffer, k, notK, false);
+  }/* push_back_associative_commute() */
+
+  /**
+   * Negates a node, doing all the double-negation elimination
+   * that's possible.
+   *
+   * @param n the node to negate (cannot be the null node)
+   */
+  static Node negate(TNode n) throw(AssertionException) {
+    AssertArgument(!n.isNull(), n);
 
-  static Node negate(TNode n){
     bool polarity = true;
     TNode base = n;
     while(base.getKind() == kind::NOT){
diff --git a/src/util/output.h b/src/util/output.h
index 0b1c86afd..d3eb3a831 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -273,7 +273,7 @@ public:
 /** The debug output singleton */
 extern DebugC DebugChannel CVC4_PUBLIC;
 #ifdef CVC4_DEBUG
-#  define Debug DebugChannel
+#  define Debug CVC4::DebugChannel
 #else /* CVC4_DEBUG */
 #  define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel
 #endif /* CVC4_DEBUG */
@@ -290,7 +290,7 @@ extern ChatC Chat CVC4_PUBLIC;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC4_PUBLIC;
 #ifdef CVC4_TRACING
-#  define Trace TraceChannel
+#  define Trace CVC4::TraceChannel
 #else /* CVC4_TRACING */
 #  define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel
 #endif /* CVC4_TRACING */
diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h
new file mode 100644
index 000000000..fc6a259b4
--- /dev/null
+++ b/src/util/subrange_bound.h
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file subrange_bound.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of subrange bounds
+ **
+ ** Simple class to represent a subrange bound, either infinite
+ ** (no bound) or finite (an arbitrary precision integer).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SUBRANGE_BOUND_H
+#define __CVC4__SUBRANGE_BOUND_H
+
+#include "util/integer.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+/**
+ * Representation of a subrange bound.  A bound can either exist and be
+ * a finite arbitrary-precision integer, or not exist (and thus be
+ * an infinite bound).  For example, the CVC language subrange [-5.._]
+ * has a lower bound of -5 and an infinite upper bound.
+ */
+class SubrangeBound {
+  bool d_nobound;
+  Integer d_bound;
+
+public:
+
+  /** Construct an infinite SubrangeBound. */
+  SubrangeBound() throw() :
+    d_nobound(true),
+    d_bound() {
+  }
+
+  /** Construct a finite SubrangeBound. */
+  SubrangeBound(const Integer& i) throw() :
+    d_nobound(false),
+    d_bound(i) {
+  }
+
+  ~SubrangeBound() throw() {
+  }
+
+  /** Get the finite SubrangeBound, failing an assertion if infinite. */
+  Integer getBound() const throw(IllegalArgumentException) {
+    CheckArgument(!d_nobound, this, "SubrangeBound is infinite");
+    return d_bound;
+  }
+
+  /** Returns true iff this is a finite SubrangeBound. */
+  bool hasBound() const throw() {
+    return !d_nobound;
+  }
+
+  /** Test two SubrangeBounds for equality. */
+  bool operator==(const SubrangeBound& b) const throw() {
+    return hasBound() == b.hasBound() &&
+      (!hasBound() || getBound() == b.getBound());
+  }
+
+  /** Test two SubrangeBounds for disequality. */
+  bool operator!=(const SubrangeBound& b) const throw() {
+    return !(*this == b);
+  }
+
+};/* class SubrangeBound */
+
+inline std::ostream&
+operator<<(std::ostream& out, const SubrangeBound& bound) throw() {
+  if(bound.hasBound()) {
+    out << bound.getBound();
+  } else {
+    out << '_';
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SUBRANGE_BOUND_H */