Initial draft of TheoryUF. Should compile without problems. A decent amount of functionality is stubbed out. Still needs a bit of cleanup.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8aa76ea81..8b83f71cf 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "theory/output_channel.h"
+#include "context/context.h"
 
 namespace CVC4 {
 namespace theory {
@@ -101,6 +102,19 @@ public:
                        const Node& n,
                        Effort level = FULL_EFFORT) = 0;
 
+protected:
+  /**
+   * Returns the next atom in the assertFact() queue.
+   * Guarentees that registerTerm is called on the theory specific subterms.
+   * @return the next atom in the assertFact() queue.
+   */
+  Node get();
+
+  /**
+   * Returns true if the assertFactQueue is empty
+   */
+  bool done() { return true; }
+
 };/* class Theory */
 
 }/* CVC4::theory namespace */