Split and document ceg theory instantiators (#2094)

14 files changed, 3114 insertions, 2343 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index b81d93081..b60cede21 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -391,8 +391,14 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/candidate_rewrite_database.h \
 	theory/quantifiers/cegqi/ceg_instantiator.cpp \
 	theory/quantifiers/cegqi/ceg_instantiator.h \
-	theory/quantifiers/cegqi/ceg_t_instantiator.cpp \
-	theory/quantifiers/cegqi/ceg_t_instantiator.h \
+	theory/quantifiers/cegqi/ceg_arith_instantiator.cpp \
+	theory/quantifiers/cegqi/ceg_arith_instantiator.h \
+	theory/quantifiers/cegqi/ceg_bv_instantiator.cpp \
+	theory/quantifiers/cegqi/ceg_bv_instantiator.h \
+	theory/quantifiers/cegqi/ceg_dt_instantiator.cpp \
+	theory/quantifiers/cegqi/ceg_dt_instantiator.h \
+	theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \
+	theory/quantifiers/cegqi/ceg_epr_instantiator.h \
 	theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \
 	theory/quantifiers/cegqi/inst_strategy_cbqi.h \
 	theory/quantifiers/conjecture_generator.cpp \
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
new file mode 100644
index 000000000..5cd7a6892
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -0,0 +1,997 @@
+/*********************                                                        */
+/*! \file ceg_arith_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of ceg_arith_instantiator
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/theory_arith_private.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+ArithInstantiator::ArithInstantiator(QuantifiersEngine* qe, TypeNode tn)
+    : Instantiator(qe, tn)
+{
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  d_one = NodeManager::currentNM()->mkConst(Rational(1));
+}
+
+void ArithInstantiator::reset(CegInstantiator* ci,
+                              SolvedForm& sf,
+                              Node pv,
+                              CegInstEffort effort)
+{
+  d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(
+      d_type, false, false);
+  d_vts_sym[1] =
+      ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(false, false);
+  for (unsigned i = 0; i < 2; i++)
+  {
+    d_mbp_bounds[i].clear();
+    d_mbp_coeff[i].clear();
+    for (unsigned j = 0; j < 2; j++)
+    {
+      d_mbp_vts_coeff[i][j].clear();
+    }
+    d_mbp_lit[i].clear();
+  }
+}
+
+bool ArithInstantiator::hasProcessEquality(CegInstantiator* ci,
+                                           SolvedForm& sf,
+                                           Node pv,
+                                           CegInstEffort effort)
+{
+  return true;
+}
+
+bool ArithInstantiator::processEquality(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<TermProperties>& term_props,
+                                        std::vector<Node>& terms,
+                                        CegInstEffort effort)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node eq_lhs = terms[0];
+  Node eq_rhs = terms[1];
+  Node lhs_coeff = term_props[0].d_coeff;
+  Node rhs_coeff = term_props[1].d_coeff;
+  // make the same coefficient
+  if (rhs_coeff != lhs_coeff)
+  {
+    if (!rhs_coeff.isNull())
+    {
+      Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl;
+      eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs);
+      eq_lhs = Rewriter::rewrite(eq_lhs);
+    }
+    if (!lhs_coeff.isNull())
+    {
+      Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl;
+      eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs);
+      eq_rhs = Rewriter::rewrite(eq_rhs);
+    }
+  }
+  Node eq = eq_lhs.eqNode(eq_rhs);
+  eq = Rewriter::rewrite(eq);
+  Node val;
+  TermProperties pv_prop;
+  Node vts_coeff_inf;
+  Node vts_coeff_delta;
+  // isolate pv in the equality
+  int ires = solve_arith(
+      ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta);
+  if (ires != 0)
+  {
+    pv_prop.d_type = 0;
+    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+bool ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                            SolvedForm& sf,
+                                            Node pv,
+                                            CegInstEffort effort)
+{
+  return true;
+}
+
+Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                            SolvedForm& sf,
+                                            Node pv,
+                                            Node lit,
+                                            CegInstEffort effort)
+{
+  Node atom = lit.getKind() == NOT ? lit[0] : lit;
+  bool pol = lit.getKind() != NOT;
+  // arithmetic inequalities and disequalities
+  if (atom.getKind() == GEQ
+      || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal()))
+  {
+    return lit;
+  }
+  return Node::null();
+}
+
+bool ArithInstantiator::processAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         Node alit,
+                                         CegInstEffort effort)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node atom = lit.getKind() == NOT ? lit[0] : lit;
+  bool pol = lit.getKind() != NOT;
+  // arithmetic inequalities and disequalities
+  Assert(atom.getKind() == GEQ
+         || (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal()));
+  // get model value for pv
+  Node pv_value = ci->getModelValue(pv);
+  // cannot contain infinity?
+  Node vts_coeff_inf;
+  Node vts_coeff_delta;
+  Node val;
+  TermProperties pv_prop;
+  // isolate pv in the inequality
+  int ires = solve_arith(
+      ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta);
+  if (ires == 0)
+  {
+    return false;
+  }
+  // disequalities are either strict upper or lower bounds
+  unsigned rmax = (atom.getKind() == GEQ || options::cbqiModel()) ? 1 : 2;
+  for (unsigned r = 0; r < rmax; r++)
+  {
+    int uires = ires;
+    Node uval = val;
+    if (atom.getKind() == GEQ)
+    {
+      // push negation downwards
+      if (!pol)
+      {
+        uires = -ires;
+        if (d_type.isInteger())
+        {
+          uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires)));
+          uval = Rewriter::rewrite(uval);
+        }
+        else
+        {
+          Assert(d_type.isReal());
+          // now is strict inequality
+          uires = uires * 2;
+        }
+      }
+    }
+    else
+    {
+      bool is_upper;
+      if (options::cbqiModel())
+      {
+        // disequality is a disjunction : only consider the bound in the
+        // direction of the model
+        // first check if there is an infinity...
+        if (!vts_coeff_inf.isNull())
+        {
+          // coefficient or val won't make a difference, just compare with zero
+          Trace("cegqi-arith-debug") << "Disequality : check infinity polarity "
+                                     << vts_coeff_inf << std::endl;
+          Assert(vts_coeff_inf.isConst());
+          is_upper = (vts_coeff_inf.getConst<Rational>().sgn() == 1);
+        }
+        else
+        {
+          Node rhs_value = ci->getModelValue(val);
+          Node lhs_value = pv_prop.getModifiedTerm(pv_value);
+          if (!pv_prop.isBasic())
+          {
+            lhs_value = pv_prop.getModifiedTerm(pv_value);
+            lhs_value = Rewriter::rewrite(lhs_value);
+          }
+          Trace("cegqi-arith-debug")
+              << "Disequality : check model values " << lhs_value << " "
+              << rhs_value << std::endl;
+          // it generally should be the case that lhs_value!=rhs_value
+          // however, this assertion is violated e.g. if non-linear is enabled
+          // since the quantifier-free arithmetic solver may pass full
+          // effort with no lemmas even when we are not guaranteed to have a
+          // model. By convention, we use GEQ to compare the values here.
+          Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value);
+          cmp = Rewriter::rewrite(cmp);
+          Assert(cmp.isConst());
+          is_upper = (cmp != ci->getQuantifiersEngine()->getTermUtil()->d_true);
+        }
+      }
+      else
+      {
+        is_upper = (r == 0);
+      }
+      Assert(atom.getKind() == EQUAL && !pol);
+      if (d_type.isInteger())
+      {
+        uires = is_upper ? -1 : 1;
+        uval = nm->mkNode(PLUS, val, nm->mkConst(Rational(uires)));
+        uval = Rewriter::rewrite(uval);
+      }
+      else
+      {
+        Assert(d_type.isReal());
+        uires = is_upper ? -2 : 2;
+      }
+    }
+    if (Trace.isOn("cegqi-arith-bound-inf"))
+    {
+      Node pvmod = pv_prop.getModifiedTerm(pv);
+      Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : ";
+      Trace("cegqi-arith-bound-inf")
+          << pvmod << " -> " << uval << ", styp = " << uires << std::endl;
+    }
+    // take into account delta
+    if (ci->useVtsDelta() && (uires == 2 || uires == -2))
+    {
+      if (options::cbqiModel())
+      {
+        Node delta_coeff = nm->mkConst(Rational(uires > 0 ? 1 : -1));
+        if (vts_coeff_delta.isNull())
+        {
+          vts_coeff_delta = delta_coeff;
+        }
+        else
+        {
+          vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff);
+          vts_coeff_delta = Rewriter::rewrite(vts_coeff_delta);
+        }
+      }
+      else
+      {
+        Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta();
+        uval = nm->mkNode(uires == 2 ? PLUS : MINUS, uval, delta);
+        uval = Rewriter::rewrite(uval);
+      }
+    }
+    if (options::cbqiModel())
+    {
+      // just store bounds, will choose based on tighest bound
+      unsigned index = uires > 0 ? 0 : 1;
+      d_mbp_bounds[index].push_back(uval);
+      d_mbp_coeff[index].push_back(pv_prop.d_coeff);
+      Trace("cegqi-arith-debug")
+          << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff
+          << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit
+          << std::endl;
+      for (unsigned t = 0; t < 2; t++)
+      {
+        d_mbp_vts_coeff[index][t].push_back(t == 0 ? vts_coeff_inf
+                                                   : vts_coeff_delta);
+      }
+      d_mbp_lit[index].push_back(lit);
+    }
+    else
+    {
+      // try this bound
+      pv_prop.d_type = uires > 0 ? 1 : -1;
+      if (ci->constructInstantiationInc(pv, uval, pv_prop, sf))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool ArithInstantiator::processAssertions(CegInstantiator* ci,
+                                          SolvedForm& sf,
+                                          Node pv,
+                                          CegInstEffort effort)
+{
+  if (!options::cbqiModel())
+  {
+    return false;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  bool use_inf = ci->useVtsInfinity()
+                 && (d_type.isInteger() ? options::cbqiUseInfInt()
+                                        : options::cbqiUseInfReal());
+  bool upper_first = false;
+  if (options::cbqiMinBounds())
+  {
+    upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
+  }
+  int best_used[2];
+  std::vector<Node> t_values[3];
+  Node pv_value = ci->getModelValue(pv);
+  // try optimal bounds
+  for (unsigned r = 0; r < 2; r++)
+  {
+    int rr = upper_first ? (1 - r) : r;
+    best_used[rr] = -1;
+    if (d_mbp_bounds[rr].empty())
+    {
+      if (use_inf)
+      {
+        Trace("cegqi-arith-bound")
+            << "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv
+            << " (type=" << d_type << ")" << std::endl;
+        // no bounds, we do +- infinity
+        Node val =
+            ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(d_type);
+        // could get rho value for infinity here
+        if (rr == 0)
+        {
+          val = nm->mkNode(UMINUS, val);
+          val = Rewriter::rewrite(val);
+        }
+        TermProperties pv_prop_no_bound;
+        if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
+        {
+          return true;
+        }
+      }
+    }
+    else
+    {
+      Trace("cegqi-arith-bound")
+          << (rr == 0 ? "Lower" : "Upper") << " bounds for " << pv
+          << " (type=" << d_type << ") : " << std::endl;
+      int best = -1;
+      Node best_bound_value[3];
+      for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
+      {
+        Node value[3];
+        if (Trace.isOn("cegqi-arith-bound"))
+        {
+          Assert(!d_mbp_bounds[rr][j].isNull());
+          Trace("cegqi-arith-bound")
+              << "  " << j << ": " << d_mbp_bounds[rr][j];
+          if (!d_mbp_vts_coeff[rr][0][j].isNull())
+          {
+            Trace("cegqi-arith-bound")
+                << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)";
+          }
+          if (!d_mbp_vts_coeff[rr][1][j].isNull())
+          {
+            Trace("cegqi-arith-bound")
+                << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)";
+          }
+          if (!d_mbp_coeff[rr][j].isNull())
+          {
+            Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")";
+          }
+          Trace("cegqi-arith-bound") << ", value = ";
+        }
+        t_values[rr].push_back(Node::null());
+        // check if it is better than the current best bound : lexicographic
+        // order infinite/finite/infinitesimal parts
+        bool new_best = true;
+        for (unsigned t = 0; t < 3; t++)
+        {
+          // get the value
+          if (t == 0)
+          {
+            value[0] = d_mbp_vts_coeff[rr][0][j];
+            if (!value[0].isNull())
+            {
+              Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + ";
+            }
+            else
+            {
+              value[0] = d_zero;
+            }
+          }
+          else if (t == 1)
+          {
+            Node t_value = ci->getModelValue(d_mbp_bounds[rr][j]);
+            t_values[rr][j] = t_value;
+            value[1] = t_value;
+            Trace("cegqi-arith-bound") << value[1];
+          }
+          else
+          {
+            value[2] = d_mbp_vts_coeff[rr][1][j];
+            if (!value[2].isNull())
+            {
+              Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )";
+            }
+            else
+            {
+              value[2] = d_zero;
+            }
+          }
+          // multiply by coefficient
+          if (value[t] != d_zero && !d_mbp_coeff[rr][j].isNull())
+          {
+            Assert(d_mbp_coeff[rr][j].isConst());
+            value[t] = nm->mkNode(
+                MULT,
+                nm->mkConst(Rational(1)
+                            / d_mbp_coeff[rr][j].getConst<Rational>()),
+                value[t]);
+            value[t] = Rewriter::rewrite(value[t]);
+          }
+          // check if new best
+          if (best != -1)
+          {
+            Assert(!value[t].isNull() && !best_bound_value[t].isNull());
+            if (value[t] != best_bound_value[t])
+            {
+              Kind k = rr == 0 ? GEQ : LEQ;
+              Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]);
+              cmp_bound = Rewriter::rewrite(cmp_bound);
+              if (cmp_bound
+                  != ci->getQuantifiersEngine()->getTermUtil()->d_true)
+              {
+                new_best = false;
+                break;
+              }
+            }
+          }
+        }
+        Trace("cegqi-arith-bound") << std::endl;
+        if (new_best)
+        {
+          for (unsigned t = 0; t < 3; t++)
+          {
+            best_bound_value[t] = value[t];
+          }
+          best = j;
+        }
+      }
+      if (best != -1)
+      {
+        Trace("cegqi-arith-bound") << "...best bound is " << best << " : ";
+        if (best_bound_value[0] != d_zero)
+        {
+          Trace("cegqi-arith-bound")
+              << "( " << best_bound_value[0] << " * INF ) + ";
+        }
+        Trace("cegqi-arith-bound") << best_bound_value[1];
+        if (best_bound_value[2] != d_zero)
+        {
+          Trace("cegqi-arith-bound")
+              << " + ( " << best_bound_value[2] << " * DELTA )";
+        }
+        Trace("cegqi-arith-bound") << std::endl;
+        best_used[rr] = best;
+        // 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()))
+        {
+          Node val = d_mbp_bounds[rr][best];
+          val = getModelBasedProjectionValue(ci,
+                                             pv,
+                                             val,
+                                             rr == 0,
+                                             d_mbp_coeff[rr][best],
+                                             pv_value,
+                                             t_values[rr][best],
+                                             sf.getTheta(),
+                                             d_mbp_vts_coeff[rr][0][best],
+                                             d_mbp_vts_coeff[rr][1][best]);
+          if (!val.isNull())
+          {
+            TermProperties pv_prop_bound;
+            pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
+            pv_prop_bound.d_type = rr == 0 ? 1 : -1;
+            if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf))
+            {
+              return true;
+            }
+          }
+        }
+      }
+    }
+  }
+  // if not using infinity, use model value of zero
+  if (!use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty())
+  {
+    Node val = d_zero;
+    TermProperties pv_prop_zero;
+    Node theta = sf.getTheta();
+    val = getModelBasedProjectionValue(ci,
+                                       pv,
+                                       val,
+                                       true,
+                                       pv_prop_zero.d_coeff,
+                                       pv_value,
+                                       d_zero,
+                                       sf.getTheta(),
+                                       Node::null(),
+                                       Node::null());
+    if (!val.isNull())
+    {
+      if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf))
+      {
+        return true;
+      }
+    }
+  }
+  if (options::cbqiMidpoint() && !d_type.isInteger())
+  {
+    Node vals[2];
+    bool bothBounds = true;
+    Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl;
+    for (unsigned rr = 0; rr < 2; rr++)
+    {
+      int best = best_used[rr];
+      if (best == -1)
+      {
+        bothBounds = false;
+      }
+      else
+      {
+        vals[rr] = d_mbp_bounds[rr][best];
+        vals[rr] = getModelBasedProjectionValue(ci,
+                                                pv,
+                                                vals[rr],
+                                                rr == 0,
+                                                Node::null(),
+                                                pv_value,
+                                                t_values[rr][best],
+                                                sf.getTheta(),
+                                                d_mbp_vts_coeff[rr][0][best],
+                                                Node::null());
+      }
+      Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl;
+    }
+    Node val;
+    if (bothBounds)
+    {
+      Assert(!vals[0].isNull() && !vals[1].isNull());
+      if (vals[0] == vals[1])
+      {
+        val = vals[0];
+      }
+      else
+      {
+        val = nm->mkNode(MULT,
+                         nm->mkNode(PLUS, vals[0], vals[1]),
+                         nm->mkConst(Rational(1) / Rational(2)));
+        val = Rewriter::rewrite(val);
+      }
+    }
+    else
+    {
+      if (!vals[0].isNull())
+      {
+        val = nm->mkNode(PLUS, vals[0], d_one);
+        val = Rewriter::rewrite(val);
+      }
+      else if (!vals[1].isNull())
+      {
+        val = nm->mkNode(MINUS, vals[1], d_one);
+        val = Rewriter::rewrite(val);
+      }
+    }
+    Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
+    if (!val.isNull())
+    {
+      TermProperties pv_prop_midpoint;
+      if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf))
+      {
+        return true;
+      }
+    }
+  }
+  // generally should not make it to this point, unless we are using a
+  // non-monotonic selection function
+
+  if (!options::cbqiNopt())
+  {
+    // if not trying non-optimal bounds, return
+    return false;
+  }
+  // try non-optimal bounds (heuristic, may help when nested quantification) ?
+  Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl;
+  for (unsigned r = 0; r < 2; r++)
+  {
+    int rr = upper_first ? (1 - r) : r;
+    for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
+    {
+      if ((int)j != best_used[rr]
+          && (!options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
+      {
+        Node val = getModelBasedProjectionValue(ci,
+                                                pv,
+                                                d_mbp_bounds[rr][j],
+                                                rr == 0,
+                                                d_mbp_coeff[rr][j],
+                                                pv_value,
+                                                t_values[rr][j],
+                                                sf.getTheta(),
+                                                d_mbp_vts_coeff[rr][0][j],
+                                                d_mbp_vts_coeff[rr][1][j]);
+        if (!val.isNull())
+        {
+          TermProperties pv_prop_nopt_bound;
+          pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
+          pv_prop_nopt_bound.d_type = rr == 0 ? 1 : -1;
+          if (ci->constructInstantiationInc(pv, val, pv_prop_nopt_bound, sf))
+          {
+            return true;
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool ArithInstantiator::needsPostProcessInstantiationForVariable(
+    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
+{
+  return std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv)
+         != sf.d_non_basic.end();
+}
+
+bool ArithInstantiator::postProcessInstantiationForVariable(
+    CegInstantiator* ci,
+    SolvedForm& sf,
+    Node pv,
+    CegInstEffort effort,
+    std::vector<Node>& lemmas)
+{
+  Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv)
+         != sf.d_non_basic.end());
+  Assert(std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) != sf.d_vars.end());
+  unsigned index =
+      std::find(sf.d_vars.begin(), sf.d_vars.end(), pv) - sf.d_vars.begin();
+  Assert(!sf.d_props[index].isBasic());
+  Node eq_lhs = sf.d_props[index].getModifiedTerm(sf.d_vars[index]);
+  if (Trace.isOn("cegqi-arith-debug"))
+  {
+    Trace("cegqi-arith-debug") << "Normalize substitution for ";
+    Trace("cegqi-arith-debug")
+        << eq_lhs << " = " << sf.d_subs[index] << std::endl;
+  }
+  Assert(sf.d_vars[index].getType().isInteger());
+  // must ensure that divisibility constraints are met
+  // solve updated rewritten equality for vars[index], if coefficient is one,
+  // then we are successful
+  Node eq_rhs = sf.d_subs[index];
+  Node eq = eq_lhs.eqNode(eq_rhs);
+  eq = Rewriter::rewrite(eq);
+  Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
+  std::map<Node, Node> msum;
+  if (!ArithMSum::getMonomialSumLit(eq, msum))
+  {
+    Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl;
+    return false;
+  }
+  Node veq;
+  if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) == 0)
+  {
+    Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl;
+    return false;
+  }
+  Node veq_c;
+  if (veq[0] != sf.d_vars[index])
+  {
+    Node veq_v;
+    if (ArithMSum::getMonomial(veq[0], veq_c, veq_v))
+    {
+      Assert(veq_v == sf.d_vars[index]);
+    }
+  }
+  sf.d_subs[index] = veq[1];
+  if (!veq_c.isNull())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    sf.d_subs[index] = nm->mkNode(INTS_DIVISION_TOTAL, veq[1], veq_c);
+    Trace("cegqi-arith-debug")
+        << "...bound type is : " << sf.d_props[index].d_type << std::endl;
+    // intger division rounding up if from a lower bound
+    if (sf.d_props[index].d_type == 1 && options::cbqiRoundUpLowerLia())
+    {
+      sf.d_subs[index] = nm->mkNode(
+          PLUS,
+          sf.d_subs[index],
+          nm->mkNode(
+              ITE,
+              nm->mkNode(
+                  EQUAL, nm->mkNode(INTS_MODULUS_TOTAL, veq[1], veq_c), d_zero),
+              d_zero,
+              d_one));
+    }
+  }
+  Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index]
+                             << " -> " << sf.d_subs[index] << std::endl;
+  return true;
+}
+
+int ArithInstantiator::solve_arith(CegInstantiator* ci,
+                                   Node pv,
+                                   Node atom,
+                                   Node& veq_c,
+                                   Node& val,
+                                   Node& vts_coeff_inf,
+                                   Node& vts_coeff_delta)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  int ires = 0;
+  Trace("cegqi-arith-debug")
+      << "isolate for " << pv << " in " << atom << std::endl;
+  std::map<Node, Node> msum;
+  if (!ArithMSum::getMonomialSumLit(atom, msum))
+  {
+    Trace("cegqi-arith-debug")
+        << "fail : could not get monomial sum" << std::endl;
+    return 0;
+  }
+  Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl;
+  if (Trace.isOn("cegqi-arith-debug"))
+  {
+    ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug");
+  }
+  TypeNode pvtn = pv.getType();
+  // remove vts symbols from polynomial
+  Node vts_coeff[2];
+  for (unsigned t = 0; t < 2; t++)
+  {
+    if (!d_vts_sym[t].isNull())
+    {
+      std::map<Node, Node>::iterator itminf = msum.find(d_vts_sym[t]);
+      if (itminf != msum.end())
+      {
+        vts_coeff[t] = itminf->second;
+        if (vts_coeff[t].isNull())
+        {
+          vts_coeff[t] = nm->mkConst(Rational(1));
+        }
+        // negate if coefficient on variable is positive
+        std::map<Node, Node>::iterator itv = msum.find(pv);
+        if (itv != msum.end())
+        {
+          // multiply by the coefficient we will isolate for
+          if (itv->second.isNull())
+          {
+            vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
+          }
+          else
+          {
+            if (!pvtn.isInteger())
+            {
+              vts_coeff[t] = nm->mkNode(
+                  MULT,
+                  nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()),
+                  vts_coeff[t]);
+              vts_coeff[t] = Rewriter::rewrite(vts_coeff[t]);
+            }
+            else if (itv->second.getConst<Rational>().sgn() == 1)
+            {
+              vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
+            }
+          }
+        }
+        Trace("cegqi-arith-debug")
+            << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+        msum.erase(d_vts_sym[t]);
+      }
+    }
+  }
+
+  ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
+  if (ires == 0)
+  {
+    Trace("cegqi-arith-debug") << "fail : isolate" << std::endl;
+    return 0;
+  }
+  if (Trace.isOn("cegqi-arith-debug"))
+  {
+    Trace("cegqi-arith-debug") << "Isolate : ";
+    if (!veq_c.isNull())
+    {
+      Trace("cegqi-arith-debug") << veq_c << " * ";
+    }
+    Trace("cegqi-arith-debug")
+        << pv << " " << atom.getKind() << " " << val << std::endl;
+  }
+  // when not pure LIA/LRA, we must check whether the lhs contains pv
+  if (val.hasSubterm(pv))
+  {
+    Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
+    return 0;
+  }
+  // if its type is integer but the substitution is not integer
+  if (pvtn.isInteger()
+      && ((!veq_c.isNull() && !veq_c.getType().isInteger())
+          || !val.getType().isInteger()))
+  {
+    // redo, split integer/non-integer parts
+    bool useCoeff = false;
+    Integer coeff = ci->getQuantifiersEngine()
+                        ->getTermUtil()
+                        ->d_one.getConst<Rational>()
+                        .getNumerator();
+    for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
+         ++it)
+    {
+      if (it->first.isNull() || it->first.getType().isInteger())
+      {
+        if (!it->second.isNull())
+        {
+          coeff = coeff.lcm(it->second.getConst<Rational>().getDenominator());
+          useCoeff = true;
+        }
+      }
+    }
+    // multiply everything by this coefficient
+    Node rcoeff = nm->mkConst(Rational(coeff));
+    std::vector<Node> real_part;
+    for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end();
+         ++it)
+    {
+      if (useCoeff)
+      {
+        if (it->second.isNull())
+        {
+          msum[it->first] = rcoeff;
+        }
+        else
+        {
+          msum[it->first] =
+              Rewriter::rewrite(nm->mkNode(MULT, it->second, rcoeff));
+        }
+      }
+      if (!it->first.isNull() && !it->first.getType().isInteger())
+      {
+        real_part.push_back(msum[it->first].isNull()
+                                ? it->first
+                                : nm->mkNode(MULT, msum[it->first], it->first));
+      }
+    }
+    // remove delta
+    vts_coeff[1] = Node::null();
+    // multiply inf
+    if (!vts_coeff[0].isNull())
+    {
+      vts_coeff[0] = Rewriter::rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0]));
+    }
+    Node realPart = real_part.empty()
+                        ? d_zero
+                        : (real_part.size() == 1 ? real_part[0]
+                                                 : nm->mkNode(PLUS, real_part));
+    Assert(ci->getOutput()->isEligibleForInstantiation(realPart));
+    // re-isolate
+    Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
+    veq_c = Node::null();
+    ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
+    Trace("cegqi-arith-debug")
+        << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " "
+        << atom.getKind() << " " << val << std::endl;
+    Trace("cegqi-arith-debug")
+        << "                 real part : " << realPart << std::endl;
+    if (ires != 0)
+    {
+      int ires_use =
+          (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1
+                                                                          : -1;
+      val = Rewriter::rewrite(
+          nm->mkNode(ires_use == -1 ? PLUS : MINUS,
+                     nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart),
+                     nm->mkNode(TO_INTEGER, realPart)));
+      // could round up for upper bounds here
+      Trace("cegqi-arith-debug") << "result : " << val << std::endl;
+      Assert(val.getType().isInteger());
+    }
+  }
+  vts_coeff_inf = vts_coeff[0];
+  vts_coeff_delta = vts_coeff[1];
+  Trace("cegqi-arith-debug")
+      << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " "
+      << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")"
+      << std::endl;
+  return ires;
+}
+
+Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
+                                                     Node e,
+                                                     Node t,
+                                                     bool isLower,
+                                                     Node c,
+                                                     Node me,
+                                                     Node mt,
+                                                     Node theta,
+                                                     Node inf_coeff,
+                                                     Node delta_coeff)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node val = t;
+  Trace("cegqi-arith-bound2") << "Value : " << val << std::endl;
+  Assert(!e.getType().isInteger() || t.getType().isInteger());
+  Assert(!e.getType().isInteger() || mt.getType().isInteger());
+  // add rho value
+  // get the value of c*e
+  Node ceValue = me;
+  Node new_theta = theta;
+  if (!c.isNull())
+  {
+    Assert(c.getType().isInteger());
+    ceValue = nm->mkNode(MULT, ceValue, c);
+    ceValue = Rewriter::rewrite(ceValue);
+    if (new_theta.isNull())
+    {
+      new_theta = c;
+    }
+    else
+    {
+      new_theta = nm->mkNode(MULT, new_theta, c);
+      new_theta = Rewriter::rewrite(new_theta);
+    }
+    Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl;
+    Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl;
+  }
+  if (!new_theta.isNull() && e.getType().isInteger())
+  {
+    Node rho;
+    if (isLower)
+    {
+      rho = nm->mkNode(MINUS, ceValue, mt);
+    }
+    else
+    {
+      rho = nm->mkNode(MINUS, mt, ceValue);
+    }
+    rho = Rewriter::rewrite(rho);
+    Trace("cegqi-arith-bound2")
+        << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
+    Trace("cegqi-arith-bound2")
+        << "..." << rho << " mod " << new_theta << " = ";
+    rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta);
+    rho = Rewriter::rewrite(rho);
+    Trace("cegqi-arith-bound2") << rho << std::endl;
+    Kind rk = isLower ? PLUS : MINUS;
+    val = nm->mkNode(rk, val, rho);
+    val = Rewriter::rewrite(val);
+    Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
+  }
+  if (!inf_coeff.isNull())
+  {
+    Assert(!d_vts_sym[0].isNull());
+    val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0]));
+    val = Rewriter::rewrite(val);
+  }
+  if (!delta_coeff.isNull())
+  {
+    // create delta here if necessary
+    val = nm->mkNode(
+        PLUS,
+        val,
+        nm->mkNode(MULT,
+                   delta_coeff,
+                   ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta()));
+    val = Rewriter::rewrite(val);
+  }
+  return val;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
new file mode 100644
index 000000000..b6e22329d
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -0,0 +1,206 @@
+/*********************                                                        */
+/*! \file ceg_arith_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ceg_arith_instantiator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+
+#include <vector>
+#include "expr/node.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Arithmetic instantiator
+ *
+ * This implements a selection function for arithmetic, which is based on
+ * variants of:
+ * - Loos/Weispfenning's method (virtual term substitution) for linear real
+ *    arithmetic,
+ * - Ferrante/Rackoff's method (interior points) for linear real arithmetic,
+ * - Cooper's method for linear arithmetic.
+ * For details, see Reynolds et al, "Solving Linear Arithmetic Using
+ * Counterexample-Guided Instantiation", FMSD 2017.
+ *
+ * This class contains all necessary information for instantiating a single
+ * real or integer typed variable of a single quantified formula.
+ */
+class ArithInstantiator : public Instantiator
+{
+ public:
+  ArithInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  virtual ~ArithInstantiator() {}
+  /** reset */
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  /** this instantiator processes equalities */
+  bool hasProcessEquality(CegInstantiator* ci,
+                          SolvedForm& sf,
+                          Node pv,
+                          CegInstEffort effort) override;
+  /**
+   * Process the equality term[0]=term[1]. If this equality is equivalent to one
+   * of the form c * pv = t, then we add the substitution c * pv -> t to sf and
+   * recurse.
+   */
+  bool processEquality(CegInstantiator* ci,
+                       SolvedForm& sf,
+                       Node pv,
+                       std::vector<TermProperties>& term_props,
+                       std::vector<Node>& terms,
+                       CegInstEffort effort) override;
+  /** this instantiator processes assertions */
+  bool hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override;
+  /** this instantiator processes literals lit of kinds EQUAL and GEQ */
+  Node hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           Node lit,
+                           CegInstEffort effort) override;
+  /** process assertion lit
+   *
+   * If lit can be turned into a bound of the form c * pv <> t, then we store
+   * information about this bound (see d_mbp_bounds).
+   *
+   * If cbqiModel is false (not the default), we recursively try adding the
+   * substitution { c * pv -> t } to sf and recursing.
+   */
+  bool processAssertion(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        Node lit,
+                        Node alit,
+                        CegInstEffort effort) override;
+  /** process assertions
+   *
+   * This is called after processAssertion has been called on all current bounds
+   * for pv. This method selects the "best" bound of those we have seen, which
+   * can be one of the following:
+   * - Maximal lower bound,
+   * - Minimal upper bound,
+   * - Midpoint of maximal lower and minimal upper bounds, [if pv is not Int,
+   *   and --cbqi-midpoint]
+   * - (+-) Infinity, [if no upper (resp. lower) bounds, and --cbqi-use-vts-inf]
+   * - Zero, [if no bounds]
+   * - Non-optimal bounds. [if the above bounds fail, and --cbqi-nopt]
+   */
+  bool processAssertions(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         CegInstEffort effort) override;
+  /**
+   * This instantiator needs to postprocess variables that have substitutions
+   * with coefficients, i.e. c*x -> t.
+   */
+  bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
+                                                SolvedForm& sf,
+                                                Node pv,
+                                                CegInstEffort effort) override;
+  /** post-process instantiation for variable
+   *
+   * If the solved form for integer variable pv is a substitution with
+   * coefficients c*x -> t, this turns its solved form into x -> div(t,c), where
+   * div is integer division.
+   */
+  bool postProcessInstantiationForVariable(CegInstantiator* ci,
+                                           SolvedForm& sf,
+                                           Node pv,
+                                           CegInstEffort effort,
+                                           std::vector<Node>& lemmas) override;
+  std::string identify() const override { return "Arith"; }
+
+ private:
+  /** zero/one */
+  Node d_zero;
+  Node d_one;
+  //--------------------------------------current bounds
+  /** Virtual term symbols (vts), where 0: infinity, 1: delta. */
+  Node d_vts_sym[2];
+  /** Current 0:lower, 1:upper bounds for the variable to instantiate */
+  std::vector<Node> d_mbp_bounds[2];
+  /** Coefficients for the lower/upper bounds for the variable to instantiate */
+  std::vector<Node> d_mbp_coeff[2];
+  /** Coefficients for virtual terms for each bound. */
+  std::vector<Node> d_mbp_vts_coeff[2][2];
+  /** The source literal (explanation) for each bound. */
+  std::vector<Node> d_mbp_lit[2];
+  //--------------------------------------end current bounds
+  /** solve arith
+   *
+   * Given variable to instantiate pv, this isolates the atom into solved form:
+   *    veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
+   * where we ensure val has Int type if pv has Int type, and val does not
+   * contain vts symbols.
+   */
+  int solve_arith(CegInstantiator* ci,
+                  Node v,
+                  Node atom,
+                  Node& veq_c,
+                  Node& val,
+                  Node& vts_coeff_inf,
+                  Node& vts_coeff_delta);
+  /** get model based projection value
+   *
+   * Given a implied (non-strict) bound:
+   *   c*e <=/>= t + inf_coeff*INF + delta_coeff*DELTA
+   * this method returns ret, the minimal (resp. maximal) term such that:
+   *   c*ret <> t + inf_coeff*INF + delta_coeff*DELTA
+   * is satisfied in the current model M, and such that the divisibilty
+   * constraint is also satisfied:
+   *   ret^M mod c*theta = (c*e)^M mod c*theta
+   * where the input theta is a constant (which is assumed to be 1 if null). The
+   * values of me and mt are the current model values of e and t respectively.
+   *
+   * For example, if e has Real type and:
+   *   isLower = false, e^M = 0, t^M = 2, inf_coeff = 0, delta_coeff = 2
+   * Then, this function returns t+2*delta.
+   *
+   * For example, if e has Int type and:
+   *   isLower = true, e^M = 4, t^M = 2, theta = 3
+   * Then, this function returns t+2, noting that (t+2)^M mod 3 = e^M mod 3 = 2.
+   *
+   * For example, if e has Int type and:
+   *   isLower = false, e^M = 1, t^M = 5, theta = 3
+   * Then, this function returns t-1, noting that (t-1)^M mod 3 = e^M mod 3 = 1.
+   *
+   * The value that is added or substracted from t in the return value when e
+   * is an integer is the value of "rho" from Figure 6 of Reynolds et al,
+   * "Solving Linear Arithmetic Using Counterexample-Guided Instantiation",
+   * FMSD 2017.
+   */
+  Node getModelBasedProjectionValue(CegInstantiator* ci,
+                                    Node e,
+                                    Node t,
+                                    bool isLower,
+                                    Node c,
+                                    Node me,
+                                    Node mt,
+                                    Node theta,
+                                    Node inf_coeff,
+                                    Node delta_coeff);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
new file mode 100644
index 000000000..678691ef4
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -0,0 +1,1139 @@
+/*********************                                                        */
+/*! \file ceg_bv_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of ceg_bv_instantiator
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
+
+#include <stack>
+#include "options/quantifiers_options.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+#include "util/random.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+struct BvLinearAttributeId
+{
+};
+using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>;
+
+// this class can be used to query the model value through the CegInstaniator
+// class
+class CegInstantiatorBvInverterQuery : public BvInverterQuery
+{
+ public:
+  CegInstantiatorBvInverterQuery(CegInstantiator* ci)
+      : BvInverterQuery(), d_ci(ci)
+  {
+  }
+  ~CegInstantiatorBvInverterQuery() {}
+  /** return the model value of n */
+  Node getModelValue(Node n) override { return d_ci->getModelValue(n); }
+  /** get bound variable of type tn */
+  Node getBoundVariable(TypeNode tn) override
+  {
+    return d_ci->getBoundVariable(tn);
+  }
+
+ protected:
+  // pointer to class that is able to query model values
+  CegInstantiator* d_ci;
+};
+
+BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
+    : Instantiator(qe, tn), d_tried_assertion_inst(false)
+{
+  // get the global inverter utility
+  // 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() {}
+void BvInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort)
+{
+  d_inst_id_counter = 0;
+  d_var_to_inst_id.clear();
+  d_inst_id_to_term.clear();
+  d_inst_id_to_alit.clear();
+  d_var_to_curr_inst_id.clear();
+  d_alit_to_model_slack.clear();
+  d_tried_assertion_inst = false;
+}
+
+void BvInstantiator::processLiteral(CegInstantiator* ci,
+                                    SolvedForm& sf,
+                                    Node pv,
+                                    Node lit,
+                                    Node alit,
+                                    CegInstEffort effort)
+{
+  Assert(d_inverter != NULL);
+  // find path to pv
+  std::vector<unsigned> path;
+  Node sv = d_inverter->getSolveVariable(pv.getType());
+  Node pvs = ci->getModelValue(pv);
+  Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
+  Node slit =
+      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl());
+  if (!slit.isNull())
+  {
+    CegInstantiatorBvInverterQuery m(ci);
+    unsigned iid = d_inst_id_counter;
+    Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
+    Node inst = d_inverter->solveBvLit(sv, slit, path, &m);
+    if (!inst.isNull())
+    {
+      inst = Rewriter::rewrite(inst);
+      if (inst.isConst() || !ci->hasNestedQuantification())
+      {
+        Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
+        // store information for id and increment
+        d_var_to_inst_id[pv].push_back(iid);
+        d_inst_id_to_term[iid] = inst;
+        d_inst_id_to_alit[iid] = alit;
+        d_inst_id_counter++;
+      }
+    }
+    else
+    {
+      Trace("cegqi-bv") << "...failed to solve." << std::endl;
+    }
+  }
+  else
+  {
+    Trace("cegqi-bv") << "...no path." << std::endl;
+  }
+}
+
+bool BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         CegInstEffort effort)
+{
+  return true;
+}
+
+Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         Node lit,
+                                         CegInstEffort effort)
+{
+  if (effort == CEG_INST_EFFORT_FULL)
+  {
+    // always use model values at full effort
+    return Node::null();
+  }
+  Node atom = lit.getKind() == NOT ? lit[0] : lit;
+  bool pol = lit.getKind() != NOT;
+  Kind k = atom.getKind();
+  if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT)
+  {
+    // others are unhandled
+    return Node::null();
+  }
+  else if (!atom[0].getType().isBitVector())
+  {
+    return Node::null();
+  }
+  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP
+           || (pol && k == EQUAL))
+  {
+    return lit;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node s = atom[0];
+  Node t = atom[1];
+
+  Node sm = ci->getModelValue(s);
+  Node tm = ci->getModelValue(t);
+  Assert(!sm.isNull() && sm.isConst());
+  Assert(!tm.isNull() && tm.isConst());
+  Trace("cegqi-bv") << "Model value: " << std::endl;
+  Trace("cegqi-bv") << "   " << s << " " << k << " " << t << " is "
+                    << std::endl;
+  Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
+
+  Node ret;
+  if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
+  {
+    // if using slack, we convert constraints to a positive equality based on
+    // the current model M, e.g.:
+    //   (not) s ~ t  --->  s = t + ( s^M - t^M )
+    if (sm != tm)
+    {
+      Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm));
+      Assert(slack.isConst());
+      // remember the slack value for the asserted literal
+      d_alit_to_model_slack[lit] = slack;
+      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
+      Trace("cegqi-bv") << "Slack is " << slack << std::endl;
+    }
+    else
+    {
+      ret = s.eqNode(t);
+    }
+  }
+  else
+  {
+    // turn disequality into an inequality
+    // e.g. s != t becomes s < t or t < s
+    if (k == EQUAL)
+    {
+      if (Random::getRandom().pickWithProb(0.5))
+      {
+        std::swap(s, t);
+      }
+      pol = true;
+    }
+    // otherwise, we optimistically solve for the boundary point of an
+    // inequality, for example:
+    //   for s < t, we solve s+1 = t
+    //   for ~( s < t ), we solve s = t
+    // notice that this equality does not necessarily hold in the model, and
+    // hence the corresponding instantiation strategy is not guaranteed to be
+    // monotonic.
+    if (!pol)
+    {
+      ret = s.eqNode(t);
+    }
+    else
+    {
+      Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
+      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
+    }
+  }
+  Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
+  return ret;
+}
+
+bool BvInstantiator::processAssertion(CegInstantiator* ci,
+                                      SolvedForm& sf,
+                                      Node pv,
+                                      Node lit,
+                                      Node alit,
+                                      CegInstEffort effort)
+{
+  // if option enabled, use approach for word-level inversion for BV
+  // instantiation
+  if (options::cbqiBv())
+  {
+    // get the best rewritten form of lit for solving for pv
+    //   this should remove instances of non-invertible operators, and
+    //   "linearize" lit with respect to pv as much as possible
+    Node rlit = rewriteAssertionForSolvePv(ci, pv, lit);
+    if (Trace.isOn("cegqi-bv"))
+    {
+      Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv
+                        << " in " << lit << std::endl;
+      if (lit != rlit)
+      {
+        Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
+      }
+    }
+    if (!rlit.isNull())
+    {
+      processLiteral(ci, sf, pv, rlit, alit, effort);
+    }
+  }
+  return false;
+}
+
+bool BvInstantiator::useModelValue(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort)
+{
+  return !d_tried_assertion_inst
+         && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort());
+}
+
+bool BvInstantiator::processAssertions(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       CegInstEffort effort)
+{
+  std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::iterator
+      iti = d_var_to_inst_id.find(pv);
+  if (iti == d_var_to_inst_id.end())
+  {
+    // no bounds
+    return false;
+  }
+  Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv
+                    << std::endl;
+  // if interleaving, do not do inversion half the time
+  if (options::cbqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
+  {
+    Trace("cegqi-bv") << "...do not do instantiation for " << pv
+                      << " (skip, based on heuristic)" << std::endl;
+  }
+  bool firstVar = sf.empty();
+  // get inst id list
+  if (Trace.isOn("cegqi-bv"))
+  {
+    Trace("cegqi-bv") << "  " << iti->second.size()
+                      << " candidate instantiations for " << pv << " : "
+                      << std::endl;
+    if (firstVar)
+    {
+      Trace("cegqi-bv") << "  ...this is the first variable" << std::endl;
+    }
+  }
+  // until we have a model-preserving selection function for BV, this must
+  // be heuristic (we only pick one literal)
+  // hence we randomize the list
+  // this helps robustness, since picking the same literal every time may
+  // lead to a stream of value instantiations, whereas with randomization
+  // we may find an invertible literal that leads to a useful instantiation.
+  std::random_shuffle(iti->second.begin(), iti->second.end());
+
+  if (Trace.isOn("cegqi-bv"))
+  {
+    for (unsigned j = 0, size = iti->second.size(); j < size; j++)
+    {
+      unsigned inst_id = iti->second[j];
+      Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+      Node inst_term = d_inst_id_to_term[inst_id];
+      Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
+      Node alit = d_inst_id_to_alit[inst_id];
+
+      // get the slack value introduced for the asserted literal
+      Node curr_slack_val;
+      std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+          d_alit_to_model_slack.find(alit);
+      if (itms != d_alit_to_model_slack.end())
+      {
+        curr_slack_val = itms->second;
+      }
+
+      // debug printing
+      Trace("cegqi-bv") << "   [" << j << "] : ";
+      Trace("cegqi-bv") << inst_term << std::endl;
+      if (!curr_slack_val.isNull())
+      {
+        Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
+                          << std::endl;
+      }
+      Trace("cegqi-bv-debug") << "   ...from : " << alit << std::endl;
+      Trace("cegqi-bv") << std::endl;
+    }
+  }
+
+  // Now, try all instantiation ids we want to try
+  // Typically we try only one, otherwise worst-case performance
+  // for constructing instantiations is exponential on the number of
+  // variables in this quantifier prefix.
+  bool ret = false;
+  bool tryMultipleInst = firstVar && options::cbqiMultiInst();
+  bool revertOnSuccess = tryMultipleInst;
+  for (unsigned j = 0, size = iti->second.size(); j < size; j++)
+  {
+    unsigned inst_id = iti->second[j];
+    Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
+    Node inst_term = d_inst_id_to_term[inst_id];
+    Node alit = d_inst_id_to_alit[inst_id];
+    // try instantiation pv -> inst_term
+    TermProperties pv_prop_bv;
+    Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl;
+    d_var_to_curr_inst_id[pv] = inst_id;
+    d_tried_assertion_inst = true;
+    ci->markSolved(alit);
+    if (ci->constructInstantiationInc(
+            pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
+    {
+      ret = true;
+    }
+    ci->markSolved(alit, false);
+    // we are done unless we try multiple instances
+    if (!tryMultipleInst)
+    {
+      break;
+    }
+  }
+  if (ret)
+  {
+    return true;
+  }
+  Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl;
+  d_var_to_curr_inst_id.erase(pv);
+
+  return false;
+}
+
+Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
+                                                Node pv,
+                                                Node lit)
+{
+  // result of rewriting the visited term
+  std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
+  visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+  // whether the visited term contains pv
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
+  std::stack<std::stack<TNode> > visit;
+  TNode cur;
+  visit.push(std::stack<TNode>());
+  visit.top().push(lit);
+  do
+  {
+    cur = visit.top().top();
+    visit.top().pop();
+    it = visited.top().find(cur);
+
+    if (it == visited.top().end())
+    {
+      std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc =
+          curr_subs.find(cur);
+      if (itc != curr_subs.end())
+      {
+        visited.top()[cur] = itc->second;
+      }
+      else
+      {
+        if (cur.getKind() == CHOICE)
+        {
+          // must replace variables of choice functions
+          // with new variables to avoid variable
+          // capture when considering substitutions
+          // with multiple literals.
+          Node bv = ci->getBoundVariable(cur[0][0].getType());
+          // should not have captured variables
+          Assert(curr_subs.find(cur[0][0]) == curr_subs.end());
+          curr_subs[cur[0][0]] = bv;
+          // we cannot cache the results of subterms
+          // of this choice expression since we are
+          // now in the context { cur[0][0] -> bv },
+          // hence we push a context here
+          visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+          visit.push(std::stack<TNode>());
+        }
+        visited.top()[cur] = Node::null();
+        visit.top().push(cur);
+        for (unsigned i = 0; i < cur.getNumChildren(); i++)
+        {
+          visit.top().push(cur[i]);
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+      {
+        children.push_back(cur.getOperator());
+      }
+      bool contains_pv = (cur == pv);
+      for (unsigned i = 0; i < cur.getNumChildren(); i++)
+      {
+        it = visited.top().find(cur[i]);
+        Assert(it != visited.top().end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur[i] != it->second;
+        children.push_back(it->second);
+        contains_pv = contains_pv || visited_contains_pv[cur[i]];
+      }
+      // careful that rewrites above do not affect whether this term contains pv
+      visited_contains_pv[cur] = contains_pv;
+
+      // rewrite the term
+      ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv);
+
+      // return original if the above function does not produce a result
+      if (ret.isNull())
+      {
+        if (childChanged)
+        {
+          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+        }
+        else
+        {
+          ret = cur;
+        }
+      }
+
+      /* We need to update contains_pv also for rewritten nodes, since
+       * the normalizePv* functions rely on the information if pv occurs in a
+       * rewritten node or not. */
+      if (ret != cur)
+      {
+        contains_pv = (ret == pv);
+        for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i)
+        {
+          contains_pv = contains_pv || visited_contains_pv[ret[i]];
+        }
+        visited_contains_pv[ret] = contains_pv;
+      }
+
+      // if was choice, pop context
+      if (cur.getKind() == CHOICE)
+      {
+        Assert(curr_subs.find(cur[0][0]) != curr_subs.end());
+        curr_subs.erase(cur[0][0]);
+        visited.pop();
+        visit.pop();
+        Assert(visited.size() == visit.size());
+        Assert(!visit.empty());
+      }
+
+      visited.top()[cur] = ret;
+    }
+  } while (!visit.top().empty());
+  Assert(visited.size() == 1);
+  Assert(visited.top().find(lit) != visited.top().end());
+  Assert(!visited.top().find(lit)->second.isNull());
+
+  Node result = visited.top()[lit];
+
+  if (Trace.isOn("cegqi-bv-nl"))
+  {
+    std::vector<TNode> trace_visit;
+    std::unordered_set<TNode, TNodeHashFunction> trace_visited;
+
+    trace_visit.push_back(result);
+    do
+    {
+      cur = trace_visit.back();
+      trace_visit.pop_back();
+
+      if (trace_visited.find(cur) == trace_visited.end())
+      {
+        trace_visited.insert(cur);
+        trace_visit.insert(trace_visit.end(), cur.begin(), cur.end());
+      }
+      else if (cur == pv)
+      {
+        Trace("cegqi-bv-nl")
+            << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl;
+      }
+    } while (!trace_visit.empty());
+  }
+
+  return result;
+}
+
+/**
+ * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t,
+ * or -pv * t. Extracting the coefficient of multiplications only succeeds if
+ * the multiplication are normalized with normalizePvMult.
+ *
+ * If sucessful it returns
+ *   1    if n ==  pv,
+ *  -1    if n == -pv,
+ *   t    if n ==  pv * t,
+ *  -t    if n == -pv * t.
+ * If n is not a linear term, a null node is returned.
+ */
+static Node getPvCoeff(TNode pv, TNode n)
+{
+  bool neg = false;
+  Node coeff;
+
+  if (n.getKind() == BITVECTOR_NEG)
+  {
+    neg = true;
+    n = n[0];
+  }
+
+  if (n == pv)
+  {
+    coeff = bv::utils::mkOne(bv::utils::getSize(pv));
+  }
+  /* All multiplications are normalized to pv * (t1 * t2). */
+  else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
+  {
+    Assert(n.getNumChildren() == 2);
+    Assert(n[0] == pv);
+    coeff = n[1];
+  }
+  else /* n is in no form to extract the coefficient for pv */
+  {
+    Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
+                         << n << std::endl;
+    return Node::null();
+  }
+  Assert(!coeff.isNull());
+
+  if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
+  return coeff;
+}
+
+/**
+ * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks
+ * terms in which pv occurs.
+ * For example,
+ *
+ *  a * -pv * b * c
+ *
+ * is rewritten to
+ *
+ *  pv * -(a * b * c)
+ *
+ * Returns the normalized node if the resulting term is linear w.r.t. pv and
+ * a null node otherwise. If pv does not occur in children it returns a
+ * multiplication over children.
+ */
+static Node normalizePvMult(
+    TNode pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  bool neg, neg_coeff = false;
+  bool found_pv = false;
+  NodeManager* nm;
+  NodeBuilder<> nb(BITVECTOR_MULT);
+  BvLinearAttribute is_linear;
+
+  nm = NodeManager::currentNM();
+  for (TNode nc : children)
+  {
+    if (!contains_pv[nc])
+    {
+      nb << nc;
+      continue;
+    }
+
+    neg = false;
+    if (nc.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      nc = nc[0];
+    }
+
+    if (!found_pv && nc == pv)
+    {
+      found_pv = true;
+      neg_coeff = neg;
+      continue;
+    }
+    else if (!found_pv && nc.getKind() == BITVECTOR_MULT
+             && nc.getAttribute(is_linear))
+    {
+      Assert(nc.getNumChildren() == 2);
+      Assert(nc[0] == pv);
+      Assert(!contains_pv[nc[1]]);
+      found_pv = true;
+      neg_coeff = neg;
+      nb << nc[1];
+      continue;
+    }
+    return Node::null(); /* non-linear */
+  }
+  Assert(nb.getNumChildren() > 0);
+
+  Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
+  if (neg_coeff)
+  {
+    coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+  }
+  coeff = Rewriter::rewrite(coeff);
+  unsigned size_coeff = bv::utils::getSize(coeff);
+  Node zero = bv::utils::mkZero(size_coeff);
+  if (coeff == zero)
+  {
+    return zero;
+  }
+  Node result;
+  if (found_pv)
+  {
+    if (coeff == bv::utils::mkOne(size_coeff))
+    {
+      return pv;
+    }
+    result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
+    contains_pv[result] = true;
+    result.setAttribute(is_linear, true);
+  }
+  else
+  {
+    result = coeff;
+  }
+  return result;
+}
+
+#ifdef CVC4_ASSERTIONS
+static bool isLinearPlus(
+    TNode n,
+    TNode pv,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  Node coeff;
+  Assert(n.getAttribute(BvLinearAttribute()));
+  Assert(n.getNumChildren() == 2);
+  if (n[0] != pv)
+  {
+    Assert(n[0].getKind() == BITVECTOR_MULT);
+    Assert(n[0].getNumChildren() == 2);
+    Assert(n[0][0] == pv);
+    Assert(!contains_pv[n[0][1]]);
+  }
+  Assert(!contains_pv[n[1]]);
+  coeff = getPvCoeff(pv, n[0]);
+  Assert(!coeff.isNull());
+  Assert(!contains_pv[coeff]);
+  return true;
+}
+#endif
+
+/**
+ * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
+ * terms in which pv occurs.
+ * For example,
+ *
+ *  a * pv + b + c * -pv
+ *
+ * is rewritten to
+ *
+ *  pv * (a - c) + b
+ *
+ * Returns the normalized node if the resulting term is linear w.r.t. pv and
+ * a null node otherwise. If pv does not occur in children it returns an
+ * addition over children.
+ */
+static Node normalizePvPlus(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  NodeManager* nm;
+  NodeBuilder<> nb_c(BITVECTOR_PLUS);
+  NodeBuilder<> nb_l(BITVECTOR_PLUS);
+  BvLinearAttribute is_linear;
+  bool neg;
+
+  nm = NodeManager::currentNM();
+  for (TNode nc : children)
+  {
+    if (!contains_pv[nc])
+    {
+      nb_l << nc;
+      continue;
+    }
+
+    neg = false;
+    if (nc.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      nc = nc[0];
+    }
+
+    if (nc == pv
+        || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
+    {
+      Node coeff = getPvCoeff(pv, nc);
+      Assert(!coeff.isNull());
+      if (neg)
+      {
+        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+      }
+      nb_c << coeff;
+      continue;
+    }
+    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
+    {
+      Assert(isLinearPlus(nc, pv, contains_pv));
+      Node coeff = getPvCoeff(pv, nc[0]);
+      Assert(!coeff.isNull());
+      Node leaf = nc[1];
+      if (neg)
+      {
+        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
+        leaf = nm->mkNode(BITVECTOR_NEG, leaf);
+      }
+      nb_c << coeff;
+      nb_l << leaf;
+      continue;
+    }
+    /* can't collect coefficients of 'pv' in 'cur' -> non-linear */
+    return Node::null();
+  }
+  Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0);
+
+  Node pv_mult_coeffs, result;
+  if (nb_c.getNumChildren() > 0)
+  {
+    Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
+    coeffs = Rewriter::rewrite(coeffs);
+    result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv);
+  }
+
+  if (nb_l.getNumChildren() > 0)
+  {
+    Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
+    leafs = Rewriter::rewrite(leafs);
+    Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
+    /* pv * 0 + t --> t */
+    if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
+    {
+      result = leafs;
+    }
+    else
+    {
+      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
+      contains_pv[result] = true;
+      result.setAttribute(is_linear, true);
+    }
+  }
+  Assert(!result.isNull());
+  return result;
+}
+
+/**
+ * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
+ * marks terms in which pv occurs.
+ * For example, equality
+ *
+ *   -pv * a + b = c + pv
+ *
+ * rewrites to
+ *
+ *   pv * (-a - 1) = c - b.
+ */
+static Node normalizePvEqual(
+    Node pv,
+    const std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  Assert(children.size() == 2);
+
+  NodeManager* nm = NodeManager::currentNM();
+  BvLinearAttribute is_linear;
+  Node coeffs[2], leafs[2];
+  bool neg;
+  TNode child;
+
+  for (unsigned i = 0; i < 2; ++i)
+  {
+    child = children[i];
+    neg = false;
+    if (child.getKind() == BITVECTOR_NEG)
+    {
+      neg = true;
+      child = child[0];
+    }
+    if (child.getAttribute(is_linear) || child == pv)
+    {
+      if (child.getKind() == BITVECTOR_PLUS)
+      {
+        Assert(isLinearPlus(child, pv, contains_pv));
+        coeffs[i] = getPvCoeff(pv, child[0]);
+        leafs[i] = child[1];
+      }
+      else
+      {
+        Assert(child.getKind() == BITVECTOR_MULT || child == pv);
+        coeffs[i] = getPvCoeff(pv, child);
+      }
+    }
+    if (neg)
+    {
+      if (!coeffs[i].isNull())
+      {
+        coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
+      }
+      if (!leafs[i].isNull())
+      {
+        leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
+      }
+    }
+  }
+
+  if (coeffs[0].isNull() || coeffs[1].isNull())
+  {
+    return Node::null();
+  }
+
+  Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
+  coeff = Rewriter::rewrite(coeff);
+  std::vector<Node> mult_children = {pv, coeff};
+  Node lhs = normalizePvMult(pv, mult_children, contains_pv);
+
+  Node rhs;
+  if (!leafs[0].isNull() && !leafs[1].isNull())
+  {
+    rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
+  }
+  else if (!leafs[0].isNull())
+  {
+    rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
+  }
+  else if (!leafs[1].isNull())
+  {
+    rhs = leafs[1];
+  }
+  else
+  {
+    rhs = bv::utils::mkZero(bv::utils::getSize(pv));
+  }
+  rhs = Rewriter::rewrite(rhs);
+
+  if (lhs == rhs)
+  {
+    return bv::utils::mkTrue();
+  }
+
+  Node result = lhs.eqNode(rhs);
+  contains_pv[result] = true;
+  return result;
+}
+
+Node BvInstantiator::rewriteTermForSolvePv(
+    Node pv,
+    Node n,
+    std::vector<Node>& children,
+    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+{
+  NodeManager* nm = NodeManager::currentNM();
+
+  // [1] rewrite cases of non-invertible operators
+
+  if (n.getKind() == EQUAL)
+  {
+    TNode lhs = children[0];
+    TNode rhs = children[1];
+
+    /* rewrite: x * x = x -> x < 2 */
+    if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv
+         && rhs[1] == pv)
+        || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv
+            && lhs[1] == pv))
+    {
+      return nm->mkNode(
+          BITVECTOR_ULT,
+          pv,
+          bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
+    }
+
+    if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
+    {
+      Node result = normalizePvEqual(pv, children, contains_pv);
+      if (!result.isNull())
+      {
+        Trace("cegqi-bv-nl")
+            << "Normalize " << n << " to " << result << std::endl;
+      }
+      else
+      {
+        Trace("cegqi-bv-nl")
+            << "Nonlinear " << n.getKind() << " " << n << std::endl;
+      }
+      return result;
+    }
+  }
+  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
+  {
+    if (options::cbqiBvLinearize() && contains_pv[n])
+    {
+      Node result;
+      if (n.getKind() == BITVECTOR_MULT)
+      {
+        result = normalizePvMult(pv, children, contains_pv);
+      }
+      else
+      {
+        result = normalizePvPlus(pv, children, contains_pv);
+      }
+      if (!result.isNull())
+      {
+        Trace("cegqi-bv-nl")
+            << "Normalize " << n << " to " << result << std::endl;
+        return result;
+      }
+      else
+      {
+        Trace("cegqi-bv-nl")
+            << "Nonlinear " << n.getKind() << " " << n << std::endl;
+      }
+    }
+  }
+
+  // [2] try to rewrite non-linear literals -> linear literals
+
+  return Node::null();
+}
+
+/** sort bv extract interval
+ *
+ * This sorts lists of bitvector extract terms where
+ * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
+ * if i1>j1 or i1=j1 and i2>j2.
+ */
+struct SortBvExtractInterval
+{
+  bool operator()(Node i, Node j)
+  {
+    Assert(i.getKind() == BITVECTOR_EXTRACT);
+    Assert(j.getKind() == BITVECTOR_EXTRACT);
+    BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
+    BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
+    if (ie.high > je.high)
+    {
+      return true;
+    }
+    else if (ie.high == je.high)
+    {
+      Assert(ie.low != je.low);
+      return ie.low > je.low;
+    }
+    return false;
+  }
+};
+
+void BvInstantiatorPreprocess::registerCounterexampleLemma(
+    std::vector<Node>& lems, std::vector<Node>& ce_vars)
+{
+  // new variables
+  std::vector<Node> vars;
+  // new lemmas
+  std::vector<Node> new_lems;
+
+  if (options::cbqiBvRmExtract())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
+    // map from terms to bitvector extracts applied to that term
+    std::map<Node, std::vector<Node> > extract_map;
+    std::unordered_set<TNode, TNodeHashFunction> visited;
+    for (unsigned i = 0, size = lems.size(); i < size; i++)
+    {
+      Trace("cegqi-bv-pp-debug2")
+          << "Register ce lemma # " << i << " : " << lems[i] << std::endl;
+      collectExtracts(lems[i], extract_map, visited);
+    }
+    for (std::pair<const Node, std::vector<Node> >& es : extract_map)
+    {
+      // sort based on the extract start position
+      std::vector<Node>& curr_vec = es.second;
+
+      SortBvExtractInterval sbei;
+      std::sort(curr_vec.begin(), curr_vec.end(), sbei);
+
+      unsigned width = es.first.getType().getBitVectorSize();
+
+      // list of points b such that:
+      //   b>0 and we must start a segment at (b-1)  or  b==0
+      std::vector<unsigned> boundaries;
+      boundaries.push_back(width);
+      boundaries.push_back(0);
+
+      Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
+      for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
+      {
+        Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
+        BitVectorExtract e =
+            curr_vec[i].getOperator().getConst<BitVectorExtract>();
+        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
+            == boundaries.end())
+        {
+          boundaries.push_back(e.high + 1);
+        }
+        if (std::find(boundaries.begin(), boundaries.end(), e.low)
+            == boundaries.end())
+        {
+          boundaries.push_back(e.low);
+        }
+      }
+      std::sort(boundaries.rbegin(), boundaries.rend());
+
+      // make the extract variables
+      std::vector<Node> children;
+      for (unsigned i = 1; i < boundaries.size(); i++)
+      {
+        Assert(boundaries[i - 1] > 0);
+        Node ex = bv::utils::mkExtract(
+            es.first, boundaries[i - 1] - 1, boundaries[i]);
+        Node var =
+            nm->mkSkolem("ek",
+                         ex.getType(),
+                         "variable to represent disjoint extract region");
+        children.push_back(var);
+        vars.push_back(var);
+      }
+
+      Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
+      Assert(conc.getType() == es.first.getType());
+      Node eq_lem = conc.eqNode(es.first);
+      Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
+      new_lems.push_back(eq_lem);
+      Trace("cegqi-bv-pp") << "...finished processing extracts for term "
+                           << es.first << std::endl;
+    }
+    Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
+  }
+
+  if (!vars.empty())
+  {
+    // could try applying subs -> vars here
+    // in practice, this led to worse performance
+
+    Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
+                         << std::endl;
+    lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+    Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
+                         << std::endl;
+    ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+  }
+}
+
+void BvInstantiatorPreprocess::collectExtracts(
+    Node lem,
+    std::map<Node, std::vector<Node> >& extract_map,
+    std::unordered_set<TNode, TNodeHashFunction>& visited)
+{
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(lem);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getKind() != FORALL)
+      {
+        if (cur.getKind() == BITVECTOR_EXTRACT)
+        {
+          if (cur[0].getKind() == INST_CONSTANT)
+          {
+            extract_map[cur[0]].push_back(cur);
+          }
+        }
+
+        for (const Node& nc : cur)
+        {
+          visit.push_back(nc);
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
new file mode 100644
index 000000000..439309e91
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -0,0 +1,216 @@
+/*********************                                                        */
+/*! \file ceg_bv_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ceg_bv_instantiator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+
+#include <unordered_map>
+#include "theory/quantifiers/bv_inverter.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Bitvector instantiator
+ *
+ * This implements an approach for counterexample-guided instantiation
+ * for bit-vector variables based on word-level inversions. For details,
+ * see Niemetz et al, "Solving Quantified Bit-Vectors Using Invertibility
+ * Conditions", CAV 2018. It is enabled by --cbqi-bv.
+ *
+ * This class contains all necessary information for instantiating a single
+ * bit-vector variable of a single quantified formula.
+ */
+class BvInstantiator : public Instantiator
+{
+ public:
+  BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
+  ~BvInstantiator() override;
+  /** reset */
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  /** this instantiator processes assertions */
+  bool hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override;
+  /** this instantiator processes bit-vector equalities and inequalities
+   *
+   * Based on the configuration --cbqi-bv-ineq, it may modify the form of lit
+   * based on a projection. For lit (not) s <> t, this may be one of:
+   * - eq-slack: s = t + ( s^M - t^M )
+   * - eq-boundary: s = t + ( s^M > t^M ? 1 : -1 )
+   * - keep: (not) s <> t, i.e. unchanged.
+   * Additionally for eq-boundary, inequalities s != t become s < t or t < s.
+   * This is the method project_* from Figure 3 of Niemetz et al, CAV 2018.
+   */
+  Node hasProcessAssertion(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           Node lit,
+                           CegInstEffort effort) override;
+  /** process assertion
+   *
+   * Computes a solved form for pv in lit based on Figure 1 of Niemetz et al,
+   * CAV 2018.
+   */
+  bool processAssertion(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        Node lit,
+                        Node alit,
+                        CegInstEffort effort) override;
+  /** process assertions
+   *
+   * This is called after processAssertion has been called on all currently
+   * asserted literals that involve pv. This chooses the best solved form for pv
+   * based on heuristics. Currently, by default, we choose a random solved form.
+   * We may try multiple or zero bounds based on the options
+   * --cbqi-multi-inst and --cbqi-bv-interleave-value.
+   */
+  bool processAssertions(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         CegInstEffort effort) override;
+  /** use model value
+   *
+   * We allow model values if we have not already tried an assertion,
+   * and only at levels below full if cbqiFullEffort is false.
+   */
+  bool useModelValue(CegInstantiator* ci,
+                     SolvedForm& sf,
+                     Node pv,
+                     CegInstEffort effort) override;
+  /** identify */
+  std::string identify() const override { return "Bv"; }
+
+ private:
+  /** pointer to the bv inverter class */
+  BvInverter* d_inverter;
+  //--------------------------------solved forms
+  /** identifier counter, used to allocate ids to each solve form */
+  unsigned d_inst_id_counter;
+  /** map from variables to list of solved form ids */
+  std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>
+      d_var_to_inst_id;
+  /** for each solved form id, the term for instantiation */
+  std::unordered_map<unsigned, Node> d_inst_id_to_term;
+  /** for each solved form id, the corresponding asserted literal */
+  std::unordered_map<unsigned, Node> d_inst_id_to_alit;
+  /** map from variable to current id we are processing */
+  std::unordered_map<Node, unsigned, NodeHashFunction> d_var_to_curr_inst_id;
+  /** the amount of slack we added for asserted literals */
+  std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
+  //--------------------------------end solved forms
+  /** whether we have tried an instantiation based on assertion in this round */
+  bool d_tried_assertion_inst;
+  /** rewrite assertion for solve pv
+   *
+   * Returns a literal that is equivalent to lit that leads to best solved form
+   * for pv.
+   */
+  Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit);
+  /** rewrite term for solve pv
+   *
+   * This is a helper function for rewriteAssertionForSolvePv.
+   * If this returns non-null value ret, then this indicates
+   * that n should be rewritten to ret. It is called as
+   * a "post-rewrite", that is, after the children of n
+   * have been rewritten and stored in the vector children.
+   *
+   * contains_pv stores whether certain nodes contain pv.
+   * where we guarantee that all subterms of terms in children
+   * appear in the domain of contains_pv.
+   */
+  Node rewriteTermForSolvePv(
+      Node pv,
+      Node n,
+      std::vector<Node>& children,
+      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+  /** process literal, called from processAssertion
+   *
+   * lit is the literal to solve for pv that has been rewritten according to
+   * internal rules here.
+   * alit is the asserted literal that lit is derived from.
+   */
+  void processLiteral(CegInstantiator* ci,
+                      SolvedForm& sf,
+                      Node pv,
+                      Node lit,
+                      Node alit,
+                      CegInstEffort effort);
+};
+
+/** Bitvector instantiator preprocess
+ *
+ * This class implements preprocess techniques that are helpful for
+ * counterexample-guided instantiation, such as introducing variables
+ * that refer to disjoint bit-vector extracts.
+ */
+class BvInstantiatorPreprocess : public InstantiatorPreprocess
+{
+ public:
+  BvInstantiatorPreprocess() {}
+  ~BvInstantiatorPreprocess() override {}
+  /** register counterexample lemma
+   *
+   * This method modifies the contents of lems based on the extract terms
+   * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
+   * a dummy equality so that segments of terms t under extracts can be solved
+   * independently.
+   *
+   * For example:
+   *   P[ ((extract 7 4) t), ((extract 3 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x74, x30 )
+   * where x74 and x30 are fresh variables of type BV_4.
+   *
+   * Another example:
+   *   P[ ((extract 7 3) t), ((extract 4 0) t)]
+   *     becomes:
+   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *   t = concat( x75, x44, x30 )
+   * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
+   * respectively.
+   *
+   * Notice we leave the original conjecture alone. This is done for performance
+   * since the added equalities ensure we are able to construct the proper
+   * solved forms for variables in t and for the intermediate variables above.
+   */
+  void registerCounterexampleLemma(std::vector<Node>& lems,
+                                   std::vector<Node>& ce_vars) override;
+
+ private:
+  /** collect extracts
+   *
+   * This method collects all extract terms in lem
+   * and stores them in d_extract_map.
+   * visited is the terms we've already visited.
+   */
+  void collectExtracts(Node lem,
+                       std::map<Node, std::vector<Node> >& extract_map,
+                       std::unordered_set<TNode, TNodeHashFunction>& visited);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
new file mode 100644
index 000000000..54dc78442
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -0,0 +1,175 @@
+/*********************                                                        */
+/*! \file ceg_dt_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of ceg_dt_instantiator
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void DtInstantiator::reset(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort)
+{
+}
+
+bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       std::vector<Node>& eqc,
+                                       CegInstEffort effort)
+{
+  Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
+                          << std::endl;
+  // look in equivalence class for a constructor
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned k = 0, size = eqc.size(); k < size; k++)
+  {
+    Node n = eqc[k];
+    if (n.getKind() == APPLY_CONSTRUCTOR)
+    {
+      Trace("cegqi-dt-debug")
+          << "...try based on constructor term " << n << std::endl;
+      std::vector<Node> children;
+      children.push_back(n.getOperator());
+      const Datatype& dt =
+          static_cast<DatatypeType>(d_type.toType()).getDatatype();
+      unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+      // now must solve for selectors applied to pv
+      for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
+      {
+        Node c = nm->mkNode(
+            APPLY_SELECTOR_TOTAL,
+            Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)),
+            pv);
+        ci->pushStackVariable(c);
+        children.push_back(c);
+      }
+      Node val = nm->mkNode(kind::APPLY_CONSTRUCTOR, children);
+      TermProperties pv_prop_dt;
+      if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
+      {
+        return true;
+      }
+      // cleanup
+      for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
+      {
+        ci->popStackVariable();
+      }
+      break;
+    }
+  }
+  return false;
+}
+
+bool DtInstantiator::hasProcessEquality(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        CegInstEffort effort)
+{
+  return true;
+}
+
+bool DtInstantiator::processEquality(CegInstantiator* ci,
+                                     SolvedForm& sf,
+                                     Node pv,
+                                     std::vector<TermProperties>& term_props,
+                                     std::vector<Node>& terms,
+                                     CegInstEffort effort)
+{
+  Node val = solve_dt(pv, terms[0], terms[1], terms[0], terms[1]);
+  if (!val.isNull())
+  {
+    TermProperties pv_prop;
+    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
+{
+  Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b
+                              << " " << sa << " " << sb << std::endl;
+  Node ret;
+  if (!a.isNull() && a == v)
+  {
+    ret = sb;
+  }
+  else if (!b.isNull() && b == v)
+  {
+    ret = sa;
+  }
+  else if (!a.isNull() && a.getKind() == APPLY_CONSTRUCTOR)
+  {
+    if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
+    {
+      if (a.getOperator() == b.getOperator())
+      {
+        for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
+        {
+          Node s = solve_dt(v, a[i], b[i], sa[i], sb[i]);
+          if (!s.isNull())
+          {
+            return s;
+          }
+        }
+      }
+    }
+    else
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      unsigned cindex = Datatype::indexOf(a.getOperator().toExpr());
+      TypeNode tn = a.getType();
+      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
+      {
+        Node nn = nm->mkNode(
+            APPLY_SELECTOR_TOTAL,
+            Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
+            sb);
+        Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
+        if (!s.isNull())
+        {
+          return s;
+        }
+      }
+    }
+  }
+  else if (!b.isNull() && b.getKind() == APPLY_CONSTRUCTOR)
+  {
+    // flip sides
+    return solve_dt(v, b, a, sb, sa);
+  }
+  if (!ret.isNull())
+  {
+    // ensure does not contain v
+    if (ret.hasSubterm(v))
+    {
+      ret = Node::null();
+    }
+  }
+  return ret;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
new file mode 100644
index 000000000..37a81b625
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file ceg_dt_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ceg_dt_instantiator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Datatypes Instantiator
+ *
+ * This class implements a selection function for datatypes based on solving
+ * for occurrences of variables in subfields of datatypes.
+ */
+class DtInstantiator : public Instantiator
+{
+ public:
+  DtInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+  virtual ~DtInstantiator() {}
+  /** reset */
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  /** process equal terms
+   *
+   * This tries to find an equality eqc[i] = eqc[j] such that pv can be solved
+   * for (via solve_dt). If a solved form for pv can be found in this way, we
+   * add the substitution for pv to sf and recurse.
+   */
+  bool processEqualTerms(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         std::vector<Node>& eqc,
+                         CegInstEffort effort) override;
+  /** this instantiator processes equalities */
+  bool hasProcessEquality(CegInstantiator* ci,
+                          SolvedForm& sf,
+                          Node pv,
+                          CegInstEffort effort) override;
+  /** process equality
+   *
+   * This tries to find a solved form for pv based on the equality
+   * terms[0] = terms[1] via solve_dt. If a solved form for pv can be found in
+   * this way, we add the substitution for pv to sf and recurse.
+   */
+  bool processEquality(CegInstantiator* ci,
+                       SolvedForm& sf,
+                       Node pv,
+                       std::vector<TermProperties>& term_props,
+                       std::vector<Node>& terms,
+                       CegInstEffort effort) override;
+  /** identify */
+  std::string identify() const override { return "Dt"; }
+
+ private:
+  /** solve datatype
+   *
+   * If this method returns a non-null node ret, then v -> ret is a
+   * solution for v in the equality a = b and ret does not contain v.
+   *
+   * For example, if cons( v, nil ) = cons( 5, nil ), this method returns 5.
+   * For example, if cons( v, nil ) = L, this method returns head( L ).
+   * For example, if cons( v, nil ) = cons( v+1, nil ), this method returns
+   * the null node.
+   */
+  Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
new file mode 100644
index 000000000..7acdab00f
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/*! \file ceg_epr_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of ceg_epr_instantiator
+ **/
+
+#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void EprInstantiator::reset(CegInstantiator* ci,
+                            SolvedForm& sf,
+                            Node pv,
+                            CegInstEffort effort)
+{
+  d_equal_terms.clear();
+}
+
+bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
+                                       SolvedForm& sf,
+                                       Node pv,
+                                       TermProperties& pv_prop,
+                                       Node n,
+                                       CegInstEffort effort)
+{
+  if (options::quantEprMatching())
+  {
+    Assert(pv_prop.isBasic());
+    d_equal_terms.push_back(n);
+    return false;
+  }
+  pv_prop.d_type = 0;
+  return ci->constructInstantiationInc(pv, n, pv_prop, sf);
+}
+
+struct sortEqTermsMatch
+{
+  std::map<Node, int> d_match_score;
+  bool operator()(Node i, Node j)
+  {
+    int match_score_i = d_match_score[i];
+    int match_score_j = d_match_score[j];
+    return match_score_i > match_score_j
+           || (match_score_i == match_score_j && i < j);
+  }
+};
+
+bool EprInstantiator::processEqualTerms(CegInstantiator* ci,
+                                        SolvedForm& sf,
+                                        Node pv,
+                                        std::vector<Node>& eqc,
+                                        CegInstEffort effort)
+{
+  if (!options::quantEprMatching())
+  {
+    return false;
+  }
+  // heuristic for best matching constant
+  sortEqTermsMatch setm;
+  for (unsigned i = 0; i < ci->getNumCEAtoms(); i++)
+  {
+    Node catom = ci->getCEAtom(i);
+    computeMatchScore(ci, pv, catom, catom, setm.d_match_score);
+  }
+  // sort by match score
+  std::sort(d_equal_terms.begin(), d_equal_terms.end(), setm);
+  TermProperties pv_prop;
+  pv_prop.d_type = 0;
+  for (unsigned i = 0, size = d_equal_terms.size(); i < size; i++)
+  {
+    if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf))
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+void EprInstantiator::computeMatchScore(CegInstantiator* ci,
+                                        Node pv,
+                                        Node catom,
+                                        std::vector<Node>& arg_reps,
+                                        TermArgTrie* tat,
+                                        unsigned index,
+                                        std::map<Node, int>& match_score)
+{
+  if (index == catom.getNumChildren())
+  {
+    Assert(tat->hasNodeData());
+    Node gcatom = tat->getNodeData();
+    Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom
+                       << std::endl;
+    for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++)
+    {
+      if (catom[i] == pv)
+      {
+        Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl;
+        match_score[gcatom[i]]++;
+      }
+      else
+      {
+        // recursive matching
+        computeMatchScore(ci, pv, catom[i], gcatom[i], match_score);
+      }
+    }
+    return;
+  }
+  std::map<TNode, TermArgTrie>::iterator it = tat->d_data.find(arg_reps[index]);
+  if (it != tat->d_data.end())
+  {
+    computeMatchScore(
+        ci, pv, catom, arg_reps, &it->second, index + 1, match_score);
+  }
+}
+
+void EprInstantiator::computeMatchScore(CegInstantiator* ci,
+                                        Node pv,
+                                        Node catom,
+                                        Node eqc,
+                                        std::map<Node, int>& match_score)
+{
+  if (!inst::Trigger::isAtomicTrigger(catom) || !catom.hasSubterm(pv))
+  {
+    return;
+  }
+  Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl;
+  eq::EqualityEngine* ee =
+      ci->getQuantifiersEngine()->getMasterEqualityEngine();
+  std::vector<Node> arg_reps;
+  for (unsigned j = 0, nchild = catom.getNumChildren(); j < nchild; j++)
+  {
+    arg_reps.push_back(ee->getRepresentative(catom[j]));
+  }
+  if (!ee->hasTerm(eqc))
+  {
+    return;
+  }
+  TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase();
+  Node rep = ee->getRepresentative(eqc);
+  Node op = tdb->getMatchOperator(catom);
+  TermArgTrie* tat = tdb->getTermArgTrie(rep, op);
+  Trace("cegqi-epr") << "EPR instantiation match term : " << catom
+                     << ", check ground terms=" << (tat != NULL) << std::endl;
+  if (tat)
+  {
+    computeMatchScore(ci, pv, catom, arg_reps, tat, 0, match_score);
+  }
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
new file mode 100644
index 000000000..cfc937bbd
--- /dev/null
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file ceg_epr_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ceg_epr_instantiator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H
+
+#include <map>
+#include <vector>
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermArgTrie;
+
+/** Effectively Propositional (EPR) Instantiator
+ *
+ * This implements a selection function for the EPR fragment.
+ */
+class EprInstantiator : public Instantiator
+{
+ public:
+  EprInstantiator(QuantifiersEngine* qe, TypeNode tn) : Instantiator(qe, tn) {}
+  virtual ~EprInstantiator() {}
+  /** reset */
+  void reset(CegInstantiator* ci,
+             SolvedForm& sf,
+             Node pv,
+             CegInstEffort effort) override;
+  /** process equal terms
+   *
+   * This adds n to the set of equal terms d_equal_terms if matching heuristics
+   * are enabled (--quant-epr-match), or simply tries the substitution pv -> n
+   * otherwise.
+   */
+  bool processEqualTerm(CegInstantiator* ci,
+                        SolvedForm& sf,
+                        Node pv,
+                        TermProperties& pv_prop,
+                        Node n,
+                        CegInstEffort effort) override;
+  /** process equal terms
+   *
+   * Called when pv is equal to the set eqc. If matching heuristics are enabled,
+   * this adds the substitution pv -> n based on the best term n in eqc.
+   */
+  bool processEqualTerms(CegInstantiator* ci,
+                         SolvedForm& sf,
+                         Node pv,
+                         std::vector<Node>& eqc,
+                         CegInstEffort effort) override;
+  /** identify */
+  std::string identify() const override { return "Epr"; }
+
+ private:
+  /**
+   * The current set of terms that are equal to the variable-to-instantate of
+   * this class.
+   */
+  std::vector<Node> d_equal_terms;
+  /** compute match score
+   *
+   * This method computes the map match_score, from ground term t to the
+   * number of times that occur in simple matches for a quantified formula.
+   * For example, for quantified formula forall xy. P( x ) V Q( x, y ) and
+   * ground terms { P( a ), Q( a, a ), Q( b, c ), Q( a, c ) }, we compute for x:
+   *   match_score[a] = 3,
+   *   match_score[b] = 1,
+   *   match_score[c] = 0.
+   * The higher the match score for a term, the more likely this class is to use
+   * t in instantiations.
+   */
+  void computeMatchScore(CegInstantiator* ci,
+                         Node pv,
+                         Node catom,
+                         std::vector<Node>& arg_reps,
+                         TermArgTrie* tat,
+                         unsigned index,
+                         std::map<Node, int>& match_score);
+  void computeMatchScore(CegInstantiator* ci,
+                         Node pv,
+                         Node catom,
+                         Node eqc,
+                         std::map<Node, int>& match_score);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 102a6327b..af003ce39 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -13,7 +13,11 @@
  **/
 
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
-#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+
+#include "theory/quantifiers/cegqi/ceg_arith_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
+#include "theory/quantifiers/cegqi/ceg_epr_instantiator.h"
 
 #include "options/quantifiers_options.h"
 #include "smt/term_formula_removal.h"
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
deleted file mode 100644
index a54382130..000000000
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ /dev/null
@@ -1,2006 +0,0 @@
-/*********************                                                        */
-/*! \file ceg_t_instantiator.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation
- **/
-
-#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
-
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/ematching/trigger.h"
-
-#include "theory/arith/arith_msum.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/bitvector.h"
-#include "util/random.h"
-
-#include <algorithm>
-#include <stack>
-
-using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-struct BvLinearAttributeId {};
-using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>;
-
-Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
-  Node val = t;
-  Trace("cegqi-arith-bound2") << "Value : " << val << std::endl;
-  Assert( !e.getType().isInteger() || t.getType().isInteger() );
-  Assert( !e.getType().isInteger() || mt.getType().isInteger() );
-  //add rho value
-  //get the value of c*e
-  Node ceValue = me;
-  Node new_theta = theta;
-  if( !c.isNull() ){
-    Assert( c.getType().isInteger() );
-    ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c );
-    ceValue = Rewriter::rewrite( ceValue );
-    if( new_theta.isNull() ){
-      new_theta = c;
-    }else{
-      new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c );
-      new_theta = Rewriter::rewrite( new_theta );
-    }
-    Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl;
-    Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl;
-  }
-  if( !new_theta.isNull() && e.getType().isInteger() ){
-    Node rho;
-    //if( !mt.getType().isInteger() ){
-      //round up/down
-      //mt = NodeManager::currentNM()->mkNode(
-    //}
-    if( isLower ){
-      rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
-    }else{
-      rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue );
-    }
-    rho = Rewriter::rewrite( rho );
-    Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
-    Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = ";
-    rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta );
-    rho = Rewriter::rewrite( rho );
-    Trace("cegqi-arith-bound2") << rho << std::endl;
-    Kind rk = isLower ? PLUS : MINUS;
-    val = NodeManager::currentNM()->mkNode( rk, val, rho );
-    val = Rewriter::rewrite( val );
-    Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl;
-  }
-  if( !inf_coeff.isNull() ){
-    Assert( !d_vts_sym[0].isNull() );
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
-    val = Rewriter::rewrite( val );
-  }
-  if( !delta_coeff.isNull() ){
-    //create delta here if necessary
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) );
-    val = Rewriter::rewrite( val );
-  }
-  return val;
-}
-
-//this isolates the atom into solved form
-//     veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
-//  ensures val is Int if pv is Int, and val does not contain vts symbols
-int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
-  int ires = 0;
-  Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl;
-  std::map< Node, Node > msum;
-  if (ArithMSum::getMonomialSumLit(atom, msum))
-  {
-    Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl;
-    if( Trace.isOn("cegqi-arith-debug") ){
-      ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug");
-    }
-    TypeNode pvtn = pv.getType();
-    //remove vts symbols from polynomial
-    Node vts_coeff[2];
-    for( unsigned t=0; t<2; t++ ){
-      if( !d_vts_sym[t].isNull() ){
-        std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] );
-        if( itminf!=msum.end() ){
-          vts_coeff[t] = itminf->second;
-          if( vts_coeff[t].isNull() ){
-            vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-          }
-          //negate if coefficient on variable is positive
-          std::map< Node, Node >::iterator itv = msum.find( pv );
-          if( itv!=msum.end() ){
-            //multiply by the coefficient we will isolate for
-            if( itv->second.isNull() ){
-              vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
-            }else{
-              if( !pvtn.isInteger() ){
-                vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
-                vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
-              }else if( itv->second.getConst<Rational>().sgn()==1 ){
-                vts_coeff[t] = ArithMSum::negate(vts_coeff[t]);
-              }
-            }
-          }
-          Trace("cegqi-arith-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
-          msum.erase( d_vts_sym[t] );
-        }
-      }
-    }
-
-    ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
-    if( ires!=0 ){
-      Node realPart;
-      if( Trace.isOn("cegqi-arith-debug") ){
-        Trace("cegqi-arith-debug") << "Isolate : ";
-        if( !veq_c.isNull() ){
-          Trace("cegqi-arith-debug") << veq_c << " * ";
-        }
-        Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
-      }
-      // when not pure LIA/LRA, we must check whether the lhs contains pv
-      if (val.hasSubterm(pv))
-      {
-        Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
-        return 0;
-      }
-      if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
-        //redo, split integer/non-integer parts
-        bool useCoeff = false;
-        Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst<Rational>().getNumerator();
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          if( it->first.isNull() || it->first.getType().isInteger() ){
-            if( !it->second.isNull() ){
-              coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
-              useCoeff = true;
-            }
-          }
-        }
-        //multiply everything by this coefficient
-        Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
-        std::vector< Node > real_part;
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          if( useCoeff ){
-            if( it->second.isNull() ){
-              msum[it->first] = rcoeff;
-            }else{
-              msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
-            }
-          }
-          if( !it->first.isNull() && !it->first.getType().isInteger() ){
-            real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
-          }
-        }
-        //remove delta  TODO: check this
-        vts_coeff[1] = Node::null();
-        //multiply inf
-        if( !vts_coeff[0].isNull() ){
-          vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
-        }
-        realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
-        Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
-        //re-isolate
-        Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl;
-        veq_c = Node::null();
-        ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind());
-        Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
-        Trace("cegqi-arith-debug") << "                 real part : " << realPart << std::endl;
-        if( ires!=0 ){
-          int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
-          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
-                                    NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
-                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );  //TODO: round up for upper bounds?
-          Trace("cegqi-arith-debug") << "result : " << val << std::endl;
-          Assert( val.getType().isInteger() );
-        }
-      }
-    }
-    vts_coeff_inf = vts_coeff[0];
-    vts_coeff_delta = vts_coeff[1];
-    Trace("cegqi-arith-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl;
-  }else{
-    Trace("cegqi-arith-debug") << "fail : could not get monomial sum" << std::endl;
-  }
-  return ires;
-}
-
-void ArithInstantiator::reset(CegInstantiator* ci,
-                              SolvedForm& sf,
-                              Node pv,
-                              CegInstEffort effort)
-{
-  d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false );
-  d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false );
-  for( unsigned i=0; i<2; i++ ){
-    d_mbp_bounds[i].clear();
-    d_mbp_coeff[i].clear();
-    for( unsigned j=0; j<2; j++ ){
-      d_mbp_vts_coeff[i][j].clear();
-    }
-    d_mbp_lit[i].clear();
-  }
-}
-
-bool ArithInstantiator::processEquality(CegInstantiator* ci,
-                                        SolvedForm& sf,
-                                        Node pv,
-                                        std::vector<TermProperties>& term_props,
-                                        std::vector<Node>& terms,
-                                        CegInstEffort effort)
-{
-  Node eq_lhs = terms[0];
-  Node eq_rhs = terms[1];
-  Node lhs_coeff = term_props[0].d_coeff;
-  Node rhs_coeff = term_props[1].d_coeff;
-  //make the same coefficient
-  if( rhs_coeff!=lhs_coeff ){
-    if( !rhs_coeff.isNull() ){
-      Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl;
-      eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs );
-      eq_lhs = Rewriter::rewrite( eq_lhs );
-    }
-    if( !lhs_coeff.isNull() ){
-      Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl;
-      eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs );
-      eq_rhs = Rewriter::rewrite( eq_rhs );
-    }
-  }
-  Node eq = eq_lhs.eqNode( eq_rhs );
-  eq = Rewriter::rewrite( eq );
-  Node val;
-  TermProperties pv_prop;
-  Node vts_coeff_inf;
-  Node vts_coeff_delta;
-  //isolate pv in the equality
-  int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
-  if( ires!=0 ){
-    pv_prop.d_type = 0;
-    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
-    {
-      return true;
-    }
-  }
-
-  return false;
-}
-
-Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci,
-                                            SolvedForm& sf,
-                                            Node pv,
-                                            Node lit,
-                                            CegInstEffort effort)
-{
-  Node atom = lit.getKind()==NOT ? lit[0] : lit;
-  bool pol = lit.getKind()!=NOT;
-  //arithmetic inequalities and disequalities
-  if (atom.getKind() == GEQ ||
-      (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) {
-    return lit;
-  } else {
-    return Node::null();
-  }
-}
-
-bool ArithInstantiator::processAssertion(CegInstantiator* ci,
-                                         SolvedForm& sf,
-                                         Node pv,
-                                         Node lit,
-                                         Node alit,
-                                         CegInstEffort effort)
-{
-  Node atom = lit.getKind()==NOT ? lit[0] : lit;
-  bool pol = lit.getKind()!=NOT;
-  //arithmetic inequalities and disequalities
-  Assert( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) );
-  // get model value for pv
-  Node pv_value = ci->getModelValue( pv );
-  //cannot contain infinity?
-  Node vts_coeff_inf;
-  Node vts_coeff_delta;
-  Node val;
-  TermProperties pv_prop;
-  //isolate pv in the inequality
-  int ires = solve_arith( ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
-  if( ires!=0 ){
-    //disequalities are either strict upper or lower bounds
-    unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2;
-    for( unsigned r=0; r<rmax; r++ ){
-      int uires = ires;
-      Node uval = val;
-      if( atom.getKind()==GEQ ){
-        //push negation downwards
-        if( !pol ){
-          uires = -ires;
-          if( d_type.isInteger() ){
-            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
-            uval = Rewriter::rewrite( uval );
-          }else{
-            Assert( d_type.isReal() );
-            //now is strict inequality
-            uires = uires*2;
-          }
-        }
-      }else{
-        bool is_upper;
-        if( options::cbqiModel() ){
-          // disequality is a disjunction : only consider the bound in the direction of the model
-          //first check if there is an infinity...
-          if( !vts_coeff_inf.isNull() ){
-            //coefficient or val won't make a difference, just compare with zero
-            Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
-            Assert( vts_coeff_inf.isConst() );
-            is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 );
-          }else{
-            Node rhs_value = ci->getModelValue( val );
-            Node lhs_value = pv_prop.getModifiedTerm( pv_value );
-            if( !pv_prop.isBasic() ){
-              lhs_value = pv_prop.getModifiedTerm( pv_value );
-              lhs_value = Rewriter::rewrite( lhs_value );
-            }
-            Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
-            // it generally should be the case that lhs_value!=rhs_value
-            // however, this assertion is violated e.g. if non-linear is enabled
-            // since the quantifier-free arithmetic solver may pass full
-            // effort with no lemmas even when we are not guaranteed to have a
-            // model. By convention, we use GEQ to compare the values here.
-            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
-            cmp = Rewriter::rewrite( cmp );
-            Assert( cmp.isConst() );
-            is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true );
-          }
-        }else{
-          is_upper = (r==0);
-        }
-        Assert( atom.getKind()==EQUAL && !pol );
-        if( d_type.isInteger() ){
-          uires = is_upper ? -1 : 1;
-          uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
-          uval = Rewriter::rewrite( uval );
-        }else{
-          Assert( d_type.isReal() );
-          uires = is_upper ? -2 : 2;
-        }
-      }
-      if( Trace.isOn("cegqi-arith-bound-inf") ){
-        Node pvmod = pv_prop.getModifiedTerm( pv );
-        Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : ";
-        Trace("cegqi-arith-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl;
-      }
-      //take into account delta
-      if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){
-        if( options::cbqiModel() ){
-          Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
-          if( vts_coeff_delta.isNull() ){
-            vts_coeff_delta = delta_coeff;
-          }else{
-            vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
-            vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
-          }
-        }else{
-          Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta();
-          uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
-          uval = Rewriter::rewrite( uval );
-        }
-      }
-      if( options::cbqiModel() ){
-        //just store bounds, will choose based on tighest bound
-        unsigned index = uires>0 ? 0 : 1;
-        d_mbp_bounds[index].push_back( uval );
-        d_mbp_coeff[index].push_back( pv_prop.d_coeff );
-        Trace("cegqi-arith-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
-        for( unsigned t=0; t<2; t++ ){
-          d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
-        }
-        d_mbp_lit[index].push_back( lit );
-      }else{
-        //try this bound
-        pv_prop.d_type = uires>0 ? 1 : -1;
-        if (ci->constructInstantiationInc(pv, uval, pv_prop, sf))
-        {
-          return true;
-        }
-      }
-    }
-  }
-
-
-  return false;
-}
-
-bool ArithInstantiator::processAssertions(CegInstantiator* ci,
-                                          SolvedForm& sf,
-                                          Node pv,
-                                          CegInstEffort effort)
-{
-  if (options::cbqiModel()) {
-    bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
-    bool upper_first = false;
-    if( options::cbqiMinBounds() ){
-      upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size();
-    }
-    int best_used[2];
-    std::vector< Node > t_values[3];
-    Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero;
-    Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one;
-    Node pv_value = ci->getModelValue( pv );
-    //try optimal bounds
-    for( unsigned r=0; r<2; r++ ){
-      int rr = upper_first ? (1-r) : r;
-      best_used[rr] = -1;
-      if( d_mbp_bounds[rr].empty() ){
-        if( use_inf ){
-          Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl;
-          //no bounds, we do +- infinity
-          Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type );
-          //TODO : rho value for infinity?
-          if( rr==0 ){
-            val = NodeManager::currentNM()->mkNode( UMINUS, val );
-            val = Rewriter::rewrite( val );
-          }
-          TermProperties pv_prop_no_bound;
-          if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf))
-          {
-            return true;
-          }
-        }
-      }else{
-        Trace("cegqi-arith-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl;
-        int best = -1;
-        Node best_bound_value[3];
-        for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
-          Node value[3];
-          if( Trace.isOn("cegqi-arith-bound") ){
-            Assert( !d_mbp_bounds[rr][j].isNull() );
-            Trace("cegqi-arith-bound") << "  " << j << ": " << d_mbp_bounds[rr][j];
-            if( !d_mbp_vts_coeff[rr][0][j].isNull() ){
-              Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)";
-            }
-            if( !d_mbp_vts_coeff[rr][1][j].isNull() ){
-              Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)";
-            }
-            if( !d_mbp_coeff[rr][j].isNull() ){
-              Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")";
-            }
-            Trace("cegqi-arith-bound") << ", value = ";
-          }
-          t_values[rr].push_back( Node::null() );
-          //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts
-          bool new_best = true;
-          for( unsigned t=0; t<3; t++ ){
-            //get the value
-            if( t==0 ){
-              value[0] = d_mbp_vts_coeff[rr][0][j];
-              if( !value[0].isNull() ){
-                Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + ";
-              }else{
-                value[0] = zero;
-              }
-            }else if( t==1 ){
-              Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] );
-              t_values[rr][j] = t_value;
-              value[1] = t_value;
-              Trace("cegqi-arith-bound") << value[1];
-            }else{
-              value[2] = d_mbp_vts_coeff[rr][1][j];
-              if( !value[2].isNull() ){
-                Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )";
-              }else{
-                value[2] = zero;
-              }
-            }
-            //multiply by coefficient
-            if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){
-              Assert( d_mbp_coeff[rr][j].isConst() );
-              value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>() ), value[t] );
-              value[t] = Rewriter::rewrite( value[t] );
-            }
-            //check if new best
-            if( best!=-1 ){
-              Assert( !value[t].isNull() && !best_bound_value[t].isNull() );
-              if( value[t]!=best_bound_value[t] ){
-                Kind k = rr==0 ? GEQ : LEQ;
-                Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] );
-                cmp_bound = Rewriter::rewrite( cmp_bound );
-                if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){
-                  new_best = false;
-                  break;
-                }
-              }
-            }
-          }
-          Trace("cegqi-arith-bound") << std::endl;
-          if( new_best ){
-            for( unsigned t=0; t<3; t++ ){
-              best_bound_value[t] = value[t];
-            }
-            best = j;
-          }
-        }
-        if( best!=-1 ){
-          Trace("cegqi-arith-bound") << "...best bound is " << best << " : ";
-          if( best_bound_value[0]!=zero ){
-            Trace("cegqi-arith-bound") << "( " << best_bound_value[0] << " * INF ) + ";
-          }
-          Trace("cegqi-arith-bound") << best_bound_value[1];
-          if( best_bound_value[2]!=zero ){
-            Trace("cegqi-arith-bound") << " + ( " << best_bound_value[2] << " * DELTA )";
-          }
-          Trace("cegqi-arith-bound") << std::endl;
-          best_used[rr] = best;
-          //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()))
-          {
-            Node val = d_mbp_bounds[rr][best];
-            val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(),
-                                                d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
-            if( !val.isNull() ){
-              TermProperties pv_prop_bound;
-              pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
-              pv_prop_bound.d_type = rr==0 ? 1 : -1;
-              if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf))
-              {
-                return true;
-              }
-            }
-          }
-        }
-      }
-    }
-    //if not using infinity, use model value of zero
-    if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
-      Node val = zero;
-      TermProperties pv_prop_zero;
-      Node theta = sf.getTheta();
-      val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() );
-      if( !val.isNull() ){
-        if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf))
-        {
-          return true;
-        }
-      }
-    }
-    if( options::cbqiMidpoint() && !d_type.isInteger() ){
-      Node vals[2];
-      bool bothBounds = true;
-      Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl;
-      for( unsigned rr=0; rr<2; rr++ ){
-        int best = best_used[rr];
-        if( best==-1 ){
-          bothBounds = false;
-        }else{
-          vals[rr] = d_mbp_bounds[rr][best];
-          vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(),
-                                                   d_mbp_vts_coeff[rr][0][best], Node::null() );
-        }
-        Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl;
-      }
-      Node val;
-      if( bothBounds ){
-        Assert( !vals[0].isNull() && !vals[1].isNull() );
-        if( vals[0]==vals[1] ){
-          val = vals[0];
-        }else{
-          val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ),
-                                                        NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) );
-          val = Rewriter::rewrite( val );
-        }
-      }else{
-        if( !vals[0].isNull() ){
-          val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one );
-          val = Rewriter::rewrite( val );
-        }else if( !vals[1].isNull() ){
-          val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one );
-          val = Rewriter::rewrite( val );
-        }
-      }
-      Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl;
-      if( !val.isNull() ){
-        TermProperties pv_prop_midpoint;
-        if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf))
-        {
-          return true;
-        }
-      }
-    }
-    //generally should not make it to this point FIXME: write proper assertion
-    //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() );
-
-    if( options::cbqiNopt() ){
-      //try non-optimal bounds (heuristic, may help when nested quantification) ?
-      Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl;
-      for( unsigned r=0; r<2; r++ ){
-        int rr = upper_first ? (1-r) : r;
-        for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
-          if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){
-            Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.getTheta(),
-                                                     d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
-            if( !val.isNull() ){
-              TermProperties pv_prop_nopt_bound;
-              pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
-              pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1;
-              if (ci->constructInstantiationInc(
-                      pv, val, pv_prop_nopt_bound, sf))
-              {
-                return true;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-bool ArithInstantiator::needsPostProcessInstantiationForVariable(
-    CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort)
-{
-  return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
-}
-
-bool ArithInstantiator::postProcessInstantiationForVariable(
-    CegInstantiator* ci,
-    SolvedForm& sf,
-    Node pv,
-    CegInstEffort effort,
-    std::vector<Node>& lemmas)
-{
-  Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() );
-  Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() );
-  unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin();
-  Assert( !sf.d_props[index].isBasic() );
-  Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] );
-  if( Trace.isOn("cegqi-arith-debug") ){
-    Trace("cegqi-arith-debug") << "Normalize substitution for ";
-    Trace("cegqi-arith-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl;
-  }
-  Assert( sf.d_vars[index].getType().isInteger() );
-  //must ensure that divisibility constraints are met
-  //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
-  Node eq_rhs = sf.d_subs[index];
-  Node eq = eq_lhs.eqNode( eq_rhs );
-  eq = Rewriter::rewrite( eq );
-  Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl;
-  std::map< Node, Node > msum;
-  if (ArithMSum::getMonomialSumLit(eq, msum))
-  {
-    Node veq;
-    if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) != 0)
-    {
-      Node veq_c;
-      if( veq[0]!=sf.d_vars[index] ){
-        Node veq_v;
-        if (ArithMSum::getMonomial(veq[0], veq_c, veq_v))
-        {
-          Assert( veq_v==sf.d_vars[index] );
-        }
-      }
-      sf.d_subs[index] = veq[1];
-      if( !veq_c.isNull() ){
-        sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
-        Trace("cegqi-arith-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl;
-        //intger division rounding up if from a lower bound
-        if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){
-          sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
-            NodeManager::currentNM()->mkNode( ITE,
-              NodeManager::currentNM()->mkNode( EQUAL,
-                NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ),
-                ci->getQuantifiersEngine()->getTermUtil()->d_zero ),
-              ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one )
-          );
-        }
-      }
-      Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl;
-    }else{
-      Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl;
-      return false;
-    }
-  }else{
-    Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl;
-    return false;
-  }
-  return true;
-}
-
-void DtInstantiator::reset(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           CegInstEffort effort)
-{
-}
-
-Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
-  Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl;
-  Node ret;
-  if( !a.isNull() && a==v ){
-    ret = sb;
-  }else if( !b.isNull() && b==v ){
-    ret = sa;
-  }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){
-    if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
-      if( a.getOperator()==b.getOperator() ){
-        for( unsigned i=0; i<a.getNumChildren(); i++ ){
-          Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] );
-          if( !s.isNull() ){
-            return s;
-          }
-        }
-      }
-    }else{
-      unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() );
-      TypeNode tn = a.getType();
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for( unsigned i=0; i<a.getNumChildren(); i++ ){
-        Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), sb );
-        Node s = solve_dt( v, a[i], Node::null(), sa[i], nn );
-        if( !s.isNull() ){
-          return s;
-        }
-      }
-    }
-  }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
-    return solve_dt( v, b, a, sb, sa );
-  }
-  if( !ret.isNull() ){
-    //ensure does not contain
-    if (ret.hasSubterm(v))
-    {
-      ret = Node::null();
-    }
-  }
-  return ret;
-}
-
-bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
-                                       SolvedForm& sf,
-                                       Node pv,
-                                       std::vector<Node>& eqc,
-                                       CegInstEffort effort)
-{
-  Trace("cegqi-dt-debug") << "try based on constructors in equivalence class."
-                          << std::endl;
-  // look in equivalence class for a constructor
-  for( unsigned k=0; k<eqc.size(); k++ ){
-    Node n = eqc[k];
-    if( n.getKind()==APPLY_CONSTRUCTOR ){
-      Trace("cegqi-dt-debug") << "...try based on constructor term " << n << std::endl;
-      std::vector< Node > children;
-      children.push_back( n.getOperator() );
-      const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype();
-      unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
-      //now must solve for selectors applied to pv
-      for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
-        Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( d_type.toType(), j ) ), pv );
-        ci->pushStackVariable( c );
-        children.push_back( c );
-      }
-      Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-      TermProperties pv_prop_dt;
-      if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf))
-      {
-        return true;
-      }else{
-        //cleanup
-        for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
-          ci->popStackVariable();
-        }
-        break;
-      }
-    }
-  }
-  return false;
-}
-
-bool DtInstantiator::processEquality(CegInstantiator* ci,
-                                     SolvedForm& sf,
-                                     Node pv,
-                                     std::vector<TermProperties>& term_props,
-                                     std::vector<Node>& terms,
-                                     CegInstEffort effort)
-{
-  Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
-  if( !val.isNull() ){
-    TermProperties pv_prop;
-    if (ci->constructInstantiationInc(pv, val, pv_prop, sf))
-    {
-      return true;
-    }
-  }
-  return false;
-}
-
-void EprInstantiator::reset(CegInstantiator* ci,
-                            SolvedForm& sf,
-                            Node pv,
-                            CegInstEffort effort)
-{
-  d_equal_terms.clear();
-}
-
-bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
-                                       SolvedForm& sf,
-                                       Node pv,
-                                       TermProperties& pv_prop,
-                                       Node n,
-                                       CegInstEffort effort)
-{
-  if( options::quantEprMatching() ){
-    Assert( pv_prop.isBasic() );
-    d_equal_terms.push_back( n );
-    return false;
-  }else{
-    pv_prop.d_type = 0;
-    return ci->constructInstantiationInc(pv, n, pv_prop, sf);
-  }
-}
-
-void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) {
-  if( index==catom.getNumChildren() ){
-    Assert( tat->hasNodeData() );
-    Node gcatom = tat->getNodeData();
-    Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl;
-    for( unsigned i=0; i<catom.getNumChildren(); i++ ){
-      if( catom[i]==pv ){
-        Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl;
-        match_score[gcatom[i]]++;
-      }else{
-        //recursive matching
-        computeMatchScore( ci, pv, catom[i], gcatom[i], match_score );
-      }
-    }
-  }else{
-    std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] );
-    if( it!=tat->d_data.end() ){
-      computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score );
-    }
-  }
-}
-
-void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) {
-  if (inst::Trigger::isAtomicTrigger(catom) && catom.hasSubterm(pv))
-  {
-    Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl;
-    std::vector< Node > arg_reps;
-    for( unsigned j=0; j<catom.getNumChildren(); j++ ){
-      arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) );
-    }
-    if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){
-      Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc );
-      Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom );
-      TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op );
-      Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl;
-      if( tat ){
-        computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score );
-      }
-    }
-  }
-}
-
-struct sortEqTermsMatch {
-  std::map< Node, int > d_match_score;
-  bool operator() (Node i, Node j) {
-    int match_score_i = d_match_score[i];
-    int match_score_j = d_match_score[j];
-    return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j );
-  }
-};
-
-bool EprInstantiator::processEqualTerms(CegInstantiator* ci,
-                                        SolvedForm& sf,
-                                        Node pv,
-                                        std::vector<Node>& eqc,
-                                        CegInstEffort effort)
-{
-  if( options::quantEprMatching() ){
-    //heuristic for best matching constant
-    sortEqTermsMatch setm;
-    for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){
-      Node catom = ci->getCEAtom( i );
-      computeMatchScore( ci, pv, catom, catom, setm.d_match_score );
-    }
-    //sort by match score
-    std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm );
-    TermProperties pv_prop;
-    pv_prop.d_type = 0;
-    for( unsigned i=0; i<d_equal_terms.size(); i++ ){
-      if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf))
-      {
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-// this class can be used to query the model value through the CegInstaniator class
-class CegInstantiatorBvInverterQuery : public BvInverterQuery
-{
- public:
-  CegInstantiatorBvInverterQuery(CegInstantiator* ci)
-      : BvInverterQuery(), d_ci(ci)
-  {
-  }
-  ~CegInstantiatorBvInverterQuery() {}
-  /** return the model value of n */
-  Node getModelValue(Node n) override { return d_ci->getModelValue(n); }
-  /** get bound variable of type tn */
-  Node getBoundVariable(TypeNode tn) override
-  {
-    return d_ci->getBoundVariable(tn);
-  }
-
- protected:
-  // pointer to class that is able to query model values
-  CegInstantiator * d_ci;
-};
-
-BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn), d_tried_assertion_inst(false)
-{
-  // get the global inverter utility
-  // 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(){
-
-}
-void BvInstantiator::reset(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           CegInstEffort effort)
-{
-  d_inst_id_counter = 0;
-  d_var_to_inst_id.clear();
-  d_inst_id_to_term.clear();
-  d_inst_id_to_alit.clear();
-  d_var_to_curr_inst_id.clear();
-  d_alit_to_model_slack.clear();
-  d_tried_assertion_inst = false;
-}
-
-void BvInstantiator::processLiteral(CegInstantiator* ci,
-                                    SolvedForm& sf,
-                                    Node pv,
-                                    Node lit,
-                                    Node alit,
-                                    CegInstEffort effort)
-{
-  Assert(d_inverter != NULL);
-  // find path to pv
-  std::vector<unsigned> path;
-  Node sv = d_inverter->getSolveVariable(pv.getType());
-  Node pvs = ci->getModelValue(pv);
-  Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
-  Node slit =
-      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl());
-  if (!slit.isNull())
-  {
-    CegInstantiatorBvInverterQuery m(ci);
-    unsigned iid = d_inst_id_counter;
-    Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
-    Node inst = d_inverter->solveBvLit(sv, slit, path, &m);
-    if (!inst.isNull())
-    {
-      inst = Rewriter::rewrite(inst);
-      if (inst.isConst() || !ci->hasNestedQuantification())
-      {
-        Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
-        // store information for id and increment
-        d_var_to_inst_id[pv].push_back(iid);
-        d_inst_id_to_term[iid] = inst;
-        d_inst_id_to_alit[iid] = alit;
-        d_inst_id_counter++;
-      }
-    }
-    else
-    {
-      Trace("cegqi-bv") << "...failed to solve." << std::endl;
-    }
-  }
-  else
-  {
-    Trace("cegqi-bv") << "...no path." << std::endl;
-  }
-}
-
-Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
-                                         SolvedForm& sf,
-                                         Node pv,
-                                         Node lit,
-                                         CegInstEffort effort)
-{
-  if (effort == CEG_INST_EFFORT_FULL)
-  {
-    // always use model values at full effort
-    return Node::null();
-  }
-  Node atom = lit.getKind() == NOT ? lit[0] : lit;
-  bool pol = lit.getKind() != NOT;
-  Kind k = atom.getKind();
-  if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT)
-  {
-    // others are unhandled
-    return Node::null();
-  }
-  else if (!atom[0].getType().isBitVector())
-  {
-    return Node::null();
-  }
-  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP
-           || (pol && k == EQUAL))
-  {
-    return lit;
-  }
-  NodeManager* nm = NodeManager::currentNM();
-  Node s = atom[0];
-  Node t = atom[1];
-
-  Node sm = ci->getModelValue(s);
-  Node tm = ci->getModelValue(t);
-  Assert(!sm.isNull() && sm.isConst());
-  Assert(!tm.isNull() && tm.isConst());
-  Trace("cegqi-bv") << "Model value: " << std::endl;
-  Trace("cegqi-bv") << "   " << s << " " << k << " " << t << " is "
-                    << std::endl;
-  Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
-
-  Node ret;
-  if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
-  {
-    // if using slack, we convert constraints to a positive equality based on
-    // the current model M, e.g.:
-    //   (not) s ~ t  --->  s = t + ( s^M - t^M )
-    if (sm != tm)
-    {
-      Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm));
-      Assert(slack.isConst());
-      // remember the slack value for the asserted literal
-      d_alit_to_model_slack[lit] = slack;
-      ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack));
-      Trace("cegqi-bv") << "Slack is " << slack << std::endl;
-    }
-    else
-    {
-      ret = s.eqNode(t);
-    }
-  } else {
-    // turn disequality into an inequality
-    // e.g. s != t becomes s < t or t < s
-    if (k == EQUAL)
-    {
-      if (Random::getRandom().pickWithProb(0.5))
-      {
-        std::swap(s, t);
-      }
-      pol = true;
-    }
-    // otherwise, we optimistically solve for the boundary point of an
-    // inequality, for example:
-    //   for s < t, we solve s+1 = t
-    //   for ~( s < t ), we solve s = t
-    // notice that this equality does not necessarily hold in the model, and
-    // hence the corresponding instantiation strategy is not guaranteed to be
-    // monotonic.
-    if (!pol)
-    {
-      ret = s.eqNode(t);
-    } else {
-      Node bv_one = bv::utils::mkOne(bv::utils::getSize(s));
-      ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t);
-    }
-  }
-  Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl;
-  return ret;
-}
-
-bool BvInstantiator::processAssertion(CegInstantiator* ci,
-                                      SolvedForm& sf,
-                                      Node pv,
-                                      Node lit,
-                                      Node alit,
-                                      CegInstEffort effort)
-{
-  // if option enabled, use approach for word-level inversion for BV instantiation
-  if( options::cbqiBv() ){
-    // get the best rewritten form of lit for solving for pv 
-    //   this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible
-    Node rlit = rewriteAssertionForSolvePv(ci, pv, lit);
-    if( Trace.isOn("cegqi-bv") ){
-      Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl;
-      if( lit!=rlit ){
-        Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl;
-      }
-    }
-    if (!rlit.isNull())
-    {
-      processLiteral(ci, sf, pv, rlit, alit, effort);
-    }
-  }
-  return false;
-}
-
-bool BvInstantiator::useModelValue(CegInstantiator* ci,
-                                   SolvedForm& sf,
-                                   Node pv,
-                                   CegInstEffort effort)
-{
-  return !d_tried_assertion_inst
-         && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort());
-}
-
-bool BvInstantiator::processAssertions(CegInstantiator* ci,
-                                       SolvedForm& sf,
-                                       Node pv,
-                                       CegInstEffort effort)
-{
-  std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv );
-  if( iti!=d_var_to_inst_id.end() ){
-    Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl;
-    // if interleaving, do not do inversion half the time
-    if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5))
-    {
-      bool firstVar = sf.empty();
-      // get inst id list
-      if (Trace.isOn("cegqi-bv"))
-      {
-        Trace("cegqi-bv") << "  " << iti->second.size()
-                          << " candidate instantiations for " << pv << " : "
-                          << std::endl;
-        if (firstVar)
-        {
-          Trace("cegqi-bv") << "  ...this is the first variable" << std::endl;
-        }
-      }
-      // until we have a model-preserving selection function for BV, this must
-      // be heuristic (we only pick one literal)
-      // hence we randomize the list
-      // this helps robustness, since picking the same literal every time may
-      // lead to a stream of value instantiations, whereas with randomization
-      // we may find an invertible literal that leads to a useful instantiation.
-      std::random_shuffle(iti->second.begin(), iti->second.end());
-
-      if (Trace.isOn("cegqi-bv"))
-      {
-        for (unsigned j = 0, size = iti->second.size(); j < size; j++)
-        {
-          unsigned inst_id = iti->second[j];
-          Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
-          Node inst_term = d_inst_id_to_term[inst_id];
-          Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end());
-          Node alit = d_inst_id_to_alit[inst_id];
-
-          // get the slack value introduced for the asserted literal
-          Node curr_slack_val;
-          std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
-              d_alit_to_model_slack.find(alit);
-          if (itms != d_alit_to_model_slack.end())
-          {
-            curr_slack_val = itms->second;
-          }
-
-          // debug printing
-          Trace("cegqi-bv") << "   [" << j << "] : ";
-          Trace("cegqi-bv") << inst_term << std::endl;
-          if (!curr_slack_val.isNull()) {
-            Trace("cegqi-bv") << "   ...with slack value : " << curr_slack_val
-                              << std::endl;
-          }
-          Trace("cegqi-bv-debug") << "   ...from : " << alit << std::endl;
-          Trace("cegqi-bv") << std::endl;
-        }
-      }
-
-      // Now, try all instantiation ids we want to try
-      // Typically we try only one, otherwise worst-case performance
-      // for constructing instantiations is exponential on the number of
-      // variables in this quantifier prefix.
-      bool ret = false;
-      bool tryMultipleInst = firstVar && options::cbqiMultiInst();
-      bool revertOnSuccess = tryMultipleInst;
-      for (unsigned j = 0, size = iti->second.size(); j < size; j++)
-      {
-        unsigned inst_id = iti->second[j];
-        Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end());
-        Node inst_term = d_inst_id_to_term[inst_id];
-        Node alit = d_inst_id_to_alit[inst_id];
-        // try instantiation pv -> inst_term
-        TermProperties pv_prop_bv;
-        Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term
-                          << std::endl;
-        d_var_to_curr_inst_id[pv] = inst_id;
-        d_tried_assertion_inst = true;
-        ci->markSolved(alit);
-        if (ci->constructInstantiationInc(
-                pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
-        {
-          ret = true;
-        }
-        ci->markSolved(alit, false);
-        // we are done unless we try multiple instances
-        if (!tryMultipleInst)
-        {
-          break;
-        }
-      }
-      if (ret)
-      {
-        return true;
-      }
-      Trace("cegqi-bv") << "...failed to add instantiation for " << pv
-                        << std::endl;
-      d_var_to_curr_inst_id.erase(pv);
-    } else {
-      Trace("cegqi-bv") << "...do not do instantiation for " << pv
-                        << " (skip, based on heuristic)" << std::endl;
-    }
-  }
-
-  return false;
-}
-
-Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
-                                                Node pv,
-                                                Node lit)
-{
-  // result of rewriting the visited term
-  std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
-  visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
-  // whether the visited term contains pv
-  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
-  std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
-  std::stack<std::stack<TNode> > visit;
-  TNode cur;
-  visit.push(std::stack<TNode>());
-  visit.top().push(lit);
-  do {
-    cur = visit.top().top();
-    visit.top().pop();
-    it = visited.top().find(cur);
-
-    if (it == visited.top().end())
-    {
-      std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc =
-          curr_subs.find(cur);
-      if (itc != curr_subs.end())
-      {
-        visited.top()[cur] = itc->second;
-      }
-      else
-      {
-        if (cur.getKind() == CHOICE)
-        {
-          // must replace variables of choice functions
-          // with new variables to avoid variable
-          // capture when considering substitutions
-          // with multiple literals.
-          Node bv = ci->getBoundVariable(cur[0][0].getType());
-          // should not have captured variables
-          Assert(curr_subs.find(cur[0][0]) == curr_subs.end());
-          curr_subs[cur[0][0]] = bv;
-          // we cannot cache the results of subterms
-          // of this choice expression since we are
-          // now in the context { cur[0][0] -> bv },
-          // hence we push a context here
-          visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
-          visit.push(std::stack<TNode>());
-        }
-        visited.top()[cur] = Node::null();
-        visit.top().push(cur);
-        for (unsigned i = 0; i < cur.getNumChildren(); i++)
-        {
-          visit.top().push(cur[i]);
-        }
-      }
-    } else if (it->second.isNull()) {
-      Node ret;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        children.push_back(cur.getOperator());
-      }
-      bool contains_pv = ( cur==pv );
-      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
-        it = visited.top().find(cur[i]);
-        Assert(it != visited.top().end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cur[i] != it->second;
-        children.push_back(it->second);
-        contains_pv = contains_pv || visited_contains_pv[cur[i]];
-      }
-      // careful that rewrites above do not affect whether this term contains pv
-      visited_contains_pv[cur] = contains_pv;
-
-      // rewrite the term
-      ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv);
-
-      // return original if the above function does not produce a result
-      if (ret.isNull()) {
-        if (childChanged) {
-          ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
-        }else{
-          ret = cur;
-        }
-      }
-
-      /* We need to update contains_pv also for rewritten nodes, since
-       * the normalizePv* functions rely on the information if pv occurs in a
-       * rewritten node or not. */
-      if (ret != cur)
-      {
-        contains_pv = (ret == pv);
-        for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i)
-        {
-          contains_pv = contains_pv || visited_contains_pv[ret[i]];
-        }
-        visited_contains_pv[ret] = contains_pv;
-      }
-
-      // if was choice, pop context
-      if (cur.getKind() == CHOICE)
-      {
-        Assert(curr_subs.find(cur[0][0]) != curr_subs.end());
-        curr_subs.erase(cur[0][0]);
-        visited.pop();
-        visit.pop();
-        Assert(visited.size() == visit.size());
-        Assert(!visit.empty());
-      }
-
-      visited.top()[cur] = ret;
-    }
-  } while (!visit.top().empty());
-  Assert(visited.size() == 1);
-  Assert(visited.top().find(lit) != visited.top().end());
-  Assert(!visited.top().find(lit)->second.isNull());
-
-  Node result = visited.top()[lit];
-
-  if (Trace.isOn("cegqi-bv-nl"))
-  {
-    std::vector<TNode> trace_visit;
-    std::unordered_set<TNode, TNodeHashFunction> trace_visited;
-
-    trace_visit.push_back(result);
-    do
-    {
-      cur = trace_visit.back();
-      trace_visit.pop_back();
-
-      if (trace_visited.find(cur) == trace_visited.end())
-      {
-        trace_visited.insert(cur);
-        trace_visit.insert(trace_visit.end(), cur.begin(), cur.end());
-      }
-      else if (cur == pv)
-      {
-        Trace("cegqi-bv-nl")
-            << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl;
-      }
-    } while (!trace_visit.empty());
-  }
-
-  return result;
-}
-
-/**
- * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t,
- * or -pv * t. Extracting the coefficient of multiplications only succeeds if
- * the multiplication are normalized with normalizePvMult.
- *
- * If sucessful it returns
- *   1    if n ==  pv,
- *  -1    if n == -pv,
- *   t    if n ==  pv * t,
- *  -t    if n == -pv * t.
- * If n is not a linear term, a null node is returned.
- */
-static Node getPvCoeff(TNode pv, TNode n)
-{
-  bool neg = false;
-  Node coeff;
-
-  if (n.getKind() == BITVECTOR_NEG)
-  {
-    neg = true;
-    n = n[0];
-  }
-
-  if (n == pv)
-  {
-    coeff = bv::utils::mkOne(bv::utils::getSize(pv));
-  }
-  /* All multiplications are normalized to pv * (t1 * t2). */
-  else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute()))
-  {
-    Assert(n.getNumChildren() == 2);
-    Assert(n[0] == pv);
-    coeff = n[1];
-  }
-  else /* n is in no form to extract the coefficient for pv */
-  {
-    Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in "
-                         << n << std::endl;
-    return Node::null();
-  }
-  Assert(!coeff.isNull());
-
-  if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff);
-  return coeff;
-}
-
-/**
- * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks
- * terms in which pv occurs.
- * For example,
- *
- *  a * -pv * b * c
- *
- * is rewritten to
- *
- *  pv * -(a * b * c)
- *
- * Returns the normalized node if the resulting term is linear w.r.t. pv and
- * a null node otherwise. If pv does not occur in children it returns a
- * multiplication over children.
- */
-static Node normalizePvMult(
-    TNode pv,
-    const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
-{
-  bool neg, neg_coeff = false;
-  bool found_pv = false;
-  NodeManager* nm;
-  NodeBuilder<> nb(BITVECTOR_MULT);
-  BvLinearAttribute is_linear;
-
-  nm = NodeManager::currentNM();
-  for (TNode nc : children)
-  {
-    if (!contains_pv[nc])
-    {
-      nb << nc;
-      continue;
-    }
-
-    neg = false;
-    if (nc.getKind() == BITVECTOR_NEG)
-    {
-      neg = true;
-      nc = nc[0];
-    }
-
-    if (!found_pv && nc == pv)
-    {
-      found_pv = true;
-      neg_coeff = neg;
-      continue;
-    }
-    else if (!found_pv && nc.getKind() == BITVECTOR_MULT
-             && nc.getAttribute(is_linear))
-    {
-      Assert(nc.getNumChildren() == 2);
-      Assert(nc[0] == pv);
-      Assert(!contains_pv[nc[1]]);
-      found_pv = true;
-      neg_coeff = neg;
-      nb << nc[1];
-      continue;
-    }
-    return Node::null(); /* non-linear */
-  }
-  Assert(nb.getNumChildren() > 0);
-
-  Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode();
-  if (neg_coeff)
-  {
-    coeff = nm->mkNode(BITVECTOR_NEG, coeff);
-  }
-  coeff = Rewriter::rewrite(coeff);
-  unsigned size_coeff = bv::utils::getSize(coeff);
-  Node zero = bv::utils::mkZero(size_coeff);
-  if (coeff == zero)
-  {
-    return zero;
-  }
-  Node result;
-  if (found_pv)
-  {
-    if (coeff == bv::utils::mkOne(size_coeff))
-    {
-      return pv;
-    }
-    result = nm->mkNode(BITVECTOR_MULT, pv, coeff);
-    contains_pv[result] = true;
-    result.setAttribute(is_linear, true);
-  }
-  else
-  {
-    result = coeff;
-  }
-  return result;
-}
-
-#ifdef CVC4_ASSERTIONS
-static bool isLinearPlus(
-    TNode n,
-    TNode pv,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
-{
-  Node coeff;
-  Assert(n.getAttribute(BvLinearAttribute()));
-  Assert(n.getNumChildren() == 2);
-  if (n[0] != pv)
-  {
-    Assert(n[0].getKind() == BITVECTOR_MULT);
-    Assert(n[0].getNumChildren() == 2);
-    Assert(n[0][0] == pv);
-    Assert(!contains_pv[n[0][1]]);
-  }
-  Assert(!contains_pv[n[1]]);
-  coeff = getPvCoeff(pv, n[0]);
-  Assert(!coeff.isNull());
-  Assert(!contains_pv[coeff]);
-  return true;
-}
-#endif
-
-/**
- * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
- * terms in which pv occurs.
- * For example,
- *
- *  a * pv + b + c * -pv
- *
- * is rewritten to
- *
- *  pv * (a - c) + b
- *
- * Returns the normalized node if the resulting term is linear w.r.t. pv and
- * a null node otherwise. If pv does not occur in children it returns an
- * addition over children.
- */
-static Node normalizePvPlus(
-    Node pv,
-    const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
-{
-  NodeManager* nm;
-  NodeBuilder<> nb_c(BITVECTOR_PLUS);
-  NodeBuilder<> nb_l(BITVECTOR_PLUS);
-  BvLinearAttribute is_linear;
-  bool neg;
-
-  nm = NodeManager::currentNM();
-  for (TNode nc : children)
-  {
-    if (!contains_pv[nc])
-    {
-      nb_l << nc;
-      continue;
-    }
-
-    neg = false;
-    if (nc.getKind() == BITVECTOR_NEG)
-    {
-      neg = true;
-      nc = nc[0];
-    }
-
-    if (nc == pv
-        || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear)))
-    {
-      Node coeff = getPvCoeff(pv, nc);
-      Assert(!coeff.isNull());
-      if (neg)
-      {
-        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
-      }
-      nb_c << coeff;
-      continue;
-    }
-    else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear))
-    {
-      Assert(isLinearPlus(nc, pv, contains_pv));
-      Node coeff = getPvCoeff(pv, nc[0]);
-      Assert(!coeff.isNull());
-      Node leaf = nc[1];
-      if (neg)
-      {
-        coeff = nm->mkNode(BITVECTOR_NEG, coeff);
-        leaf = nm->mkNode(BITVECTOR_NEG, leaf);
-      }
-      nb_c << coeff;
-      nb_l << leaf;
-      continue;
-    }
-    /* can't collect coefficients of 'pv' in 'cur' -> non-linear */
-    return Node::null();
-  }
-  Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0);
-
-  Node pv_mult_coeffs, result;
-  if (nb_c.getNumChildren() > 0)
-  {
-    Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode();
-    coeffs = Rewriter::rewrite(coeffs);
-    result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv);
-  }
-
-  if (nb_l.getNumChildren() > 0)
-  {
-    Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode();
-    leafs = Rewriter::rewrite(leafs);
-    Node zero = bv::utils::mkZero(bv::utils::getSize(pv));
-    /* pv * 0 + t --> t */
-    if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero)
-    {
-      result = leafs;
-    }
-    else
-    {
-      result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs);
-      contains_pv[result] = true;
-      result.setAttribute(is_linear, true);
-    }
-  }
-  Assert(!result.isNull());
-  return result;
-}
-
-/**
- * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
- * marks terms in which pv occurs.
- * For example, equality
- *
- *   -pv * a + b = c + pv
- *
- * rewrites to
- *
- *   pv * (-a - 1) = c - b.
- */
-static Node normalizePvEqual(
-    Node pv,
-    const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
-{
-  Assert(children.size() == 2);
-
-  NodeManager* nm = NodeManager::currentNM();
-  BvLinearAttribute is_linear;
-  Node coeffs[2], leafs[2];
-  bool neg;
-  TNode child;
-
-  for (unsigned i = 0; i < 2; ++i)
-  {
-    child = children[i];
-    neg = false;
-    if (child.getKind() == BITVECTOR_NEG)
-    {
-      neg = true;
-      child = child[0];
-    }
-    if (child.getAttribute(is_linear) || child == pv)
-    {
-      if (child.getKind() == BITVECTOR_PLUS)
-      {
-        Assert(isLinearPlus(child, pv, contains_pv));
-        coeffs[i] = getPvCoeff(pv, child[0]);
-        leafs[i] = child[1];
-      }
-      else
-      {
-        Assert(child.getKind() == BITVECTOR_MULT || child == pv);
-        coeffs[i] = getPvCoeff(pv, child);
-      }
-    }
-    if (neg)
-    {
-      if (!coeffs[i].isNull())
-      {
-        coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]);
-      }
-      if (!leafs[i].isNull())
-      {
-        leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]);
-      }
-    }
-  }
-
-  if (coeffs[0].isNull() || coeffs[1].isNull())
-  {
-    return Node::null();
-  }
-
-  Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]);
-  coeff = Rewriter::rewrite(coeff);
-  std::vector<Node> mult_children = {pv, coeff};
-  Node lhs = normalizePvMult(pv, mult_children, contains_pv);
-
-  Node rhs;
-  if (!leafs[0].isNull() && !leafs[1].isNull())
-  {
-    rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]);
-  }
-  else if (!leafs[0].isNull())
-  {
-    rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]);
-  }
-  else if (!leafs[1].isNull())
-  {
-    rhs = leafs[1];
-  }
-  else
-  {
-    rhs = bv::utils::mkZero(bv::utils::getSize(pv));
-  }
-  rhs = Rewriter::rewrite(rhs);
-
-  if (lhs == rhs)
-  {
-    return bv::utils::mkTrue();
-  }
-
-  Node result = lhs.eqNode(rhs);
-  contains_pv[result] = true;
-  return result;
-}
-
-Node BvInstantiator::rewriteTermForSolvePv(
-    Node pv,
-    Node n,
-    std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
-{
-  NodeManager* nm = NodeManager::currentNM();
-
-  // [1] rewrite cases of non-invertible operators
-
-  if (n.getKind() == EQUAL)
-  {
-    TNode lhs = children[0];
-    TNode rhs = children[1];
-
-    /* rewrite: x * x = x -> x < 2 */
-    if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv
-         && rhs[1] == pv)
-        || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv
-            && lhs[1] == pv))
-    {
-      return nm->mkNode(
-          BITVECTOR_ULT,
-          pv,
-          bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
-    }
-
-    if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
-    {
-      Node result = normalizePvEqual(pv, children, contains_pv);
-      if (!result.isNull())
-      {
-        Trace("cegqi-bv-nl")
-            << "Normalize " << n << " to " << result << std::endl;
-      }
-      else
-      {
-        Trace("cegqi-bv-nl")
-            << "Nonlinear " << n.getKind() << " " << n << std::endl;
-      }
-      return result;
-    }
-  }
-  else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
-  {
-    if (options::cbqiBvLinearize() && contains_pv[n])
-    {
-      Node result;
-      if (n.getKind() == BITVECTOR_MULT)
-      {
-        result = normalizePvMult(pv, children, contains_pv);
-      }
-      else
-      {
-        result = normalizePvPlus(pv, children, contains_pv);
-      }
-      if (!result.isNull())
-      {
-        Trace("cegqi-bv-nl")
-            << "Normalize " << n << " to " << result << std::endl;
-        return result;
-      }
-      else
-      {
-        Trace("cegqi-bv-nl")
-            << "Nonlinear " << n.getKind() << " " << n << std::endl;
-      }
-    }
-  }
-
-  // [2] try to rewrite non-linear literals -> linear literals
-
-  return Node::null();
-}
-
-/** sort bv extract interval
- *
- * This sorts lists of bitvector extract terms where
- * ((_ extract i1 i2) t) < ((_ extract j1 j2) t)
- * if i1>j1 or i1=j1 and i2>j2.
- */
-struct SortBvExtractInterval
-{
-  bool operator()(Node i, Node j)
-  {
-    Assert(i.getKind() == BITVECTOR_EXTRACT);
-    Assert(j.getKind() == BITVECTOR_EXTRACT);
-    BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>();
-    BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>();
-    if (ie.high > je.high)
-    {
-      return true;
-    }
-    else if (ie.high == je.high)
-    {
-      Assert(ie.low != je.low);
-      return ie.low > je.low;
-    }
-    return false;
-  }
-};
-
-void BvInstantiatorPreprocess::registerCounterexampleLemma(
-    std::vector<Node>& lems, std::vector<Node>& ce_vars)
-{
-  // new variables
-  std::vector<Node> vars;
-  // new lemmas
-  std::vector<Node> new_lems;
-
-  if (options::cbqiBvRmExtract())
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
-    // map from terms to bitvector extracts applied to that term
-    std::map<Node, std::vector<Node> > extract_map;
-    std::unordered_set<TNode, TNodeHashFunction> visited;
-    for (unsigned i = 0, size = lems.size(); i < size; i++)
-    {
-      Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : "
-                                  << lems[i] << std::endl;
-      collectExtracts(lems[i], extract_map, visited);
-    }
-    for (std::pair<const Node, std::vector<Node> >& es : extract_map)
-    {
-      // sort based on the extract start position
-      std::vector<Node>& curr_vec = es.second;
-
-      SortBvExtractInterval sbei;
-      std::sort(curr_vec.begin(), curr_vec.end(), sbei);
-
-      unsigned width = es.first.getType().getBitVectorSize();
-
-      // list of points b such that:
-      //   b>0 and we must start a segment at (b-1)  or  b==0
-      std::vector<unsigned> boundaries;
-      boundaries.push_back(width);
-      boundaries.push_back(0);
-
-      Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl;
-      for (unsigned i = 0, size = curr_vec.size(); i < size; i++)
-      {
-        Trace("cegqi-bv-pp") << "  " << i << " : " << curr_vec[i] << std::endl;
-        BitVectorExtract e =
-            curr_vec[i].getOperator().getConst<BitVectorExtract>();
-        if (std::find(boundaries.begin(), boundaries.end(), e.high + 1)
-            == boundaries.end())
-        {
-          boundaries.push_back(e.high + 1);
-        }
-        if (std::find(boundaries.begin(), boundaries.end(), e.low)
-            == boundaries.end())
-        {
-          boundaries.push_back(e.low);
-        }
-      }
-      std::sort(boundaries.rbegin(), boundaries.rend());
-
-      // make the extract variables
-      std::vector<Node> children;
-      for (unsigned i = 1; i < boundaries.size(); i++)
-      {
-        Assert(boundaries[i - 1] > 0);
-        Node ex = bv::utils::mkExtract(
-            es.first, boundaries[i - 1] - 1, boundaries[i]);
-        Node var =
-            nm->mkSkolem("ek",
-                         ex.getType(),
-                         "variable to represent disjoint extract region");
-        children.push_back(var);
-        vars.push_back(var);
-      }
-
-      Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children);
-      Assert(conc.getType() == es.first.getType());
-      Node eq_lem = conc.eqNode(es.first);
-      Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl;
-      new_lems.push_back(eq_lem);
-      Trace("cegqi-bv-pp") << "...finished processing extracts for term "
-                            << es.first << std::endl;
-    }
-    Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl;
-  }
-
-  if (!vars.empty())
-  {
-    // could try applying subs -> vars here
-    // in practice, this led to worse performance
-
-    Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
-                         << std::endl;
-    lems.insert(lems.end(), new_lems.begin(), new_lems.end());
-    Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
-                         << std::endl;
-    ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
-  }
-}
-
-void BvInstantiatorPreprocess::collectExtracts(
-    Node lem,
-    std::map<Node, std::vector<Node> >& extract_map,
-    std::unordered_set<TNode, TNodeHashFunction>& visited)
-{
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(lem);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-      if (cur.getKind() != FORALL)
-      {
-        if (cur.getKind() == BITVECTOR_EXTRACT)
-        {
-          if (cur[0].getKind() == INST_CONSTANT)
-          {
-            extract_map[cur[0]].push_back(cur);
-          }
-        }
-
-        for (const Node& nc : cur)
-        {
-          visit.push_back(nc);
-        }
-      }
-    }
-  } while (!visit.empty());
-}
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
deleted file mode 100644
index 306b65cc3..000000000
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h
+++ /dev/null
@@ -1,332 +0,0 @@
-/*********************                                                        */
-/*! \file ceg_t_instantiator.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief theory-specific counterexample-guided quantifier instantiation
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CEG_T_INSTANTIATOR_H
-#define __CVC4__CEG_T_INSTANTIATOR_H
-
-#include "theory/quantifiers/bv_inverter.h"
-#include "theory/quantifiers/cegqi/ceg_instantiator.h"
-
-#include <unordered_set>
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** TODO (#1367) : document these classes, also move to separate files. */
-
-class ArithInstantiator : public Instantiator {
- public:
-  ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
-  virtual ~ArithInstantiator(){}
-  void reset(CegInstantiator* ci,
-             SolvedForm& sf,
-             Node pv,
-             CegInstEffort effort) override;
-  bool hasProcessEquality(CegInstantiator* ci,
-                          SolvedForm& sf,
-                          Node pv,
-                          CegInstEffort effort) override
-  {
-    return true;
-  }
-  bool processEquality(CegInstantiator* ci,
-                       SolvedForm& sf,
-                       Node pv,
-                       std::vector<TermProperties>& term_props,
-                       std::vector<Node>& terms,
-                       CegInstEffort effort) override;
-  bool hasProcessAssertion(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           CegInstEffort effort) override
-  {
-    return true;
-  }
-  Node hasProcessAssertion(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           Node lit,
-                           CegInstEffort effort) override;
-  bool processAssertion(CegInstantiator* ci,
-                        SolvedForm& sf,
-                        Node pv,
-                        Node lit,
-                        Node alit,
-                        CegInstEffort effort) override;
-  bool processAssertions(CegInstantiator* ci,
-                         SolvedForm& sf,
-                         Node pv,
-                         CegInstEffort effort) override;
-  bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
-                                                SolvedForm& sf,
-                                                Node pv,
-                                                CegInstEffort effort) override;
-  bool postProcessInstantiationForVariable(CegInstantiator* ci,
-                                           SolvedForm& sf,
-                                           Node pv,
-                                           CegInstEffort effort,
-                                           std::vector<Node>& lemmas) override;
-  std::string identify() const override { return "Arith"; }
-
- private:
-  Node d_vts_sym[2];
-  std::vector<Node> d_mbp_bounds[2];
-  std::vector<Node> d_mbp_coeff[2];
-  std::vector<Node> d_mbp_vts_coeff[2][2];
-  std::vector<Node> d_mbp_lit[2];
-  int solve_arith(CegInstantiator* ci,
-                  Node v,
-                  Node atom,
-                  Node& veq_c,
-                  Node& val,
-                  Node& vts_coeff_inf,
-                  Node& vts_coeff_delta);
-  Node getModelBasedProjectionValue(CegInstantiator* ci,
-                                    Node e,
-                                    Node t,
-                                    bool isLower,
-                                    Node c,
-                                    Node me,
-                                    Node mt,
-                                    Node theta,
-                                    Node inf_coeff,
-                                    Node delta_coeff);
-};
-
-class DtInstantiator : public Instantiator {
-public:
-  DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
-  virtual ~DtInstantiator(){}
-  void reset(CegInstantiator* ci,
-             SolvedForm& sf,
-             Node pv,
-             CegInstEffort effort) override;
-  bool processEqualTerms(CegInstantiator* ci,
-                         SolvedForm& sf,
-                         Node pv,
-                         std::vector<Node>& eqc,
-                         CegInstEffort effort) override;
-  bool hasProcessEquality(CegInstantiator* ci,
-                          SolvedForm& sf,
-                          Node pv,
-                          CegInstEffort effort) override
-  {
-    return true;
-  }
-  bool processEquality(CegInstantiator* ci,
-                       SolvedForm& sf,
-                       Node pv,
-                       std::vector<TermProperties>& term_props,
-                       std::vector<Node>& terms,
-                       CegInstEffort effort) override;
-  std::string identify() const override { return "Dt"; }
-
- private:
-  Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
-};
-
-class TermArgTrie;
-
-class EprInstantiator : public Instantiator {
- public:
-  EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
-  virtual ~EprInstantiator(){}
-  void reset(CegInstantiator* ci,
-             SolvedForm& sf,
-             Node pv,
-             CegInstEffort effort) override;
-  bool processEqualTerm(CegInstantiator* ci,
-                        SolvedForm& sf,
-                        Node pv,
-                        TermProperties& pv_prop,
-                        Node n,
-                        CegInstEffort effort) override;
-  bool processEqualTerms(CegInstantiator* ci,
-                         SolvedForm& sf,
-                         Node pv,
-                         std::vector<Node>& eqc,
-                         CegInstEffort effort) override;
-  std::string identify() const override { return "Epr"; }
-
- private:
-  std::vector<Node> d_equal_terms;
-  void computeMatchScore(CegInstantiator* ci,
-                         Node pv,
-                         Node catom,
-                         std::vector<Node>& arg_reps,
-                         TermArgTrie* tat,
-                         unsigned index,
-                         std::map<Node, int>& match_score);
-  void computeMatchScore(CegInstantiator* ci,
-                         Node pv,
-                         Node catom,
-                         Node eqc,
-                         std::map<Node, int>& match_score);
-};
-
-/** Bitvector instantiator
- *
- * This implements an approach for counterexample-guided instantiation
- * for bit-vector variables based on word-level inversions.
- * It is enabled by --cbqi-bv.
- */
-class BvInstantiator : public Instantiator {
- public:
-  BvInstantiator(QuantifiersEngine* qe, TypeNode tn);
-  ~BvInstantiator() override;
-  void reset(CegInstantiator* ci,
-             SolvedForm& sf,
-             Node pv,
-             CegInstEffort effort) override;
-  bool hasProcessAssertion(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           CegInstEffort effort) override
-  {
-    return true;
-  }
-  Node hasProcessAssertion(CegInstantiator* ci,
-                           SolvedForm& sf,
-                           Node pv,
-                           Node lit,
-                           CegInstEffort effort) override;
-  bool processAssertion(CegInstantiator* ci,
-                        SolvedForm& sf,
-                        Node pv,
-                        Node lit,
-                        Node alit,
-                        CegInstEffort effort) override;
-  bool processAssertions(CegInstantiator* ci,
-                         SolvedForm& sf,
-                         Node pv,
-                         CegInstEffort effort) override;
-  /** use model value
-   *
-   * We allow model values if we have not already tried an assertion,
-   * and only at levels below full if cbqiFullEffort is false.
-   */
-  bool useModelValue(CegInstantiator* ci,
-                     SolvedForm& sf,
-                     Node pv,
-                     CegInstEffort effort) override;
-  std::string identify() const override { return "Bv"; }
-
- private:
-  // point to the bv inverter class
-  BvInverter * d_inverter;
-  unsigned d_inst_id_counter;
-  /** information about solved forms */
-  std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id;
-  std::unordered_map< unsigned, Node > d_inst_id_to_term;
-  std::unordered_map<unsigned, Node> d_inst_id_to_alit;
-  // variable to current id we are processing
-  std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
-  /** the amount of slack we added for asserted literals */
-  std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
-  /** whether we have tried an instantiation based on assertion in this round */
-  bool d_tried_assertion_inst;
-  /** rewrite assertion for solve pv
-  * returns a literal that is equivalent to lit that leads to best solved form for pv
-  */
-  Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit);
-  /** rewrite term for solve pv
-   * This is a helper function for rewriteAssertionForSolvePv.
-   * If this returns non-null value ret, then this indicates
-   * that n should be rewritten to ret. It is called as
-   * a "post-rewrite", that is, after the children of n
-   * have been rewritten and stored in the vector children.
-   *
-   * contains_pv stores whether certain nodes contain pv.
-   * where we guarantee that all subterms of terms in children
-   * appear in the domain of contains_pv.
-   */
-  Node rewriteTermForSolvePv(
-      Node pv,
-      Node n,
-      std::vector<Node>& children,
-      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
-  /** process literal, called from processAssertion
-  * lit is the literal to solve for pv that has been rewritten according to
-  * internal rules here.
-  * alit is the asserted literal that lit is derived from.
-  */
-  void processLiteral(CegInstantiator* ci,
-                      SolvedForm& sf,
-                      Node pv,
-                      Node lit,
-                      Node alit,
-                      CegInstEffort effort);
-};
-
-/** Bitvector instantiator preprocess
- *
- * This class implements preprocess techniques that are helpful for
- * counterexample-guided instantiation, such as introducing variables
- * that refer to disjoint bit-vector extracts.
- */
-class BvInstantiatorPreprocess : public InstantiatorPreprocess
-{
- public:
-  BvInstantiatorPreprocess() {}
-  ~BvInstantiatorPreprocess() override {}
-  /** register counterexample lemma
-   *
-   * This method modifies the contents of lems based on the extract terms
-   * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
-   * a dummy equality so that segments of terms t under extracts can be solved
-   * independently.
-   *
-   * For example:
-   *   P[ ((extract 7 4) t), ((extract 3 0) t)]
-   *     becomes:
-   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
-   *   t = concat( x74, x30 )
-   * where x74 and x30 are fresh variables of type BV_4.
-   *
-   * Another example:
-   *   P[ ((extract 7 3) t), ((extract 4 0) t)]
-   *     becomes:
-   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
-   *   t = concat( x75, x44, x30 )
-   * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
-   * respectively.
-   *
-   * Notice we leave the original conjecture alone. This is done for performance
-   * since the added equalities ensure we are able to construct the proper
-   * solved forms for variables in t and for the intermediate variables above.
-   */
-  void registerCounterexampleLemma(std::vector<Node>& lems,
-                                   std::vector<Node>& ce_vars) override;
-
- private:
-  /** collect extracts
-   *
-   * This method collects all extract terms in lem
-   * and stores them in d_extract_map.
-   * visited is the terms we've already visited.
-   */
-  void collectExtracts(Node lem,
-                       std::map<Node, std::vector<Node> >& extract_map,
-                       std::unordered_set<TNode, TNodeHashFunction>& visited);
-};
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
-
-#endif
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 37f11f9cd..3d966726b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -21,7 +21,7 @@
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+#include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
 #include "theory/quantifiers/conjecture_generator.h"
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index 24e3ca98c..4c96f6cb9 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -22,7 +22,7 @@
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-#include "theory/quantifiers/cegqi/ceg_t_instantiator.cpp"
+#include "theory/quantifiers/cegqi/ceg_bv_instantiator.cpp"
 
 #include <cxxtest/TestSuite.h>
 #include <iostream>