fixes/redesign of source layout from meeting

25 files changed, 3 insertions, 1186 deletions

diff --git a/src/include/assert.h b/src/include/assert.h
deleted file mode 100644
index a66503641..000000000
--- a/src/include/assert.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** assert.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_ASSERT_H
-#define __CVC4_ASSERT_H
-
-#include <cassert>
-
-#ifdef DEBUG
-// the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
-#else
-// TODO: use a compiler annotation when assertions are off ?
-// (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
-
-#endif /* __CVC4_ASSERT_H */
diff --git a/src/include/attr_type.h b/src/include/attr_type.h
deleted file mode 100644
index d24385f8e..000000000
--- a/src/include/attr_type.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** attr_type.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_ATTR_TYPE_H
-#define __CVC4_ATTR_TYPE_H
-
-#include "expr_attribute.h"
-
-namespace CVC4 {
-
-class Type;
-
-// an "attribute type" for types
-// this is essentially a traits structure
-class Type_attr {
-public:
-  enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
-  typedef Type value_type;//Expr?
-  static const Type_attr marker;
-};
-
-extern AttrTable<Type_attr> type_table;
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_ATTR_TYPE_H */
diff --git a/src/include/command.h b/src/include/command.h
deleted file mode 100644
index 944b9c621..000000000
--- a/src/include/command.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** command.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_COMMAND_H
-#define __CVC4_COMMAND_H
-
-namespace CVC4 {
-
-class Command { // distinct from Exprs
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_COMMAND_H */
diff --git a/src/include/context.h b/src/include/context.h
deleted file mode 100644
index fce2f0b8d..000000000
--- a/src/include/context.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** context.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_CONTEXT_H
-#define __CVC4_CONTEXT_H
-
-namespace CVC4 {
-
-class Context;
-
-class ContextManager {
-public:
-  void switchContext(Context);
-  Context snapshot();
-};/* class ContextManager */
-
-class ContextObject {
-public:
-  void snapshot();
-  void restore();
-};/* class ContextObject */
-
-template <class T>
-class CDO;
-
-template <class T>
-class CDMap;
-
-template <class T>
-class CDList;
-
-template <class T>
-class CDSet;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_CONTEXT_H */
diff --git a/src/include/vc.h b/src/include/cvc4.h
index 845d1eb6d..109496001 100644
--- a/src/include/vc.h
+++ b/src/include/cvc4.h
@@ -13,7 +13,7 @@
 #define __CVC4_VC_H
 
 #include "command.h"
-#include "expr.h"
+#include "cvc4_expr.h"
 
 /* TODO provide way of querying whether you fall into a fragment /
  * returning what fragment you're in */
diff --git a/src/include/expr.h b/src/include/cvc4_expr.h
index e92ece93d..17e7f4f82 100644
--- a/src/include/expr.h
+++ b/src/include/cvc4_expr.h
@@ -71,6 +71,8 @@ public:
                  const std::vector<Expr>& newTerms) const;
 
   static Expr null() { return s_null; }
+
+  friend class ExprBuilder;
 };/* class Expr */
 
 } /* CVC4 namespace */
diff --git a/src/include/debug.h b/src/include/debug.h
deleted file mode 100644
index 36942d1ae..000000000
--- a/src/include/debug.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** debug.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_DEBUG_H
-#define __CVC4_DEBUG_H
-
-#include <cassert>
-
-#ifdef DEBUG
-// the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
-#else
-// TODO: use a compiler annotation when assertions are off ?
-// (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
-
-#endif /* __CVC4_DEBUG_H */
diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h
deleted file mode 100644
index ec0172535..000000000
--- a/src/include/decision_engine.h
+++ /dev/null
@@ -1,42 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** decision_engine.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_DECISION_ENGINE_H
-#define __CVC4_DECISION_ENGINE_H
-
-#include "literal.h"
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
-/**
- * A decision mechanism for the next decision.
- */
-class DecisionEngine {
-public:
-  /**
-   * Get the next decision.
-   */
-  virtual Literal nextDecision() = 0;
-
-  // TODO: design decision: decision engine should be notified of
-  // propagated lits, and also why(?) (so that it can make decisions
-  // based on the utility of various theories and various theory
-  // literals).  How?  Maybe TheoryEngine has a backdoor into
-  // DecisionEngine "behind the back" of the PropEngine?
-
-};/* class DecisionEngine */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_DECISION_ENGINE_H */
diff --git a/src/include/exception.h b/src/include/exception.h
deleted file mode 100644
index 792a98701..000000000
--- a/src/include/exception.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** exception.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Exception class.
- **/
-
-#ifndef __CVC4_EXCEPTION_H
-#define __CVC4_EXCEPTION_H
-
-#include <string>
-#include <iostream>
-
-namespace CVC4 {
-
-  class Exception {
-  protected:
-    std::string d_msg;
-  public:
-    // Constructors
-    Exception(): d_msg("Unknown exception") { }
-    Exception(const std::string& msg): d_msg(msg) { }
-    Exception(const char* msg): d_msg(msg) { }
-    // Destructor
-    virtual ~Exception() { }
-    // NON-VIRTUAL METHODs for setting and printing the error message
-    void setMessage(const std::string& msg) { d_msg = msg; }
-    // Printing: feel free to redefine toString().  When inherited,
-    // it's recommended that this method print the type of exception
-    // before the actual message.
-    virtual std::string toString() const { return d_msg; }
-    // No need to overload operator<< for the inherited classes
-    friend std::ostream& operator<<(std::ostream& os, const Exception& e);
-
-  }; // end of class Exception
-
-  inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
-    return os << e.toString();
-  }
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_EXCEPTION_H */
diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h
deleted file mode 100644
index 77700096e..000000000
--- a/src/include/expr_attribute.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_attribute.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_EXPR_ATTRIBUTE_H
-#define __CVC4_EXPR_ATTRIBUTE_H
-
-// TODO WARNING this file needs work !
-
-#include <stdint.h>
-#include "config.h"
-#include "context.h"
-#include "expr.h"
-
-namespace CVC4 {
-
-template <class value_type>
-class AttrTables;
-
-// global (or TSS)
-extern CDMap<uint64_t> g_hash_bool;
-extern CDMap<uint64_t> g_hash_int;
-extern CDMap<Expr>     g_hash_expr;
-extern CDMap<void*>    g_hash_ptr;
-
-template <class T>
-class AttrTable;
-
-template <>
-class AttrTable<bool> {
-public:
-  class BitAccessor {
-    uint64_t& d_word;
-    unsigned d_bit;
-  public:
-    BitAccessor& operator=(bool b);
-    // continue...
-  };
-
-  // bool specialization
-  static CDMap<uint64_t> *s_hash;
-
-  template <class Attr>
-  BitAccessor& find(Expr e, const Attr&);
-
-  template <class Attr>
-  bool find(Expr e, const Attr&) const;
-};
-
-template <>
-class AttrTable<uint64_t> {
-public:  
-  // int(egral) specialization
-  static CDMap<uint64_t> *s_hash;
-  uint64_t& find(Expr);
-  uint64_t& find(Expr) const;
-};
-
-template <class T>
-class AttrTable<T*> {
-  // pointer specialization
-  static CDMap<void*> *s_hash;
-public:
-};
-
-template <>
-class AttrTable<Expr> {
-public:
-  // Expr specialization
-  static CDMap<Expr> *s_hash;
-  Expr find(Expr);
-};
-
-CDMap<uint64_t>* AttrTable<bool>::s_hash     = &g_hash_bool;
-CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
-CDMap<Expr>*     AttrTable<Expr>::s_hash     = &g_hash_expr;
-
-template <class T>
-CDMap<void*>*    AttrTable<T*>::s_hash       = &g_hash_ptr;
-
-template <class Attr>
-class AttributeTable {
-  typedef typename Attr::value_type value_type;
-
-  AttrTable<value_type>& d_table;
-  
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_ATTRIBUTE_H */
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
deleted file mode 100644
index a95ecb2e3..000000000
--- a/src/include/expr_builder.h
+++ /dev/null
@@ -1,144 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_builder.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_EXPR_BUILDER_H
-#define __CVC4_EXPR_BUILDER_H
-
-#include <vector>
-#include "expr_manager.h"
-#include "kind.h"
-
-namespace CVC4 {
-
-class AndExprBuilder;
-class OrExprBuilder;
-class PlusExprBuilder;
-class MinusExprBuilder;
-class MultExprBuilder;
-
-class ExprBuilder {
-  ExprManager* d_em;
-
-  Kind d_kind;
-
-  // TODO: store some flags here and install into attribute map when
-  // the expr is created?  (we'd have to do that since we don't know
-  // it's hash code yet)
-
-  // initially false, when you extract the Expr this is set and you can't
-  // extract another
-  bool d_used;
-
-  unsigned d_nchildren;
-  union {
-    ExprValue*         u_arr[10];
-    std::vector<Expr>* u_vec;
-  } d_children;
-
-public:
-
-  ExprBuilder();
-  ExprBuilder(const Expr&);
-  ExprBuilder(const ExprBuilder&);
-
-  // Compound expression constructors
-  ExprBuilder& eqExpr(const Expr& right);
-  ExprBuilder& notExpr();
-  ExprBuilder& negate(); // avoid double-negatives
-  ExprBuilder& andExpr(const Expr& right);
-  ExprBuilder& orExpr(const Expr& right);
-  ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart);
-  ExprBuilder& iffExpr(const Expr& right);
-  ExprBuilder& impExpr(const Expr& right);
-  ExprBuilder& xorExpr(const Expr& right);
-  ExprBuilder& skolemExpr(int i);
-  ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
-                         const std::vector<Expr>& newTerms);
-  /*
-  ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
-  */
-
-  /* TODO design: these modify ExprBuilder */
-  ExprBuilder& operator!() { return notExpr(); }
-  ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
-  ExprBuilder& operator||(const Expr& right) { return orExpr(right);  }
-
-  // "Stream" expression constructor syntax
-  ExprBuilder& operator<<(const Kind& op);
-  ExprBuilder& operator<<(const Expr& child);
-
-  // For pushing sequences of children
-  ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
-  template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
-
-  operator Expr();// not const
-
-  AndExprBuilder   operator&&(Expr);
-  OrExprBuilder    operator||(Expr);
-  PlusExprBuilder  operator+ (Expr);
-  PlusExprBuilder  operator- (Expr);
-  MultExprBuilder  operator* (Expr);
-
-};/* class ExprBuilder */
-
-class AndExprBuilder {
-  ExprManager* d_em;
-
-public:
-
-  AndExprBuilder&   operator&&(Expr);
-  OrExprBuilder     operator||(Expr);
-
-  operator ExprBuilder();
-
-};/* class AndExprBuilder */
-
-class OrExprBuilder {
-  ExprManager* d_em;
-
-public:
-
-  AndExprBuilder    operator&&(Expr);
-  OrExprBuilder&    operator||(Expr);
-
-  operator ExprBuilder();
-
-};/* class OrExprBuilder */
-
-class PlusExprBuilder {
-  ExprManager* d_em;
-
-public:
-
-  PlusExprBuilder&  operator+(Expr);
-  PlusExprBuilder&  operator-(Expr);
-  MultExprBuilder   operator*(Expr);
-
-  operator ExprBuilder();
-
-};/* class PlusExprBuilder */
-
-class MultExprBuilder {
-  ExprManager* d_em;
-
-public:
-
-  PlusExprBuilder   operator+(Expr);
-  PlusExprBuilder   operator-(Expr);
-  MultExprBuilder&  operator*(Expr);
-
-  operator ExprBuilder();
-
-};/* class MultExprBuilder */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_BUILDER_H */
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
deleted file mode 100644
index 59a3eb7a3..000000000
--- a/src/include/expr_manager.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_manager.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_EXPR_MANAGER_H
-#define __CVC4_EXPR_MANAGER_H
-
-#include <vector>
-#include "expr.h"
-#include "kind.h"
-
-namespace CVC4 {
-
-class ExprManager {
-  static __thread ExprManager* s_current;
-
-public:
-  static ExprManager* currentEM() { return s_current; }
-
-  // general expression-builders
-  Expr mkExpr(Kind kind);
-  Expr mkExpr(Kind kind, Expr child1);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  // N-ary version
-  Expr mkExpr(Kind kind, std::vector<Expr> children);
-
-  // TODO: these use the current EM (but must be renamed)
-  /*
-  static Expr mkExpr(Kind kind)
-  { currentEM()->mkExpr(kind); }
-  static Expr mkExpr(Kind kind, Expr child1);
-  { currentEM()->mkExpr(kind, child1); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2);
-  { currentEM()->mkExpr(kind, child1, child2); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-  { currentEM()->mkExpr(kind, child1, child2, child3); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
-  */
-
-  // do we want a varargs one?  perhaps not..
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_MANAGER_H */
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
deleted file mode 100644
index ea14c3fa7..000000000
--- a/src/include/expr_value.h
+++ /dev/null
@@ -1,71 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_value.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
- ** reference count on ExprValue instances and
- **/
-
-#ifndef __CVC4_EXPR_VALUE_H
-#define __CVC4_EXPR_VALUE_H
-
-#include <stdint.h>
-#include "expr.h"
-
-namespace CVC4 {
-
-/**
- * This is an ExprValue.
- */
-class ExprValue {
-  // this header fits into one 64-bit word
-
-  /** The ID */
-  unsigned d_id        : 32;
-
-  /** The expression's reference count.  @see cvc4::Expr. */
-  unsigned d_rc        :  8;
-
-  /** Kind of the expression */
-  unsigned d_kind      :  8;
-
-  /** Number of children */
-  unsigned d_nchildren : 16;
-
-  /** Variable number of child nodes */
-  Expr     d_children[0];
-
-  friend class Expr;
-
-public:
-  /** Hash this expression.
-   *  @return the hash value of this expression. */
-  uint64_t hash() const;
-
-  // Iterator support
-
-  typedef Expr* iterator;
-  typedef Expr const* const_iterator;
-
-  iterator begin();
-  iterator end();
-  iterator rbegin();
-  iterator rend();
-
-  const_iterator begin() const;
-  const_iterator end() const;
-  const_iterator rbegin() const;
-  const_iterator rend() const;
-};
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_EXPR_VALUE_H */
diff --git a/src/include/kind.h b/src/include/kind.h
deleted file mode 100644
index 5d99330ca..000000000
--- a/src/include/kind.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** kind.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_KIND_H
-#define __CVC4_KIND_H
-
-namespace CVC4 {
-
-// TODO: create this file (?) from theory solver headers so that we
-// have a collection of kinds from all.  This file is mainly a
-// placeholder for design & development work.
-
-enum Kind {
-  AND,
-  OR,
-  XOR,
-  NOT,
-  PLUS,
-  MINUS,
-  ITE,
-  IFF,
-  SKOLEM,
-  SUBST
-};/* enum Kind */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_KIND_H */
diff --git a/src/include/literal.h b/src/include/literal.h
deleted file mode 100644
index 8b147c640..000000000
--- a/src/include/literal.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** literal.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_LITERAL_H
-#define __CVC4_LITERAL_H
-
-namespace CVC4 {
-
-class Literal;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_LITERAL_H */
diff --git a/src/include/model.h b/src/include/model.h
deleted file mode 100644
index c07b75dfa..000000000
--- a/src/include/model.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** model.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_MODEL_H
-#define __CVC4_MODEL_H
-
-namespace CVC4 {
-
-class Model {
-};/* class Model */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_MODEL_H */
diff --git a/src/include/parser.h b/src/include/parser.h
deleted file mode 100644
index e30b31b1c..000000000
--- a/src/include/parser.h
+++ /dev/null
@@ -1,64 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** parser.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Parser abstraction.
- **/
-
-#ifndef __CVC4_PARSER_H
-#define __CVC4_PARSER_H
-
-#include "exception.h"
-#include "lang.h"
-
-namespace CVC4 {
-
-  class ValidityChecker;
-  class Expr;
-  
-  // Internal parser state and other data
-  class ParserData;
-
-  class Parser {
-  private:
-    ParserData* d_data;
-    // Internal methods for constructing and destroying the actual parser
-    void initParser();
-    void deleteParser();
-  public:
-    // Constructors
-    Parser(ValidityChecker* vc, InputLanguage lang,
-	   // The 'interactive' flag is ignored when fileName != ""
-	   bool interactive = true,
-	   const std::string& fileName = "");
-    Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
-	   bool interactive = false);
-    // Destructor
-    ~Parser();
-    // Read the next command.  
-    Expr next();
-    // Check if we are done (end of input has been reached)
-    bool done() const;
-    // The same check can be done by using the class Parser's value as
-    // a Boolean
-    operator bool() const { return done(); }
-    void printLocation(std::ostream & out) const;
-    // Reset any local data that depends on validity checker
-    void reset();
-  }; // end of class Parser
-
-  // The global pointer to ParserTemp.  Each instance of class Parser
-  // sets this pointer before any calls to the lexer.  We do it this
-  // way because flex and bison use global vars, and we want each
-  // Parser object to appear independent.
-  class ParserTemp;
-  extern ParserTemp* parserTemp;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_H */
diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h
deleted file mode 100644
index debb75e70..000000000
--- a/src/include/parser_exception.h
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** parser_exception.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- ** Exception class.
- **/
-
-#ifndef __CVC4_PARSER_EXCEPTION_H
-#define __CVC4_PARSER_EXCEPTION_H
-
-#include "exception.h"
-#include <string>
-#include <iostream>
-
-namespace CVC4 {
-
-  class ParserException: public Exception {
-  public:
-    // Constructors
-    ParserException() { }
-    ParserException(const std::string& msg): Exception(msg) { }
-    ParserException(const char* msg): Exception(msg) { }
-    // Destructor
-    virtual ~ParserException() { }
-    virtual std::string toString() const {
-      return "Parse Error: " + d_msg;
-    }
-  }; // end of class ParserException
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_EXCEPTION_H */
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
deleted file mode 100644
index de25c5594..000000000
--- a/src/include/prop_engine.h
+++ /dev/null
@@ -1,43 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** prop_engine.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_PROP_ENGINE_H
-#define __CVC4_PROP_ENGINE_H
-
-#include "expr.h"
-#include "decision_engine.h"
-#include "theory_engine.h"
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// Prover and above (and requires the services of) a specific
-// propositional solver, DPLL or otherwise.
-
-class PropEngine {
-  DecisionEngine* d_de;
-
-public:
-  /**
-   * Create a PropEngine with a particular decision and theory engine.
-   */
-  PropEngine(DecisionEngine*, TheoryEngine*);
-
-  /**
-   * Converts to CNF if necessary.
-   */
-  void solve(Expr);
-
-};/* class PropEngine */
-
-}
-
-#endif /* __CVC4_PROP_ENGINE_H */
diff --git a/src/include/prover.h b/src/include/prover.h
deleted file mode 100644
index de29f48c0..000000000
--- a/src/include/prover.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** prover.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_PROVER_H
-#define __CVC4_PROVER_H
-
-#include <vector>
-#include "expr.h"
-#include "result.h"
-#include "model.h"
-
-// In terms of abstraction, this is below (and provides services to)
-// ValidityChecker and above (and requires the services of)
-// PropEngine.
-
-namespace CVC4 {
-
-// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
-// hood): use a type parameter and have check() delegate, or subclass
-// Prover and override check()?
-//
-// Probably better than that is to have a configuration object that
-// indicates which passes are desired.  The configuration occurs
-// elsewhere (and can even occur at runtime).  A simple "pass manager"
-// of sorts determines check()'s behavior.
-//
-// The CNF conversion can go on in PropEngine.
-
-class Prover {
-  /** Current set of assertions. */
-  // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Expr> d_assertList;
-
-private:
-  /**
-   * Pre-process an Expr.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Expr.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-  void preprocess(Expr);
-
-  /**
-   * Adds a formula to the current context.
-   */
-  void addFormula(Expr);
-
-  /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
-
-  /**
-   * Quick check of consistency in current context: calls
-   * processAssertionList() then look for inconsistency (based only on
-   * that).
-   */
-  Result quickCheck();
-
-  /**
-   * Process the assertion list: for literals and conjunctions of
-   * literals, assert to T-solver.
-   */
-  void processAssertionList();
-
-public:
-  /**
-   * Add a formula to the current context: preprocess, do per-theory
-   * setup, use processAssertionList(), asserting to T-solver for
-   * literals and conjunction of literals.  Returns false iff
-   * inconsistent.
-   */
-  Result assert(Expr);
-
-  /**
-   * Add a formula to the current context and call check().  Returns
-   * true iff consistent.
-   */
-  Result query(Expr);
-
-  /**
-   * Simplify a formula without doing "much" work.  Requires assist
-   * from the SAT Engine.
-   */
-  Expr simplify(Expr);
-
-  /**
-   * Get a (counter)model (only if preceded by a SAT or INVALID query.
-   */
-  Model getModel();
-
-  /**
-   * Push a user-level context.
-   */
-  void push();
-
-  /**
-   * Pop a user-level context.  Throws an exception if nothing to pop.
-   */
-  void pop();
-};/* class Prover */
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_PROVER_H */
diff --git a/src/include/result.h b/src/include/result.h
deleted file mode 100644
index 50f488682..000000000
--- a/src/include/result.h
+++ /dev/null
@@ -1,65 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** result.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_RESULT_H
-#define __CVC4_RESULT_H
-
-namespace CVC4 {
-
-// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
-// but this requires doing the same for Prover and needs discussion.
-
-// TODO: subclass to provide models, etc.  This is really just
-// intended as a three-valued response code.
-
-/**
- * Three-valued, immutable SMT result, with optional explanation.
- */
-class Result {
-public:
-  enum SAT {
-    UNSAT = 0,
-    SAT = 1,
-    SAT_UNKNOWN = 2
-  };
-
-  enum Validity {
-    INVALID = 0,
-    VALID = 1,
-    VALIDITY_UNKNOWN = 2
-  };
-
-  enum UnknownExplanation {
-    REQUIRES_FULL_CHECK,
-    INCOMPLETE,
-    TIMEOUT,
-    BAIL,
-    OTHER
-  };
-
-private:
-  enum SAT      d_sat;
-  enum Validity d_validity;
-  enum { TYPE_SAT, TYPE_VALIDITY } d_which;
-
-public:
-  Result(enum SAT);
-  Result(enum Validity);
-
-  enum SAT isSAT();
-  enum Validity isValid();
-  enum UnknownExplanation whyUnknown();
-
-};/* class Result */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_RESULT_H */
diff --git a/src/include/sat.h b/src/include/sat.h
deleted file mode 100644
index 00a94c142..000000000
--- a/src/include/sat.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** sat.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_SAT_H
-#define __CVC4_SAT_H
-
-namespace CVC4 {
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_SAT_H */
diff --git a/src/include/theory.h b/src/include/theory.h
deleted file mode 100644
index 935c23b08..000000000
--- a/src/include/theory.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** theory.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_THEORY_H
-#define __CVC4_THEORY_H
-
-#include "expr.h"
-#include "literal.h"
-
-namespace CVC4 {
-
-/**
- * Base class for T-solvers.  Abstract DPLL(T).
- */
-class Theory {
-public:
-  /**
-   * Subclasses of Theory may add additional efforts.  DO NOT CHECK
-   * equality with one of these values (e.g. if STANDARD xxx) but
-   * rather use range checks (or use the helper functions below).
-   * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
-   * with MAX_EFFORT.
-   */
-  enum Effort {
-    MIN_EFFORT = 0,
-    QUICK_CHECK = 10,
-    STANDARD = 50,
-    FULL_EFFORT = 100
-  };/* enum Effort */
-
-  // TODO add compiler annotation "constant function" here
-  static bool minEffortOnly(Effort e)        { return e == MIN_EFFORT; }
-  static bool quickCheckOrMore(Effort e)     { return e >= QUICK_CHECK; }
-  static bool quickCheckOnly(Effort e)       { return e >= QUICK_CHECK && e < STANDARD; }
-  static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
-  static bool standardEffortOnly(Effort e)   { return e >= STANDARD && e < FULL_EFFORT; }
-  static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
-
-  /**
-   * Prepare for an Expr.
-   */
-  virtual void setup(Expr) = 0;
-
-  /**
-   * Assert a literal in the current context.
-   */
-  virtual void assert(Literal) = 0;
-
-  /**
-   * Check the current assignment's consistency.  Return false iff inconsistent.
-   */
-  virtual bool check(Effort level = FULL_EFFORT) = 0;
-
-  /**
-   * T-propagate new literal assignments in the current context.
-   */
-  // TODO design decision: instead of returning a set of literals
-  // here, perhaps we have an interface back into the prop engine
-  // where we assert directly.  we might sometimes unknowingly assert
-  // something clearly inconsistent (esp. in a parallel context).
-  // This would allow the PropEngine to cancel our further work since
-  // we're already inconsistent---also could strategize dynamically on
-  // whether enough theory prop work has occurred.
-  virtual void propagate(Effort level = FULL_EFFORT) = 0;
-
-  /**
-   * Return an explanation for the literal (which was previously propagated by this theory)..
-   */
-  virtual Expr explain(Literal) = 0;
-
-};/* class Theory */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_THEORY_H */
diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h
deleted file mode 100644
index 2a0841d8d..000000000
--- a/src/include/theory_engine.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** theory_engine.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_THEORY_ENGINE_H
-#define __CVC4_THEORY_ENGINE_H
-
-namespace CVC4 {
-
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
-/**
- * This is essentially an abstraction for a collection of theories.  A
- * TheoryEngine provides services to a PropEngine, making various
- * T-solvers look like a single unit to the propositional part of
- * CVC4.
- */
-class TheoryEngine {
-public:
-};/* class TheoryEngine */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_THEORY_ENGINE_H */
diff --git a/src/include/unique_id.h b/src/include/unique_id.h
deleted file mode 100644
index 1a6f3427a..000000000
--- a/src/include/unique_id.h
+++ /dev/null
@@ -1,35 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** unique_id.h
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 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.
- **
- **/
-
-#ifndef __CVC4_UNIQUE_ID_H
-#define __CVC4_UNIQUE_ID_H
-
-namespace CVC4 {
-
-// NOTE that UniqueID is intended for startup registration; it
-// shouldn't be used in multi-threaded contexts.
-
-template <class T>
-class UniqueID {
-  static unsigned s_topID;
-  const unsigned d_thisID;
-
-public:
-  UniqueID() : d_thisID( s_topID++ ) { }
-  operator unsigned() const { return d_thisID; }
-};
-
-template <class T>
-unsigned UniqueID<T>::s_topID = 0;
-
-} /* CVC4 namespace */
-
-#endif /* __CVC4_UNIQUE_ID_H */