Refactoring CEGQI interface (#3239)

12 files changed, 122 insertions, 178 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 3a498277a..b1a2a2533 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -32,8 +32,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-ArithInstantiator::ArithInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn)
+ArithInstantiator::ArithInstantiator(TypeNode tn) : Instantiator(tn)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
@@ -267,7 +266,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
           << pvmod << " -> " << uval << ", styp = " << uires << std::endl;
     }
     // take into account delta
-    if (ci->useVtsDelta() && (uires == 2 || uires == -2))
+    if (uires == 2 || uires == -2)
     {
       if (options::cbqiModel())
       {
@@ -329,9 +328,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
-  bool use_inf = ci->useVtsInfinity()
-                 && (d_type.isInteger() ? options::cbqiUseInfInt()
-                                        : options::cbqiUseInfReal());
+  bool use_inf =
+      d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal();
   bool upper_first = Random::getRandom().pickWithProb(0.5);
   if (options::cbqiMinBounds())
   {
@@ -505,7 +503,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         // if using cbqiMidpoint, only add the instance based on one bound if
         // the bound is non-strict
         if (!options::cbqiMidpoint() || d_type.isInteger()
-            || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull()))
+            || d_mbp_vts_coeff[rr][1][best].isNull())
         {
           Node val = d_mbp_bounds[rr][best];
           val = getModelBasedProjectionValue(ci,
@@ -917,7 +915,7 @@ int ArithInstantiator::solve_arith(CegInstantiator* ci,
                         ? d_zero
                         : (real_part.size() == 1 ? real_part[0]
                                                  : nm->mkNode(PLUS, real_part));
-    Assert(ci->getOutput()->isEligibleForInstantiation(realPart));
+    Assert(ci->isEligibleForInstantiation(realPart));
     // re-isolate
     Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
     veq_c = Node::null();
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index 8799ce1cd..ee3e3e27d 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -42,7 +42,7 @@ namespace quantifiers {
 class ArithInstantiator : public Instantiator
 {
  public:
-  ArithInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  ArithInstantiator(TypeNode tn);
   virtual ~ArithInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 90b7002b3..eacc3032c 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -53,15 +53,14 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
   CegInstantiator* d_ci;
 };
 
-BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn), d_inst_id_counter(0)
+BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv)
+    : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0)
 {
-  // get the global inverter utility
-  // this must be global since we need to:
+  // The inverter utility d_inverter is global to all BvInstantiator classes.
+  // This must be global since we need to:
   // * process Skolem functions properly across multiple variables within the
   // same quantifier
   // * cache Skolem variables uniformly across multiple quantified formulas
-  d_inverter = qe->getBvInverter();
 }
 
 BvInstantiator::~BvInstantiator() {}
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index 466eba6a2..a548c959e 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -38,7 +38,7 @@ namespace quantifiers {
 class BvInstantiator : public Instantiator
 {
  public:
-  BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  BvInstantiator(TypeNode tn, BvInverter* inv);
   ~BvInstantiator() override;
   /** reset */
   void reset(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
index cf9736abe..ef43d50a5 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -32,7 +32,7 @@ namespace quantifiers {
 class DtInstantiator : public Instantiator
 {
  public:
-  DtInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+  DtInstantiator(TypeNode tn) : Instantiator(tn) {}
   virtual ~DtInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
index 05932de7e..b32fa5d4c 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
@@ -33,7 +33,7 @@ namespace quantifiers {
 class EprInstantiator : public Instantiator
 {
  public:
-  EprInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+  EprInstantiator(TypeNode tn) : Instantiator(tn) {}
   virtual ~EprInstantiator() {}
   /** reset */
   void reset(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index bc21cce81..e2a6432db 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -23,6 +23,7 @@
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -136,14 +137,10 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop)
   d_theta.pop_back();
 }
 
-CegInstantiator::CegInstantiator(QuantifiersEngine* qe,
-                                 CegqiOutput* out,
-                                 bool use_vts_delta,
-                                 bool use_vts_inf)
-    : d_qe(qe),
-      d_out(out),
-      d_use_vts_delta(use_vts_delta),
-      d_use_vts_inf(use_vts_inf),
+CegInstantiator::CegInstantiator(Node q, InstStrategyCegqi* parent)
+    : d_quant(q),
+      d_parent(parent),
+      d_qe(parent->getQuantifiersEngine()),
       d_is_nested_quant(false),
       d_effort(CEG_INST_EFFORT_NONE)
 {
@@ -171,7 +168,9 @@ void CegInstantiator::computeProgVars( Node n ){
     if (d_vars_set.find(n) != d_vars_set.end())
     {
       d_prog_var[n].insert(n);
-    }else if( !d_out->isEligibleForInstantiation( n ) ){
+    }
+    else if (!isEligibleForInstantiation(n))
+    {
       d_inelig.insert(n);
       return;
     }
@@ -431,19 +430,19 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
     TypeNode tn = v.getType();
     Instantiator * vinst;
     if( tn.isReal() ){
-      vinst = new ArithInstantiator( d_qe, tn );
+      vinst = new ArithInstantiator(tn);
     }else if( tn.isSort() ){
       Assert( options::quantEpr() );
-      vinst = new EprInstantiator( d_qe, tn );
+      vinst = new EprInstantiator(tn);
     }else if( tn.isDatatype() ){
-      vinst = new DtInstantiator( d_qe, tn );
+      vinst = new DtInstantiator(tn);
     }else if( tn.isBitVector() ){
-      vinst = new BvInstantiator( d_qe, tn );
+      vinst = new BvInstantiator(tn, d_parent->getBvInverter());
     }else if( tn.isBoolean() ){
-      vinst = new ModelValueInstantiator( d_qe, tn );
+      vinst = new ModelValueInstantiator(tn);
     }else{
       //default
-      vinst = new Instantiator( d_qe, tn );
+      vinst = new Instantiator(tn);
     }
     d_instantiator[v] = vinst;
   }
@@ -1056,13 +1055,41 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
     }
   }
   Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
-  bool ret = d_out->doAddInstantiation( subs );
+  bool ret = d_parent->doAddInstantiation(subs);
   for( unsigned i=0; i<lemmas.size(); i++ ){
-    d_out->addLemma( lemmas[i] );
+    d_parent->addLemma(lemmas[i]);
   }
   return ret;
 }
 
+bool CegInstantiator::isEligibleForInstantiation(Node n) const
+{
+  if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM)
+  {
+    return true;
+  }
+  if (n.getAttribute(VirtualTermSkolemAttribute()))
+  {
+    // virtual terms are allowed
+    return true;
+  }
+  TypeNode tn = n.getType();
+  if (tn.isSort())
+  {
+    QuantEPR* qepr = d_qe->getQuantEPR();
+    if (qepr != NULL)
+    {
+      // legal if in the finite set of constants of type tn
+      if (qepr->isEPRConstant(tn, n))
+      {
+        return true;
+      }
+    }
+  }
+  // only legal if current quantified formula contains n
+  return expr::hasSubterm(d_quant, n);
+}
+
 bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   if( !non_basic.empty() ){
@@ -1700,8 +1727,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   }
 }
 
-
-Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
+Instantiator::Instantiator(TypeNode tn) : d_type(tn)
+{
   d_closed_enum_type = tn.isClosedEnumerable();
 }
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index da57cdd16..8110dcd95 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -30,16 +30,9 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 
-class CegqiOutput {
-public:
-  virtual ~CegqiOutput() {}
-  virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0;
-  virtual bool isEligibleForInstantiation( Node n ) = 0;
-  virtual bool addLemma( Node lem ) = 0;
-};
-
 class Instantiator;
 class InstantiatorPreprocess;
+class InstStrategyCegqi;
 
 /** Term Properties
  *
@@ -181,10 +174,11 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status);
  */
 class CegInstantiator {
  public:
-  CegInstantiator(QuantifiersEngine* qe,
-                  CegqiOutput* out,
-                  bool use_vts_delta = true,
-                  bool use_vts_inf = true);
+  /**
+   * The instantiator will be constructing instantiations for quantified formula
+   * q, parent is the owner of this object.
+   */
+  CegInstantiator(Node q, InstStrategyCegqi* parent);
   virtual ~CegInstantiator();
   /** check
    * This adds instantiations based on the state of d_vars in current context
@@ -214,8 +208,6 @@ class CegInstantiator {
    */
   void registerCounterexampleLemma(std::vector<Node>& lems,
                                    std::vector<Node>& ce_vars);
-  /** get the output channel of this class */
-  CegqiOutput* getOutput() { return d_out; }
   //------------------------------interface for instantiators
   /** get quantifiers engine */
   QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
@@ -276,12 +268,14 @@ class CegInstantiator {
   bool isEligible(Node n);
   /** does n have variable pv? */
   bool hasVariable(Node n, Node pv);
-  /** are we using delta for LRA virtual term substitution? */
-  bool useVtsDelta() { return d_use_vts_delta; }
-  /** are we using infinity for LRA virtual term substitution? */
-  bool useVtsInfinity() { return d_use_vts_inf; }
   /** are we processing a nested quantified formula? */
-  bool hasNestedQuantification() { return d_is_nested_quant; }
+  bool hasNestedQuantification() const { return d_is_nested_quant; }
+  /**
+   * Are we allowed to instantiate the current quantified formula with n? This
+   * includes restrictions such as if n is a variable, it must occur free in
+   * the current quantified formula.
+   */
+  bool isEligibleForInstantiation(Node n) const;
   //------------------------------------ static queries
   /** Is k a kind for which counterexample-guided instantiation is possible?
    *
@@ -333,18 +327,12 @@ class CegInstantiator {
   static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr);
   //------------------------------------ end static queries
  private:
+  /** The quantified formula of this instantiator */
+  Node d_quant;
+  /** The parent of this instantiator */
+  InstStrategyCegqi* d_parent;
   /** quantified formula associated with this instantiator */
   QuantifiersEngine* d_qe;
-  /** output channel of this instantiator */
-  CegqiOutput* d_out;
-  /** whether we are using delta for virtual term substitution
-    * (for quantified LRA).
-    */
-  bool d_use_vts_delta;
-  /** whether we are using infinity for virtual term substitution
-    * (for quantified LRA).
-    */
-  bool d_use_vts_inf;
 
   //-------------------------------globally cached
   /** cache from nodes to the set of variables it contains
@@ -613,19 +601,19 @@ class CegInstantiator {
  */
 class Instantiator {
 public:
-  Instantiator( QuantifiersEngine * qe, TypeNode tn );
-  virtual ~Instantiator(){}
-  /** reset
-   * This is called once, prior to any of the below methods are called.
-   * This function sets up any initial information necessary for constructing
-   * instantiations for pv based on the current context.
-   */
-  virtual void reset(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort)
-  {
-  }
+ Instantiator(TypeNode tn);
+ virtual ~Instantiator() {}
+ /** reset
+  * This is called once, prior to any of the below methods are called.
+  * This function sets up any initial information necessary for constructing
+  * instantiations for pv based on the current context.
+  */
+ virtual void reset(CegInstantiator* ci,
+                    SolvedForm& sf,
+                    Node pv,
+                    CegInstEffort effort)
+ {
+ }
 
   /** has process equal term
    *
@@ -819,15 +807,15 @@ public:
 
 class ModelValueInstantiator : public Instantiator {
 public:
-  ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
-  virtual ~ModelValueInstantiator(){}
-  bool useModelValue(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override
-  {
-    return true;
-  }
+ ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {}
+ virtual ~ModelValueInstantiator() {}
+ bool useModelValue(CegInstantiator* ci,
+                    SolvedForm& sf,
+                    Node pv,
+                    CegInstEffort effort) override
+ {
+   return true;
+ }
   std::string identify() const override { return "ModelValue"; }
 };
 
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index ab5bbc25f..ac4d05194 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -30,26 +30,12 @@
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 
-bool CegqiOutputInstStrategy::doAddInstantiation(std::vector<Node>& subs)
-{
-  return d_out->doAddInstantiation(subs);
-}
-
-bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n)
-{
-  return d_out->isEligibleForInstantiation(n);
-}
-
-bool CegqiOutputInstStrategy::addLemma(Node lem)
-{
-  return d_out->addLemma(lem);
-}
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
     : QuantifiersModule(qe),
@@ -57,15 +43,19 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
       d_incomplete_check(false),
       d_added_cbqi_lemma(qe->getUserContext()),
       d_elim_quants(qe->getSatContext()),
-      d_out(new CegqiOutputInstStrategy(this)),
+      d_bv_invert(nullptr),
       d_nested_qe_waitlist_size(qe->getUserContext()),
       d_nested_qe_waitlist_proc(qe->getUserContext())
-//, d_added_inst( qe->getUserContext() )
 {
   d_qid_count = 0;
   d_small_const =
       NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
   d_check_vts_lemma_lc = false;
+  if (options::cbqiBv())
+  {
+    // if doing instantiation for BV, need the inverter class
+    d_bv_invert.reset(new quantifiers::BvInverter);
+  }
 }
 
 InstStrategyCegqi::~InstStrategyCegqi() {}
@@ -665,41 +655,22 @@ bool InstStrategyCegqi::addLemma( Node lem ) {
   return d_quantEngine->addLemma( lem );
 }
 
-bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
-  if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
-    if( n.getAttribute(VirtualTermSkolemAttribute()) ){
-      // virtual terms are allowed
-      return true;
-    }else{
-      TypeNode tn = n.getType();
-      if( tn.isSort() ){
-        QuantEPR * qepr = d_quantEngine->getQuantEPR();
-        if( qepr!=NULL ){
-          //legal if in the finite set of constants of type tn
-          if( qepr->isEPRConstant( tn, n ) ){
-            return true;
-          }
-        }
-      }
-      //only legal if current quantified formula contains n
-      return expr::hasSubterm(d_curr_quant, n);
-    }
-  }else{
-    return true;
-  }
-}
 
 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it =
       d_cinst.find(q);
   if( it==d_cinst.end() ){
-    d_cinst[q].reset(
-        new CegInstantiator(d_quantEngine, d_out.get(), true, true));
+    d_cinst[q].reset(new CegInstantiator(q, this));
     return d_cinst[q].get();
   }
   return it->second.get();
 }
 
+BvInverter* InstStrategyCegqi::getBvInverter() const
+{
+  return d_bv_invert.get();
+}
+
 void InstStrategyCegqi::presolve() {
   if (!options::cbqiPreRegInst())
   {
@@ -712,3 +683,6 @@ void InstStrategyCegqi::presolve() {
   }
 }
 
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index ecae4ab64..32f41e476 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -19,6 +19,7 @@
 #define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 
 #include "theory/decision_manager.h"
+#include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
@@ -27,26 +28,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class InstStrategyCegqi;
-
-/**
- * An output channel class, used by instantiator objects below. The methods
- * of this class call the corresponding functions of InstStrategyCegqi below.
- */
-class CegqiOutputInstStrategy : public CegqiOutput
-{
- public:
-  CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {}
-  /** The module whose functions we call. */
-  InstStrategyCegqi* d_out;
-  /** add instantiation */
-  bool doAddInstantiation(std::vector<Node>& subs) override;
-  /** is eligible for instantiation */
-  bool isEligibleForInstantiation(Node n) override;
-  /** add lemma */
-  bool addLemma(Node lem) override;
-};
-
 /**
  * Counterexample-guided quantifier instantiation module.
  *
@@ -82,6 +63,8 @@ class InstStrategyCegqi : public QuantifiersModule
   std::string identify() const override { return std::string("Cegqi"); }
   /** get instantiator for quantifier */
   CegInstantiator* getInstantiator(Node q);
+  /** get the BV inverter utility */
+  BvInverter* getBvInverter() const;
   /** pre-register quantifier */
   void preRegisterQuantifier(Node q) override;
   // presolve
@@ -92,12 +75,6 @@ class InstStrategyCegqi : public QuantifiersModule
   //------------------- interface for CegqiOutputInstStrategy
   /** Instantiate the current quantified formula forall x. Q with x -> subs. */
   bool doAddInstantiation(std::vector<Node>& subs);
-  /**
-   * Are we allowed to instantiate the current quantified formula with n? This
-   * includes restrictions such as if n is a variable, it must occur free in
-   * the current quantified formula.
-   */
-  bool isEligibleForInstantiation(Node n);
   /** Add lemma lem via the output channel of this class. */
   bool addLemma(Node lem);
   //------------------- end interface for CegqiOutputInstStrategy
@@ -127,15 +104,12 @@ class InstStrategyCegqi : public QuantifiersModule
   /** Whether cegqi handles each quantified formula. */
   std::map<Node, CegHandledStatus> d_do_cbqi;
   /**
-   * An output channel used by instantiators for communicating with this
-   * class.
-   */
-  std::unique_ptr<CegqiOutputInstStrategy> d_out;
-  /**
    * The instantiator for each quantified formula q registered to this class.
    * This object is responsible for finding instantiatons for q.
    */
   std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
+  /** inversion utility for BV instantiation */
+  std::unique_ptr<BvInverter> d_bv_invert;
   /**
    * The decision strategy for each quantified formula q registered to this
    * class.
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();
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 */