diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-12 16:14:29 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-12 16:14:29 -0600 |
| commit | 04114df7dd58bd7391704a94fe98e2935b39130d (patch) | |
| tree | 26b403b9368c9cfeea0775ec94cc2dcb01b930ca /src/theory/quantifiers/dynamic_rewrite.h | |
| parent | c9e58c9cf4b90e42d314b92054a010513da1502a (diff) | |
Minor improvements to sygus sampler (#1598)
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 */ |