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.h | |
parent | 6edae99ca2d1af88ebe82256132d0d058913a13c (diff) |
IDL example theory (to be used with --use-theory=idl).
Diffstat (limited to 'src/theory/idl/idl_assertion_db.h')
-rw-r--r-- | src/theory/idl/idl_assertion_db.h | 69 |
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; + }; +}; + +} +} +} + + + + |