diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-28 18:32:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-28 18:32:15 -0500 |
commit | 395aaff1ed21b37b49cba1a453a26effb2f4ca59 (patch) | |
tree | 60f99e0fb3b7aa9fa4191426b5b163c286d96f9d /src/theory/quantifiers_engine.h | |
parent | 85842c3ad03ab94586c6b34eb01149f449bff52d (diff) |
Split term canonize utility to own file and document (#2398)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index aabca1640..662803323 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -47,6 +47,7 @@ namespace quantifiers { class TermDb; class TermDbSygus; class TermUtil; + class TermCanonize; class Instantiate; class Skolemize; class TermEnumeration; @@ -129,6 +130,8 @@ public: quantifiers::TermDbSygus* getTermDatabaseSygus() const; /** get term utilities */ quantifiers::TermUtil* getTermUtil() const; + /** get term canonizer */ + quantifiers::TermCanonize* getTermCanonize() const; /** get quantifiers attributes */ quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ @@ -344,6 +347,8 @@ public: std::unique_ptr<quantifiers::QuantEPR> d_qepr; /** term utilities */ std::unique_ptr<quantifiers::TermUtil> d_term_util; + /** term utilities */ + std::unique_ptr<quantifiers::TermCanonize> d_term_canon; /** term database */ std::unique_ptr<quantifiers::TermDb> d_term_db; /** sygus term database */ |