diff options
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 */ |