additional headers and modifications; now passes syntax check

15 files changed, 155 insertions, 41 deletions

diff --git a/src/include/attr_type.h b/src/include/attr_type.h
index a546d7dab..e5eb222fe 100644
--- a/src/include/attr_type.h
+++ b/src/include/attr_type.h
@@ -10,18 +10,22 @@
 #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 value_type Type;//Expr?
+  typedef Type value_type;//Expr?
   static const Type_attr marker;
 };
 
-AttributeTable<Type_attr>
+extern AttrTable<Type_attr> type_table;
 
 } /* CVC4 namespace */
 
diff --git a/src/include/context.h b/src/include/context.h
index 845660ed7..1997e63d6 100644
--- a/src/include/context.h
+++ b/src/include/context.h
@@ -12,6 +12,8 @@
 
 namespace CVC4 {
 
+class Context;
+
 class ContextManager {
 public:
   void switchContext(Context);
@@ -24,6 +26,18 @@ public:
   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/decision_engine.h b/src/include/decision_engine.h
index 6ff8d7f29..8745adad5 100644
--- a/src/include/decision_engine.h
+++ b/src/include/decision_engine.h
@@ -7,6 +7,8 @@
  ** New York University
  **/
 
+#include "literal.h"
+
 #ifndef __CVC4_DECISION_ENGINE_H
 #define __CVC4_DECISION_ENGINE_H
 
diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h
index b5f7dfe13..1c10a6663 100644
--- a/src/include/expr_attribute.h
+++ b/src/include/expr_attribute.h
@@ -10,17 +10,27 @@
 #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<uint_64t> g_hash_bool;
-extern CDMap<uint_64t> g_hash_int;
+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:
@@ -33,7 +43,7 @@ public:
   };
 
   // bool specialization
-  static CDMap<uint_64t> *s_hash;
+  static CDMap<uint64_t> *s_hash;
 
   template <class Attr>
   BitAccessor& find(Expr e, const Attr&);
@@ -43,12 +53,12 @@ public:
 };
 
 template <>
-class AttrTable<uint_64t> {
+class AttrTable<uint64_t> {
 public:  
   // int(egral) specialization
   static CDMap<uint64_t> *s_hash;
-  uint_64t& find(x);
-  uint_64t& find(x) const;
+  uint64_t& find(Expr);
+  uint64_t& find(Expr) const;
 };
 
 template <class T>
@@ -63,13 +73,15 @@ class AttrTable<Expr> {
 public:
   // Expr specialization
   static CDMap<Expr> *s_hash;
-  find(x)
+  Expr find(Expr);
 };
 
-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;
+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 {
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
index 2e9bf49a4..59503aa4f 100644
--- a/src/include/expr_builder.h
+++ b/src/include/expr_builder.h
@@ -10,6 +10,10 @@
 #ifndef __CVC4_EXPR_BUILDER_H
 #define __CVC4_EXPR_BUILDER_H
 
+#include <vector>
+#include "expr_manager.h"
+#include "kind.h"
+
 namespace CVC4 {
 
 class AndExprBuilder;
@@ -33,8 +37,8 @@ class ExprBuilder {
 
   unsigned d_nchildren;
   union {
-    Expr         u_arr[10];
-    vector<Expr> u_vec;
+    ExprValue*         u_arr[10];
+    std::vector<Expr>* u_vec;
   } d_children;
 
 public:
@@ -52,18 +56,21 @@ public:
   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);  }
+  /* 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 Op& op);
+  ExprBuilder& operator<<(const Kind& op);
   ExprBuilder& operator<<(const Expr& child);
 
   // For pushing sequences of children
-  ExprBuilder& append(const vector<Expr>& children) { return append(children.begin(), children.end()); }
+  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
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
index f49235831..0c265f57f 100644
--- a/src/include/expr_manager.h
+++ b/src/include/expr_manager.h
@@ -10,13 +10,17 @@
 #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* current;
+  static __thread ExprManager* s_current;
 
 public:
-  static ExprManager* currentEM() { return d_current; }
+  static ExprManager* currentEM() { return s_current; }
 
   // general expression-builders
   Expr build(Kind kind);
@@ -31,9 +35,10 @@ public:
   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);
+  Expr build(Kind kind, std::vector<Expr> children);
 
-  // these use the current EM
+  // TODO: these use the current EM (but must be renamed)
+  /*
   static Expr build(Kind kind)
   { currentEM()->build(kind); }
   static Expr build(Kind kind, Expr child1);
@@ -59,6 +64,7 @@ public:
   // N-ary version
   static Expr build(Kind kind, vector<Expr> children)
   { currentEM()->build(kind, children); }
+  */
 
   // do we want a varargs one?  perhaps not..
 };
diff --git a/src/include/kind.h b/src/include/kind.h
index f45495bb0..9307cc677 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -26,3 +26,5 @@ enum Kind {
 };/* enum Kind */
 
 }/* CVC4 namespace */
+
+#endif /* __CVC4_KIND_H */
diff --git a/src/include/literal.h b/src/include/literal.h
new file mode 100644
index 000000000..93855edb8
--- /dev/null
+++ b/src/include/literal.h
@@ -0,0 +1,19 @@
+/*********************                                           -*- C++ -*-  */
+/** literal.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_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
new file mode 100644
index 000000000..205dcf18f
--- /dev/null
+++ b/src/include/model.h
@@ -0,0 +1,20 @@
+/*********************                                           -*- C++ -*-  */
+/** model.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_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
index 8f1032286..c5af769e3 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -10,6 +10,10 @@
 #ifndef __CVC4_PARSER_H
 #define __CVC4_PARSER_H
 
+#include <iostream>
+#include "vc.h"
+#include "expr.h"
+
 namespace CVC4 {
 
 // In terms of abstraction, this is below (and provides services to)
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
index 1ec0316a9..90d07a47b 100644
--- a/src/include/prop_engine.h
+++ b/src/include/prop_engine.h
@@ -10,6 +10,10 @@
 #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)
diff --git a/src/include/prover.h b/src/include/prover.h
index 7abfafe63..e48d6336c 100644
--- a/src/include/prover.h
+++ b/src/include/prover.h
@@ -10,6 +10,11 @@
 #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.
diff --git a/src/include/result.h b/src/include/result.h
index 1cecc5301..cfabd3be2 100644
--- a/src/include/result.h
+++ b/src/include/result.h
@@ -23,39 +23,41 @@ namespace CVC4 {
  */
 class Result {
 public:
-  enum {
+  enum SAT {
     UNSAT = 0,
     SAT = 1,
-    UNKNOWN = 2
-  } SAT;
+    SAT_UNKNOWN = 2
+  };
 
-  enum {
+  enum Validity {
     INVALID = 0,
     VALID = 1,
-    UNKNOWN = 2
-  } Validity;
+    VALIDITY_UNKNOWN = 2
+  };
 
-  enum {
+  enum UnknownExplanation {
     REQUIRES_FULL_CHECK,
     INCOMPLETE,
     TIMEOUT,
     BAIL,
     OTHER
-  } UnknownExplanation;
+  };
 
 private:
-  SAT      d_sat;
-  Validity d_validity;
-  enum { SAT, VALIDITY } d_which;
+  enum SAT      d_sat;
+  enum Validity d_validity;
+  enum { TYPE_SAT, TYPE_VALIDITY } d_which;
 
 public:
-  Result(SAT);
-  Result(Validity);
+  Result(enum SAT);
+  Result(enum Validity);
 
-  SAT isSAT();
-  Validity isValid();
-  UnknownExplanation whyUnknown();
+  enum SAT isSAT();
+  enum Validity isValid();
+  enum UnknownExplanation whyUnknown();
 
 };/* class Result */
 
 }/* CVC4 namespace */
+
+#endif /* __CVC4_RESULT_H */
diff --git a/src/include/theory.h b/src/include/theory.h
index b08e9e7ba..6659dc680 100644
--- a/src/include/theory.h
+++ b/src/include/theory.h
@@ -10,6 +10,9 @@
 #ifndef __CVC4_THEORY_H
 #define __CVC4_THEORY_H
 
+#include "expr.h"
+#include "literal.h"
+
 namespace CVC4 {
 
 /**
@@ -57,7 +60,14 @@ public:
   /**
    * T-propagate new literal assignments in the current context.
    */
-  virtual LiteralSet propagate();
+  // TODO design decisoin: 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)..
diff --git a/src/include/vc.h b/src/include/vc.h
index a75aa0548..57d8a957e 100644
--- a/src/include/vc.h
+++ b/src/include/vc.h
@@ -10,6 +10,9 @@
 #ifndef __CVC4_VC_H
 #define __CVC4_VC_H
 
+#include "command.h"
+#include "expr.h"
+
 /* TODO provide way of querying whether you fall into a fragment /
  * returning what fragment you're in */