CBQI BV choice expressions (#1296)

* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.

* Minor

* Make unique bound variables for choice functions in BvInstantor, clean up.

* Incorporate missing optimizations

* Clang format

* Unused field.

* Minor

* Fix, add regression.

* Fix regression.

* Fix bug that led to incorrect cleanup of instantiations.

* Add missing regression

* Improve handling of choice rewriting.

* Fix

* Clang format

* Use canonical variables for choice functions in cbqi bv.

* Add regression

* Clang format.

* Address review.

* Clang format

8 files changed, 360 insertions, 340 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 01cf59c15..c2f9facce 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -150,7 +150,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
 
     // The new assertion is the assumption that the body
     // of the choice operator holds for the Skolem
-    newAssertion = node[1].substitute(node[0], skolem);
+    newAssertion = node[1].substitute(node[0][0], skolem);
   }
 
   //if a non-variable Boolean term, replace it
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index f84f9dc37..371ca1f58 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -50,7 +50,7 @@ public:
 
   /**
    * By introducing skolem variables, this function removes all occurrences of:
-   * (1) term ITEs
+   * (1) term ITEs,
    * (2) terms of type Boolean that are not Boolean term variables,
    * (3) lambdas, and
    * (4) Hilbert choice expressions.
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 957385a14..d777dc4f8 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -52,21 +52,7 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
   if (its == d_solve_var.end())
   {
-    std::stringstream ss;
-    if (tn.isFunction())
-    {
-      Assert(tn.getNumChildren() == 2);
-      Assert(tn[0].isBoolean());
-      ss << "slv_f";
-    }
-    else
-    {
-      ss << "slv";
-    }
-    Node k = NodeManager::currentNM()->mkSkolem(ss.str(), tn);
-    // marked as a virtual term (it is eligible for instantiation)
-    VirtualTermSkolemAttribute vtsa;
-    k.setAttribute(vtsa, true);
+    Node k = NodeManager::currentNM()->mkSkolem("slv", tn);
     d_solve_var[tn] = k;
     return k;
   }
@@ -76,75 +62,50 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   }
 }
 
-Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn)
+Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
 {
   // condition should be rewritten
-  Assert(Rewriter::rewrite(cond) == cond);
-  std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
-      d_inversion_skolem_cache.find(cond);
-  if (it == d_inversion_skolem_cache.end())
+  Node new_cond = Rewriter::rewrite(cond);
+  if (new_cond != cond)
   {
-    Node skv;
-    if (cond.getKind() == EQUAL)
+    Trace("cegqi-bv-skvinv-debug") << "Condition " << cond
+                                   << " was rewritten to " << new_cond
+                                   << std::endl;
+  }
+  Node c;
+  // optimization : if condition is ( x = v ) should just return v and not
+  // introduce a Skolem this can happen when we ask for the multiplicative
+  // inversion with bv1
+  TNode solve_var = getSolveVariable(tn);
+  if (new_cond.getKind() == EQUAL)
+  {
+    for (unsigned i = 0; i < 2; i++)
     {
-      // optimization : if condition is ( x = v ) should just return v and not
-      // introduce a Skolem this can happen when we ask for the multiplicative
-      // inversion with bv1
-      Node x = getSolveVariable(tn);
-      for (unsigned i = 0; i < 2; i++)
+      if (new_cond[i] == solve_var)
       {
-        if (cond[i] == x)
-        {
-          skv = cond[1 - i];
-          Trace("cegqi-bv-skvinv")
-              << "SKVINV : " << skv << " is trivially associated with conditon "
-              << cond << std::endl;
-          break;
-        }
+        c = new_cond[1 - i];
+        Trace("cegqi-bv-skvinv") << "SKVINV : " << c
+                                 << " is trivially associated with conditon "
+                                 << new_cond << std::endl;
+        break;
       }
     }
-    if (skv.isNull())
-    {
-      // TODO : compute the value if the condition is deterministic, e.g. calc
-      // multiplicative inverse of 2 constants
-      skv = NodeManager::currentNM()->mkSkolem(
-          "skvinv", tn, "created for BvInverter");
-      Trace("cegqi-bv-skvinv")
-          << "SKVINV : " << skv << " is the skolem associated with conditon "
-          << cond << std::endl;
-      // marked as a virtual term (it is eligible for instantiation)
-      VirtualTermSkolemAttribute vtsa;
-      skv.setAttribute(vtsa, true);
-    }
-    d_inversion_skolem_cache[cond] = skv;
-    return skv;
-  }
-  else
-  {
-    Assert(it->second.getType() == tn);
-    return it->second;
   }
-}
-
-Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  // function maps conditions to skolems
-  TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn);
-  return getSolveVariable(ftn);
-}
-
-Node BvInverter::getInversionNode(Node cond, TypeNode tn)
-{
-  // condition should be rewritten
-  Node new_cond = Rewriter::rewrite(cond);
-  if (new_cond != cond)
+  // TODO : compute the value if the condition is deterministic, e.g. calc
+  // multiplicative inverse of 2 constants
+  if (c.isNull())
   {
-    Trace("bv-invert-debug") << "Condition " << cond << " was rewritten to "
-                             << new_cond << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    Node x = m->getBoundVariable(tn);
+    Node ccond = new_cond.substitute(solve_var, x);
+    c = nm->mkNode(kind::CHOICE, nm->mkNode(BOUND_VAR_LIST, x), ccond);
+    Trace("cegqi-bv-skvinv") << "SKVINV : Make " << c << " for " << new_cond
+                             << std::endl;
   }
-  Node f = getInversionSkolemFunctionFor(tn);
-  return NodeManager::currentNM()->mkNode(kind::APPLY_UF, f, new_cond);
+  // currently shouldn't cache since
+  // the return value depends on the
+  // state of m (which bound variable is returned).
+  return c;
 }
 
 bool BvInverter::isInvertible(Kind k, unsigned index)
@@ -219,97 +180,6 @@ Node BvInverter::getPathToPv(
   return Node::null();
 }
 
-Node BvInverter::eliminateSkolemFunctions(TNode n,
-                                          std::vector<Node>& side_conditions)
-{
-  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
-  std::stack<TNode> visit;
-  TNode cur;
-
-  visit.push(n);
-  do
-  {
-    cur = visit.top();
-    visit.pop();
-    it = visited.find(cur);
-
-    if (it == visited.end())
-    {
-      visited[cur] = Node::null();
-      visit.push(cur);
-      for (unsigned i = 0; i < cur.getNumChildren(); i++)
-      {
-        visit.push(cur[i]);
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Trace("bv-invert-debug")
-          << "eliminateSkolemFunctions from " << cur << "..." << std::endl;
-
-      Node ret = cur;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
-      {
-        children.push_back(cur.getOperator());
-      }
-      for (unsigned i = 0; i < cur.getNumChildren(); i++)
-      {
-        it = visited.find(cur[i]);
-        Assert(it != visited.end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cur[i] != it->second;
-        children.push_back(it->second);
-      }
-      if (childChanged)
-      {
-        ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
-      }
-      // now, check if it is a skolem function
-      if (ret.getKind() == APPLY_UF)
-      {
-        Node op = ret.getOperator();
-        TypeNode tnp = op.getType();
-        // is this a skolem function?
-        std::map<TypeNode, Node>::iterator its = d_solve_var.find(tnp);
-        if (its != d_solve_var.end() && its->second == op)
-        {
-          Assert(ret.getNumChildren() == 1);
-          Assert(ret[0].getType().isBoolean());
-
-          Node cond = ret[0];
-          // must rewrite now to ensure we lookup the correct skolem
-          cond = Rewriter::rewrite(cond);
-
-          // if so, we replace by the (finalized) skolem variable
-          // Notice that since we are post-rewriting, skolem functions are
-          // already eliminated from cond
-          ret = getInversionSkolemFor(cond, ret.getType());
-
-          // also must add (substituted) side condition to vector
-          // substitute ( solve variable -> inversion skolem )
-          TNode solve_var = getSolveVariable(ret.getType());
-          TNode tret = ret;
-          cond = cond.substitute(solve_var, tret);
-          if (std::find(side_conditions.begin(), side_conditions.end(), cond)
-              == side_conditions.end())
-          {
-            side_conditions.push_back(cond);
-          }
-        }
-      }
-      Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << cur
-                               << " returned " << ret << std::endl;
-      visited[cur] = ret;
-    }
-  } while (!visit.empty());
-  Assert(visited.find(n) != visited.end());
-  Assert(!visited.find(n)->second.isNull());
-  return visited[n];
-}
-
 Node BvInverter::getPathToPv(
     Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path)
 {
@@ -329,7 +199,7 @@ Node BvInverter::getPathToPv(
 Node BvInverter::solve_bv_lit(Node sv,
                               Node lit,
                               std::vector<unsigned>& path,
-                              BvInverterModelQuery* m,
+                              BvInverterQuery* m,
                               BvInverterStatus& status)
 {
   Assert(!path.empty());
@@ -413,7 +283,7 @@ Node BvInverter::solve_bv_lit(Node sv,
       }
       status.d_conds.push_back(sc);
       /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn);
+      Node skv = getInversionNode(sc, solve_tn, m);
       t = skv;
       if (!path.empty())
       {
@@ -469,7 +339,7 @@ Node BvInverter::solve_bv_lit(Node sv,
       }
       status.d_conds.push_back(sc);
       /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn);
+      Node skv = getInversionNode(sc, solve_tn, m);
       t = skv;
       if (!path.empty())
       {
@@ -502,7 +372,7 @@ Node BvInverter::solve_bv_lit(Node sv,
         Node sc = nm->mkNode(IMPLIES, scl, scr);
         status.d_conds.push_back(sc);
         /* t = skv (fresh skolem constant)  */
-        Node skv = getInversionNode(sc, solve_tn);
+        Node skv = getInversionNode(sc, solve_tn, m);
         t = skv;
         if (!path.empty())
         {
@@ -599,7 +469,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition  */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS  */
           t = skv;
           break;
@@ -641,7 +511,7 @@ Node BvInverter::solve_bv_lit(Node sv,
           }
           Node sc = nm->mkNode(IMPLIES, scl, scr);
           status.d_conds.push_back(sc);
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           t = skv;
           break;
         }
@@ -694,7 +564,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS */
           t = skv;
           break;
@@ -713,7 +583,7 @@ Node BvInverter::solve_bv_lit(Node sv,
           Node sc = nm->mkNode(IMPLIES, scl, scr);
           status.d_conds.push_back(sc);
           /* t = skv (fresh skolem constant)  */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           t = skv;
           break;
         }
@@ -749,7 +619,7 @@ Node BvInverter::solve_bv_lit(Node sv,
             Node sc = nm->mkNode(IMPLIES, scl, scr);
             status.d_conds.push_back(sc);
             /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn);
+            Node skv = getInversionNode(sc, solve_tn, m);
             t = skv;
           }
           else
@@ -793,7 +663,7 @@ Node BvInverter::solve_bv_lit(Node sv,
             Node sc = nm->mkNode(IMPLIES, scl, scr);
             status.d_conds.push_back(sc);
             /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn);
+            Node skv = getInversionNode(sc, solve_tn, m);
             t = skv;
           }
           else
@@ -863,7 +733,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
           /* t = skv (fresh skolem constant)
            * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn);
+          Node skv = getInversionNode(sc, solve_tn, m);
           /* now solving with the skolem node as the RHS */
           t = skv;
           break;
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 1c60d11ea..56f8d492b 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -28,12 +28,20 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-// virtual class for model queries
-class BvInverterModelQuery {
+/** BvInverterQuery
+ *
+ * This is a virtual class for queries
+ * required by the BvInverter class.
+ */
+class BvInverterQuery
+{
  public:
-  BvInverterModelQuery() {}
-  ~BvInverterModelQuery() {}
+  BvInverterQuery() {}
+  ~BvInverterQuery() {}
+  /** returns the current model value of n */
   virtual Node getModelValue(Node n) = 0;
+  /** returns a bound variable of type tn */
+  virtual Node getBoundVariable(TypeNode tn) = 0;
 };
 
 // class for storing information about the solved status
@@ -53,17 +61,26 @@ class BvInverter {
  public:
   BvInverter() {}
   ~BvInverter() {}
-
   /** get dummy fresh variable of type tn, used as argument for sv */
   Node getSolveVariable(TypeNode tn);
 
-  /** get inversion node, if :
+  /** get inversion node
+   *
+   * This expects a condition cond where:
+   *   (exists x. cond)
+   * is a BV tautology where x is getSolveVariable( tn ).
    *
-   *   f = getInversionSkolemFunctionFor( tn )
+   * It returns a term of the form:
+   *   (choice y. cond { x -> y })
+   * where y is a bound variable and x is getSolveVariable( tn ).
    *
-   * This returns f( cond ).
+   * In some cases, we may return a term t
+   * if cond implies an equality on the solve variable.
+   * For example, if cond is x = t where x is
+   * getSolveVariable( tn ), then we return t
+   * instead of introducing the choice function.
    */
-  Node getInversionNode(Node cond, TypeNode tn);
+  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
 
   /** Get path to pv in lit, replace that occurrence by sv and all others by
    * pvs. If return value R is non-null, then : lit.path = pv R.path = sv
@@ -72,62 +89,26 @@ class BvInverter {
   Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
                    std::vector<unsigned>& path);
 
-  /** eliminate skolem functions in node n
-   *
-   * This eliminates all Skolem functions from Node n and replaces them with
-   * finalized Skolem variables.
-   *
-   * For each skolem variable we introduce, we ensure its associated side
-   * condition is added to side_conditions.
-   *
-   * Apart from Skolem functions, all subterms of n should be eligible for
-   * instantiation.
-   */
-  Node eliminateSkolemFunctions(TNode n, std::vector<Node>& side_conditions);
-
   /** solve_bv_lit
    * solve for sv in lit, where lit.path = sv
    * status accumulates side conditions
    */
-  Node solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& path,
-                    BvInverterModelQuery* m, BvInverterStatus& status);
+  Node solve_bv_lit(Node sv,
+                    Node lit,
+                    std::vector<unsigned>& path,
+                    BvInverterQuery* m,
+                    BvInverterStatus& status);
 
  private:
   /** dummy variables for each type */
   std::map<TypeNode, Node> d_solve_var;
 
-  /** stores the inversion skolems, for each condition */
-  std::unordered_map<Node, Node, NodeHashFunction> d_inversion_skolem_cache;
-
   /** helper function for getPathToPv */
   Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
 
   // is operator k invertible?
   bool isInvertible(Kind k, unsigned index);
-
-  /** get inversion skolem for condition
-   * precondition : exists x. cond( x ) is a tautology in BV,
-   *               where x is getSolveVariable( tn ).
-   * returns fresh skolem k of type tn, where we may assume cond( k ).
-   */
-  Node getInversionSkolemFor(Node cond, TypeNode tn);
-
-  /** get inversion skolem function for type tn.
-   *   This is a function of type ( Bool -> tn ) that is used for explicitly
-   * storing side conditions inside terms. For all ( cond, tn ), if :
-   *
-   *   f = getInversionSkolemFunctionFor( tn )
-   *   k = getInversionSkolemFor( cond, tn )
-   *   then:
-   *   f( cond ) is a placeholder for k.
-   *
-   * In the call eliminateSkolemFunctions, we replace all f( cond ) with k and
-   * add cond{ x -> k } to side_conditions. The advantage is that f( cond )
-   * explicitly contains the side condition so it automatically updates with
-   * substitutions.
-   */
-  Node getInversionSkolemFunctionFor(TypeNode tn);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 57bfb2d14..e7749cd92 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -46,24 +46,35 @@ CegInstantiator::~CegInstantiator() {
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
-    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
-      d_prog_var[n][n] = true;
+    if (n.getKind() == kind::CHOICE)
+    {
+      Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
+      d_prog_var[n[0][0]].clear();
+    }
+    if (d_vars_set.find(n) != d_vars_set.end())
+    {
+      d_prog_var[n].insert(n);
     }else if( !d_out->isEligibleForInstantiation( n ) ){
-      d_inelig[n] = true;
+      d_inelig.insert(n);
       return;
     }
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       computeProgVars( n[i] );
       if( d_inelig.find( n[i] )!=d_inelig.end() ){
-        d_inelig[n] = true;
-      }
-      for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
-        d_prog_var[n][it->first] = true;
-      }
-      //selectors applied to program variables are also variables
-      if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){
-        d_prog_var[n][n] = true;
+        d_inelig.insert(n);
       }
+      // all variables in child are contained in this
+      d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
+    }
+    // selectors applied to program variables are also variables
+    if (n.getKind() == APPLY_SELECTOR_TOTAL
+        && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
+    {
+      d_prog_var[n].insert(n);
+    }
+    if (n.getKind() == kind::CHOICE)
+    {
+      d_prog_var.erase(n[0][0]);
     }
   }
 }
@@ -113,7 +124,8 @@ void CegInstantiator::unregisterInstantiationVariable( Node v ) {
 bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
-    bool needsPostprocess = false;
+    bool needsPostprocess =
+        sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty();
     std::vector< Instantiator * > pp_inst;
     std::map< Instantiator *, Node > pp_inst_to_var;
     std::vector< Node > lemmas;
@@ -522,8 +534,13 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
 bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   if( !non_basic.empty() ){
-    for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){
-      if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){
+    for (std::unordered_set<Node, NodeHashFunction>::iterator it =
+             d_prog_var[n].begin();
+         it != d_prog_var[n].end();
+         ++it)
+    {
+      if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end())
+      {
         return false;
       }
     }
@@ -699,6 +716,7 @@ bool CegInstantiator::check() {
   for( unsigned r=0; r<2; r++ ){
     SolvedForm sf;
     d_stack_vars.clear();
+    d_bound_var_index.clear();
     //try to add an instantiation
     if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){
       return true;
@@ -979,6 +997,26 @@ Node CegInstantiator::getModelValue( Node n ) {
   return d_qe->getModel()->getValue( n );
 }
 
+Node CegInstantiator::getBoundVariable(TypeNode tn)
+{
+  unsigned index = 0;
+  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb =
+      d_bound_var_index.find(tn);
+  if (itb != d_bound_var_index.end())
+  {
+    index = itb->second;
+  }
+  d_bound_var_index[tn] = index + 1;
+  while (index >= d_bound_var[tn].size())
+  {
+    std::stringstream ss;
+    ss << "x" << index;
+    Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn);
+    d_bound_var[tn].push_back(x);
+  }
+  return d_bound_var[tn][index];
+}
+
 void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
   if( n.getKind()==FORALL ){
     d_is_nested_quant = true;
@@ -1010,6 +1048,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   //Assert( d_vars.empty() );
   d_vars.clear();
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+  d_vars_set.insert(ce_vars.begin(), ce_vars.end());
 
   //determine variable order: must do Reals before Ints
   if( !d_vars.empty() ){
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 0808b5ed0..1e59bfb43 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -40,8 +40,11 @@ public:
 
 class Instantiator;
 
-//stores properties for a variable to solve for in CEGQI
-//  For LIA, this includes the coefficient of the variable, and the bound type for the variable
+/** Term Properties
+ * stores properties for a variable to solve for in CEGQI
+ *  For LIA, this includes the coefficient of the variable, and the bound type
+ * for the variable.
+ */
 class TermProperties {
 public:
   TermProperties() : d_type(0) {}
@@ -76,9 +79,10 @@ public:
   }
 };
 
-//Solved form
-//  This specifies a substitution:
-//  { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| }
+/** Solved form
+ *  This specifies a substitution:
+ *  { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| }
+ */
 class SolvedForm {
 public:
   // list of variables
@@ -89,7 +93,7 @@ public:
   std::vector< TermProperties > d_props;
   // the variables that have non-basic information regarding how they are substituted
   //   an example is for linear arithmetic, we store "substitution with coefficients".
-  std::vector< Node > d_non_basic;
+  std::vector<Node> d_non_basic;
   // push the substitution pv_prop.getModifiedTerm(pv) -> n
   void push_back( Node pv, Node n, TermProperties& pv_prop ){
     d_vars.push_back( pv );
@@ -134,35 +138,105 @@ public:
   }
 };
 
+/** Ceg instantiator
+ *
+ * This class manages counterexample-guided quantifier instantiation
+ * for a single quantified formula.
+ */
 class CegInstantiator {
-private:
-  QuantifiersEngine * d_qe;
-  CegqiOutput * d_out;
+ private:
+  /** quantified formula associated with this instantiator */
+  QuantifiersEngine* d_qe;
+  /** output channel of this instantiator */
+  CegqiOutput* d_out;
+  /** whether we are using delta for virtual term substitution
+    * (for quantified LRA).
+    */
   bool d_use_vts_delta;
+  /** whether we are using infinity for virtual term substitution
+    * (for quantified LRA).
+    */
   bool d_use_vts_inf;
-  //program variable contains cache
-  std::map< Node, std::map< Node, bool > > d_prog_var;
-  std::map< Node, bool > d_inelig;
-  //current assertions
-  std::map< TheoryId, std::vector< Node > > d_curr_asserts;
-  std::map< Node, std::vector< Node > > d_curr_eqc;
-  std::map< TypeNode, std::vector< Node > > d_curr_type_eqc;
-  //auxiliary variables
-  std::vector< Node > d_aux_vars;
-  // relevant theory ids
-  std::vector< TheoryId > d_tids;
-  //literals to equalities for aux vars
-  std::map< Node, std::map< Node, Node > > d_aux_eq;
-  //the CE variables
-  std::vector< Node > d_vars;
-  //index of variables reported in instantiation
-  std::vector< unsigned > d_var_order_index;
-  //atoms of the CE lemma
+  /** cache from nodes to the set of variables it contains
+    * (from the quantified formula we are instantiating).
+    */
+  std::unordered_map<Node,
+                     std::unordered_set<Node, NodeHashFunction>,
+                     NodeHashFunction>
+      d_prog_var;
+  /** cache of the set of terms that we have established are
+   * ineligible for instantiation.
+    */
+  std::unordered_set<Node, NodeHashFunction> d_inelig;
+  /** current assertions per theory */
+  std::map<TheoryId, std::vector<Node> > d_curr_asserts;
+  /** map from representatives to the terms in their equivalence class */
+  std::map<Node, std::vector<Node> > d_curr_eqc;
+  /** map from types to representatives of that type */
+  std::map<TypeNode, std::vector<Node> > d_curr_type_eqc;
+  /** auxiliary variables
+   * These variables include the result of removing ITE
+   * terms from the quantified formula we are processing.
+   * These variables must be eliminated from constraints
+   * as a preprocess step to check().
+   */
+  std::vector<Node> d_aux_vars;
+  /** relevant theory ids
+   * A list of theory ids that contain at least one
+   * constraint in the body of the quantified formula we
+   * are processing.
+   */
+  std::vector<TheoryId> d_tids;
+  /** literals to equalities for aux vars
+   * This stores entries of the form
+   *   L -> ( k -> t )
+   * where
+   *   k is a variable in d_aux_vars,
+   *   L is a literal that if asserted implies that our
+   *    instantiation should map { k -> t }.
+   * For example, if a term of the form
+   *   ite( C, t1, t2 )
+   * was replaced by k, we get this (top-level) assertion:
+   *   ite( C, k=t1, k=t2 )
+   * The vector d_aux_eq contains the exact form of
+   * the literals in the above constraint that they would
+   * appear in assertions, meaning d_aux_eq may contain:
+   *   t1=k -> ( k -> t1 )
+   *   t2=k -> ( k -> t2 )
+   * where t1=k and t2=k are the rewritten form of
+   * k=t1 and k=t2 respectively.
+   */
+  std::map<Node, std::map<Node, Node> > d_aux_eq;
+  /** the variables we are instantiating
+   * These are the inst constants of the quantified formula
+   * we are processing.
+   */
+  std::vector<Node> d_vars;
+  /** set form of d_vars */
+  std::unordered_set<Node, NodeHashFunction> d_vars_set;
+  /** index of variables reported in instantiation */
+  std::vector<unsigned> d_var_order_index;
+  /** are we handled a nested quantified formula? */
   bool d_is_nested_quant;
-  std::vector< Node > d_ce_atoms;
-  //collect atoms
-  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
-private:
+  /** the atoms of the CE lemma */
+  std::vector<Node> d_ce_atoms;
+  /** cache bound variables for type returned
+   * by getBoundVariable(...).
+   */
+  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
+      d_bound_var;
+  /** current index of bound variables for type.
+   * The next call to getBoundVariable(...) for
+   * type tn returns the d_bound_var_index[tn]^th
+   * element of d_bound_var[tn], or a fresh variable
+   * if not in bounds.
+   */
+  std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
+      d_bound_var_index;
+  /** collect atoms */
+  void collectCeAtoms(Node n, std::map<Node, bool>& visited);
+
+ private:
   //map from variables to their instantiators
   std::map< Node, Instantiator * > d_instantiator;
   //cache of current substitutions tried between register/unregister
@@ -170,7 +244,7 @@ private:
   std::map< Node, unsigned > d_curr_index;
   //stack of temporary variables we are solving (e.g. subfields of datatypes)
   std::vector< Node > d_stack_vars;
-  //used instantiators
+  /** for each variable, the instantiator used for that variable */
   std::map< Node, Instantiator * > d_active_instantiators;
   //register variable
   void registerInstantiationVariable( Node v, unsigned index );
@@ -224,10 +298,16 @@ public:
   CegqiOutput * getOutput() { return d_out; }
   //get quantifiers engine
   QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
-
-//interface for instantiators
-public:
+  //------------------------------interface for instantiators
+  /** push stack variable
+   * This adds a new variable to solve for in the stack
+   * of variables we are processing. This stack is only
+   * used for datatypes, where e.g. the DtInstantiator
+   * solving for a list x may push the stack "variables"
+   * head(x) and tail(x).
+   */
   void pushStackVariable( Node v );
+  /** pop stack variable */
   void popStackVariable();
   /** do add instantiation increment
    *
@@ -248,16 +328,27 @@ public:
                              SolvedForm& sf,
                              unsigned effort,
                              bool revertOnSuccess = false);
+  /** get the current model value of term n */
   Node getModelValue( Node n );
-public:
+  /** get bound variable for type
+   *
+   * This gets the next (canonical) bound variable of
+   * type tn. This can be used for instance when
+   * constructing instantiations that involve choice expressions.
+   */
+  Node getBoundVariable(TypeNode tn);
+  //------------------------------end interface for instantiators
   unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
   Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
-  // is eligible
+  /** is n a term that is eligible for instantiation? */
   bool isEligible( Node n );
-  // has variable
+  /** does n have variable pv? */
   bool hasVariable( Node n, Node pv );
+  /** are we using delta for LRA virtual term substitution? */
   bool useVtsDelta() { return d_use_vts_delta; }
+  /** are we using infinity for LRA virtual term substitution? */
   bool useVtsInfinity() { return d_use_vts_inf; }
+  /** are we processing a nested quantified formula? */
   bool hasNestedQuantification() { return d_is_nested_quant; }
 };
 
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 60566da1b..756c63cb4 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -846,16 +846,21 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N
 }
 
 // this class can be used to query the model value through the CegInstaniator class
-class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery {
-public:
-  CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) : 
-    BvInverterModelQuery(), d_ci( ci ){}
-  ~CegInstantiatorBvInverterModelQuery(){}
-  // get the model value of n
+class CegInstantiatorBvInverterQuery : public BvInverterQuery
+{
+ public:
+  CegInstantiatorBvInverterQuery(CegInstantiator* ci)
+      : BvInverterQuery(), d_ci(ci)
+  {
+  }
+  ~CegInstantiatorBvInverterQuery() {}
+  /** return the model value of n */
   Node getModelValue( Node n ) {
     return d_ci->getModelValue( n );
   }
-protected:
+  /** get bound variable of type tn */
+  Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); }
+ protected:
   // pointer to class that is able to query model values
   CegInstantiator * d_ci;
 };
@@ -891,10 +896,12 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf,
   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 );
   if( !slit.isNull() ){
-    CegInstantiatorBvInverterModelQuery m( ci );
+    CegInstantiatorBvInverterQuery m(ci);
     unsigned iid = d_inst_id_counter;
+    Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
     Node inst = d_inverter->solve_bv_lit( sv, slit, path, &m, d_inst_id_to_status[iid] );
     if( !inst.isNull() ){
       inst = Rewriter::rewrite(inst);
@@ -1010,7 +1017,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf,
   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( pv, lit );
+    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 ){
@@ -1139,32 +1146,10 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf,
   return false;
 }
 
-
-bool BvInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
-  // we may need to post-process the instantiation since inversion skolems need to be finalized
-  // TODO : technically skolem functions can appear in datatypes with bit-vector fields. We need to eliminate them there too.
-  return true;
-}
-
-bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) {
-  Trace("cegqi-bv") << "BvInstantiator::postProcessInstantiation " << pv << std::endl;
-  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();
-  Trace("cegqi-bv") << "  postprocess : " << pv << " -> " << sf.d_subs[index] << std::endl;
-  // eliminate skolem functions from the substitution
-  unsigned prev_lem_size = lemmas.size();
-  sf.d_subs[index] = d_inverter->eliminateSkolemFunctions( sf.d_subs[index], lemmas );
-  if( Trace.isOn("cegqi-bv") ){
-    Trace("cegqi-bv") << "  got : " << pv << " -> " << sf.d_subs[index] << std::endl;
-    for( unsigned i=prev_lem_size; i<lemmas.size(); i++ ){
-      Trace("cegqi-bv") << "  side condition : " << lemmas[i] << std::endl;
-    }
-  }
-
-  return true;
-}
-  
-Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) {
+Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
+                                                Node pv,
+                                                Node lit)
+{
   NodeManager* nm = NodeManager::currentNM();
   // result of rewriting the visited term
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
@@ -1180,10 +1165,34 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) {
     it = visited.find(cur);
 
     if (it == visited.end()) {
-      visited[cur] = Node::null();
-      visit.push(cur);
-      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
-        visit.push(cur[i]);
+      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());
+        TNode var = cur[0][0];
+        Node sbody = cur[1].substitute(var, 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 make a separate call to
+        // rewriteAssertionForSolvePv here,
+        // where the recursion depth is the maximum
+        // depth of nested choice expressions.
+        Node rsbody = rewriteAssertionForSolvePv(ci, pv, sbody);
+        visited[cur] =
+            nm->mkNode(CHOICE, nm->mkNode(BOUND_VAR_LIST, bv), rsbody);
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push(cur);
+        for (unsigned i = 0; i < cur.getNumChildren(); i++)
+        {
+          visit.push(cur[i]);
+        }
       }
     } else if (it->second.isNull()) {
       Node ret;
@@ -1201,24 +1210,11 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) {
         children.push_back(it->second);
         contains_pv = contains_pv || visited_contains_pv[cur[i]];
       }
-      
-      // [1] rewrite cases of non-invertible operators
-      
-      // if cur is urem( x, y ) where x contains pv but y does not, then
-      // rewrite urem( x, y ) ---> x - udiv( x, y )*y
-      if (cur.getKind()==BITVECTOR_UREM_TOTAL) {
-        if( visited_contains_pv[cur[0]] && !visited_contains_pv[cur[1]] ){
-          ret = nm->mkNode( BITVECTOR_SUB, children[0], 
-                  nm->mkNode( BITVECTOR_MULT,
-                    nm->mkNode( BITVECTOR_UDIV_TOTAL, children[0], children[1] ),
-                    children[1] ) );
-        }
-      }
-      
-      // [2] try to rewrite non-linear literals -> linear literals
-      
-      
-      // return original if the above steps do not produce a result
+
+      // 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);
@@ -1236,3 +1232,32 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) {
   return visited[lit];
 }
 
+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 is urem( x, y ) where x contains pv but y does not, then
+  // rewrite urem( x, y ) ---> x - udiv( x, y )*y
+  if (n.getKind() == BITVECTOR_UREM_TOTAL)
+  {
+    if (contains_pv[n[0]] && !contains_pv[n[1]])
+    {
+      return nm->mkNode(
+          BITVECTOR_SUB,
+          children[0],
+          nm->mkNode(BITVECTOR_MULT,
+                     nm->mkNode(BITVECTOR_UDIV_TOTAL, children[0], children[1]),
+                     children[1]));
+    }
+  }
+
+  // [2] try to rewrite non-linear literals -> linear literals
+
+  return Node::null();
+}
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 9f47e7211..30dd1bffa 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -101,7 +101,23 @@ private:
   /** rewrite assertion for solve pv
   * returns a literal that is equivalent to lit that leads to best solved form for pv
   */
-  Node rewriteAssertionForSolvePv( Node pv, Node lit );
+  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.
@@ -121,8 +137,6 @@ private:
                         Node alit, unsigned effort);
   bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
                          unsigned effort);
-  bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas );
   bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
   std::string identify() const { return "Bv"; }
 };