Refactor cegqi instantiation infrastructure so that it is more independent of instantiation for LIA. (#1111)

4 files changed, 144 insertions, 132 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index db283ccfc..42394122e 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -192,10 +192,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
             //must be an eligible term
             if( isEligible( n ) ){
               Node ns;
-              Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
+              TermProperties pv_prop;  //coefficient of pv in the equality we solve (null is 1)
               bool proc = false;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( pvtn, n, sf, pv_coeff, false );
+                ns = applySubstitution( pvtn, n, sf, pv_prop, false );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                   //substituted version must be new and cannot contain pv
@@ -206,7 +206,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
                 proc = true;
               }
               if( proc ){
-                if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){
+                if( vinst->processEqualTerm( this, sf, pv, pv_prop, ns, effort ) ){
                   return true;
                 }
               }
@@ -229,7 +229,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
           std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
           std::vector< Node > lhs;
           std::vector< bool > lhs_v;
-          std::vector< Node > lhs_coeff;
+          std::vector< TermProperties > lhs_prop;
           Assert( it_reqc!=d_curr_eqc.end() );
           for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
             Node n = it_reqc->second[kk];
@@ -237,9 +237,9 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
             //must be an eligible term
             if( isEligible( n ) ){
               Node ns;
-              Node pv_coeff;
+              TermProperties pv_prop;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( pvtn, n, sf, pv_coeff );
+                ns = applySubstitution( pvtn, n, sf, pv_prop );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                 }
@@ -249,27 +249,26 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
               if( !ns.isNull() ){
                 bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
                 Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
-                std::vector< Node > term_coeffs;
+                std::vector< TermProperties > term_props;
                 std::vector< Node > terms;
-                term_coeffs.push_back( pv_coeff );
+                term_props.push_back( pv_prop );
                 terms.push_back( ns );
                 for( unsigned j=0; j<lhs.size(); j++ ){
                   //if this term or the another has pv in it, try to solve for it
                   if( hasVar || lhs_v[j] ){
                     Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
-                    //processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
-                    term_coeffs.push_back( lhs_coeff[j] );
+                    term_props.push_back( lhs_prop[j] );
                     terms.push_back( lhs[j] );
-                    if( vinst->processEquality( this, sf, pv, term_coeffs, terms, effort ) ){
+                    if( vinst->processEquality( this, sf, pv, term_props, terms, effort ) ){
                       return true;
                     }
-                    term_coeffs.pop_back();
+                    term_props.pop_back();
                     terms.pop_back();
                   }
                 }
                 lhs.push_back( ns );
                 lhs_v.push_back( hasVar );
-                lhs_coeff.push_back( pv_coeff );
+                lhs_prop.push_back( pv_prop );
               }else{
                 Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
               }
@@ -322,10 +321,10 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e
       }
 #endif
       Node mv = getModelValue( pv );
-      Node pv_coeff_m;
+      TermProperties pv_prop_m;
       Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
       int new_effort = use_model_value ? effort : 1;
-      if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){
+      if( doAddInstantiationInc( pv, mv, pv_prop_m, sf, new_effort ) ){
         return true;
       }
     }
@@ -348,16 +347,17 @@ void CegInstantiator::popStackVariable() {
   d_stack_vars.pop_back();
 }
 
-bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) {
-  if( d_curr_subs_proc[pv][n].find( pv_coeff )==d_curr_subs_proc[pv][n].end() ){
-    d_curr_subs_proc[pv][n][pv_coeff] = true;
+bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv_prop, SolvedForm& sf, unsigned effort ) {
+  Node cnode = pv_prop.getCacheNode();
+  if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
+    d_curr_subs_proc[pv][n][cnode] = true;
     if( Trace.isOn("cbqi-inst") ){
       for( unsigned j=0; j<sf.d_subs.size(); j++ ){
         Trace("cbqi-inst") << " ";
       }
       Trace("cbqi-inst") << sf.d_subs.size() << ": ";
-      if( !pv_coeff.isNull() ){
-        Trace("cbqi-inst") << pv_coeff << " * ";
+      if( !pv_prop.d_coeff.isNull() ){
+        Trace("cbqi-inst") << pv_prop.d_coeff << " * ";
       }
       Trace("cbqi-inst") << pv << " -> " << n << std::endl;
       Assert( n.getType().isSubtypeOf( pv.getType() ) );
@@ -371,15 +371,15 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int
     a_subs.push_back( n );
     std::vector< Node > a_var;
     a_var.push_back( pv );
-    std::vector< Node > a_coeff;
+    std::vector< TermProperties > a_prop;
     std::vector< Node > a_has_coeff;
-    if( !pv_coeff.isNull() ){
-      a_coeff.push_back( pv_coeff );
+    if( !pv_prop.d_coeff.isNull() ){
+      a_prop.push_back( pv_prop );
       a_has_coeff.push_back( pv );
     }
     bool success = true;
     std::map< int, Node > prev_subs;
-    std::map< int, Node > prev_coeff;
+    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;
@@ -390,20 +390,20 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int
         prev_subs[j] = sf.d_subs[j];
         TNode tv = pv;
         TNode ts = n;
-        Node a_pv_coeff;
-        Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+        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 );
         if( !new_subs.isNull() ){
           sf.d_subs[j] = new_subs;
-          if( !a_pv_coeff.isNull() ){
-            prev_coeff[j] = sf.d_coeff[j];
-            if( sf.d_coeff[j].isNull() ){
+          if( !a_pv_prop.d_coeff.isNull() ){
+            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_coeff[j] = a_pv_coeff;
+              sf.d_props[j].d_coeff = a_pv_prop.d_coeff;
             }else{
-              sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
+              sf.d_props[j].d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_props[j].d_coeff, a_pv_prop.d_coeff ) );
             }
           }
           if( sf.d_subs[j]!=prev_subs[j] ){
@@ -422,14 +422,14 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int
     }
     if( success ){
       Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
-      sf.push_back( pv, n, pv_coeff, bt );
+      sf.push_back( pv, n, pv_prop );
       Node prev_theta = sf.d_theta;
       Node new_theta = sf.d_theta;
-      if( !pv_coeff.isNull() ){
+      if( !pv_prop.d_coeff.isNull() ){
         if( new_theta.isNull() ){
-          new_theta = pv_coeff;
+          new_theta = pv_prop.d_coeff;
         }else{
-          new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff );
+          new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_prop.d_coeff );
           new_theta = Rewriter::rewrite( new_theta );
         }
       }
@@ -440,7 +440,7 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int
       sf.d_theta = prev_theta;
       if( !success ){
         Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
-        sf.pop_back( pv, n, pv_coeff, bt );
+        sf.pop_back( pv, n, pv_prop );
       }
     }
     if( success ){
@@ -451,8 +451,8 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int
       for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
         sf.d_subs[it->first] = it->second;
       }
-      for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){
-        sf.d_coeff[it->first] = it->second;
+      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();
@@ -493,8 +493,8 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector
   return ret;
 }
 
-Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
-                                         std::vector< Node >& vars, Node& pv_coeff, bool try_coeff ) {
+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 ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
   bool req_coeff = false;
@@ -526,10 +526,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
       std::vector< Node > nvars;
       std::vector< Node > nsubs;
       for( unsigned i=0; i<vars.size(); i++ ){
-        if( !coeff[i].isNull() ){
+        if( !prop[i].d_coeff.isNull() ){
           Assert( vars[i].getType().isInteger() );
-          Assert( coeff[i].isConst() );
-          Node nn =NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/coeff[i].getConst<Rational>() ) );
+          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>() ) );
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
           nn =  Rewriter::rewrite( nn );
           nsubs.push_back( nn );
@@ -553,18 +553,18 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
           if( its!=vars.end() ){
             int index = its-vars.begin();
-            if( coeff[index].isNull() ){
+            if( prop[index].d_coeff.isNull() ){
               //apply substitution
               msum_term[it->first] = subs[index];
             }else{
               //apply substitution, multiply to ensure no divisibility conflict
               msum_term[it->first] = subs[index];
               //relative coefficient
-              msum_coeff[it->first] = coeff[index];
-              if( pv_coeff.isNull() ){
-                pv_coeff = coeff[index];
+              msum_coeff[it->first] = prop[index].d_coeff;
+              if( pv_prop.d_coeff.isNull() ){
+                pv_prop.d_coeff = prop[index].d_coeff;
               }else{
-                pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] );
+                pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff );
               }
             }
           }else{
@@ -572,16 +572,16 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           }
         }
         //make sum with normalized coefficient
-        if( !pv_coeff.isNull() ){
-          pv_coeff = Rewriter::rewrite( pv_coeff );
-          Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl;
+        if( !pv_prop.d_coeff.isNull() ){
+          pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
+          Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
           std::vector< Node > children;
           for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
             Node c_coeff;
             if( !msum_coeff[it->first].isNull() ){
-              c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
+              c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
             }else{
-              c_coeff = pv_coeff;
+              c_coeff = pv_prop.d_coeff;
             }
             if( !it->second.isNull() ){
               c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
@@ -600,7 +600,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           nret = Rewriter::rewrite( nret );
           //ensure that nret does not contain vars
           if( !TermDb::containsTerms( nret, vars ) ){
-            //result is ( nret / pv_coeff )
+            //result is ( nret / pv_prop.d_coeff )
             return nret;
           }else{
             Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nret << " contains free variable." << std::endl;
@@ -1032,8 +1032,9 @@ Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn )
 }
 
 
-bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
-  return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
+bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
+  pv_prop.d_type = 0;
+  return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
 }
 
 
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index c260486ff..bf555916f 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -40,15 +40,19 @@ public:
 
 class Instantiator;
 
-
-//TODO: refactor pv_coeff to pv_prop throughout
-//generic class that stores properties for a variable to solve for in CEGQI
+//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(-1) {}
+  TermProperties() : d_type(0) {}
+  // type of property for a term
+  //  for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound)
   int d_type;
   // for arithmetic
   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; }
 };
 
 //solved form, involves substitution with coefficients
@@ -56,36 +60,29 @@ 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< 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() );
     d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
-    d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
-    d_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.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;
   }
-  void push_back( Node pv, Node n, Node pv_coeff, int bt ){
+  void push_back( Node pv, Node n, TermProperties& pv_prop ){
     d_vars.push_back( pv );
     d_subs.push_back( n );
-    d_coeff.push_back( pv_coeff );
-    d_btyp.push_back( bt );
-    if( !pv_coeff.isNull() ){
+    d_props.push_back( pv_prop );
+    if( !pv_prop.d_coeff.isNull() ){
       d_has_coeff.push_back( pv );
     }
   }
-  void pop_back( Node pv, Node n, Node pv_coeff, int bt ){
+  void pop_back( Node pv, Node n, TermProperties& pv_prop ){
     d_vars.pop_back();
     d_subs.pop_back();
-    d_coeff.pop_back();
-    d_btyp.pop_back();
-    if( !pv_coeff.isNull() ){
+    d_props.pop_back();
+    if( !pv_prop.d_coeff.isNull() ){
       d_has_coeff.pop_back();
     }
   }
@@ -159,14 +156,14 @@ public:
 public:
   void pushStackVariable( Node v );
   void popStackVariable();
-  bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort );
+  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, Node& pv_coeff, bool try_coeff = true ) {
-    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff );
+  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< Node >& coeff, std::vector< Node >& has_coeff,
-                          std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
+  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]; }
@@ -191,15 +188,16 @@ public:
   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 );
+  //called when pv_prop.d_coeff * pv = n, 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
   virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
 
   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
+  //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
-  virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
+  virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { return false; }
 
   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; }
@@ -228,7 +226,6 @@ public:
   std::string identify() const { return "ModelValue"; }
 };
 
-
 }
 }
 }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index fa7dbabab..130d73af6 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -223,11 +223,11 @@ void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, un
   }
 }
 
-bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
   Node eq_lhs = terms[0];
   Node eq_rhs = terms[1];
-  Node lhs_coeff = term_coeffs[0];
-  Node rhs_coeff = term_coeffs[1];
+  Node lhs_coeff = term_props[0].d_coeff;
+  Node rhs_coeff = term_props[1].d_coeff;
   //make the same coefficient
   if( rhs_coeff!=lhs_coeff ){
     if( !rhs_coeff.isNull() ){
@@ -244,13 +244,14 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N
   Node eq = eq_lhs.eqNode( eq_rhs );
   eq = Rewriter::rewrite( eq );
   Node val;
-  Node veq_c;
+  TermProperties pv_prop;
   Node vts_coeff_inf;
   Node vts_coeff_delta;
   //isolate pv in the equality
-  int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+  int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta );
   if( ires!=0 ){
-    if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+    pv_prop.d_type = 0;
+    if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
       return true;
     }
   }
@@ -285,11 +286,11 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
     //must be an eligible term
     if( ci->isEligible( atom_lhs ) ){
       //apply substitution to LHS of atom
-      Node atom_lhs_coeff;
-      atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff );
+      TermProperties atom_lhs_prop;
+      atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_prop );
       if( !atom_lhs.isNull() ){
-        if( !atom_lhs_coeff.isNull() ){
-          atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
+        if( !atom_lhs_prop.d_coeff.isNull() ){
+          atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) );
         }
       }
       //if it contains pv, not infinity
@@ -302,9 +303,9 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
         Node vts_coeff_inf;
         Node vts_coeff_delta;
         Node val;
-        Node veq_c;
+        TermProperties pv_prop;
         //isolate pv in the inequality
-        int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+        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;
@@ -337,8 +338,8 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
                 }else{
                   Node rhs_value = ci->getModelValue( val );
                   Node lhs_value = pv_value;
-                  if( !veq_c.isNull() ){
-                    lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+                  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;
@@ -362,8 +363,8 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
               }
             }
             Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
-            if( !veq_c.isNull() ){
-              Trace("cbqi-bound-inf") << veq_c << " * ";
+            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
@@ -386,15 +387,16 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf,
               //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( veq_c );
-              Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
+              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
-              if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){
+              pv_prop.d_type = uires>0 ? 1 : -1;
+              if( ci->doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
                 return true;
               }
             }
@@ -434,7 +436,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
             val = NodeManager::currentNM()->mkNode( UMINUS, val );
             val = Rewriter::rewrite( val );
           }
-          if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+          TermProperties pv_prop_no_bound;
+          if( ci->doAddInstantiationInc( pv, val, pv_prop_no_bound, sf, effort ) ){
             return true;
           }
         }
@@ -528,7 +531,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
             val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta,
                                                 d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
             if( !val.isNull() ){
-              if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){
+              TermProperties pv_prop_bound;
+              pv_prop_bound.d_coeff = d_mbp_coeff[rr][best];
+              pv_prop_bound.d_type = rr==0 ? 1 : -1;
+              if( ci->doAddInstantiationInc( pv, val, pv_prop_bound, sf, effort ) ){
                 return true;
               }
             }
@@ -539,10 +545,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
     //if not using infinity, use model value of zero
     if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
       Node val = zero;
-      Node c; //null (one) coefficient
-      val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() );
+      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() );
       if( !val.isNull() ){
-        if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){
+        if( ci->doAddInstantiationInc( pv, val, pv_prop_zero, sf, effort ) ){
           return true;
         }
       }
@@ -583,7 +589,8 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
       }
       Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
       if( !val.isNull() ){
-        if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+        TermProperties pv_prop_midpoint;
+        if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){
           return true;
         }
       }
@@ -601,7 +608,10 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf,
             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,
                                                      d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
             if( !val.isNull() ){
-              if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){
+              TermProperties pv_prop_nopt_bound;
+              pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j];
+              pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1;
+              if( ci->doAddInstantiationInc( pv, val, pv_prop_nopt_bound, sf, effort ) ){
                 return true;
               }
             }
@@ -621,12 +631,13 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo
   Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.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_coeff[index].isNull() );
-  Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+  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_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_coeff[index], sf.d_vars[index] );
+  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 );
@@ -645,9 +656,9 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo
       sf.d_subs[index] = veq[1];
       if( !veq_c.isNull() ){
         sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
-        Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl;
+        Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl;
         //intger division rounding up if from a lower bound
-        if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+        if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){
           sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
             NodeManager::currentNM()->mkNode( ITE,
               NodeManager::currentNM()->mkNode( EQUAL,
@@ -732,7 +743,8 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No
         children.push_back( c );
       }
       Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
-      if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+      TermProperties pv_prop_dt;
+      if( ci->doAddInstantiationInc( pv, val, pv_prop_dt, sf, effort ) ){
         return true;
       }else{
         //cleanup
@@ -746,11 +758,11 @@ bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, No
   return false;
 }
 
-bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
   Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
   if( !val.isNull() ){
-    Node veq_c;
-    if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+    TermProperties pv_prop;
+    if( ci->doAddInstantiationInc( pv, val, pv_prop, sf, effort ) ){
       return true;
     }
   }
@@ -761,13 +773,14 @@ void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsi
   d_equal_terms.clear();
 }
 
-bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
+bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort ) {
   if( options::quantEprMatching() ){
-    Assert( pv_coeff.isNull() );
+    Assert( pv_prop.d_coeff.isNull() );
     d_equal_terms.push_back( n );
     return false;
   }else{
-    return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
+    pv_prop.d_type = 0;
+    return ci->doAddInstantiationInc( pv, n, pv_prop, sf, effort );
   }
 }
 
@@ -832,9 +845,10 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N
     }
     //sort by match score
     std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm );
-    Node pv_coeff;
+    TermProperties pv_prop;
+    pv_prop.d_type = 0;
     for( unsigned i=0; i<d_equal_terms.size(); i++ ){
-      if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){
+      if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_prop, sf, effort ) ){
         return true;
       }
     }
@@ -1023,7 +1037,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node
         if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
           //only ground terms  TODO: more
           if( d_prog_var[atom[1-t]].empty() ){
-            Node veq_c;
+            TermProperties pv_prop;
             Node uval;
             if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
               uval = atom[1-t];
@@ -1031,7 +1045,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node
               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 ) ){
+            if( doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){
               return true;
             }
           }
@@ -1042,7 +1056,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node
   */
 }
 
-bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) {
   //processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort );
   return false;
 }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index dfb7921c8..a24878caf 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -40,7 +40,7 @@ public:
   virtual ~ArithInstantiator(){}
   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 processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, 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 );
@@ -59,7 +59,7 @@ public:
   void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
   bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, 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 processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort );
   std::string identify() const { return "Dt"; }
 };
 
@@ -74,7 +74,7 @@ public:
   EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
   virtual ~EprInstantiator(){}
   void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
+  bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, TermProperties& pv_prop, Node n, unsigned effort );
   bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
   std::string identify() const { return "Epr"; }
 };
@@ -135,7 +135,7 @@ public:
   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 processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, 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 );