Implement virtual term substitution for non-nested quantifiers. Fix soundness bug in strings related to explaining length terms.

1 files changed, 737 insertions, 30 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index dab32af71..0c4648e51 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -32,6 +32,700 @@ using namespace CVC4::theory::datatypes;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
+
+
+
+CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){
+  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_true = NodeManager::currentNM()->mkConst( true );
+}
+
+void CegInstantiator::computeProgVars( Node n ){
+  if( d_prog_var.find( n )==d_prog_var.end() ){
+    d_prog_var[n].clear();
+    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
+      d_prog_var[n][n] = true;
+    }else if( !d_out->isEligibleForInstantiation( n ) ){
+      d_inelig[n] = true;
+      return;
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      computeProgVars( n[i] );
+      if( d_inelig.find( n[i] )!=d_inelig.end() ){
+        d_inelig[n] = true;
+        return;
+      }
+      if( d_has_delta.find( n[i] )!=d_has_delta.end() ){
+        d_has_delta[n] = true;
+      }
+      for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
+        d_prog_var[n][it->first] = true;
+      }
+    }
+    if( n==d_n_delta ){
+      d_has_delta[n] = true;
+    }
+  }
+}
+
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
+                                        std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                                        unsigned i, unsigned effort ){
+  if( i==d_vars.size() ){
+    return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 );
+  }else{
+    eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+    std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc;
+    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+    Node pv = d_vars[i];
+    TypeNode pvtn = pv.getType();
+
+    if( (i+1)<d_vars.size() || effort!=2 ){
+      //[1] easy case : pv is in the equivalence class as another term not containing pv
+      if( ee->hasTerm( pv ) ){
+        Node pvr = ee->getRepresentative( pv );
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
+        while( !eqc_i.isFinished() ){
+          Node n = *eqc_i;
+          if( n!=pv ){
+            Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl;
+            //compute d_subs_fv, which program variables are contained in n
+            computeProgVars( n );
+            //must be an eligible term
+            if( d_inelig.find( n )==d_inelig.end() ){
+              Node ns;
+              Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
+              bool proc = false;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                  //substituted version must be new and cannot contain pv
+                  proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
+                }
+              }else{
+                ns = n;
+                proc = true;
+              }
+              if( d_has_delta.find( ns )!=d_has_delta.end() ){
+                //also must set delta to zero
+                ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero );
+                ns = Rewriter::rewrite( ns );
+                computeProgVars( ns );
+              }
+              if( proc ){
+                //try the substitution
+                subs_proc[0][ns][pv_coeff] = true;
+                if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
+                  return true;
+                }
+              }
+            }
+          }
+          ++eqc_i;
+        }
+      }
+
+      //[2] : we can solve an equality for pv
+      ///iterate over equivalence classes to find cases where we can solve for the variable
+      if( pvtn.isInteger() || pvtn.isReal() ){
+        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+        while( !eqcs_i.isFinished() ){
+          Node r = *eqcs_i;
+          TypeNode rtn = r.getType();
+          if( rtn.isInteger() || rtn.isReal() ){
+            std::vector< Node > lhs;
+            std::vector< bool > lhs_v;
+            std::vector< Node > lhs_coeff;
+            eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+            while( !eqc_i.isFinished() ){
+              Node n = *eqc_i;
+              computeProgVars( n );
+              //must be an eligible term
+              if( d_inelig.find( n )==d_inelig.end() ){
+                Node ns;
+                Node pv_coeff;
+                if( !d_prog_var[n].empty() ){
+                  ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff );
+                  if( !ns.isNull() ){
+                    computeProgVars( ns );
+                  }
+                }else{
+                  ns = n;
+                }
+                if( !ns.isNull() ){
+                  bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
+                  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("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl;
+                      Node eq_lhs = lhs[j];
+                      Node eq_rhs = ns;
+                      //make the same coefficient
+                      if( pv_coeff!=lhs_coeff[j] ){
+                        if( !pv_coeff.isNull() ){
+                          Trace("cegqi-si-inst-debug") << "...mult lhs by " << pv_coeff << std::endl;
+                          eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs );
+                          eq_lhs = Rewriter::rewrite( eq_lhs );
+                        }
+                        if( !lhs_coeff[j].isNull() ){
+                          Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl;
+                          eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs );
+                          eq_rhs = Rewriter::rewrite( eq_rhs );
+                        }
+                      }
+                      Node eq = eq_lhs.eqNode( eq_rhs );
+                      eq = Rewriter::rewrite( eq );
+                      Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
+                      std::map< Node, Node > msum;
+                      if( QuantArith::getMonomialSumLit( eq, msum ) ){
+                        if( !d_n_delta.isNull() ){
+                          msum.erase( d_n_delta );
+                        }
+                        if( Trace.isOn("cegqi-si-inst-debug") ){
+                          Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
+                          QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
+                          Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                        }
+                        Node veq;
+                        if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
+                          Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+                          Node veq_c;
+                          if( veq[0]!=pv ){
+                            Node veq_v;
+                            if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+                              Assert( veq_v==pv );
+                            }
+                          }
+                          if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){
+                            subs_proc[0][veq[1]][veq_c] = true;
+                            if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
+                              return true;
+                            }
+                          }
+                        }
+                      }
+                    }
+                  }
+                  lhs.push_back( ns );
+                  lhs_v.push_back( hasVar );
+                  lhs_coeff.push_back( pv_coeff );
+                }
+              }
+              ++eqc_i;
+            }
+          }
+          ++eqcs_i;
+        }
+      }
+
+      //[3] directly look at assertions
+      unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+      for( unsigned r=0; r<rmax; r++ ){
+        TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
+        Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
+        Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl;
+        if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) {
+          Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl;
+          context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+          for (unsigned j = 0; it != it_end; ++ it, ++j) {
+            Node lit = (*it).assertion;
+            Trace("cegqi-si-inst-debug2") << "  look at " << lit << std::endl;
+            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().isInteger() || 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 = d_zero;
+              }
+
+              computeProgVars( atom_lhs );
+              //must be an eligible term
+              if( d_inelig.find( atom_lhs )==d_inelig.end() ){
+                //apply substitution to LHS of atom
+                if( !d_prog_var[atom_lhs].empty() ){
+                  Node atom_lhs_coeff;
+                  atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff );
+                  if( !atom_lhs.isNull() ){
+                    computeProgVars( atom_lhs );
+                    if( !atom_lhs_coeff.isNull() ){
+                      atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
+                    }
+                  }
+                }
+                //if it contains pv
+                if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
+                  Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+                  Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+                  Trace("cegqi-si-inst-debug") << "       substituted : " << satom << ", pol = " << pol << std::endl;
+                  std::map< Node, Node > msum;
+                  if( QuantArith::getMonomialSumLit( satom, msum ) ){
+                    if( !d_n_delta.isNull() ){
+                      msum.erase( d_n_delta );
+                    }
+                    if( Trace.isOn("cegqi-si-inst-debug") ){
+                      Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
+                      QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
+                      Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                    }
+                    Node vatom;
+                    //isolate pv in the inequality
+                    int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
+                    if( ires!=0 ){
+                      Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
+                      Node val = vatom[ ires==1 ? 1 : 0 ];
+                      Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                      //get monomial
+                      Node veq_c;
+                      if( pvm!=pv ){
+                        Node veq_v;
+                        if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                          Assert( veq_v==pv );
+                        }
+                      }
+                      //disequalities are both strict upper and lower bounds
+                      unsigned rmax = atom.getKind()==GEQ ? 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( pvtn.isInteger() ){
+                              uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                              uval = Rewriter::rewrite( uval );
+                            }else if( pvtn.isReal() ){
+                              //now is strict inequality
+                              uires = uires*2;
+                            }else{
+                              Assert( false );
+                            }
+                          }
+                        }else{
+                          Assert( atom.getKind()==EQUAL && !pol );
+                          if( pvtn.isInteger() ){
+                            uires = r==0 ? -1 : 1;
+                            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                            uval = Rewriter::rewrite( uval );
+                          }else if( pvtn.isReal() ){
+                            uires = r==0 ? -2 : 2;
+                          }else{
+                            Assert( false );
+                          }
+                        }
+                        if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){
+                          subs_proc[uires][uval][veq_c] = true;
+                          if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
+                            return true;
+                          }
+                        }else{
+                          Trace("cegqi-si-inst-debug") << "...already processed." << std::endl;
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+
+    //[4] resort to using value in model
+    if( effort>0 ){
+      Node mv = d_qe->getModel()->getValue( pv );
+      Node pv_coeff_m;
+      Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl;
+      return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 );
+    }else{
+      return false;
+    }
+  }
+}
+
+
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
+                                           std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
+                                           unsigned i, unsigned effort ) {
+  //must ensure variables have been computed for n
+  computeProgVars( n );
+  //substitute into previous substitutions, when applicable
+  std::vector< Node > a_subs;
+  a_subs.push_back( n );
+  std::vector< Node > a_var;
+  a_var.push_back( pv );
+  std::vector< Node > a_coeff;
+  std::vector< Node > a_has_coeff;
+  if( !pv_coeff.isNull() ){
+    a_coeff.push_back( pv_coeff );
+    a_has_coeff.push_back( pv );
+  }
+
+  bool success = true;
+  std::map< int, Node > prev_subs;
+  std::map< int, Node > prev_coeff;
+  std::vector< Node > new_has_coeff;
+  for( unsigned j=0; j<subs.size(); j++ ){
+    Assert( d_prog_var.find( subs[j] )!=d_prog_var.end() );
+    if( d_prog_var[subs[j]].find( pv )!=d_prog_var[subs[j]].end() ){
+      prev_subs[j] = subs[j];
+      TNode tv = pv;
+      TNode ts = n;
+      Node a_pv_coeff;
+      Node new_subs = applySubstitution( subs[j], a_subs, a_var, a_coeff, a_has_coeff, a_pv_coeff, true );
+      if( !new_subs.isNull() ){
+        subs[j] = new_subs;
+        if( !a_pv_coeff.isNull() ){
+          prev_coeff[j] = coeff[j];
+          if( coeff[j].isNull() ){
+            Assert( std::find( has_coeff.begin(), has_coeff.end(), vars[j] )==has_coeff.end() );
+            //now has coefficient
+            new_has_coeff.push_back( vars[j] );
+            has_coeff.push_back( vars[j] );
+            coeff[j] = a_pv_coeff;
+          }else{
+            coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) );
+          }
+        }
+        if( subs[j]!=prev_subs[j] ){
+          computeProgVars( subs[j] );
+        }
+      }else{
+        success = false;
+        break;
+      }
+    }
+  }
+  if( success ){
+    subs.push_back( n );
+    vars.push_back( pv );
+    coeff.push_back( pv_coeff );
+    if( !pv_coeff.isNull() ){
+      has_coeff.push_back( pv );
+    }
+    subs_typ.push_back( styp );
+    Trace("cegqi-si-inst-debug") << i << ": ";
+    if( !pv_coeff.isNull() ){
+      Trace("cegqi-si-inst-debug") << pv_coeff << "*";
+    }
+    Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl;
+    success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort );
+    if( !success ){
+      subs.pop_back();
+      vars.pop_back();
+      coeff.pop_back();
+      if( !pv_coeff.isNull() ){
+        has_coeff.pop_back();
+      }
+      subs_typ.pop_back();
+    }
+  }
+  if( success ){
+    return true;
+  }else{
+    //revert substitution information
+    for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
+      subs[it->first] = it->second;
+    }
+    for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){
+      coeff[it->first] = it->second;
+    }
+    for( unsigned i=0; i<new_has_coeff.size(); i++ ){
+      has_coeff.pop_back();
+    }
+    return false;
+  }
+}
+
+bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
+                                             std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) {
+  if( j==has_coeff.size() ){
+    return addInstantiation( subs, vars, subs_typ );
+  }else{
+    Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() );
+    unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin();
+    Node prev = subs[index];
+    Assert( !coeff[index].isNull() );
+    Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl;
+    if( 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, coeff[index], vars[index] );
+      Node eq_rhs = subs[index];
+      Node eq = eq_lhs.eqNode( eq_rhs );
+      eq = Rewriter::rewrite( eq );
+      Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSumLit( eq, msum ) ){
+        Node veq;
+        if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){
+          Node veq_c;
+          if( veq[0]!=vars[index] ){
+            Node veq_v;
+            if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+              Assert( veq_v==vars[index] );
+            }
+          }
+          subs[index] = veq[1];
+          if( !veq_c.isNull() ){
+            subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
+            if( subs_typ[index]>=1 && subs_typ[index]<=2 ){
+              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+                NodeManager::currentNM()->mkNode( ITE,
+                  NodeManager::currentNM()->mkNode( EQUAL,
+                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+                    d_zero ),
+                  d_zero, d_one )
+              );
+            }
+          }
+          Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl;
+          if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
+            return true;
+          }
+            //equalities are both upper and lower bounds
+            /*
+            if( subs_typ[index]==0 && !veq_c.isNull() ){
+              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+                NodeManager::currentNM()->mkNode( ITE,
+                  NodeManager::currentNM()->mkNode( EQUAL,
+                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+                    NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
+                  NodeManager::currentNM()->mkConst( Rational( 0 ) ),
+                  NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
+              );
+              if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
+                return true;
+              }
+            }
+            */
+        }
+      }
+    }else if( vars[index].getType().isReal() ){
+      // can always invert
+      subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst<Rational>() ), subs[index] );
+      subs[index] = Rewriter::rewrite( subs[index] );
+      Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl;
+      if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){
+        return true;
+      }
+    }else{
+      Assert( false );
+    }
+    subs[index] = prev;
+    Trace("cegqi-si-inst-debug") << "...failed." << std::endl;
+    return false;
+  }
+}
+
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) {
+  // do delta rationals
+  std::map< int, Node > prev;
+  for( unsigned i=0; i<subs.size(); i++ ){
+    if( subs_typ[i]==2 || subs_typ[i]==-2 ){
+      prev[i] = subs[i];
+      Node delta = d_qe->getTermDatabase()->getVtsDelta();
+      d_n_delta = delta;
+      subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], delta );
+    }
+  }
+  //check if we have already added this instantiation
+  bool success = d_out->addInstantiation( subs, subs_typ );
+  if( !success ){
+    //revert the substitution
+    for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){
+      subs[it->first] = it->second;
+    }
+  }
+  return success;
+}
+
+
+Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
+                                                std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
+  Assert( d_prog_var.find( n )!=d_prog_var.end() );
+  Assert( n==Rewriter::rewrite( n ) );
+  bool req_coeff = false;
+  if( !has_coeff.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( !req_coeff ){
+    Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    if( n!=nret ){
+      nret = Rewriter::rewrite( nret );
+    }
+    //result is nret
+    return nret;
+  }else{
+    if( try_coeff ){
+      //must convert to monomial representation
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSum( n, msum ) ){
+        std::map< Node, Node > msum_coeff;
+        std::map< Node, Node > msum_term;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          //check if in substitution
+          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() ){
+              //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];
+              }else{
+                pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] );
+              }
+            }
+          }else{
+            msum_term[it->first] = it->first;
+          }
+        }
+        //make sum with normalized coefficient
+        Assert( !pv_coeff.isNull() );
+        pv_coeff = Rewriter::rewrite( pv_coeff );
+        Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_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>() ) );
+          }else{
+            c_coeff = pv_coeff;
+          }
+          if( !it->second.isNull() ){
+            c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
+          }
+          Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
+          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 );
+        //result is ( nret / pv_coeff )
+        return nret;
+      }else{
+        Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
+      }
+    }
+    // failed to apply the substitution
+    return Node::null();
+  }
+}
+
+//check if delta has a lower bound L
+// if so, add lemma L>0 => L>d
+void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
+  return;
+  /*  disable for now
+  if( !d_n_delta.isNull() ){
+    Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH );
+    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){
+      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+      for (unsigned j = 0; it != it_end; ++ it, ++j) {
+        Node lit = (*it).assertion;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        bool pol = lit.getKind()!=NOT;
+        if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){
+          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 = d_zero;
+          }
+          computeProgVars( atom_lhs );
+          //must be an eligible term with delta
+          if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){
+            Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+            Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl;
+            std::map< Node, Node > msum;
+            if( QuantArith::getMonomialSumLit( satom, msum ) ){
+              Node vatom;
+              //isolate delta in the inequality
+              int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true );
+              if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){
+                Node val = vatom[ ires==1 ? 1 : 0 ];
+                Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                //get monomial
+                if( pvm!=d_n_delta ){
+                  Node veq_c;
+                  Node veq_v;
+                  if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                    Assert( veq_v==d_n_delta );
+                    val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                    val = Rewriter::rewrite( val );
+                  }else{
+                    val = Node::null();
+                  }
+                }
+                if( !val.isNull()  ){
+                  Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero );
+                  lem1 = Rewriter::rewrite( lem1 );
+                  if( !lem1.isConst() || lem1==d_true ){
+                    Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta );
+                    Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 );
+                    lems.push_back( lem );
+                    Trace("cegqi-delta") << "...lemma : " << lem << std::endl;
+                  }
+                }
+              }else{
+                Trace("cegqi-delta") << "...wrong polarity." << std::endl;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  */
+}
+
+bool CegInstantiator::check() {
+
+  for( unsigned r=0; r<2; r++ ){
+    std::vector< Node > subs;
+    std::vector< Node > vars;
+    std::vector< Node > coeff;
+    std::vector< Node > has_coeff;
+    std::vector< int > subs_typ;
+    //try to add an instantiation
+    if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){
+      return true;
+    }
+  }
+  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  return false;
+}
+
+
+//old implementation
+
 InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
     InstStrategy( ie ), d_th( th ), d_counter( 0 ){
   d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
@@ -350,6 +1044,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
 
 
 
+//new implementation
+
 bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
   return d_out->addInstantiation( subs, subs_typ );
 }
@@ -380,15 +1076,6 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
     if( it==d_cinst.end() ){
       cinst = new CegInstantiator( d_quantEngine, d_out );
-      if( d_n_delta.isNull() ){
-        d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" );
-        Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
-        d_quantEngine->getOutputChannel().lemma( delta_lem );
-        d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
-        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
-        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
-      }
-      cinst->d_n_delta = d_n_delta;
       for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
         cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
       }
@@ -397,37 +1084,47 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
       cinst = it->second;
     }
     if( d_check_delta_lemma ){
+      //minimize the free delta heuristically
       Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl;
-      d_check_delta_lemma = false;
-      std::vector< Node > dlemmas;
-      cinst->getDeltaLemmas( dlemmas );
-      Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl;
-      if( !dlemmas.empty() ){
-        bool addedLemma = false;
-        for( unsigned i=0; i<dlemmas.size(); i++ ){
-          if( addLemma( dlemmas[i] ) ){
-            addedLemma = true;
-          }
+      Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
+      if( !delta.isNull() ){
+        if( d_n_delta_ub.isNull() ){
+          d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
         }
-        if( addedLemma ){
-          return STATUS_UNKNOWN;
+        d_check_delta_lemma = false;
+        std::vector< Node > dlemmas;
+        cinst->getDeltaLemmas( dlemmas );
+        Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl;
+        if( !dlemmas.empty() ){
+          bool addedLemma = false;
+          for( unsigned i=0; i<dlemmas.size(); i++ ){
+            if( addLemma( dlemmas[i] ) ){
+              addedLemma = true;
+            }
+          }
+          if( addedLemma ){
+            return STATUS_UNKNOWN;
+          }
         }
       }
     }
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     bool addedLemma = cinst->check();
-    d_used_delta = d_used_delta || cinst->d_used_delta;
     d_curr_quant = Node::null();
     return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
   }else if( e==2 ){
-    if( d_check_delta_lemma_lc && d_used_delta ){
-      d_check_delta_lemma_lc = false;
-      d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
-      d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
-      Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl;
-      Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
-      d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+    //minimize the free delta heuristically on demand
+    if( d_check_delta_lemma_lc ){
+      Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
+      if( !delta.isNull() ){
+        d_check_delta_lemma_lc = false;
+        d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
+        d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
+        Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl;
+        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_n_delta_ub );
+        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+      }
     }
   }
   return STATUS_UNKNOWN;
@@ -446,7 +1143,17 @@ bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector
     }
   }
   */
-  return d_quantEngine->addInstantiation( d_curr_quant, subs, false );
+  //check if we need virtual term substitution (if used delta)
+  bool used_delta = false;
+  Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( false, false );
+  if( !delta.isNull() ){
+    for( unsigned i=0; i<subs.size(); i++ ){
+      if( TermDb::containsTerm( subs[i], delta ) ){
+        used_delta = true;
+      }
+    }
+  }
+  return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_delta );
 }
 
 bool InstStrategyCegqi::addLemma( Node lem ) {