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

1 files changed, 42 insertions, 0 deletions

diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
new file mode 100644
index 000000000..7c27e9d0d
--- /dev/null
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -0,0 +1,42 @@
+#include "theory/idl/idl_assertion_db.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLAssertionDB::IDLAssertionDB(context::Context* c)
+: d_assertions(c)
+, d_variableLists(c)
+{}
+
+void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) {
+  // Is there a list for the variable already?
+  unsigned previous = -1;
+  var_to_unsigned_map::iterator find = d_variableLists.find(var);
+  if (find != d_variableLists.end()) {
+    previous = (*find).second;
+  }
+  // Add to the DB
+  d_variableLists[var] = d_assertions.size();
+  d_assertions.push_back(IDLAssertionListElement(assertion, previous));
+}
+
+IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var)
+: d_db(db)
+, d_current(-1)
+{
+  var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var);
+  if (find != d_db.d_variableLists.end()) {
+    d_current = (*find).second;
+  }
+}
+
+void IDLAssertionDB::iterator::next() {
+  if (d_current != (unsigned)(-1)) {
+    d_current = d_db.d_assertions[d_current].d_previous;
+  }
+}
+
+IDLAssertion IDLAssertionDB::iterator::get() const {
+  return d_db.d_assertions[d_current].d_assertion;
+}