Cegqi refactor substitutions (#1129)

This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).

Improvements to the code:

(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).

This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)

3 files changed, 330 insertions, 239 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 42394122e..9375ffb74 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -123,8 +123,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
     }
     if( needsPostprocess ){
       //must make copy so that backtracking reverts sf
-      SolvedForm sf_tmp;
-      sf_tmp.copy( sf );
+      SolvedForm sf_tmp = sf;
       bool postProcessSuccess = true;
       for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){
         if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){
@@ -293,13 +292,18 @@ 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->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;
+                if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){
+                  // apply substitutions
+                  Node slit = applySubstitutionToLiteral( lit, sf );
+                  if( !slit.isNull() ){
+                    // check if contains pv
+                    if( hasVariable( slit, pv ) ){
+                      if( vinst->processAssertion( this, sf, pv, slit, effort ) ){
+                       return true;
+                      }
+                    }
                   }
-                //}
+                }
               }
             }
           }
@@ -356,10 +360,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
         Trace("cbqi-inst") << " ";
       }
       Trace("cbqi-inst") << sf.d_subs.size() << ": ";
-      if( !pv_prop.d_coeff.isNull() ){
-        Trace("cbqi-inst") << pv_prop.d_coeff << " * ";
-      }
-      Trace("cbqi-inst") << pv << " -> " << n << std::endl;
+      Node mod_pv = pv_prop.getModifiedTerm( pv );
+      Trace("cbqi-inst") << mod_pv << " -> " << n << std::endl;
       Assert( n.getType().isSubtypeOf( pv.getType() ) );
     }
     //must ensure variables have been computed for n
@@ -372,17 +374,17 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
     std::vector< Node > a_var;
     a_var.push_back( pv );
     std::vector< TermProperties > a_prop;
-    std::vector< Node > a_has_coeff;
-    if( !pv_prop.d_coeff.isNull() ){
-      a_prop.push_back( pv_prop );
-      a_has_coeff.push_back( pv );
+    a_prop.push_back( pv_prop );
+    std::vector< Node > a_non_basic;
+    if( !pv_prop.isBasic() ){
+      a_non_basic.push_back( pv );
     }
     bool success = true;
     std::map< int, Node > prev_subs;
     std::map< int, TermProperties > prev_prop;
     std::map< int, Node > prev_sym_subs;
-    std::vector< Node > new_has_coeff;
-    Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
+    std::vector< Node > new_non_basic;
+    Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
     for( unsigned j=0; j<sf.d_subs.size(); j++ ){
       Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
       Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
@@ -391,20 +393,21 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
         TNode tv = pv;
         TNode ts = n;
         TermProperties a_pv_prop;
-        Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_prop, a_has_coeff, a_var, a_pv_prop, true );
+        Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_var, a_subs, a_prop, a_non_basic, a_pv_prop, true );
         if( !new_subs.isNull() ){
           sf.d_subs[j] = new_subs;
-          if( !a_pv_prop.d_coeff.isNull() ){
+          // the substitution apply to this term resulted in a non-basic substitution relationship
+          if( !a_pv_prop.isBasic() ){
             prev_prop[j] = sf.d_props[j];
-            if( sf.d_props[j].d_coeff.isNull() ){
-              Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() );
-              //now has coefficient
-              new_has_coeff.push_back( sf.d_vars[j] );
-              sf.d_has_coeff.push_back( sf.d_vars[j] );
-              sf.d_props[j].d_coeff = a_pv_prop.d_coeff;
-            }else{
-              sf.d_props[j].d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_props[j].d_coeff, a_pv_prop.d_coeff ) );
+            // if previously was basic, becomes non-basic
+            if( sf.d_props[j].isBasic() ){
+              Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() );
+              new_non_basic.push_back( sf.d_vars[j] );
+              sf.d_non_basic.push_back( sf.d_vars[j] );
             }
+            // now combine the property
+            sf.d_props[j].combineProperty( a_pv_prop );
+            Assert( !sf.d_props[j].isBasic() );
           }
           if( sf.d_subs[j]!=prev_subs[j] ){
             computeProgVars( sf.d_subs[j] );
@@ -423,21 +426,9 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
     if( success ){
       Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
       sf.push_back( pv, n, pv_prop );
-      Node prev_theta = sf.d_theta;
-      Node new_theta = sf.d_theta;
-      if( !pv_prop.d_coeff.isNull() ){
-        if( new_theta.isNull() ){
-          new_theta = pv_prop.d_coeff;
-        }else{
-          new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_prop.d_coeff );
-          new_theta = Rewriter::rewrite( new_theta );
-        }
-      }
-      sf.d_theta = new_theta;
       Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
       unsigned i = d_curr_index[pv];
       success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort );
-      sf.d_theta = prev_theta;
       if( !success ){
         Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
         sf.pop_back( pv, n, pv_prop );
@@ -454,8 +445,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv
       for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){
         sf.d_props[it->first] = it->second;
       }
-      for( unsigned i=0; i<new_has_coeff.size(); i++ ){
-        sf.d_has_coeff.pop_back();
+      for( unsigned i=0; i<new_non_basic.size(); i++ ){
+        sf.d_non_basic.pop_back();
       }
       return false;
     }
@@ -493,33 +484,33 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector
   return ret;
 }
 
-Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff,
-                                         std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff ) {
+bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
-  Assert( n==Rewriter::rewrite( n ) );
-  bool req_coeff = false;
-  if( !has_coeff.empty() ){
+  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( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){
-        req_coeff = true;
-        break;
+      if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){
+        return false;
       }
     }
   }
+  return true;
+}
+
+Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
+                                         std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) {
+  computeProgVars( n );
+  Assert( n==Rewriter::rewrite( n ) );
+  bool is_basic = canApplyBasicSubstitution( n, non_basic );
   if( Trace.isOn("cegqi-si-apply-subs-debug") ){
-    Trace("cegqi-si-apply-subs-debug") << "req_coeff = " << req_coeff << "  " << tn << std::endl;
+    Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
     for( unsigned i=0; i<subs.size(); i++ ){
       Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
       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 ){
-      nret = Rewriter::rewrite( nret );
-    }
-    return nret;
+  Node nret;
+  if( is_basic ){
+    nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
   }else{
     if( !tn.isInteger() ){
       //can do basic substitution instead with divisions
@@ -529,7 +520,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
         if( !prop[i].d_coeff.isNull() ){
           Assert( vars[i].getType().isInteger() );
           Assert( prop[i].d_coeff.isConst() );
-          Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
+          Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) );
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
           nn =  Rewriter::rewrite( nn );
           nsubs.push_back( nn );
@@ -537,11 +528,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           nsubs.push_back( subs[i] );
         }
       }
-      Node nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
-      if( n!=nret ){
-        nret = Rewriter::rewrite( nret );
-      }
-      return nret;
+      nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() );
     }else if( try_coeff ){
       //must convert to monomial representation
       std::map< Node, Node > msum;
@@ -596,14 +583,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             children.push_back( c );
             Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
           }
-          Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
-          nret = Rewriter::rewrite( nret );
+          Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+          nretc = Rewriter::rewrite( nretc );
           //ensure that nret does not contain vars
-          if( !TermDb::containsTerms( nret, vars ) ){
+          if( !TermDb::containsTerms( nretc, vars ) ){
             //result is ( nret / pv_prop.d_coeff )
-            return nret;
+            nret = nretc;
           }else{
-            Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nret << " contains free variable." << std::endl;
+            Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
           }
         }else{
           //implies that we have a monomial that has a free variable
@@ -613,11 +600,61 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
         Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
       }
     }
-    // failed to apply the substitution
-    return Node::null();
   }
+  if( n!=nret && !nret.isNull() ){
+    nret = Rewriter::rewrite( nret );
+  }
+  return nret;
 }
 
+Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, 
+                                                  std::vector< TermProperties >& prop, std::vector< Node >& non_basic ) {
+  computeProgVars( lit );
+  bool is_basic = canApplyBasicSubstitution( lit, non_basic );
+  Node lret;
+  if( is_basic ){
+   lret = lit.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+  }else{
+    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() ) ){
+      Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+      Node atom_lhs;
+      Node atom_rhs;
+      if( atom.getKind()==GEQ ){
+        atom_lhs = atom[0];
+        atom_rhs = atom[1];
+      }else{
+        atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+        atom_lhs = Rewriter::rewrite( atom_lhs );
+        atom_rhs = getQuantifiersEngine()->getTermDatabase()->d_zero;
+      }
+      //must be an eligible term
+      if( isEligible( atom_lhs ) ){
+        //apply substitution to LHS of atom
+        TermProperties atom_lhs_prop;
+        atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop );
+        if( !atom_lhs.isNull() ){
+          if( !atom_lhs_prop.d_coeff.isNull() ){
+            atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
+          }
+          lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+          if( !pol ){
+            lret = lret.negate();
+          }
+        }
+      }
+    }else{
+      // don't know how to apply substitution to literal
+    }
+  }
+  if( lit!=lret && !lret.isNull() ){
+    lret = Rewriter::rewrite( lret );
+  }
+  return lret;
+}
+  
 bool CegInstantiator::check() {
   if( d_qe->getTheoryEngine()->needCheck() ){
     Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index bf555916f..8ffba8d7b 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -52,38 +52,81 @@ public:
   Node d_coeff;
   // get cache node 
   // we consider terms + TermProperties that are unique up to their cache node (see doAddInstantiationInc)
-  Node getCacheNode() { return d_coeff; }
+  virtual Node getCacheNode() const { return d_coeff; }
+  // is non-basic 
+  virtual bool isBasic() const { return d_coeff.isNull(); }
+  // get modified term 
+  virtual Node getModifiedTerm( Node pv ) const {
+    if( !d_coeff.isNull() ){
+      return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv );
+    }else{
+      return pv;
+    }
+  }
+  // combine property 
+  virtual void combineProperty( TermProperties& p ){
+    if( !p.d_coeff.isNull() ){
+      if( d_coeff.isNull() ){
+        d_coeff = p.d_coeff;
+      }else{
+        d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) );
+      }
+    }
+  }
 };
 
-//solved form, involves substitution with coefficients
+//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
   std::vector< Node > d_vars;
+  // list of terms that they are substituted to
   std::vector< Node > d_subs;
+  // properties for each variable
   std::vector< TermProperties > d_props;
-  std::vector< Node > d_has_coeff;
-  Node d_theta;
-  void copy( SolvedForm& sf ){
-    d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() );
-    d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
-    d_props.insert( d_props.end(), sf.d_props.begin(), sf.d_props.end() );
-    d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
-    d_theta = sf.d_theta;
-  }
+  // 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;
+  // push the substitution pv_prop.getModifiedTerm(pv) -> n
   void push_back( Node pv, Node n, TermProperties& pv_prop ){
     d_vars.push_back( pv );
     d_subs.push_back( n );
     d_props.push_back( pv_prop );
-    if( !pv_prop.d_coeff.isNull() ){
-      d_has_coeff.push_back( pv );
+    if( !pv_prop.isBasic() ){
+      d_non_basic.push_back( pv );
+      // update theta value
+      Node new_theta = getTheta();
+      if( new_theta.isNull() ){
+        new_theta = pv_prop.d_coeff;
+      }else{
+        new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff );
+        new_theta = Rewriter::rewrite( new_theta );
+      }
+      d_theta.push_back( new_theta );
     }
   }
+  // pop the substitution pv_prop.getModifiedTerm(pv) -> n
   void pop_back( Node pv, Node n, TermProperties& pv_prop ){
     d_vars.pop_back();
     d_subs.pop_back();
     d_props.pop_back();
-    if( !pv_prop.d_coeff.isNull() ){
-      d_has_coeff.pop_back();
+    if( !pv_prop.isBasic() ){
+      d_non_basic.pop_back();
+      // update theta value
+      d_theta.pop_back();
+    }
+  }
+public:
+  // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
+  std::vector< Node > d_theta;
+  // get the current value for theta (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017)
+  Node getTheta() {
+    if( d_theta.empty() ){
+      return Node::null();
+    }else{
+      return d_theta[d_theta.size()-1];
     }
   }
 };
@@ -138,6 +181,32 @@ private:
   //process
   void processAssertions();
   void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
+private:
+  /** can use basic substitution */
+  bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic );
+  /** apply substitution
+  * We wish to process the substitution: 
+  *   ( pv = n * sf )
+  * where pv is a variable with type tn, and * denotes application of substitution.
+  * The return value "ret" and pv_prop is such that the above equality is equivalent to
+  *   ( pv_prop.getModifiedTerm(pv) = ret )
+  */
+  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) {
+    return applySubstitution( tn, n, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic, pv_prop, try_coeff );
+  }
+  /** apply substitution, with solved form expanded to subs/prop/non_basic/vars */
+  Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
+                          std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff = true );
+  /** apply substitution to literal lit 
+  * The return value is equivalent to ( lit * sf )
+  * where * denotes application of substitution.
+  */
+  Node applySubstitutionToLiteral( Node lit, SolvedForm& sf ) {
+    return applySubstitutionToLiteral( lit, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic );
+  }
+  /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */
+  Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, 
+                                   std::vector< Node >& non_basic );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
   virtual ~CegInstantiator();
@@ -158,12 +227,6 @@ public:
   void popStackVariable();
   bool doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort );
   Node getModelValue( Node n );
-  // TODO: move to solved form?
-  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) {
-    return applySubstitution( tn, n, sf.d_subs, sf.d_props, sf.d_has_coeff, sf.d_vars, pv_prop, try_coeff );
-  }
-  Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& has_coeff,
-                          std::vector< Node >& vars, TermProperties& pv_prop, bool try_coeff = true );
 public:
   unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
   Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
@@ -188,30 +251,43 @@ public:
   virtual ~Instantiator(){}
   virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {}
 
-  //called when pv_prop.d_coeff * pv = n, and n is eligible for instantiation
+  //  Called when the entailment:
+  //    E |= pv_prop.getModifiedTerm(pv) = n
+  //  holds in the current context E, and n is eligible for instantiation.
   virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
-  //eqc is the equivalence class of pv
+  //  Called about process equal term, where eqc is the list of eligible terms in the equivalence class of pv
   virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
 
+  // whether the instantiator implements processEquality
   virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
-  //term_props.size() = terms.size() = 2
-  //  called when terms[0] = 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
+  //  term_props.size() = terms.size() = 2
+  //  Called when the entailment:
+  //    E ^ term_props[0].getModifiedTerm(x0) = terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1
+  //  holds in current context E for fresh variables xi, terms[i] are eligible, and at least one terms[i] contains pv for i = 0,1.
+  //  Notice in the basic case, E |= terms[0] = terms[1].
+  //  Returns true if an instantiation was successfully added via a recursive call
   virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; }
 
+  // whether the instantiator implements processAssertion for any literal
   virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  // whether the instantiator implements processAssertion for literal lit
   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
+  // Called when the entailment:
+  //   E |= lit 
+  // holds in current context E. Typically, lit belongs to the list of current assertions.
+  // 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; }
+  // Called after processAssertion is called for each literal asserted to the instantiator.
   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
+  //do we use the model value as instantiation for pv
   virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  //do we allow the model value as instantiation for pv
   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
+  //do we need to postprocess the solved form for pv?
   virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  // propocess the solved form for pv, returns true if we successfully postprocessed
   virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
 
   /** Identify this module (for debugging) */
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 130d73af6..6f94249ef 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -271,136 +271,109 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
   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() ) ){
-    Assert( atom.getKind()!=GEQ || atom[1].isConst() );
-    Node atom_lhs;
-    Node atom_rhs;
-    if( atom.getKind()==GEQ ){
-      atom_lhs = atom[0];
-      atom_rhs = atom[1];
-    }else{
-      atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
-      atom_lhs = Rewriter::rewrite( atom_lhs );
-      atom_rhs = ci->getQuantifiersEngine()->getTermDatabase()->d_zero;
-    }
-    //must be an eligible term
-    if( ci->isEligible( atom_lhs ) ){
-      //apply substitution to LHS of atom
-      TermProperties atom_lhs_prop;
-      atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_prop );
-      if( !atom_lhs.isNull() ){
-        if( !atom_lhs_prop.d_coeff.isNull() ){
-          atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
+  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?
+  Trace("cbqi-inst-debug") << "..[3] Substituted assertion : " << atom << ", pol = " << pol << std::endl;
+  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;
+          }
         }
-      }
-      //if it contains pv, not infinity
-      if( !atom_lhs.isNull() && ci->hasVariable( atom_lhs, pv ) ){
-        Node pv_value = ci->getModelValue( pv );
-        Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
-        //cannot contain infinity?
-        Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
-        Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
-        Node vts_coeff_inf;
-        Node vts_coeff_delta;
-        Node val;
-        TermProperties pv_prop;
-        //isolate pv in the inequality
-        int ires = solve_arith( ci, pv, satom, 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("cbqi-inst-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_value;
-                  if( !pv_prop.d_coeff.isNull() ){
-                    lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, pv_prop.d_coeff );
-                    lhs_value = Rewriter::rewrite( lhs_value );
-                  }
-                  Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
-                  Assert( lhs_value!=rhs_value );
-                  Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
-                  cmp = Rewriter::rewrite( cmp );
-                  Assert( cmp.isConst() );
-                  is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->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;
-              }
-            }
-            Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
-            if( !pv_prop.d_coeff.isNull() ){
-              Trace("cbqi-bound-inf") << pv_prop.d_coeff << " * ";
-            }
-            Trace("cbqi-bound-inf") << pv << " -> " << 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()->getTermDatabase()->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("cbqi-inst-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->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
-                return true;
-              }
+      }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("cbqi-inst-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("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
+            Assert( lhs_value!=rhs_value );
+            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+            cmp = Rewriter::rewrite( cmp );
+            Assert( cmp.isConst() );
+            is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermDatabase()->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("cbqi-bound-inf") ){
+        Node pvmod = pv_prop.getModifiedTerm( pv );
+        Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
+        Trace("cbqi-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()->getTermDatabase()->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("cbqi-inst-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->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
+          return true;
         }
       }
     }
@@ -528,7 +501,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
           //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict
           if( !options::cbqiMidpoint() || d_type.isInteger() || 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.d_theta,
+            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;
@@ -546,7 +519,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
     if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
       Node val = zero;
       TermProperties pv_prop_zero;
-      val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.d_theta, Node::null(), Node::null() );
+      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->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){
           return true;
@@ -563,7 +537,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
           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.d_theta,
+          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("cbqi-bound") << "Bound : " << vals[rr] << std::endl;
@@ -605,7 +579,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
         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.d_theta,
+            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;
@@ -624,20 +598,22 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
 }
 
 bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
-  return std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end();
+  return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end();
 }
 
 bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
-  Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() );
+  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].d_coeff.isNull() );
-  Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_props[index].d_coeff << " * ";
-  Trace("cbqi-inst-debug") << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+  Assert( !sf.d_props[index].isBasic() );
+  Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] );
+  if( Trace.isOn("cbqi-inst-debug") ){
+    Trace("cbqi-inst-debug") << "Normalize substitution for ";
+    Trace("cbqi-inst-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_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_props[index].d_coeff, sf.d_vars[index] );
   Node eq_rhs = sf.d_subs[index];
   Node eq = eq_lhs.eqNode( eq_rhs );
   eq = Rewriter::rewrite( eq );
@@ -775,7 +751,7 @@ void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsi
 
 bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
   if( options::quantEprMatching() ){
-    Assert( pv_prop.d_coeff.isNull() );
+    Assert( pv_prop.isBasic() );
     d_equal_terms.push_back( n );
     return false;
   }else{
@@ -1057,6 +1033,8 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node
 }
 
 bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
+  Assert( term_props[0].isBasic() );
+  Assert( term_props[1].isBasic() );
   //processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort );
   return false;
 }