From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 26 Feb 2015 14:16:15 +0000 (+0100)
Subject: Robust strategy for single invocation LIA synthesis conjectures.  Add regressions.
X-Git-Tag: cvc5-1.0.0~6384
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4f5c9dbbd0125294500cf5788cb131b355979fb6;p=cvc5.git

Robust strategy for single invocation LIA synthesis conjectures.  Add regressions.
---

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e291dce9d..bcad52087 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -31,7 +31,7 @@ namespace CVC4 {
 
 CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
   d_refine_count = 0;
-  d_ceg_si = NULL;
+  d_ceg_si = new CegConjectureSingleInv( this );
 }
 
 void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
@@ -60,8 +60,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
     }
     d_syntax_guided = true;
     if( options::cegqiSingleInv() ){
-      d_ceg_si = new CegConjectureSingleInv( qe, q, this );
-      d_ceg_si->initialize();
+      d_ceg_si->initialize( qe, q );
     }
   }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
     d_syntax_guided = false;
@@ -131,7 +130,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
 }
 
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
-  d_conj = new CegConjecture( d_quantEngine->getSatContext() );
+  d_conj = new CegConjecture( qe->getSatContext() );
   d_last_inst_si = false;
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index f9c8e42fd..1a1169578 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -32,8 +32,9 @@ using namespace std;
 
 namespace CVC4 {
 
-CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p ) : d_qe( qe ), d_parent( p ), d_quant( q ){
-  d_sol = new CegConjectureSingleInvSol( qe );
+CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
+  d_sol = NULL;
+  d_c_inst_match_trie = NULL;
 }
 
 Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
@@ -58,8 +59,15 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   }
 }
 
-void CegConjectureSingleInv::initialize() {
-  Node q = d_quant;
+void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
+  //initialize data
+  d_sol = new CegConjectureSingleInvSol( qe );
+  d_qe = qe;
+  d_quant = q;
+  if( options::incrementalSolving() ){
+    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
+  }
+  //process
   Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl;
   // conj -> conj*
   std::map< Node, std::vector< Node > > children;
@@ -405,176 +413,306 @@ bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vect
 }
 
 
-void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
-  if( !d_single_inv.isNull() ) {
+
+void CegConjectureSingleInv::computeProgVars( Node n ){
+  if( d_prog_var.find( n )==d_prog_var.end() ){
+    d_prog_var[n].clear();
+    if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
+      d_prog_var[n][n] = true;
+    }else if( n.getKind()==SKOLEM && std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )==d_single_inv_arg_sk.end() ){
+      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;
+      }
+      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;
+      }
+    }
+  }
+}
+
+bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+                                               std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ){
+  if( i==d_single_inv_sk.size() ){
+    for( unsigned j=0; j<has_coeff.size(); j++ ){
+      //unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin();
+      //Assert( !coeff[index].isNull() );
+      //must normalize TODO
+      return false;
+    }
+    
+    //check if we have already added this instantiation
+    bool alreadyExists;
+    if( options::incrementalSolving() ){
+      alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() );
+    }else{
+      alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs );
+    }
+    if( alreadyExists ){
+      return false;
+    }else{
+      Trace("cegqi-engine") << "  * single invocation: " << std::endl;
+      for( unsigned j=0; j<vars.size(); j++ ){
+        Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
+        Trace("cegqi-engine") << "    * " << v;
+        Trace("cegqi-engine") << " (" << vars[j] << ")";
+        Trace("cegqi-engine") << " -> " << subs[j] << std::endl;
+      }
+      Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
+      lem = Rewriter::rewrite( lem );
+      Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
+      if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
+        lems.push_back( lem );
+        d_lemmas_produced.push_back( lem );
+        d_inst.push_back( std::vector< Node >() );
+        d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+      }
+      return true;
+    }
+  }else{
     eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
-    Trace("cegqi-engine") << "  * single invocation: " << std::endl;
-    std::vector< Node > subs;
-    std::map< Node, int > subs_from_model;
-    std::vector< Node > waiting_to_slv;
-    for( unsigned i=0; i<d_single_inv_sk.size(); i++ ){
-      Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
-      Node pv = d_single_inv_sk[i];
-      Trace("cegqi-engine") << "    * " << v;
-      Trace("cegqi-engine") << " (" << pv << ")";
-      Trace("cegqi-engine") << " -> ";
-      Node slv;
-      if( ee->hasTerm( pv ) ){
-        Node r = ee->getRepresentative( pv );
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-        bool isWaitingSlv = false;
-        while( !eqc_i.isFinished() ){
-          Node n = *eqc_i;
-          if( n!=pv ){
-            if( slv.isNull() || isWaitingSlv ){
-              std::vector< Node > vars;
-              collectProgVars( n, vars );
-              if( slv.isNull() || vars.empty() ){
-                // n cannot contain pv
-                bool isLoop = std::find( vars.begin(), vars.end(), pv )!=vars.end();
-                if( !isLoop ){
-                  for( unsigned j=0; j<vars.size(); j++ ){
-                    if( std::find( waiting_to_slv.begin(), waiting_to_slv.end(), vars[j] )!=waiting_to_slv.end() ){
-                      isLoop = true;
-                      break;
-                    }
-                  }
-                  if( !isLoop ){
-                    slv = n;
-                    isWaitingSlv = !vars.empty();
-                  }
-                }
+    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_single_inv_sk[i];
+    Node pvr;
+    Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
+    
+    //[1] easy case : pv is in the equivalence class as another term not containing pv
+    if( ee->hasTerm( pv ) ){
+      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") << 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;
+            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[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
               }
+            }else{
+              ns = n;
+              proc = true;
             }
-          }
-          ++eqc_i;
-        }
-        if( isWaitingSlv ){
-          Trace("cegqi-engine-debug") << "waiting:";
-          waiting_to_slv.push_back( pv );
-        }
-      }else{
-        Trace("cegqi-engine-debug") << "N/A:";
-      }
-      if( slv.isNull() ){
-        //get model value
-        Node mv = d_qe->getModel()->getValue( pv );
-        subs.push_back( mv );
-        subs_from_model[pv] = i;
-        if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){
-          Trace("cegqi-engine") << "M:" << mv;
-        }
-      }else{
-        subs.push_back( slv );
-        Trace("cegqi-engine") << slv;
-      }
-      Trace("cegqi-engine") << std::endl;
-    }
-    for( int i=(int)(waiting_to_slv.size()-1); i>=0; --i ){
-      int index = d_single_inv_sk_index[waiting_to_slv[i]];
-      Trace("cegqi-engine-debug") << "Go back and solve " << d_single_inv_sk[index] << std::endl;
-      Trace("cegqi-engine-debug") << "Substitute " << subs[index] << " to ";
-      subs[index] = applyProgVarSubstitution( subs[index], subs_from_model, subs );
-      Trace("cegqi-engine-debug") << subs[index] << std::endl;
-    }
-    //try to improve substitutions : look for terms that contain terms in question
-    bool success;
-    do{
-      success = false;
-      if( !subs_from_model.empty() ){
-        std::map< int, std::vector< Node > > cls_terms;
-        std::map< Node, std::vector< int > > vars;
-        std::map< Node, std::map< int, std::vector< Node > > > node_eqc;
-        std::map< Node, Node > node_rep;
-        int vn_max = -1;
-        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-        while( !eqcs_i.isFinished() ){
-          Node r = *eqcs_i;
-          TypeNode rtn = r.getType();
-          if( rtn.isInteger() || rtn.isReal() ){
-            eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-            while( !eqc_i.isFinished() ){
-              Node n = *eqc_i;
-              if( classifyTerm( n, subs_from_model, vars[n] ) ){
-                Trace("cegqi-si-debug") << "Term " << n << " in eqc " << r << " with " << vars[n].size() << " unset variables." << std::endl;
-                int vs = (int)vars[n].size();
-                cls_terms[vs].push_back( n );
-                node_eqc[r][vs].push_back( n );
-                node_rep[n] = r;
-                vn_max = vs>vn_max ? vs : vn_max;
+            if( proc ){
+              //try the substitution
+              subs_proc[ns][pv_coeff] = true;
+              if( addInstantiationInc( ns, pv, pv_coeff, subs, vars, coeff, has_coeff, i, lems ) ){
+                return true;
               }
-              ++eqc_i;
             }
           }
-          ++eqcs_i;
         }
-        // will try processed, then unprocessed
-        for( unsigned p=0; p<2; p++ ){
-          Trace("cegqi-si-debug") << "Try " << ( p==0 ? "un" : "" ) << "processed equalities..." << std::endl;
-          //prefer smallest # variables first on LHS
-          for( int vn = 1; vn<=vn_max; vn++ ){
-            Trace("cegqi-si-debug") << "  Having " << vn << " variables on LHS..." << std::endl;
-            for( unsigned i=0; i<cls_terms[vn].size(); i++ ){
-              Node lhs = cls_terms[vn][i];
-              Node r = node_rep[lhs];
-              //prefer smallest # variables on RHS
-              for( int vnc = 0; vnc<=vn_max; vnc++ ){
-                Trace("cegqi-si-debug") << "    Having " << vnc << " variables on RHS..." << std::endl;
-                for( unsigned j=0; j<node_eqc[r][vnc].size(); j++ ){
-                  Node rhs = node_eqc[r][vnc][j];
-                  if( lhs!=rhs ){
-                    Trace("cegqi-si-debug") << "      try " << lhs << " " << rhs << std::endl;
-                    //for each variable in LHS
-                    for( unsigned k=0; k<vars[lhs].size(); k++ ){
-                      int v = vars[lhs][k];
-                      Trace("cegqi-si-debug") << "        variable " << v << std::endl;
-                      Assert( (int)vars[lhs].size()==vn );
-                      //check if already processed
-                      bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end();
-                      if( proc==(p==1) ){
-                        if( solveEquality( lhs, rhs, v, subs_from_model, subs ) ){
-                          Trace("cegqi-si-debug") << "Success, set " << lhs << " " << rhs << " " << v << std::endl;
-                          d_eq_processed[lhs][rhs][v] = true;
-                          success = true;
-                          break;
+        ++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( pv.getType().isInteger() || pv.getType().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;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                }
+              }else{
+                ns = n;
+                pv_coeff = Node::null();
+              }
+              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") << 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( 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::isolateEqCoeff( pv, msum, veq ) ){
+                        Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+                        Node veq_c;
+                        if( veq[0]!=v ){
+                          Node veq_v;
+                          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+                            Assert( veq_v==v );
+                          }
+                        }
+                        if( veq_c.isNull() ){ //TODO
+                          computeProgVars( veq[1] );
+                          subs_proc[veq[1]][veq_c] = true;
+                          if( addInstantiationInc( veq[1], pv, veq_c, subs, vars, coeff, has_coeff, i, lems ) ){
+                            return true;
+                          }
                         }
                       }
                     }
-                    if( success ){ break; }
                   }
                 }
-                if( success ){ break; }
+                lhs.push_back( ns );
+                lhs_v.push_back( hasVar );
+                lhs_coeff.push_back( pv_coeff );
               }
-              if( success ){ break; }
             }
-            if( success ){ break; }
+            ++eqc_i;
           }
-          if( success ){ break; }
         }
+        ++eqcs_i;
       }
-    }while( !subs_from_model.empty() && success );
+    }
     
-    if( Trace.isOn("cegqi-si-warn") ){
-      if( !subs_from_model.empty() ){
-        Trace("cegqi-si-warn") << "Warning : could not find values for : " << std::endl;
-        for( std::map< Node, int >::iterator it = subs_from_model.begin(); it != subs_from_model.end(); ++it ){
-          Trace("cegqi-si-warn") << "  " << it->first << std::endl;
-        }
+    //[3] directly look at assertions
+    //TODO
+    
+    
+    //[4] resort to using value in model     
+    Node mv = d_qe->getModel()->getValue( pv );
+    Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl;
+    return addInstantiationInc( mv, pv, pv_coeff, subs, vars, coeff, has_coeff, i, lems );
+  }
+}
+
+
+bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, 
+                                                  std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems ) {
+  //substitute into previous substitutions, when applicable
+  std::map< int, Node > prev;
+  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[j] = subs[j];
+      TNode tv = pv;
+      TNode ts = n;
+      subs[j] = subs[j].substitute( tv, ts );
+      if( subs[j]!=prev[j] ){
+        subs[j] = Rewriter::rewrite( subs[j] );
       }
     }
-    
-    Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
-    lem = Rewriter::rewrite( lem );
-    Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
-    if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
-      lems.push_back( lem );
-      d_lemmas_produced.push_back( lem );
-      d_inst.push_back( std::vector< Node >() );
-      d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+  }
+  subs.push_back( n );
+  vars.push_back( pv );
+  coeff.push_back( pv_coeff );
+  if( !pv_coeff.isNull() ){
+    has_coeff.push_back( pv );
+  }
+  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;
+  if( addInstantiation( subs, vars, coeff, has_coeff, i+1, lems ) ){
+    return true;
+  }else{
+    subs.pop_back();
+    vars.pop_back();
+    coeff.pop_back();
+    if( !pv_coeff.isNull() ){
+      has_coeff.pop_back();
+    }
+    //revert substitution
+    for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); it++ ){
+      subs[it->first] = it->second;
+    }
+    return false;
+  }
+}
+
+Node CegConjectureSingleInv::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() );
+  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 ){
+      Rewriter::rewrite( nret );
+    }
+    return nret;
+  }else{
+    if( try_coeff ){
+      //must convert to monomial representation
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSum( n, msum ) ){
+        //TODO
+        
+      }
     }
+    // failed to apply the substitution
+    return Node::null();
   }
 }
 
+void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
+  if( !d_single_inv.isNull() ) {
+    std::vector< Node > subs;
+    std::vector< Node > vars;
+    std::vector< Node > coeff;
+    std::vector< Node > has_coeff;
+    //try to add an instantiation
+    if( !addInstantiation( subs, vars, coeff, has_coeff, 0, lems ) ){
+      Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+    }
+  }
+}
+
+/*
 bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
   Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[v] << " based on " << lhs << " = " << rhs << std::endl;
   subs_from_model.erase( d_single_inv_sk[v] );
@@ -606,75 +744,7 @@ bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map<
   subs[v] = prev_subs_v;
   return false;
 }
-
-Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
-  std::vector< Node > vars;
-  collectProgVars( n, vars );
-  if( !vars.empty() ){
-    std::vector< Node > ssubs;
-    //get substitution
-    for( unsigned i=0; i<vars.size(); i++ ){
-      Assert( d_single_inv_sk_index.find( vars[i] )!=d_single_inv_sk_index.end() );
-      int index = d_single_inv_sk_index[vars[i]];
-      ssubs.push_back( subs[index] );
-      //it is now constrained
-      if( subs_from_model.find( vars[i] )!=subs_from_model.end() ){
-        subs_from_model.erase( vars[i] );
-      }
-    }
-    n = n.substitute( vars.begin(), vars.end(), ssubs.begin(), ssubs.end() );
-    n = Rewriter::rewrite( n );
-    return n;
-  }else{
-    return n;
-  }
-}
-
-bool CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ) {
-  if( n.getKind()==SKOLEM ){
-    std::map< Node, int >::iterator it = subs_from_model.find( n );
-    if( it!=subs_from_model.end() ){
-      if( std::find( vars.begin(), vars.end(), it->second )==vars.end() ){
-        vars.push_back( it->second );
-      }
-      return true;
-    }else{
-      // if it is symbolic argument, we are also fine
-      if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){
-        return true;
-      }else{
-        //if it is another program, we are also fine
-        if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
-          return true;
-        }else{
-          return false;
-        }
-      }
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !classifyTerm( n[i], subs_from_model, vars ) ){
-        return false;
-      }
-    }
-    return true;
-  }
-}
-
-void CegConjectureSingleInv::collectProgVars( Node n, std::vector< Node >& vars ) {
-  if( n.getKind()==SKOLEM ){
-    if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
-      if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
-        vars.push_back( n );
-      }
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectProgVars( n[i], vars );
-    }
-  }
-}
-
+*/
 
 Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
   Assert( index<d_inst.size() );
@@ -691,6 +761,7 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
 }
 
 Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
+  Assert( d_sol!=NULL );
   Assert( !d_lemmas_produced.empty() );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index a1f9d5a1f..f8edfacf0 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -43,14 +43,8 @@ private:
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
 
   Node constructSolution( unsigned i, unsigned index );
-  bool classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars );
-  void collectProgVars( Node n, std::vector< Node >& vars );
-  Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
-  //equalities processed
-  std::map< Node, std::map< Node, std::map< int, bool > > > d_eq_processed;
-  bool solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
 public:
-  CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p );
+  CegConjectureSingleInv( CegConjecture * p );
   // original conjecture
   Node d_quant;
   // single invocation version of quant
@@ -70,16 +64,29 @@ public:
   //lemmas produced
   std::vector< Node > d_lemmas_produced;
   std::vector< std::vector< Node > > d_inst;
+  inst::InstMatchTrie d_inst_match_trie;
+  inst::CDInstMatchTrie * d_c_inst_match_trie;
   // solution
   std::vector< Node > d_varList;
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
+  //program variable contains cache
+  std::map< Node, std::map< Node, bool > > d_prog_var;
+  std::map< Node, bool > d_inelig;
+  
+  void computeProgVars( Node n );
+  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+                         std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems );
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, 
+                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned i, std::vector< Node >& lems );
+  Node 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 = true );
 public:
   //get the single invocation lemma
   Node getSingleInvLemma( Node guard );
   //initialize
-  void initialize();
+  void initialize( QuantifiersEngine * qe, Node q );
   //check
   void check( std::vector< Node >& lems );
   //get solution
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index ccc4cfd15..1d3bf7c2a 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -68,6 +68,22 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
           msum[Node::null()] = negate( lit[1] );
         }
         return true;
+      }else{
+        //subtract the other side
+        std::map< Node, Node > msum2;
+        if( getMonomialSum( lit[1], msum2 ) ){
+          for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){
+            std::map< Node, Node >::iterator it2 = msum.find( it->first );
+            if( it2!=msum.end() ){
+              Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second, 
+                                                                it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
+              msum[it->first] = Rewriter::rewrite( r );
+            }else{
+              msum[it->first] = negate( it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
+            }
+          }
+          return true;
+        }
       }
     }
   }
@@ -100,7 +116,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
         if( r.isOne() ){
           veq = negate(veq);
         }else{
-          //TODO : lcd computation
+          //TODO : gcd computation
           return false;
         }
       }
@@ -114,6 +130,44 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
   }
 }
 
+bool QuantArith::isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq ) {
+  std::map< Node, Node >::iterator itv = msum.find( v );
+  if( itv!=msum.end() ){
+    std::vector< Node > children;
+    Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
+    if ( r.sgn()!=0 ){
+      for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+        if( it->first!=v ){
+          Node m;
+          if( !it->first.isNull() ){
+            if ( !it->second.isNull() ){
+              m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
+            }else{
+              m = it->first;
+            }
+          }else{
+            m = it->second;
+          }
+          children.push_back(m);
+        }
+      }
+      veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
+                                (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
+      if( r.sgn()==1 ){
+        veq = negate(veq);
+      }
+      veq = Rewriter::rewrite( veq );
+      Node vc = v;
+      if( !r.isOne() && !r.isNegativeOne() ){
+        vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc );
+      }
+      veq = NodeManager::currentNM()->mkNode( EQUAL, vc, veq );
+      return true;
+    }
+  }
+  return false;
+}
+
 Node QuantArith::negate( Node t ) {
   Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
   tt = Rewriter::rewrite( tt );
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f0dfb1ed6..eebf87dc0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -37,6 +37,7 @@ public:
   static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
   static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
+  static bool isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq );
   static Node negate( Node t );
   static Node offset( Node t, int i );
   static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 08c8a7e3e..2e2007c0a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1957,7 +1957,9 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
             mon[ro].push_back( nc );
             changed = true;
           }else{
-            mon[r].push_back( n[r][i] );
+            if( !n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero() ){
+              mon[r].push_back( n[r][i] );
+            }
           }
         }
       }else{
@@ -1965,7 +1967,9 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
           mon[ro].push_back( nc );
           changed = true;
         }else{
-          mon[r].push_back( n[r] );
+          if( !n[r].isConst() || !n[r].getConst<Rational>().isZero() ){
+            mon[r].push_back( n[r] );
+          }
         }
       }
     }
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index b5ea8b476..ef65ead1f 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -23,11 +23,15 @@ TESTS = hd-01-d1-prog.sy \
         commutative.sy \
         constant.sy \
         multi-fun-polynomial2.sy \
-        unbdd_inv_gen_winf1.sy
+        unbdd_inv_gen_winf1.sy \
+	max.sy \
+	array_sum_2_5.sy \
+	parity-AIG-d0.sy \
+	twolets1.sy \
+	array_search_2.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
-	max.sl \
 	max.smt2 \
 	sygus-uf.sl
 
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
new file mode 100644
index 000000000..5d8cd8752
--- /dev/null
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var k Int)
+(constraint (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0))))
+(constraint (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2))))
+(constraint (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1))))
+(check-synth)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
new file mode 100644
index 000000000..48b5c8a4d
--- /dev/null
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(declare-var x1 Int)
+(declare-var x2 Int)
+(constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2))))
+(constraint (=> (<= (+ x1 x2) 5) (= (findSum x1 x2 ) 0)))
+(check-synth)
diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl
deleted file mode 100644
index fdd925196..000000000
--- a/test/regress/regress0/sygus/max.sl
+++ /dev/null
@@ -1,33 +0,0 @@
-; EXPECT: unsat
-; COMMAND-LINE: --cegqi
-(set-logic LIA)
-
-(synth-fun max ((x Int) (y Int)) Int
-  ((Start Int (0 1 x y
-               (+ Start Start)
-               (- Start Start)
-               (ite StartBool Start Start)))
-   (StartBool Bool ((and StartBool StartBool)
-                    (not StartBool)
-                    (<= Start Start)))))
-
-;(synth-fun min ((x Int) (y Int)) Int
-;  ((Start Int ((Constant Int) (Variable Int)
-;               (+ Start Start)
-;               (- Start Start)
-;               (ite StartBool Start Start)))
-;   (StartBool Bool ((and StartBool StartBool)
-;                    (not StartBool)
-;                    (<= Start Start)))))
-
-(declare-var x Int)
-(declare-var y Int)
-
-(constraint (>= (max x y) x))
-(constraint (>= (max x y) y))
-(constraint (or (= x (max x y))
-                (= y (max x y))))
-;(constraint (= (+ (max x y) (min x y))
-;               (+ x y)))
-
-(check-synth)
diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
new file mode 100644
index 000000000..4fc515353
--- /dev/null
+++ b/test/regress/regress0/sygus/max.sy
@@ -0,0 +1,33 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+
+(synth-fun max ((x Int) (y Int)) Int
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+;(synth-fun min ((x Int) (y Int)) Int
+;  ((Start Int ((Constant Int) (Variable Int)
+;               (+ Start Start)
+;               (- Start Start)
+;               (ite StartBool Start Start)))
+;   (StartBool Bool ((and StartBool StartBool)
+;                    (not StartBool)
+;                    (<= Start Start)))))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (max x y) x))
+(constraint (>= (max x y) y))
+(constraint (or (= x (max x y))
+                (= y (max x y))))
+;(constraint (= (+ (max x y) (min x y))
+;               (+ x y)))
+
+(check-synth)
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
new file mode 100644
index 000000000..c4fbd1c17
--- /dev/null
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -0,0 +1,30 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic BV)
+
+(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+  (xor (not (xor a b)) (not (xor c d))))
+
+(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool ((and Start Start) (not Start) a b c d))))
+
+(declare-var a Bool)
+(declare-var b Bool)
+(declare-var c Bool)
+(declare-var d Bool)
+
+(constraint
+ (= (parity a b c d) 
+    (and (AIG a b c d)
+        (not (and (and (not (and a b)) (not (and (not a) (not b))))
+               (and (not (and (not c) (not d))) (not (and c d))))))))
+
+
+(check-synth)
+
+; Solution:
+;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+;(not
+;  (and
+;   (and (not (and (not a) b)) (not (and d (not c))))
+;   (and (not (and (not b) a)) (not (and (not d) c)))))) 
\ No newline at end of file
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
new file mode 100644
index 000000000..24b0f2c09
--- /dev/null
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(set-logic LIA)
+
+;; f1 is x plus 2 ;; f2 is 2x plus 5
+
+(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
+
+(synth-fun f1 ((x Int)) Int
+	   (
+	   (Start Int (
+	   	      (let0 Intx CInt CInt)
+	   	      )
+ 	   )
+ 	   (Intx Int (x))
+	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+	   )
+)
+
+(synth-fun f2 ((x Int)) Int
+	   (
+	   (Start Int (x
+	   	      (let0 Intx Start CInt)
+	   	      )
+ 	   )
+     (Intx Int (x))
+	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+	   )
+)
+
+
+(declare-var x Int)
+
+(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8))))
+(constraint (= (- (f2 x)(f1 x)) (+ x 2)))
+
+(check-synth)
+