From 44490619ebd55d59fea574a1759482f4c37ef42e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Sep 2019 19:58:51 -0500
Subject: Refactoring CEGQI interface (#3239)

---
 src/theory/quantifiers_engine.h | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'src/theory/quantifiers_engine.h')

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 */
-- 
cgit v1.2.3