diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-06-05 16:35:37 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-06-06 14:51:32 -0400 |
commit | 482167cc10c5df25e107e0b44a24c125f7b18bd2 (patch) | |
tree | b3a132657bbe28c4af493c0152e634ffedf28c3f /src/theory/idl/idl_assertion_db.cpp | |
parent | 6edae99ca2d1af88ebe82256132d0d058913a13c (diff) |
IDL example theory (to be used with --use-theory=idl).
Diffstat (limited to 'src/theory/idl/idl_assertion_db.cpp')
-rw-r--r-- | src/theory/idl/idl_assertion_db.cpp | 42 |
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; +} |