IDL example theory (to be used with --use-theory=idl).

1 files changed, 69 insertions, 0 deletions

diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
new file mode 100644
index 000000000..3972819da
--- /dev/null
+++ b/src/theory/idl/idl_assertion_db.h
@@ -0,0 +1,69 @@
+#pragma once
+
+#include "theory/idl/idl_assertion.h"
+#include "context/cdlist.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * Context-dependent database assertions, organized by variable. Each variable
+ * can be associated a list of IDL assertions. The list of assertions can
+ * be iterated over using the provided iterator class.
+ */
+class IDLAssertionDB {
+
+  /** Elements of the assertion lists */
+  struct IDLAssertionListElement {
+    /** The assertion itself */
+    IDLAssertion d_assertion;
+    /** The inndex of the previous element (-1 for null) */
+    unsigned d_previous;
+
+    IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
+    : d_assertion(assertion), d_previous(previous)
+    {}
+  };
+
+  /** All assertions in a context dependent stack */
+  context::CDList<IDLAssertionListElement> d_assertions;
+
+  typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map;
+
+  /** Map from variables to the first element of their list */
+  var_to_unsigned_map d_variableLists;
+
+public:
+
+  /** Create a new assertion database */
+  IDLAssertionDB(context::Context* c);
+
+  /** Add a new assertion, attach to the list of the given variable */
+  void add(const IDLAssertion& assertion, TNode var);
+
+  /** Iteration over the constraints of a variable */
+  class iterator {
+    /** The database */
+    const IDLAssertionDB& d_db;
+    /** Index of the current constraint */
+    unsigned d_current;
+  public:
+    /** Construct the iterator for the variable */
+    iterator(IDLAssertionDB& db, TNode var);
+    /** Is this iterator done */
+    bool done() const { return d_current == (unsigned)(-1); }
+    /** Next element */
+    void next();
+    /** Get the assertion */
+    IDLAssertion get() const;
+  };
+};
+
+}
+}
+}
+
+
+
+