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.h | |
| parent | 5b71632328be3d5a0677e12415d28c0d712aac3c (diff) | |
Refactoring CEGQI interface (#3239)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index dfe8a44ad..1f8c13f7b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" @@ -114,8 +113,6 @@ public: quantifiers::EqualityInference* getEqualityInference() const; /** get relevant domain */ quantifiers::RelevantDomain* getRelevantDomain() const; - /** get the BV inverter utility */ - quantifiers::BvInverter* getBvInverter() const; //---------------------- end utilities //---------------------- modules (TODO remove these #1163) /** get bounded integers utility */ @@ -309,8 +306,6 @@ public: std::unique_ptr<quantifiers::FirstOrderModel> d_model; /** relevant domain */ std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; - /** inversion utility for BV instantiation */ - std::unique_ptr<quantifiers::BvInverter> d_bv_invert; /** model builder */ std::unique_ptr<quantifiers::QModelBuilder> d_builder; /** utility for effectively propositional logic */ |