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, 0 insertions, 167 deletions

diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
deleted file mode 100644
index f2009ad80..000000000
--- a/src/expr/expr_manager.h
+++ /dev/null
@@ -1,167 +0,0 @@
-/*********************                                                        */
-/** expr_manager.h
- ** Original author: dejan
- ** Major contributors: cconway, mdeters
- ** Minor contributors (to current version): taking
- ** 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 manager interface.
- **/
-
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
-
-#include "cvc4_config.h"
-#include "expr/kind.h"
-#include <vector>
-
-namespace CVC4 {
-
-class Expr;
-class Type;
-class BooleanType;
-class FunctionType;
-class KindType;
-class SmtEngine;
-class NodeManager;
-
-namespace context {
-  class Context;
-}/* CVC4::context namespace */
-
-class CVC4_PUBLIC ExprManager {
-
-public:
-
-  /**
-   * Creates an expression manager.
-   */
-  ExprManager();
-
-  /**
-   * Destroys the expression manager. No will be deallocated at this point, so
-   * any expression references that used to be managed by this expression
-   * manager and are left-over are bad.
-   */
-  ~ExprManager();
-
-  /** Get the type for booleans */
-  BooleanType* booleanType() const;
-
-  /** Get the type for sorts. */
-  KindType* kindType() const;
-
-  /**
-   * Make a unary expression of a given kind (TRUE, FALSE,...).
-   * @param kind the kind of expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind);
-
-  /**
-   * Make a unary expression of a given kind (NOT, BVNOT, ...).
-   * @param kind the kind of expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, const Expr& child1);
-
-  /**
-   * Make a binary expression of a given kind (AND, PLUS, ...).
-   * @param kind the kind of expression
-   * @param child1 the first child of the new expression
-   * @param child2 the second child of the new expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
-
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4, const Expr& child5);
-
-  /**
-   * Make an n-ary expression of given kind given a vector of it's children
-   * @param kind the kind of expression to build
-   * @param children the subexpressions
-   * @return the n-ary expression
-   */
-  Expr mkExpr(Kind kind, const std::vector<Expr>& children);
-
-  /** Make a function type from domain to range. */
-  FunctionType*
-    mkFunctionType(Type* domain,
-                   Type* range);
-
-  /** Make a function type with input types from argTypes. <code>argTypes</code>
-   * must have at least one element. */
-  FunctionType*
-    mkFunctionType(const std::vector<Type*>& argTypes,
-                   Type* range);
-
-  /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
-   * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
-   * least 2 elements.
-   */
-  FunctionType*
-    mkFunctionType(const std::vector<Type*>& sorts);
-
-  /** Make a predicate type with input types from <code>sorts</code>. The result with
-   * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
-   * least one element.
-   */
-  FunctionType*
-    mkPredicateType(const std::vector<Type*>& sorts);
-
-  /** Make a new sort with the given name. */
-  Type* mkSort(const std::string& name);
-
-  // variables are special, because duplicates are permitted
-  Expr mkVar(Type* type, const std::string& name);
-  Expr mkVar(Type* type);
-
-  /** Returns the minimum arity of the given kind. */
-  static unsigned int minArity(Kind kind);
-
-  /** Returns the maximum arity of the given kind. */
-  static unsigned int maxArity(Kind kind);
-
-private:
-  /** The context */
-  context::Context* d_ctxt;
-
-  /** The internal node manager */
-  NodeManager* d_nodeManager;
-
-  /**
-   * Returns the internal node manager.  This should only be used by
-   * internal users, i.e. the friend classes.
-   */
-  NodeManager* getNodeManager() const;
-
-  /**
-   * Returns the internal Context.  Used by internal users, i.e. the
-   * friend classes.
-   */
-  context::Context* getContext() const;
-
-  /**
-   * SmtEngine will use all the internals, so it will grab the
-   * NodeManager.
-   */
-  friend class SmtEngine;
-
-  /** ExprManagerScope reaches in to get the NodeManager */
-  friend class ExprManagerScope;
-};
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_MANAGER_H */
-