diff options
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.h')
-rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index be2ff4c78..2b5464151 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -19,6 +19,7 @@ #include <map> +#include "context/cdlist.h" #include "theory/quantifiers_engine.h" #include "theory/uf/equality_engine.h" @@ -51,6 +52,8 @@ namespace quantifiers { */ class DynamicRewriter { + typedef context::CDList<Node> NodeList; + public: DynamicRewriter(const std::string& name, QuantifiersEngine* qe); ~DynamicRewriter() {} @@ -105,6 +108,8 @@ class DynamicRewriter std::map<Node, Node> d_term_to_internal; /** stores congruence closure over terms given to this class. */ eq::EqualityEngine d_equalityEngine; + /** list of all equalities asserted to equality engine */ + NodeList d_rewrites; }; } /* CVC4::theory::quantifiers namespace */ |