commit of project structure including autotools support

15 files changed, 611 insertions, 0 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
new file mode 100644
index 000000000..11fef4d27
--- /dev/null
+++ b/src/Makefile.am
@@ -0,0 +1 @@
+INCLUDES = -I@srcdir@/include
diff --git a/src/include/Makefile.am b/src/include/Makefile.am
new file mode 100644
index 000000000..fa37abd9a
--- /dev/null
+++ b/src/include/Makefile.am
@@ -0,0 +1,14 @@
+EXTRA_DIST = \
+	assert.h \
+	attr_type.h \
+	command.h
+	expr_attribute.h \
+	expr_builder.h \
+	expr.h \
+	expr_manager.h \
+	expr_value.h \
+	kind.h \
+	parser.h \
+	sat.h \
+	unique_id.h \
+	vc.h
diff --git a/src/include/assert.h b/src/include/assert.h
new file mode 100644
index 000000000..473cd21f1
--- /dev/null
+++ b/src/include/assert.h
@@ -0,0 +1,24 @@
+/*********************                                           -*- C++ -*-  */
+/** assert.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#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
new file mode 100644
index 000000000..a546d7dab
--- /dev/null
+++ b/src/include/attr_type.h
@@ -0,0 +1,28 @@
+/*********************                                           -*- C++ -*-  */
+/** attr_type.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_ATTR_TYPE_H
+#define __CVC4_ATTR_TYPE_H
+
+namespace CVC4 {
+
+// 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 value_type Type;//Expr?
+  static const Type_attr marker;
+};
+
+AttributeTable<Type_attr>
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_ATTR_TYPE_H */
diff --git a/src/include/command.h b/src/include/command.h
new file mode 100644
index 000000000..45b59a95b
--- /dev/null
+++ b/src/include/command.h
@@ -0,0 +1,20 @@
+/*********************                                           -*- C++ -*-  */
+/** command.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#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/expr.h b/src/include/expr.h
new file mode 100644
index 000000000..5e3559fd7
--- /dev/null
+++ b/src/include/expr.h
@@ -0,0 +1,54 @@
+/*********************                                           -*- C++ -*-  */
+/** expr.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_H
+#define __CVC4_EXPR_H
+
+namespace CVC4 {
+
+class ExprValue;
+
+/**
+ * Encapsulation of an ExprValue pointer.  The reference count is
+ * maintained in the ExprValue.
+ */
+class Expr {
+  /** A convenient null-valued encapsulated pointer */
+  static Expr s_null;
+
+  /** The referenced ExprValue */
+  ExprValue* d_ev;
+
+  /** This constructor is reserved for use by the Expr package; one
+   *  must construct an Expr using one of the build mechanisms of the
+   *  Expr package.
+   *
+   *  Increments the reference count. */
+  explicit Expr(ExprValue*);
+
+  /** Destructor.  Decrements the reference count and, if zero,
+   *  collects the ExprValue. */
+  ~Expr();
+
+public:
+  /** Access to the encapsulated expression.
+   *  @return the encapsulated expression. */
+  ExprValue* operator->();
+
+  /** Const access to the encapsulated expressoin.
+   *  @return the encapsulated expression [const]. */
+  const ExprValue* operator->() const;
+
+};/* class Expr */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_H */
diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h
new file mode 100644
index 000000000..b5f7dfe13
--- /dev/null
+++ b/src/include/expr_attribute.h
@@ -0,0 +1,84 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_attribute.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_ATTRIBUTE_H
+#define __CVC4_EXPR_ATTRIBUTE_H
+
+namespace CVC4 {
+
+template <class value_type>
+class AttrTables;
+
+// global (or TSS)
+extern CDMap<uint_64t> g_hash_bool;
+extern CDMap<uint_64t> g_hash_int;
+extern CDMap<Expr>     g_hash_expr;
+extern CDMap<void*>    g_hash_ptr;
+
+template <>
+class AttrTable<bool> {
+public:
+  class BitAccessor {
+    uint64_t& d_word;
+    unsigned d_bit;
+  public:
+    BitAccessor& operator=(bool b);
+    // continue...
+  };
+
+  // bool specialization
+  static CDMap<uint_64t> *s_hash;
+
+  template <class Attr>
+  BitAccessor& find(Expr e, const Attr&);
+
+  template <class Attr>
+  bool find(Expr e, const Attr&) const;
+};
+
+template <>
+class AttrTable<uint_64t> {
+public:  
+  // int(egral) specialization
+  static CDMap<uint64_t> *s_hash;
+  uint_64t& find(x);
+  uint_64t& find(x) 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;
+  find(x)
+};
+
+template <> AttrTable<bool>::s_hash     = &g_hash_bool;
+template <> AttrTable<uint_64t>::s_hash = &g_hash_int;
+template <> AttrTable<Expr>::s_hash     = &g_hash_expr;
+template <> AttrTable<void*>::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
new file mode 100644
index 000000000..2e9bf49a4
--- /dev/null
+++ b/src/include/expr_builder.h
@@ -0,0 +1,131 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_builder.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_BUILDER_H
+#define __CVC4_EXPR_BUILDER_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 {
+    Expr         u_arr[10];
+    vector<Expr> u_vec;
+  } d_children;
+
+public:
+
+  // 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);
+
+  ExprBuilder& operator!() const { return notExpr(); }
+  ExprBuilder& operator&&(const Expr& right) const { return andExpr(right); }
+  ExprBuilder& operator||(const Expr& right) const { return orExpr(right);  }
+
+  // "Stream" expression constructor syntax
+  ExprBuilder& operator<<(const Op& op);
+  ExprBuilder& operator<<(const Expr& child);
+
+  // For pushing sequences of children
+  ExprBuilder& append(const 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
new file mode 100644
index 000000000..f49235831
--- /dev/null
+++ b/src/include/expr_manager.h
@@ -0,0 +1,68 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_MANAGER_H
+#define __CVC4_EXPR_MANAGER_H
+
+namespace CVC4 {
+
+class ExprManager {
+  static __thread ExprManager* current;
+
+public:
+  static ExprManager* currentEM() { return d_current; }
+
+  // general expression-builders
+  Expr build(Kind kind);
+  Expr build(Kind kind, Expr child1);
+  Expr build(Kind kind, Expr child1, Expr child2);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
+  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
+  // N-ary version
+  Expr build(Kind kind, vector<Expr> children);
+
+  // these use the current EM
+  static Expr build(Kind kind)
+  { currentEM()->build(kind); }
+  static Expr build(Kind kind, Expr child1);
+  { currentEM()->build(kind, child1); }
+  static Expr build(Kind kind, Expr child1, Expr child2);
+  { currentEM()->build(kind, child1, child2); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
+  { currentEM()->build(kind, child1, child2, child3); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+  { currentEM()->build(kind, child1, child2, child3, child4); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); }
+  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
+  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); }
+  // N-ary version
+  static Expr build(Kind kind, vector<Expr> children)
+  { currentEM()->build(kind, children); }
+
+  // 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
new file mode 100644
index 000000000..ca12b8e03
--- /dev/null
+++ b/src/include/expr_value.h
@@ -0,0 +1,71 @@
+/*********************
+/** expr_value.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** 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
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_VALUE_H
+#define __CVC4_EXPR_VALUE_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];
+
+public:
+  /** Hash this expression.
+   *  @return the hash value of this expression. */
+  unsigned hash() const;
+
+  /** Convert to (wrap in) an Expr.
+   *  @return an Expr pointing to this expression. */
+  operator Expr();
+
+  // 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
new file mode 100644
index 000000000..26a3dd607
--- /dev/null
+++ b/src/include/kind.h
@@ -0,0 +1,24 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXPR_MANAGER_H
+#define __CVC4_EXPR_MANAGER_H
+
+namespace CVC4 {
+
+enum Kind {
+  AND,
+  OR,
+  XOR,
+  NOT,
+  PLUS,
+  MINUS,
+  UMINUS,
+  
+};
diff --git a/src/include/parser.h b/src/include/parser.h
new file mode 100644
index 000000000..0cfc89a28
--- /dev/null
+++ b/src/include/parser.h
@@ -0,0 +1,17 @@
+/*********************                                           -*- C++ -*-  */
+/** parser.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PARSER_H
+#define __CVC4_PARSER_H
+
+namespace CVC4 {
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_H */
diff --git a/src/include/sat.h b/src/include/sat.h
new file mode 100644
index 000000000..13578ec8d
--- /dev/null
+++ b/src/include/sat.h
@@ -0,0 +1,17 @@
+/*********************                                           -*- C++ -*-  */
+/** sat.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_SAT_H
+#define __CVC4_SAT_H
+
+namespace CVC4 {
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_SAT_H */
diff --git a/src/include/unique_id.h b/src/include/unique_id.h
new file mode 100644
index 000000000..55fa24e51
--- /dev/null
+++ b/src/include/unique_id.h
@@ -0,0 +1,33 @@
+/*********************                                           -*- C++ -*-  */
+/** unique_id.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#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 */
diff --git a/src/include/vc.h b/src/include/vc.h
new file mode 100644
index 000000000..d4b293a28
--- /dev/null
+++ b/src/include/vc.h
@@ -0,0 +1,25 @@
+/*********************                                           -*- C++ -*-  */
+/** vc.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_VC_H
+#define __CVC4_VC_H
+
+/* TODO provide way of querying whether you fall into a fragment /
+ * returning what fragment you're in */
+
+namespace CVC4 {
+
+class ValidityChecker {
+public:
+  void doCommand(Command);
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_VC_H */