diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
| commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
| tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers_engine.h | |
| parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) | |
Document term db (#1220)
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b1608e497..0bb5b10e5 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -124,7 +124,16 @@ private: quantifiers::QModelBuilder* d_builder; /** utility for effectively propositional logic */ QuantEPR * d_qepr; -private: + /** term database */ + quantifiers::TermDb* d_term_db; + /** sygus term database */ + quantifiers::TermDbSygus* d_sygus_tdb; + /** term utilities */ + quantifiers::TermUtil* d_term_util; + /** quantifiers attributes */ + std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; + + private: /** instantiation engine */ quantifiers::InstantiationEngine* d_inst_engine; /** model engine */ @@ -155,7 +164,8 @@ private: quantifiers::QuantAntiSkolem * d_anti_skolem; /** quantifiers instantiation propagtor */ quantifiers::InstPropagator * d_inst_prop; -public: //effort levels + + public: // effort levels (TODO : make an enum and use everywhere #1293) enum { QEFFORT_CONFLICT, QEFFORT_STANDARD, @@ -194,14 +204,6 @@ private: std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; /** quantifiers that have been skolemized */ BoolMap d_skolemized; - /** term database */ - quantifiers::TermDb* d_term_db; - /** term database */ - quantifiers::TermDbSygus* d_sygus_tdb; - /** term utilities */ - quantifiers::TermUtil* d_term_util; - /** quantifiers attributes */ - std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ |