Better organization of quantifiers modules, promote full saturation to module. Add heuristics for cbqi LIA instantiation with coefficients.

10 files changed, 351 insertions, 242 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 3a626cb92..8e6673fb9 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -67,12 +67,23 @@ void CegInstantiator::computeProgVars( Node n ){
   }
 }
 
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
-                                        std::vector< Node >& coeff, std::vector< int >& btyp,
-                                        std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                        std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                                         std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
   if( i==d_vars.size() ){
-    return addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, 0, cons );
+    //solved for all variables, now construct instantiation
+    if( !sf.d_has_coeff.empty() ){
+      if( options::cbqiSymLia() ){
+        //use symbolic solved forms
+        SolvedForm csf;
+        csf.copy( ssf );
+        return addInstantiationCoeff( csf, vars, btyp, 0, cons );
+      }else{
+        return addInstantiationCoeff( sf, vars, btyp, 0, cons );
+      }
+    }else{
+      return addInstantiation( sf.d_subs, vars, cons );
+    }
   }else{
     std::map< Node, std::map< Node, bool > > subs_proc;
     //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
@@ -98,7 +109,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 
     //if in effort=2, we must choose at least one model value
     if( (i+1)<d_vars.size() || effort!=2 ){
-      
+
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
       std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
@@ -116,7 +127,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               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 );
+                ns = applySubstitution( n, sf, vars, pv_coeff, false );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                   //substituted version must be new and cannot contain pv
@@ -129,7 +140,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               if( proc ){
                 //try the substitution
                 subs_proc[ns][pv_coeff] = true;
-                if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -162,7 +173,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               Node ns;
               Node pv_coeff;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff );
+                ns = applySubstitution( n, sf, vars, pv_coeff );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                 }
@@ -216,7 +227,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                         Node val = veq[1];
                         if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
                           subs_proc[val][veq_c] = true;
-                          if( addInstantiationInc( val, pv, veq_c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                          if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                             return true;
                           }
                         }
@@ -253,7 +264,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
                 curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
               }
-              if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+              if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                 return true;
               }else{
                 //cleanup
@@ -316,7 +327,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                   //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 );
+                    atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff );
                     if( !atom_lhs.isNull() ){
                       computeProgVars( atom_lhs );
                       if( !atom_lhs_coeff.isNull() ){
@@ -472,7 +483,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                             //try this bound
                             if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
                               subs_proc[uval][veq_c] = true;
-                              if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                              if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                                 return true;
                               }
                             }
@@ -509,7 +520,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                   val = NodeManager::currentNM()->mkNode( UMINUS, val );
                   val = Rewriter::rewrite( val );
                 }
-                if( addInstantiationInc( val, pv, Node::null(), 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -603,7 +614,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
                     subs_proc[val][mbp_coeff[rr][best]] = true;
-                    if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                    if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                       return true;
                     }
                   }
@@ -619,7 +630,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
             if( !val.isNull() ){
               if( subs_proc[val].find( c )==subs_proc[val].end() ){
                 subs_proc[val][c] = true;
-                if( addInstantiationInc( val, pv, c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                   return true;
                 }
               }
@@ -639,7 +650,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
                     subs_proc[val][mbp_coeff[rr][j]] = true;
-                    if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort, cons, curr_var ) ){
+                    if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
                       return true;
                     }
                   }
@@ -662,7 +673,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       //we only resort to values in the case of booleans
       Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
 #endif
-      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, btyp, has_coeff, theta, i, new_effort, cons, curr_var ) ){
+      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
         return true;
       }
     }
@@ -672,15 +683,14 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 }
 
 
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars,
-                                           std::vector< Node >& coeff, std::vector< int >& btyp, 
-                                           std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                           std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                                            std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
   if( Trace.isOn("cbqi-inst") ){
-    for( unsigned j=0; j<subs.size(); j++ ){
+    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
       Trace("cbqi-inst") << " ";
     }
-    Trace("cbqi-inst") << subs.size() << ": ";
+    Trace("cbqi-inst") << sf.d_subs.size() << ": ";
     if( !pv_coeff.isNull() ){
       Trace("cbqi-inst") << pv_coeff << " * ";
     }
@@ -688,7 +698,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   }
   //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 );
@@ -703,47 +713,51 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   bool success = true;
   std::map< int, Node > prev_subs;
   std::map< int, Node > prev_coeff;
+  std::map< int, Node > prev_sym_subs;
   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];
+  for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+    Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
+    if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
+      prev_subs[j] = sf.d_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 );
+      Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
       if( !new_subs.isNull() ){
-        subs[j] = new_subs;
+        sf.d_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() );
+          prev_coeff[j] = sf.d_coeff[j];
+          if( sf.d_coeff[j].isNull() ){
+            Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() );
             //now has coefficient
             new_has_coeff.push_back( vars[j] );
-            has_coeff.push_back( vars[j] );
-            coeff[j] = a_pv_coeff;
+            sf.d_has_coeff.push_back( vars[j] );
+            sf.d_coeff[j] = a_pv_coeff;
           }else{
-            coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) );
+            sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
           }
         }
-        if( subs[j]!=prev_subs[j] ){
-          computeProgVars( subs[j] );
+        if( sf.d_subs[j]!=prev_subs[j] ){
+          computeProgVars( sf.d_subs[j] );
         }
       }else{
-        Trace("cbqi-inst-debug") << "...failed to apply substitution to " << subs[j] << std::endl;
+        Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
         success = false;
         break;
       }
     }
+    if( options::cbqiSymLia() && pv_coeff.isNull() ){
+      //apply simple substitutions also to sym_subs
+      prev_sym_subs[j] = ssf.d_subs[j];
+      ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() );
+      ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] );
+    }
   }
   if( success ){
-    subs.push_back( n );
     vars.push_back( pv );
-    coeff.push_back( pv_coeff );
     btyp.push_back( bt );
-    if( !pv_coeff.isNull() ){
-      has_coeff.push_back( pv );
-    }
+    sf.push_back( pv, n, pv_coeff );
+    ssf.push_back( pv, n, pv_coeff );
     Node new_theta = theta;
     if( !pv_coeff.isNull() ){
       if( new_theta.isNull() ){
@@ -759,18 +773,15 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
       curr_var.pop_back();
       is_cv = true;
     }
-    success = addInstantiation( subs, vars, coeff, btyp, has_coeff, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+    success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
     if( !success ){
       if( is_cv ){
         curr_var.push_back( pv );
       }
-      subs.pop_back();
+      sf.pop_back( pv, n, pv_coeff );
+      ssf.pop_back( pv, n, pv_coeff );
       vars.pop_back();
-      coeff.pop_back();
       btyp.pop_back();
-      if( !pv_coeff.isNull() ){
-        has_coeff.pop_back();
-      }
     }
   }
   if( success ){
@@ -778,33 +789,38 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b
   }else{
     //revert substitution information
     for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
-      subs[it->first] = it->second;
+      sf.d_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;
+      sf.d_coeff[it->first] = it->second;
     }
     for( unsigned i=0; i<new_has_coeff.size(); i++ ){
-      has_coeff.pop_back();
+      sf.d_has_coeff.pop_back();
+    }
+    for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){
+      ssf.d_subs[it->first] = it->second;
     }
     return false;
   }
 }
 
-bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
-                                             std::vector< Node >& coeff, std::vector< int >& btyp, std::vector< Node >& has_coeff, unsigned j, std::map< Node, Node >& cons ) {
-  if( j==has_coeff.size() ){
-    return addInstantiation( subs, vars, cons );
+bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
+                                             unsigned j, std::map< Node, Node >& cons ) {
+
+
+  if( j==sf.d_has_coeff.size() ){
+    return addInstantiation( sf.d_subs, vars, cons );
   }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("cbqi-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << std::endl;
+    Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
+    unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
+    Node prev = sf.d_subs[index];
+    Assert( !sf.d_coeff[index].isNull() );
+    Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl;
     Assert( 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_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] );
+    Node eq_rhs = sf.d_subs[index];
     Node eq = eq_lhs.eqNode( eq_rhs );
     eq = Rewriter::rewrite( eq );
     Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
@@ -819,13 +835,13 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
             Assert( veq_v==vars[index] );
           }
         }
-        subs[index] = veq[1];
+        sf.d_subs[index] = veq[1];
         if( !veq_c.isNull() ){
-          subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
+          sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
           Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
           //intger division rounding up if from a lower bound
-          if( btyp[index]==1 ){
-            subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+          if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+            sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
               NodeManager::currentNM()->mkNode( ITE,
                 NodeManager::currentNM()->mkNode( EQUAL,
                   NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
@@ -834,13 +850,29 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
             );
           }
         }
-        Trace("cbqi-inst-debug") << "...normalize integers : " << subs[index] << std::endl;
-        if( addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, j+1, cons ) ){
+        Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl;
+        if( options::cbqiSymLia() ){
+          //must apply substitution to previous subs
+          std::vector< Node > curr_var;
+          std::vector< Node > curr_subs;
+          curr_var.push_back( vars[index] );
+          curr_subs.push_back( sf.d_subs[index] );
+          for( unsigned k=0; k<index; k++ ){
+            Node prevs = sf.d_subs[k];
+            sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() );
+            if( prevs!=sf.d_subs[k] ){
+              Trace("cbqi-inst-debug2") << "      rewrite " << vars[k] << " -> " << prevs << " to ";
+              sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] );
+              Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl;
+            }
+          }
+        }
+        if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
           return true;
         }
       }
     }
-    subs[index] = prev;
+    sf.d_subs[index] = prev;
     Trace("cbqi-inst-debug") << "...failed." << std::endl;
     return false;
   }
@@ -887,8 +919,8 @@ Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& su
   }
 }
 
-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 ) {
+Node CegInstantiator::applySubstitution( 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 ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
   bool req_coeff = false;
@@ -1030,16 +1062,15 @@ bool CegInstantiator::check() {
   }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
-    std::vector< Node > subs;
+    SolvedForm sf;
+    SolvedForm ssf;
     std::vector< Node > vars;
-    std::vector< Node > coeff;
     std::vector< int > btyp;
-    std::vector< Node > has_coeff;
     Node theta;
     std::map< Node, Node > cons;
     std::vector< Node > curr_var;
     //try to add an instantiation
-    if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+    if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
       return true;
     }
   }
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 2074e0f4b..9b3b15dc5 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -68,24 +68,50 @@ private:
 private:
   //for adding instantiations during check
   void computeProgVars( Node n );
+  //solved form, involves substitution with coefficients
+  class SolvedForm {
+  public:
+    std::vector< Node > d_subs;
+    std::vector< Node > d_coeff;
+    std::vector< Node > d_has_coeff;
+    void copy( SolvedForm& sf ){
+      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_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
+    }
+    void push_back( Node pv, Node n, Node pv_coeff ){
+      d_subs.push_back( n );
+      d_coeff.push_back( pv_coeff );
+      if( !pv_coeff.isNull() ){
+        d_has_coeff.push_back( pv );
+      }
+    }
+    void pop_back( Node pv, Node n, Node pv_coeff ){
+      d_subs.pop_back();
+      d_coeff.pop_back();
+      if( !pv_coeff.isNull() ){
+        d_has_coeff.pop_back();
+      }
+    }
+  };
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
-                         std::vector< Node >& coeff, std::vector< int >& btyp, 
-                         std::vector< Node >& has_coeff, Node theta,
-                         unsigned i, unsigned effort,
+  bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                         std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                          std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars,
-                            std::vector< Node >& coeff, std::vector< int >& btyp, 
-                            std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort,
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                            std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
                             std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
-                              std::vector< Node >& coeff, std::vector< int >& btyp, 
-                              std::vector< Node >& has_coeff, unsigned j, std::map< Node, Node >& cons );
+  bool addInstantiationCoeff( SolvedForm& sf,
+                              std::vector< Node >& vars, std::vector< int >& btyp,
+                              unsigned j, std::map< Node, Node >& cons );
   bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
   Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
-  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 );
-  Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, 
+  Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
+    return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
+  }
+  Node applySubstitution( 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 getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta,
                                      Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta );
   void processAssertions();
   void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
@@ -95,7 +121,7 @@ public:
   bool check();
   //presolve for quantified formula
   void presolve( Node q );
-  //register the counterexample lemma (stored in lems), modify vector 
+  //register the counterexample lemma (stored in lems), modify vector
   void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
 };
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 8958034df..a55dfda84 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -456,114 +456,146 @@ bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
   }
 }
 */
+FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe ){
 
-void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+}
+
+void FullSaturation::reset_round( Theory::Effort e ) {
 
 }
 
-int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
-  if( e<5 ){
-    return STATUS_UNFINISHED;
-  }else{
-    //first, try from relevant domain
-    RelevantDomain * rd = d_quantEngine->getRelevantDomain();
-    unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
-    for( unsigned r=rstart; r<2; r++ ){
-      if( rd || r>0 ){
+void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
+  if( quant_e==QuantifiersEngine::QEFFORT_LAST_CALL ){
+    double clSet = 0;
+    if( Trace.isOn("fs-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
+    }
+    int addedLemmas = 0;
+    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        if( process( q, e ) ){
+          //added lemma
+          addedLemmas++;
+        }
+      }
+    }
+    if( Trace.isOn("fs-engine") ){
+      Trace("fs-engine") << "Added lemmas = " << addedLemmas  << std::endl;
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+    }
+  }
+}
+
+bool FullSaturation::process( Node f, Theory::Effort effort ){
+  //first, try from relevant domain
+  RelevantDomain * rd = d_quantEngine->getRelevantDomain();
+  unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+  for( unsigned r=rstart; r<2; r++ ){
+    if( rd || r>0 ){
+      if( r==0 ){
+        Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
+      }else{
+        Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+      }
+      rd->compute();
+      unsigned final_max_i = 0;
+      std::vector< unsigned > maxs;
+      for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+        unsigned ts;
         if( r==0 ){
-          Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
+          ts = rd->getRDomain( f, i )->d_terms.size();
         }else{
-          Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+          ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
         }
-        rd->compute();
-        unsigned final_max_i = 0;
-        std::vector< unsigned > maxs;
-        for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
-          unsigned ts;
-          if( r==0 ){
-            ts = rd->getRDomain( f, i )->d_terms.size();
-          }else{
-            ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
-          }
-          maxs.push_back( ts );
-          Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
-          if( ts>final_max_i ){
-            final_max_i = ts;
-          }
+        maxs.push_back( ts );
+        Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
+        if( ts>final_max_i ){
+          final_max_i = ts;
         }
-        Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
+      }
+      Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
 
-        unsigned max_i = 0;
-        bool success;
-        while( max_i<=final_max_i ){
-          Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
-          std::vector< unsigned > childIndex;
-          int index = 0;
-          do {
-            while( index>=0 && index<(int)f[0].getNumChildren() ){
-              if( index==(int)childIndex.size() ){
-                childIndex.push_back( -1 );
-              }else{
-                Assert( index==(int)(childIndex.size())-1 );
-                unsigned nv = childIndex[index]+1;
-                if( options::cbqi() ){
-                  //skip inst constant nodes
-                  while( nv<maxs[index] && nv<=max_i &&
-                         r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
-                    nv++;
-                  }
-                }
-                if( nv<maxs[index] && nv<=max_i ){
-                  childIndex[index] = nv;
-                  index++;
-                }else{
-                  childIndex.pop_back();
-                  index--;
+      unsigned max_i = 0;
+      bool success;
+      while( max_i<=final_max_i ){
+        Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+        std::vector< unsigned > childIndex;
+        int index = 0;
+        do {
+          while( index>=0 && index<(int)f[0].getNumChildren() ){
+            if( index==(int)childIndex.size() ){
+              childIndex.push_back( -1 );
+            }else{
+              Assert( index==(int)(childIndex.size())-1 );
+              unsigned nv = childIndex[index]+1;
+              if( options::cbqi() ){
+                //skip inst constant nodes
+                while( nv<maxs[index] && nv<=max_i &&
+                        r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+                  nv++;
                 }
               }
-            }
-            success = index>=0;
-            if( success ){
-              Trace("inst-alg-rd") << "Try instantiation { ";
-              for( unsigned j=0; j<childIndex.size(); j++ ){
-                Trace("inst-alg-rd") << childIndex[j] << " ";
-              }
-              Trace("inst-alg-rd") << "}" << std::endl;
-              //try instantiation
-              std::vector< Node > terms;
-              for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-                if( r==0 ){
-                  terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
-                }else{
-                  terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
-                }
-              }
-              if( d_quantEngine->addInstantiation( f, terms, false ) ){
-                Trace("inst-alg-rd") << "Success!" << std::endl;
-                ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
-                return STATUS_UNKNOWN;
+              if( nv<maxs[index] && nv<=max_i ){
+                childIndex[index] = nv;
+                index++;
               }else{
+                childIndex.pop_back();
                 index--;
               }
             }
-          }while( success );
-          max_i++;
-        }
-      }
-      if( r==0 ){
-        //complete guess
-        if( d_guessed.find( f )==d_guessed.end() ){
-          Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
-          d_guessed[f] = true;
-          InstMatch m( f );
-          if( d_quantEngine->addInstantiation( f, m ) ){
-            ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
-            return STATUS_UNKNOWN;
           }
+          success = index>=0;
+          if( success ){
+            Trace("inst-alg-rd") << "Try instantiation { ";
+            for( unsigned j=0; j<childIndex.size(); j++ ){
+              Trace("inst-alg-rd") << childIndex[j] << " ";
+            }
+            Trace("inst-alg-rd") << "}" << std::endl;
+            //try instantiation
+            std::vector< Node > terms;
+            for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+              if( r==0 ){
+                terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+              }else{
+                terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+              }
+            }
+            if( d_quantEngine->addInstantiation( f, terms, false ) ){
+              Trace("inst-alg-rd") << "Success!" << std::endl;
+              ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+              return true;
+            }else{
+              index--;
+            }
+          }
+        }while( success );
+        max_i++;
+      }
+    }
+    if( r==0 ){
+      //complete guess
+      if( d_guessed.find( f )==d_guessed.end() ){
+        Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+        d_guessed[f] = true;
+        InstMatch m( f );
+        if( d_quantEngine->addInstantiation( f, m ) ){
+          ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+          return true;
         }
       }
     }
-    //term enumerator?
   }
-  return STATUS_UNKNOWN;
+  //term enumerator?
+  return false;
+}
+
+void FullSaturation::registerQuantifier( Node q ) {
+
+}
+
+void FullSaturation::assertNode( Node n ) {
+
 }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 02ddd233e..5163653cf 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -105,20 +105,22 @@ public:
   void addUserNoPattern( Node f, Node pat );
 };/* class InstStrategyAutoGenTriggers */
 
-class InstStrategyFreeVariable : public InstStrategy{
+class FullSaturation : public QuantifiersModule {
 private:
   /** guessed instantiations */
   std::map< Node, bool > d_guessed;
   /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  bool process( Node f, Theory::Effort effort );
 public:
-  InstStrategyFreeVariable( QuantifiersEngine* qe ) :
-      InstStrategy( qe ){}
-  ~InstStrategyFreeVariable(){}
+  FullSaturation( QuantifiersEngine* qe );
+  ~FullSaturation(){}
+  void reset_round( Theory::Effort e );
+  void check( Theory::Effort e, unsigned quant_e );
+  void registerQuantifier( Node q );
+  void assertNode( Node n );
   /** identify */
-  std::string identify() const { return std::string("FreeVariable"); }
-};/* class InstStrategyFreeVariable */
+  std::string identify() const { return std::string("FullSaturation"); }
+};/* class FullSaturation */
 
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2d637e1a0..8f1ef42d8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -31,14 +31,13 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe ) :
-QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
+QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_splx(NULL), d_i_cegqi( NULL ){
 
 }
 
 InstantiationEngine::~InstantiationEngine() {
   delete d_i_ag;
   delete d_isup;
-  delete d_i_fs;
   delete d_i_splx;
   delete d_i_cegqi;
 }
@@ -57,13 +56,7 @@ void InstantiationEngine::finishInit(){
     d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
     d_instStrategies.push_back( d_i_ag );
   }
-
-  //full saturation : instantiate from relevant domain, then arbitrary terms
-  if( options::fullSaturateQuant() ){
-    d_i_fs = new InstStrategyFreeVariable( d_quantEngine );
-    d_instStrategies.push_back( d_i_fs );
-  }
-
+  
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
     if( !options::cbqi2() ){
@@ -88,7 +81,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   if( options::cbqi() ){
     //check if any cbqi lemma has not been added yet
     bool addedLemma = false;
-    for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
         d_added_cbqi_lemma[f] = true;
@@ -136,7 +129,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   }
   //if not, proceed to instantiation round
   //reset the instantiation strategies
-  for( size_t i=0; i<d_instStrategies.size(); ++i ){
+  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
     InstStrategy* is = d_instStrategies[i];
     is->processResetInstantiationRound( effort );
   }
@@ -158,8 +151,8 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
       if( e_use>=0 ){
         Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
         //check each instantiation strategy
-        for( size_t i=0; i<d_instStrategies.size(); ++i ){
-          InstStrategy* is = d_instStrategies[i];
+        for( unsigned j=0; j<d_instStrategies.size(); j++ ){
+          InstStrategy* is = d_instStrategies[j];
           Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
           int quantStatus = is->process( q, effort, e_use );
           Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
@@ -200,7 +193,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ) {
   d_cbqi_set_quant_inactive = false;
   if( options::cbqi() ){
     //set inactive the quantified formulas whose CE literals are asserted false
-    for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) && hasAddedCbqiLemma( q ) ){
@@ -236,12 +229,12 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     bool quantActive = false;
     d_quants.clear();
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( d_quantEngine->hasOwnership( n, this ) && d_quantEngine->getModel()->isQuantifierActive( n ) ){
-        if( !options::cbqi() || !TermDb::hasInstConstAttr(n) ){
+      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        if( !options::cbqi() || !TermDb::hasInstConstAttr(q) ){
           quantActive = true;
         }
-        d_quants.push_back( n );
+        d_quants.push_back( q );
       }
     }
     Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index c789cd3b2..3b7a5f4f8 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -66,8 +66,6 @@ private:
   InstStrategyUserPatterns* d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
   InstStrategyAutoGenTriggers* d_i_ag;
-  /** full saturate */
-  InstStrategyFreeVariable * d_i_fs;
   /** simplex (cbqi) */
   InstStrategySimplex * d_i_splx;
   /** generic cegqi */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 752e88c5a..a3a18cf30 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -265,7 +265,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
       Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
-      if( !riter.d_incomplete || options::fmfFullSaturate() ){
+      if( !riter.d_incomplete ){
         int triedLemmas = 0;
         int addedLemmas = 0;
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a31fbe6e7..cd5f90a37 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -131,8 +131,6 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
-option fmfFullSaturate --fmf-full-saturate bool :default false
- instantiate with all known ground terms for infinite domain quantifiers when finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
  enable Inst-Gen instantiation techniques for finite model finding 
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
@@ -247,6 +245,10 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
   preregister ground instantiations in counterexample-based quantifier instantiation
 option cbqiMinBounds --cbqi-min-bounds bool :default false
   use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
+option cbqiSymLia --cbqi-sym-lia bool :default false
+  use symbolic integer division in substitutions for counterexample-based quantifier instantiation
+option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
+  round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a2c6a9ddf..e5b5c4080 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -39,6 +39,7 @@
 #include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/quant_equality_engine.h"
+#include "theory/quantifiers/inst_strategy_e_matching.h"
 
 using namespace std;
 using namespace CVC4;
@@ -186,7 +187,14 @@ d_presolve(u, true){
   }else{
     d_uee = NULL;
   }
-
+  
+  //full saturation : instantiate from relevant domain, then arbitrary terms
+  if( options::fullSaturateQuant() ){
+    d_fs = new quantifiers::FullSaturation( this );
+    d_modules.push_back( d_fs );
+  }else{
+    d_fs = NULL;
+  }
 
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
@@ -228,6 +236,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_lte_part_inst;
   delete d_fun_def_engine;
   delete d_uee;
+  delete d_fs;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
@@ -327,7 +336,16 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   
   d_hasAddedLemma = false;
-  
+  bool setIncomplete = false;
+  if( e==Theory::EFFORT_LAST_CALL ){
+    //sources of incompleteness
+    if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
+      Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl;
+      setIncomplete = true;
+    }
+  }
+  bool usedModelBuilder = false;
+    
   Trace("quant-engine-debug") << "Quantifiers Engine call to check, level = " << e << std::endl;
   if( needsCheck ){
     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
@@ -387,12 +405,13 @@ void QuantifiersEngine::check( Theory::Effort e ){
       ++(d_statistics.d_instantiation_rounds);
     }
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
-    for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
+    for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
       bool success = true;
       //build the model if any module requested it
       if( needsModelE==quant_e ){
         Assert( d_builder!=NULL );
         Trace("quant-engine-debug") << "Build model..." << std::endl;
+        usedModelBuilder = true;
         d_builder->d_addedLemmas = 0;
         d_builder->buildModel( d_model, false );
         //we are done if model building was unsuccessful
@@ -412,10 +431,23 @@ void QuantifiersEngine::check( Theory::Effort e ){
       //if we have added one, stop
       if( d_hasAddedLemma ){
         break;
-      //otherwise, complete the model generation if necessary
-      }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() && e==Theory::EFFORT_LAST_CALL ){
-        Trace("quant-engine-debug") << "Build completed model..." << std::endl;
-        d_builder->buildModel( d_model, true );
+      }else if( e==Theory::EFFORT_LAST_CALL && quant_e==QEFFORT_MODEL ){
+        //if we have a chance not to set incomplete
+        if( !setIncomplete ){
+          setIncomplete = true;
+          //check if we should set the incomplete flag
+          for( unsigned i=0; i<qm.size(); i++ ){
+            if( qm[i]->checkComplete() ){
+              Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl;
+              setIncomplete = false;
+              break;
+            }
+          }
+        }
+        //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
+        if( !setIncomplete ){
+          break;
+        }
       }
     }
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
@@ -432,34 +464,21 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }else{
     Trace("quant-engine") << "Quantifiers Engine does not need check." << std::endl;
   }
+  
   //SAT case
   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
-    if( options::produceModels() && !d_model->isModelSet() ){
-      //use default model builder when no module built the model
-      Trace("quant-engine-debug") << "Build the model..." << std::endl;
-      d_te->getModelBuilder()->buildModel( d_model, true );
-      Trace("quant-engine-debug") << "Done building the model." << std::endl;
-    }
-    bool setInc = false;
-    if( needsCheck ){
-      setInc = true;
-      for( unsigned i=0; i<qm.size(); i++ ){
-        if( qm[i]->checkComplete() ){
-          Trace("quant-engine-debug") << "Do not set incomplete because " << qm[i]->identify().c_str() << " was complete." << std::endl;
-          setInc = false;
-        }
-      }
-    }else{
-      Trace("quant-engine-debug") << "Do not set incomplete because check wasn't necessary." << std::endl;
-    }
-    //check other sources of incompleteness
-    if( !setInc ){
-      if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
-        Trace("quant-engine-debug") << "Set incomplete due to LTE partial instantiation." << std::endl;
-        setInc = true;
+    if( options::produceModels() ){
+      if( usedModelBuilder ){
+        Trace("quant-engine-debug") << "Build completed model..." << std::endl;
+        d_builder->buildModel( d_model, true );
+      }else if( !d_model->isModelSet() ){
+        //use default model builder when no module built the model
+        Trace("quant-engine-debug") << "Build the model..." << std::endl;
+        d_te->getModelBuilder()->buildModel( d_model, true );
+        Trace("quant-engine-debug") << "Done building the model." << std::endl;
       }
     }
-    if( setInc ){
+    if( setIncomplete ){
       Trace("quant-engine-debug") << "Set incomplete flag." << std::endl;
       getOutputChannel().setIncomplete();
     }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3cdd5bae7..4e3bba501 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -97,6 +97,7 @@ namespace quantifiers {
   class AlphaEquivalence;
   class FunDefEngine;
   class QuantEqualityEngine;
+  class FullSaturation;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -150,11 +151,14 @@ private:
   quantifiers::FunDefEngine * d_fun_def_engine;
   /** quantifiers equality engine */
   quantifiers::QuantEqualityEngine * d_uee;
+  /** full saturation */
+  quantifiers::FullSaturation * d_fs;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
     QEFFORT_STANDARD,
     QEFFORT_MODEL,
+    QEFFORT_LAST_CALL,
     //none
     QEFFORT_NONE,
   };
@@ -244,6 +248,8 @@ public:  //modules
   quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
   /** quantifiers equality engine */
   quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; }
+  /** get full saturation */
+  quantifiers::FullSaturation * getFullSaturation() { return d_fs; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;