PARSER STUFF:

* Other minor changes to the new parser to match coding guidelines,
  add documentation, ....

* Add CFLAGS stuff to configure.ac parser Makefile.ams.  This ensures
  that profiling, coverage, optimization, debugging, and warning
  level options will apply to the new parser as well (which is in C,
  not C++).  This fixes the deprecated warning we were seeing this
  evening.

* Now, if you have ANTLR_HOME set in your environment, you don't need
  to specify --with-antlr-dir to ./configure or have libantlr3c
  installed in standard places.  --with-antlr-dir still overrides
  $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or
  doesn't work, the standard places are still tried.

* Extend "silent make" to new parser stuff.

* Added src/parser/bounded_token_buffer.{h,cpp} to the list of
  exclusions in contrib/update-copyright.pl and mention them as
  excluded from CVC4 copyright in COPYING.  They are antlr3-derived
  works, covered under a BSD license.

OTHER STUFF:

* expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now
  auto-generated by a "mkexpr" script.  This provides the correct
  instantiations of mkConst() for public use, e.g., by the parser.

* Fix doxygen documentation in expr, expr_manager.. closes bug #35

* Node::isAtomic() implemented in a better way, based on theory kinds
  files.  Fixes bug #40.  To support this, a "nonatomic_operator"
  command has been added.  All other "parameterized" or "operator"
  kinds are atomic.

* Added expr_black test

* Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind
  that takes a "bool" payload; for example, to make "true" you now do
  nodeManager->mkConst(true).

* Make new "cvc4_public.h" and "cvc4parser_public.h" headers.  Private
  headers should include "cvc4_private.h"
  (resp. "cvc4parser_private.h"), which existed previously.  Public
  headers should include the others.  **No one** should include the
  autoheader #include (which has been renamed "cvc4autoconfig.h")
  directly, and public CVC4 headers can't access its #defines.  This
  is to avoid us having the same distribution problem as libantlr3c.

* Preliminary fixes based on Tim's code review of attributes (bug #61).
  This includes splitting hairy template internals into
  attribute_internals.h, for which another code review ticket will be
  opened.  Bug is still outstanding, but pending further
  refactoring/documentation.

* Some *HashFcns renamed to *HashStrategy to match refactoring done
  elsewhere (done by Chris?) earlier this week.

* Simplified creation of make rules for generated files (expr.cpp,
  expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h,
  metakind.h).

* CVC4::Configuration interface and implementation split (so private
  stuff doesn't leak into public headers).

* Some documentation/code formatting fixes.

* Add required versions of autotools to autogen.sh.

* src/expr/mkmetakind: fix a nonportable thing in invocation of "expr"
  that was causing warnings on Red Hat.

* src/context/cdmap.h: add workaround to what appears to be a g++ 4.1
  parsing bug.

1 files changed, 325 insertions, 0 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
new file mode 100644
index 000000000..12307e679
--- /dev/null
+++ b/src/expr/expr_template.h
@@ -0,0 +1,325 @@
+/*********************                                                        */
+/** expr_template.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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.
+ **
+ ** Public-facing expression interface.
+ **/
+
+#include "cvc4_public.h"
+
+// circular dependency: force expr_manager.h first
+#include "expr/expr_manager.h"
+
+#ifndef __CVC4__EXPR_H
+#define __CVC4__EXPR_H
+
+#include <string>
+#include <iostream>
+#include <stdint.h>
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one.  We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 35 "${template}"
+
+namespace CVC4 {
+
+// The internal expression representation
+template <bool ref_count>
+class NodeTemplate;
+
+/**
+ * Class encapsulating CVC4 expressions and methods for constructing new
+ * expressions.
+ */
+class CVC4_PUBLIC Expr {
+protected:
+
+  /** The internal expression representation */
+  NodeTemplate<true>* d_node;
+
+  /** The responsible expression manager */
+  ExprManager* d_exprManager;
+
+  /**
+   * Constructor for internal purposes.
+   * @param em the expression manager that handles this expression
+   * @param node the actual expression node pointer
+   */
+  Expr(ExprManager* em, NodeTemplate<true>* node);
+
+public:
+
+  /** Default constructor, makes a null expression. */
+  Expr();
+
+  /**
+   * Copy constructor, makes a copy of a given expression
+   * @param e the expression to copy
+   */
+  Expr(const Expr& e);
+
+  /**
+   * Initialize from an integer. Fails if the integer is not 0.
+   * NOTE: This is here purely to support the auto-initialization
+   * behavior of the ANTLR3 C backend. Should be removed if future
+   * versions of ANTLR fix the problem.
+   */
+  Expr(uintptr_t n);
+
+  /** Destructor */
+  ~Expr();
+
+  /**
+   * Assignment operator, makes a copy of the given expression. If the
+   * expression managers of the two expressions differ, the expression of
+   * the given expression will be used.
+   * @param e the expression to assign
+   * @return the reference to this expression after assignment
+   */
+  Expr& operator=(const Expr& e);
+
+  /*
+   * Assignment from an integer. Fails if the integer is not 0.
+   * NOTE: This is here purely to support the auto-initialization
+   * behavior of the ANTLR3 C backend (i.e., a rule attribute
+   * <code>Expr e</code> gets initialized with <code>e = NULL;</code>.
+   * Should be removed if future versions of ANTLR fix the problem.
+   */
+  Expr& operator=(uintptr_t n);
+
+  /**
+   * Syntactic comparison operator. Returns true if expressions belong to the
+   * same expression manager and are syntactically identical.
+   * @param e the expression to compare to
+   * @return true if expressions are syntactically the same, false otherwise
+   */
+  bool operator==(const Expr& e) const;
+
+  /**
+   * Syntactic dis-equality operator.
+   * @param e the expression to compare to
+   * @return true if expressions differ syntactically, false otherwise
+   */
+  bool operator!=(const Expr& e) const;
+
+  /**
+   * Order comparison operator. The only invariant on the order of expressions
+   * is that the expressions that were created sooner will be smaller in the
+   * ordering than all the expressions created later. Null expression is the
+   * smallest element of the ordering. The behavior of the operator is
+   * undefined if the expressions come from two different expression managers.
+   * @param e the expression to compare to
+   * @return true if this expression is smaller than the given one
+   */
+  bool operator<(const Expr& e) const;
+
+  /**
+   * Returns the kind of the expression (AND, PLUS ...).
+   * @return the kind of the expression
+   */
+  Kind getKind() const;
+
+  /**
+   * Returns the number of children of this expression.
+   * @return the number of children
+   */
+  size_t getNumChildren() const;
+
+  /**
+   * Check if this is an expression that has an operator.
+   * @return true if this expression has an operator
+   */
+  bool hasOperator() const;
+
+  /**
+   * Get the operator of this expression.
+   * @throws IllegalArgumentException if it has no operator
+   * @return the operator of this expression
+   */
+  Expr getOperator() const;
+
+  /** Returns the type of the expression, if it has been computed.
+   * Returns NULL if the type of the expression is not known.
+   */
+  Type* getType() const;
+
+  /**
+   * Returns the string representation of the expression.
+   * @return a string representation of the expression
+   */
+  std::string toString() const;
+
+  /**
+   * Outputs the string representation of the expression to the stream.
+   * @param out the output stream
+   */
+  void toStream(std::ostream& out) const;
+
+  /**
+   * Check if this is a null expression.
+   * @return true if a null expression
+   */
+  bool isNull() const;
+
+  /**
+   * Check if this is a null expression.
+   * @return true if NOT a null expression
+   */
+  operator bool() const;
+
+  /**
+   * Check if this is an expression representing a constant.
+   * @return true if a constant expression
+   */
+  bool isConst() const;
+
+  /**
+   * Check if this is an expression representing a constant.
+   * @return true if a constant expression
+   */
+  bool isAtomic() const;
+
+  /** Extract a constant of type T */
+  template <class T>
+  const T& getConst() const;
+
+  /**
+   * Returns the expression reponsible for this expression.
+   */
+  ExprManager* getExprManager() const;
+
+  /**
+   * Very basic pretty printer for Expr.
+   * This is equivalent to calling e.getNode().printAst(...)
+   * @param out output stream to print to.
+   * @param indent number of spaces to indent the formula by.
+   */
+  void printAst(std::ostream& out, int indent = 0) const;
+
+private:
+
+  /**
+   * Pretty printer for use within gdb
+   * This is not intended to be used outside of gdb.
+   * This writes to the ostream Warning() and immediately flushes
+   * the ostream.
+   */
+  void debugPrint();
+
+protected:
+
+  /**
+   * Returns the actual internal node.
+   * @return the internal node
+   */
+  NodeTemplate<true> getNode() const;
+
+  // Friend to access the actual internal node information and private methods
+  friend class SmtEngine;
+  friend class ExprManager;
+};
+
+/**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
+/**
+ * Extending the expression with the capability to construct Boolean
+ * expressions.
+ */
+class CVC4_PUBLIC BoolExpr : public Expr {
+
+public:
+
+  /** Default constructor, makes a null expression */
+  BoolExpr();
+
+  /**
+   * Convert an expression to a Boolean expression
+   */
+  BoolExpr(const Expr& e);
+
+  /**
+   * Negate this expression.
+   * @return the logical negation of this expression.
+   */
+  BoolExpr notExpr() const;
+
+  /**
+   * Conjunct the given expression to this expression.
+   * @param e the expression to conjunct
+   * @return the conjunction of this expression and e
+   */
+  BoolExpr andExpr(const BoolExpr& e) const;
+
+  /**
+   * Disjunct the given expression to this expression.
+   * @param e the expression to disjunct
+   * @return the disjunction of this expression and e
+   */
+  BoolExpr orExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an exclusive or expression out of this expression and the given
+   * expression.
+   * @param e the right side of the xor
+   * @return the xor of this expression and e
+   */
+  BoolExpr xorExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an equivalence expression out of this expression and the given
+   * expression.
+   * @param e the right side of the equivalence
+   * @return the equivalence expression
+   */
+  BoolExpr iffExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an implication expression out of this expression and the given
+   * expression.
+   * @param e the right side of the equivalence
+   * @return the equivalence expression
+   */
+  BoolExpr impExpr(const BoolExpr& e) const;
+
+  /**
+   * Make a Boolean if-then-else expression using this expression as the
+   * condition, and given the then and else parts
+   * @param then_e the then branch expression
+   * @param else_e the else branch expression
+   * @return the if-then-else expression
+   */
+  BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
+
+  /**
+   * Make a term if-then-else expression using this expression as the
+   * condition, and given the then and else parts
+   * @param then_e the then branch expression
+   * @param else_e the else branch expression
+   * @return the if-then-else expression
+   */
+  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
+};
+
+${getConst_instantiations}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_H */