diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-04 19:58:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-04 19:58:51 -0500 |
| commit | 44490619ebd55d59fea574a1759482f4c37ef42e (patch) | |
| tree | 97d1ac9b7be977dc888f4c012a51c2901836561c /src/theory/quantifiers_engine.cpp | |
| parent | 5b71632328be3d5a0677e12415d28c0d712aac3c (diff) | |
Refactoring CEGQI interface (#3239)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5bac55462..f57667be5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -190,7 +190,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_rel_dom(nullptr), - d_bv_invert(nullptr), d_builder(nullptr), d_qepr(nullptr), d_term_util(new quantifiers::TermUtil(this)), @@ -256,12 +255,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Assert( !options::incrementalSolving() ); d_qepr.reset(new quantifiers::QuantEPR); } - - if (options::cbqi() && options::cbqiBv()) - { - // if doing instantiation for BV, need the inverter class - d_bv_invert.reset(new quantifiers::BvInverter); - } //---- end utilities //allow theory combination to go first, once initially @@ -341,10 +334,6 @@ quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const { return d_rel_dom.get(); } -quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const -{ - return d_bv_invert.get(); -} quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const { return d_builder.get(); |