Initial infrastructure for BV instantiation via word-level inversions. (#1056)

* Initial infrastructure for BV instantiation via word-level inversions.

* Minor clean up.

* Change visited to unordered set.

4 files changed, 313 insertions, 29 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 05e86c9e8..db283ccfc 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -11,7 +11,7 @@
  **
  ** \brief Implementation of counterexample-guided quantifier instantiation
  **/
- 
+
 #include "theory/quantifiers/ceg_instantiator.h"
 #include "theory/quantifiers/ceg_t_instantiator.h"
 
@@ -131,7 +131,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
           postProcessSuccess = false;
           break;
         }
-      } 
+      }
       if( postProcessSuccess ){
         return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars );
       }else{
@@ -294,9 +294,13 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
               Node lit = ita->second[j];
               if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){
                 lits.push_back( lit );
-                if( vinst->processAssertion( this, sf, pv, lit, effort ) ){
-                  return true;
-                }
+                //if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){
+                  // apply substitutions check if eligible and contains pv
+                  // TODO
+                  if( vinst->processAssertion( this, sf, pv, lit, effort ) ){
+                    return true;
+                  }
+                //}
               }
             }
           }
@@ -326,7 +330,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
       }
     }
     Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
-    if( is_cv ){  
+    if( is_cv ){
       d_stack_vars.push_back( pv );
     }
     d_active_instantiators.erase( pv );
@@ -509,7 +513,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) );
     }
   }
-  
+
   if( !req_coeff ){
     Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     if( n!=nret ){
@@ -995,7 +999,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
         Node v = lems[i][0];
         d_aux_eq[rlem][v] = lems[i][1];
          Trace("cbqi-debug") << "  " << rlem << " implies " << v << " = " << lems[i][1] << std::endl;
-      } 
+      }
     }*/
     lems[i] = rlem;
   }
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index aed1be3a4..c260486ff 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -41,14 +41,27 @@ public:
 class Instantiator;
 
 
+//TODO: refactor pv_coeff to pv_prop throughout
+//generic class that stores properties for a variable to solve for in CEGQI
+class TermProperties {
+public:
+  TermProperties() : d_type(-1) {}
+  int d_type;
+  // for arithmetic
+  Node d_coeff;
+};
+
 //solved form, involves substitution with coefficients
 class SolvedForm {
 public:
   std::vector< Node > d_vars;
   std::vector< Node > d_subs;
+  //TODO: refactor below coeff -> prop;
   std::vector< Node > d_coeff;
   std::vector< int > d_btyp;
+  //std::vector< TermProperties > d_props;
   std::vector< Node > d_has_coeff;
+  //std::vector< Node > d_has_prop;
   Node d_theta;
   void copy( SolvedForm& sf ){
     d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() );
@@ -105,7 +118,7 @@ private:
   bool d_is_nested_quant;
   std::vector< Node > d_ce_atoms;
   //collect atoms
-  void collectCeAtoms( Node n, std::map< Node, bool >& visited );  
+  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
 private:
   //map from variables to their instantiators
   std::map< Node, Instantiator * > d_instantiator;
@@ -114,7 +127,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 
+  //used instantiators
   std::map< Node, Instantiator * > d_active_instantiators;
   //register variable
   void registerInstantiationVariable( Node v, unsigned index );
@@ -141,7 +154,7 @@ public:
   CegqiOutput * getOutput() { return d_out; }
   //get quantifiers engine
   QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
-  
+
 //interface for instantiators
 public:
   void pushStackVariable( Node v );
@@ -157,9 +170,9 @@ public:
 public:
   unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
   Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
-  // is eligible 
+  // is eligible
   bool isEligible( Node n );
-  // has variable 
+  // has variable
   bool hasVariable( Node n, Node pv );
   bool useVtsDelta() { return d_use_vts_delta; }
   bool useVtsInfinity() { return d_use_vts_inf; }
@@ -167,7 +180,6 @@ public:
 };
 
 
-
 // an instantiator for individual variables
 //   will make calls into CegInstantiator::doAddInstantiationInc
 class Instantiator {
@@ -178,29 +190,32 @@ public:
   Instantiator( QuantifiersEngine * qe, TypeNode tn );
   virtual ~Instantiator(){}
   virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {}
-  
+
   //called when pv_coeff * pv = n, and n is eligible for instantiation
   virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
   //eqc is the equivalence class of pv
   virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
-  
-  //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv
+
   virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv
+  //  returns true if an instantiation was successfully added via a recursive call
   virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
-  
-  //called when assertion lit holds.  note that lit is unsubstituted, first must substitute/solve/check eligible
+
   virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
+  //called when assertion lit holds.  note that lit is unsubstituted, first must substitute/solve/check eligible
+  //  returns true if an instantiation was successfully added via a recursive call
   virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
   virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; }
-  
+
   //do we allow instantiation for the model value of pv
   virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
   virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; }
-  
+
   //do we need to postprocess the solved form? did we successfully postprocess
   virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
   virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
-  
+
   /** Identify this module (for debugging) */
   virtual std::string identify() const { return "Default"; }
 };
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index cd541a2a6..fa7dbabab 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -11,7 +11,7 @@
  **
  ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation
  **/
- 
+
 #include "theory/quantifiers/ceg_t_instantiator.h"
 
 #include "options/quantifiers_options.h"
@@ -258,6 +258,13 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N
   return false;
 }
 
+bool ArithInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  Node atom = lit.getKind()==NOT ? lit[0] : lit;
+  bool pol = lit.getKind()!=NOT;
+  //arithmetic inequalities and disequalities
+  return atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() );
+}
+
 bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
   Trace("cbqi-inst-debug2") << "  look at " << lit << std::endl;
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
@@ -583,7 +590,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
     }
     //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("cbqi-bound") << "Try non-optimal bounds..." << std::endl;
@@ -757,8 +764,8 @@ void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsi
 bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
   if( options::quantEprMatching() ){
     Assert( pv_coeff.isNull() );
-    d_equal_terms.push_back( n ); 
-    return false;  
+    d_equal_terms.push_back( n );
+    return false;
   }else{
     return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
   }
@@ -814,7 +821,7 @@ struct sortEqTermsMatch {
   }
 };
 
-    
+
 bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
   if( options::quantEprMatching() ){
     //heuristic for best matching constant
@@ -835,7 +842,179 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N
   return false;
 }
 
-bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+Node BvInverter::getSolveVariable( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator its = d_solve_var.find( tn );
+  if( its==d_solve_var.end() ){
+    Node k = NodeManager::currentNM()->mkSkolem( "s", tn );
+    d_solve_var[tn] = k;
+    return k;
+  }else{
+    return its->second;
+  }
+}
+
+Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited ) {
+  if( visited.find( lit )==visited.end() ){
+    visited.insert( lit );
+    if( lit==pv ){
+      return sv;
+    }else{
+      unsigned rmod = 0; // TODO : randomize?
+      for( unsigned i=0; i<lit.getNumChildren(); i++ ){
+        unsigned ii = ( i + rmod )%lit.getNumChildren();
+        Node litc = getPathToPv( lit[ii], pv, sv, path, visited );
+        if( !litc.isNull() ){
+          // path is outermost term index last
+          path.push_back( ii );
+          std::vector< Node > children;
+          if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){
+            children.push_back( lit.getOperator() );
+          }
+          for( unsigned j=0; j<lit.getNumChildren(); j++ ){
+            children.push_back( j==ii ? litc : lit[j] );
+          }
+          return NodeManager::currentNM()->mkNode( lit.getKind(), children );
+        }
+      }
+    }
+  }
+  return Node::null();
+}
+
+Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path ) {
+  std::unordered_set< TNode, TNodeHashFunction > visited;
+  Node slit = getPathToPv( lit, pv, sv, path, visited );
+  if( !slit.isNull() ){
+    // substitute pvs for the other occurrences of pv
+    TNode tpv = pv;
+    TNode tpvs = pvs;
+    slit = slit.substitute( tpv, tpvs );
+  }
+  return slit;
+}
+
+Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path,
+                                      BvInverterModelQuery * m, BvInverterStatus& status ) {
+  while( !path.empty() ){
+    unsigned index = path.back();
+    Assert( index<sv_t.getNumChildren() );
+    path.pop_back();
+    Kind k = sv_t.getKind();
+    // inversions
+    if( k==BITVECTOR_PLUS ){
+      t = NodeManager::currentNM()->mkNode( BITVECTOR_SUB, t, sv_t[1-index] );
+    }else if( k==BITVECTOR_SUB ){
+      t = NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] );
+    //}else if( k==BITVECTOR_MULT ){
+      // TODO
+    }else if( k==BITVECTOR_NEG || k==BITVECTOR_NOT ){
+      t = NodeManager::currentNM()->mkNode( k, t );
+    //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){
+      // TODO
+    //}else if( k==BITVECTOR_CONCAT ){
+      // TODO
+    //}else if( k==BITVECTOR_SHL || k==BITVECTOR_LSHR ){
+      // TODO
+    //}else if( k==BITVECTOR_ASHR ){
+      // TODO
+    }else{
+      Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k << ", from " << sv_t << std::endl;
+      return Node::null();
+    }
+    sv_t = sv_t[index];
+  }
+  Assert( sv_t==sv );
+  // finalize based on the kind of constraint
+  //TODO
+  if( rk==EQUAL ){
+    return t;
+  }else{
+    Trace("bv-invert") << "bv-invert : Unknown relation kind for bit-vector literal " << rk << std::endl;
+    return Node::null();
+  }
+}
+
+Node BvInverter::solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path,
+                               BvInverterModelQuery * m, BvInverterStatus& status ){
+  Assert( !path.empty() );
+  unsigned index = path.back();
+  Assert( index<lit.getNumChildren() );
+  path.pop_back();
+  Kind k = lit.getKind();
+  if( k==NOT ){
+    Assert( index==0 );
+    return solve_bv_lit( sv, lit[index], !pol, path, m, status );
+  }else if( k==EQUAL ){
+    return solve_bv_constraint( sv, lit[index], lit[1-index], k, pol, path, m, status );
+  }else if( k==BITVECTOR_ULT || k==BITVECTOR_ULE || k==BITVECTOR_SLT || k==BITVECTOR_SLE ){
+    if( !pol ){
+      if( k==BITVECTOR_ULT ){
+        k = index==1 ? BITVECTOR_ULE : BITVECTOR_UGE;
+      }else if( k==BITVECTOR_ULE ){
+        k = index==1 ? BITVECTOR_ULT : BITVECTOR_UGT;
+      }else if( k==BITVECTOR_SLT ){
+        k = index==1 ? BITVECTOR_SLE : BITVECTOR_SGE;
+      }else{
+        Assert( k==BITVECTOR_SLE );
+        k = index==1 ? BITVECTOR_SLT : BITVECTOR_SGT;
+      }
+    }else if( index==1 ){
+      if( k==BITVECTOR_ULT ){
+        k = BITVECTOR_UGT;
+      }else if( k==BITVECTOR_ULE ){
+        k = BITVECTOR_UGE;
+      }else if( k==BITVECTOR_SLT ){
+        k = BITVECTOR_SGT;
+      }else{
+        Assert( k==BITVECTOR_SLE );
+        k = BITVECTOR_SGE;
+      }
+    }
+    return solve_bv_constraint( sv, lit[index], lit[1-index], k, true, path, m, status );
+  }else{
+    Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector literal " << lit << std::endl;
+  }
+  return Node::null();
+}
+
+void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+  d_inst_id_counter = 0;
+  d_var_to_inst_id.clear();
+  d_inst_id_to_term.clear();
+  d_inst_id_to_status.clear();
+}
+
+class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery {
+protected:
+  CegInstantiator * d_ci;
+public:
+  CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) : 
+    BvInverterModelQuery(), d_ci( ci ){}
+  Node getModelValue( Node n ) {
+    return d_ci->getModelValue( n );
+  }
+};
+
+void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  // find path to pv
+  std::vector< unsigned > path;
+  Node sv = d_inverter.getSolveVariable( pv.getType() );
+  Node pvs = ci->getModelValue( pv );
+  Node slit = d_inverter.getPathToPv( lit, pv, sv, pvs, path );
+  if( !slit.isNull() ){
+    CegInstantiatorBvInverterModelQuery m( ci );
+    unsigned iid = d_inst_id_counter;
+    Node inst = d_inverter.solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] );
+    if( !inst.isNull() ){
+      // 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_counter++;
+    }else{
+      // cleanup information
+      d_inst_id_to_status.erase( iid );
+    }
+  }
   /*   TODO: algebraic reasoning for bitvector instantiation
   if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){
     for( unsigned t=0; t<2; t++ ){
@@ -849,7 +1028,7 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod
             if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
               uval = atom[1-t];
             }else{
-              uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], 
+              uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t],
                                                        bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
             }
             if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){
@@ -861,8 +1040,35 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod
     }
   }
   */
+}
+
+bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+  //processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort );
+  return false;
+}
+
+bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  return true;
+}
 
+bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  //processLiteral( ci, sf, pv, lit, effort );
   return false;
 }
 
+bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) {
+  std::map< Node, std::vector< unsigned > >::iterator iti = d_var_to_inst_id.find( pv );
+  if( iti!=d_var_to_inst_id.end() ){
+    // get inst id list
+    Trace("bv-inst") << "bv-inst : " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl;
+    for( unsigned j=0; j<iti->second.size(); j++ ){
+      Trace("bv-inst") << "[" << j << "] : " << iti->second[j];
+      // print information about solved status TODO
+
+      Trace("bv-inst") << std::endl;
+    }
+  }
+
+  return false;
+}
 
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 787c2547a..dfb7921c8 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -20,6 +20,8 @@
 
 #include "theory/quantifiers/ceg_instantiator.h"
 
+#include <unordered_set>
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
@@ -40,6 +42,7 @@ public:
   bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
   bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
   bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
   bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
   bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort );
   bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
@@ -76,11 +79,67 @@ public:
   std::string identify() const { return "Epr"; }
 };
 
+
+// virtual class for model queries
+class BvInverterModelQuery {
+public:
+  BvInverterModelQuery(){}
+  virtual Node getModelValue( Node n ) = 0;
+};
+
+// class for storing information about the solved status
+class BvInverterStatus {
+public:
+  BvInverterStatus() : d_status(0) {}
+  int d_status;
+  std::vector< Node > d_conds;
+};
+
+// inverter class
+// TODO : move to theory/bv/ if generally useful?
+class BvInverter {
+private:
+  std::map< TypeNode, Node > d_solve_var;
+  Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited );
+public:
+  // get dummy fresh variable of type tn, used as argument for sv 
+  Node getSolveVariable( TypeNode tn );
+  // Get path to pv in lit, replace that occurrence by sv and all others by pvs.
+  // e.g. if return value R is non-null, then:
+  //   lit.path = pv
+  //   R.path = sv
+  //   R.path' = pvs for all lit.path' = pv, where path' != path
+  Node getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path );
+public:
+  // solve for sv in constraint ( (pol ? _ : not) sv_t <rk> t ), where sv_t.path = sv
+  // status accumulates side conditions
+  Node solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path,
+                            BvInverterModelQuery * m, BvInverterStatus& status );
+  // solve for sv in lit, where lit.path = sv
+  // status accumulates side conditions
+  Node solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path,
+                     BvInverterModelQuery * m, BvInverterStatus& status );
+};
+
 class BvInstantiator : public Instantiator {
+private:
+  BvInverter d_inverter;
+  unsigned d_inst_id_counter;
+  std::map< Node, std::vector< unsigned > > d_var_to_inst_id;
+  std::map< unsigned, Node > d_inst_id_to_term;
+  std::map< unsigned, BvInverterStatus > d_inst_id_to_status;
+private:
+  void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
 public:
   BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~BvInstantiator(){}
+  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
   bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
+  bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort );
   bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
   std::string identify() const { return "Bv"; }
 };