Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.

13 files changed, 171 insertions, 84 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 34f399f45..227540f45 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -258,7 +258,7 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
 option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
   template mode for sygus invariant synthesis
 
-option sygusDirectEval --sygus-direct-eval bool :default false
+option sygusDirectEval --sygus-direct-eval bool :default true
   direct unfolding of evaluation functions
   
 # approach applied to general quantified formulas
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index cfbadbf32..5fdc549d0 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -459,7 +459,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
 
   if (Theory::isLeafOf(node, theory::THEORY_BV)) {
     // if it is a leaf may ask for fullModel
-    value = getModelFromSatSolver(node, fullModel); 
+    value = getModelFromSatSolver(node, true); 
     Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
     Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); 
     if (!value.isNull()) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 3b54e3794..a103d1f63 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -216,7 +216,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
       // only shared terms could not have been bit-blasted
       Assert (hasBBTerm(var) || isSharedTerm(var));
 
-      Node const_value = getModelFromSatSolver(var, fullModel);
+      Node const_value = getModelFromSatSolver(var, true);
 
       if(const_value != Node()) {
         Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index c821b50cd..b549c329a 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -491,7 +491,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
     // only shared terms could not have been bit-blasted
     Assert (hasBBTerm(var) || isSharedTerm(var));
 
-    Node const_value = getModelFromSatSolver(var, fullModel);
+    Node const_value = getModelFromSatSolver(var, true);
     Assert (const_value.isNull() || const_value.isConst());
     if(const_value != Node()) {
       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 152a335a5..2bcb6ca1b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -349,7 +349,7 @@ Node RewriteRule<SdivEliminate>::apply(TNode node) {
   Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
   Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
 
-  Node a_udiv_b   = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b);
+  Node a_udiv_b   = utils::mkNode(options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UDIV, abs_a, abs_b);
   Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b);
   
   Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0);
@@ -377,7 +377,7 @@ Node RewriteRule<SremEliminate>::apply(TNode node) {
   Node abs_a   = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a);
   Node abs_b   = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b);
 
-  Node a_urem_b   = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b);
+  Node a_urem_b   = utils::mkNode( options::bitvectorDivByZeroConst() ? kind::BITVECTOR_UREM_TOTAL : kind::BITVECTOR_UREM, abs_a, abs_b);
   Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b);
   
   Node result    = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b);
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 5bd6680f2..b32a70212 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -420,13 +420,14 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     }
   }
   //push
-  if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG ){
+  if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG || k==ITE ){
      //negation normal form
     if( parent==k && isArgDatatype( dt[c], 0, pdt ) ){
       return false;
     }
     Kind nk = UNDEFINED_KIND;
-    Kind reqk = UNDEFINED_KIND;  //required kind for all children
+    Kind reqk = UNDEFINED_KIND;       //required kind for all children
+    std::map< unsigned, Kind > reqkc; //required kind for some children
     if( parent==NOT ){
       if( k==AND ) {
         nk = OR;reqk = NOT;
@@ -437,8 +438,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
       }else if( k==XOR ) {
         nk = IFF;
       }
-    }
-    if( parent==BITVECTOR_NOT ){
+    }else if( parent==BITVECTOR_NOT ){
       if( k==BITVECTOR_AND ) {
         nk = BITVECTOR_OR;reqk = BITVECTOR_NOT;
       }else if( k==BITVECTOR_OR ){
@@ -448,16 +448,21 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
       }else if( k==BITVECTOR_XOR ) {
         nk = BITVECTOR_XNOR;
       }
-    }
-    if( parent==UMINUS ){
+    }else if( parent==UMINUS ){
       if( k==PLUS ){
         nk = PLUS;reqk = UMINUS;
       }
-    }
-    if( parent==BITVECTOR_NEG ){
+    }else if( parent==BITVECTOR_NEG ){
       if( k==PLUS ){
         nk = PLUS;reqk = BITVECTOR_NEG;
       }
+    }else if( k==ITE ){
+      //ITE lifting
+      if( parent!=ITE ){
+        nk = ITE;
+        reqkc[1] = parent;
+        reqkc[2] = parent;
+      }
     }
     if( nk!=UNDEFINED_KIND ){
       Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk;
@@ -468,37 +473,38 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
       int pcr = d_tds->getKindArg( tnp, nk );
       if( pcr!=-1 ){
         Assert( pcr<(int)pdt.getNumConstructors() );
-        if( reqk!=UNDEFINED_KIND ){
+        if( reqk!=UNDEFINED_KIND || !reqkc.empty() ){
           //must have same number of arguments
           if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){
-            bool success = true;
-            std::map< int, TypeNode > childTypes;
             for( unsigned i=0; i<pdt[pcr].getNumArgs(); i++ ){
               TypeNode tna = d_tds->getArgType( pdt[pcr], i );
               Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
+              std::vector< Kind > rks;
               if( reqk!=UNDEFINED_KIND ){
-                //child must have a NOT
-                int nindex = d_tds->getKindArg( tna, reqk );
+                rks.push_back( reqk );
+              }
+              std::map< unsigned, Kind >::iterator itr = reqkc.find( i );
+              if( itr!=reqkc.end() ){
+                rks.push_back( itr->second );
+              }
+              for( unsigned j=0; j<rks.size(); j++ ){
+                Kind rkc = rks[j];
+                //child must have reqk
+                int nindex = d_tds->getKindArg( tna, rkc );
                 if( nindex!=-1 ){
                   const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
                   if( d_tds->getArgType( dt[c], i )!=d_tds->getArgType( adt[nindex], 0 ) ){
                     Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl;
-                    success = false;
-                    break;
+                    return true;
                   }
                 }else{
-                  Trace("sygus-split-debug") << "...argument " << i << " does not have " << reqk << "." << std::endl;
-                  success = false;
-                  break;
+                  Trace("sygus-split-debug") << "...argument " << i << " does not have " << rkc << "." << std::endl;
+                  return true;
                 }
-              }else{
-                childTypes[i] = tna;
               }
             }
-            if( success ){
-              Trace("sygus-split-debug") << "...success" << std::endl;
-              return false;
-            }
+            Trace("sygus-split-debug") << "...success" << std::endl;
+            return false;
           }else{
             Trace("sygus-split-debug") << "...#arg mismatch." << std::endl;
           }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index cae3e730e..8af11b1af 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
 #include "prop/prop_engine.h"
+#include "theory/bv/theory_bv_rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -56,12 +57,15 @@ void CegConjecture::assign( Node q ) {
     }
   }
   d_quant = q;
+  Assert( d_candidates.empty() );
+  std::vector< Node > vars;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    vars.push_back( q[0][i] );
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
   Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
   //construct base instantiation
-  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) );
+  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
   if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
     CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
@@ -272,9 +276,26 @@ void CegInstantiation::preRegisterQuantifier( Node q ) {
         if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
           const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
           if( dt.isSygus() ){
-            //take ownership of this quantified formula (will use direct evaluation instead of instantiation)
-            d_quantEngine->setOwner( q, this );
-            d_eval_axioms[q] = true;
+            //do unfolding if it induces Boolean structure, 
+            //do direct evaluation if it does not induce Boolean structure,
+            //  the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms
+            bool directEval = true;
+            TypeNode ptn = pat.getType();
+            if( ptn.isBoolean() || ptn.isBitVector() ){
+              directEval = false;
+            }else{
+              unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() );
+              Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex );
+              Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl;
+              if( base.getKind()==ITE ){
+                directEval = false;
+              }
+            }
+            if( directEval ){
+              //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation)
+              d_quantEngine->setOwner( q, this );
+              d_eval_axioms[q] = true;
+            }
           }
         }
       }
@@ -413,8 +434,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           }
           if( !eager_eval_lem.empty() ){
             for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
-              Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl;
-              d_quantEngine->addLemma( eager_eval_lem[j] );
+              Node lem = eager_eval_lem[j];
+              if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
+                //FIXME: hack to incorporate hacks from BV for division by zero
+                lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
+              }
+              Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
+              d_quantEngine->addLemma( lem );
             }
             return;
           }
@@ -435,6 +461,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           }
         }
         //must get a counterexample to the value of the current candidate
+        Assert( conj->d_candidates.size()==model_values.size() );
         Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
         //check whether we will run CEGIS on inner skolem variables
         bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 );
@@ -686,6 +713,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited )
             }
             Assert( subs[j-1].getType()==var_list[j-1].getType() );
           }
+          Assert( vars.size()==subs.size() );
           bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
           Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
           Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 33856d226..a5d4174dd 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -534,6 +534,7 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
     return false;
   }else{
     Trace("cegqi-engine") << siss.str() << std::endl;
+    Assert( d_single_inv_var.size()==subs.size() );
     Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
     if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){
       Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
@@ -595,6 +596,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) {
           for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){
             subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) );
           }
+          Assert( d_sip->d_all_vars.size()==subs.size() );
           inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() );
           Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl;
           Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl;
@@ -751,6 +753,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     std::sort( indices.begin(), indices.end(), ssii );
     Trace("csi-sol") << "Construct solution" << std::endl;
     s = constructSolution( indices, sol_index, 0 );
+    Assert( vars.size()==d_sol->d_varList.size() );
     s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
   }
   d_orig_solution = s;
@@ -922,6 +925,7 @@ void SingleInvocationPartition::process( Node n ) {
         std::vector< Node > funcs;
         //normalize the invocations
         if( !terms.empty() ){
+          Assert( terms.size()==subs.size() );
           cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
         }
         std::vector< Node > children;
@@ -940,6 +944,7 @@ void SingleInvocationPartition::process( Node n ) {
         }
         Trace("si-prt") << std::endl;
         cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+        Assert( terms.size()==subs.size() );
         cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
         Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl;
         //now must check if it has other bound variables
@@ -974,6 +979,7 @@ void SingleInvocationPartition::process( Node n ) {
             }
           }
         }
+        Assert( terms.size()==subs.size() );
         cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
       }
       cr = Rewriter::rewrite( cr );
@@ -982,6 +988,7 @@ void SingleInvocationPartition::process( Node n ) {
       TermDb::getBoundVars( cr, d_all_vars );
       if( singleInvocation ){
         //replace with single invocation formulation
+        Assert( si_terms.size()==si_subs.size() );
         cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
         cr = Rewriter::rewrite( cr );
         Trace("si-prt") << ".....si version=" << cr << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index eff641736..e81245034 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2480,8 +2480,8 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
   std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
   if( it==d_sygus_to_builtin[tn].end() ){
     Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl;
-    Assert( n.getKind()==APPLY_CONSTRUCTOR );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( n.getKind()==APPLY_CONSTRUCTOR );
     unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
     Assert( n.getNumChildren()==dt[i].getNumArgs() );
     std::map< TypeNode, int > var_count;
@@ -3200,9 +3200,17 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
   }
 }
 
+Node TermDbSygus::getAnchor( Node n ) {
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    return getAnchor( n[0] );
+  }else{
+    return n;
+  }
+}
+
 void TermDbSygus::registerEvalTerm( Node n ) {
   if( options::sygusDirectEval() ){
-    if( n.getKind()==APPLY_UF ){
+    if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
       Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
       TypeNode tn = n[0].getType();
       if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
@@ -3210,58 +3218,72 @@ void TermDbSygus::registerEvalTerm( Node n ) {
         if( dt.isSygus() ){
           Node f = n.getOperator();
           Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl;
-          Assert( n[0].getKind()!=APPLY_CONSTRUCTOR );
-          d_evals[n[0]].push_back( n );
-          TypeNode tn = n[0].getType();
-          Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
-          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-          Node var_list = Node::fromExpr( dt.getSygusVarList() );
-          Assert( dt.isSygus() );
-          d_eval_args[n[0]].push_back( std::vector< Node >() );
-          for( unsigned j=1; j<n.getNumChildren(); j++ ){
-            if( var_list[j-1].getType().isBoolean() ){
-              //TODO: remove this case when boolean term conversion is eliminated
-              Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-              d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
-            }else{
-              d_eval_args[n[0]].back().push_back( n[j] );
+          if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
+            d_evals[n[0]].push_back( n );
+            TypeNode tn = n[0].getType();
+            Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+            Node var_list = Node::fromExpr( dt.getSygusVarList() );
+            Assert( dt.isSygus() );
+            d_eval_args[n[0]].push_back( std::vector< Node >() );
+            for( unsigned j=1; j<n.getNumChildren(); j++ ){
+              if( var_list[j-1].getType().isBoolean() ){
+                //TODO: remove this case when boolean term conversion is eliminated
+                Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+                d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) );
+              }else{
+                d_eval_args[n[0]].back().push_back( n[j] );
+              }
             }
+            Node a = getAnchor( n[0] );
+            d_subterms[a][n[0]] = true;
           }
-
         }
       }    
     }
   }
 }
 
-void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) {
-  std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
-  if( it!=d_eval_args.end() && !it->second.empty() ){
-    unsigned start = d_node_mv_args_proc[n][v];
-    Node antec = n.eqNode( v ).negate();
-    TypeNode tn = n.getType();
-    Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl;
-    Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
-    Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn );
-    Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
-    std::vector< Node > vars;
-    Node var_list = Node::fromExpr( dt.getSygusVarList() );
-    for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
-      vars.push_back( var_list[j] );
-    }
-    //for each evaluation
-    for( unsigned i=start; i<it->second.size(); i++ ){
-      Assert( vars.size()==it->second[i].size() );
-      Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
-      Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); 
-      lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
-      Trace("sygus-eager") << "Lemma : " << lem << std::endl;
-      lems.push_back( lem );
-    }
-    d_node_mv_args_proc[n][v] = it->second.size();
+void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) {
+  std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
+  if( its!=d_subterms.end() ){
+    Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
+    for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){
+      Node n = itss->first;
+      Trace("sygus-eager-debug") << "...process : " << n << std::endl;
+      std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
+      if( it!=d_eval_args.end() && !it->second.empty() ){
+        TNode at = a;
+        TNode vt = v;
+        Node vn = n.substitute( at, vt );
+        vn = Rewriter::rewrite( vn );
+        unsigned start = d_node_mv_args_proc[n][vn];
+        Node antec = n.eqNode( vn ).negate();
+        TypeNode tn = n.getType();
+        Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        Assert( dt.isSygus() );
+        Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
+        Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
+        Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, tn );
+        Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
+        std::vector< Node > vars;
+        Node var_list = Node::fromExpr( dt.getSygusVarList() );
+        for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
+          vars.push_back( var_list[j] );
+        }
+        //for each evaluation
+        for( unsigned i=start; i<it->second.size(); i++ ){
+          Assert( vars.size()==it->second[i].size() );
+          Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
+          Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); 
+          lem = NodeManager::currentNM()->mkNode( OR, antec, lem );
+          Trace("sygus-eager") << "Lemma : " << lem << std::endl;
+          lems.push_back( lem );
+        }
+        d_node_mv_args_proc[n][vn] = it->second.size();
+      }
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 4291587a4..b7b798cd4 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -557,7 +557,6 @@ public:
 private:
   std::map< TypeNode, std::map< int, Node > > d_generic_base;
   std::map< TypeNode, std::vector< Node > > d_generic_templ;
-  Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
   bool getMatch( Node p, Node n, std::map< int, Node >& s );
   bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s );
 public:
@@ -622,6 +621,7 @@ public:
   /** get value */
   Node getTypeMaxValue( TypeNode tn );
   TypeNode getSygusTypeForVar( Node v );
+  Node getGenericBase( TypeNode tn, const Datatype& dt, int c );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
   Node sygusToBuiltin( Node n, TypeNode tn );
   Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
@@ -641,8 +641,11 @@ public:
   /** print sygus term */
   static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs );
   
+  /** get anchor */
+  static Node getAnchor( Node n );
 //for eager instantiation
 private:
+  std::map< Node, std::map< Node, bool > > d_subterms;
   std::map< Node, std::vector< Node > > d_evals;
   std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
   std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 21be4ea4f..8984cc5f4 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -655,6 +655,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
       for( unsigned i=0; i<d_modules.size(); i++ ){
         d_modules[i]->registerQuantifier( f );
       }
+      //TODO: remove this
       Node ceBody = d_term_db->getInstConstantBody( f );
       //also register it with the strong solver
       //if( options::finiteModelFind() ){
@@ -887,6 +888,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
   Node body;
   //process partial instantiation if necessary
   if( d_term_db->d_vars[q].size()!=vars.size() ){
+    Assert( vars.size()==terms.size() );
     body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     std::vector< Node > uninst_vars;
     //doing a partial instantiation, must add quantifier for all uninstantiated variables
@@ -901,6 +903,7 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std
     Trace("partial-inst") << "                      : " << body << std::endl;
   }else{
     if( options::cbqi() ){
+      Assert( vars.size()==terms.size() );
       body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
     }else{
       //do optimized version
@@ -933,6 +936,7 @@ Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
 }
 
 Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
+  Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
   return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
 }
 
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 695c52cc6..b503a65b8 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -50,7 +50,8 @@ TESTS = commutative.sy \
         no-mention.sy \
         max2-univ.sy \
         strings-small.sy \
-        strings-unconstrained.sy
+        strings-unconstrained.sy \
+        hd-sdiv.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress0/sygus/hd-sdiv.sy
new file mode 100644
index 000000000..3ac9334b2
--- /dev/null
+++ b/test/regress/regress0/sygus/hd-sdiv.sy
@@ -0,0 +1,16 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
+(set-logic BV)
+
+(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32)
+    ((Start (BitVec 32) ((bvsdiv Start Start)
+						             (bvand Start Start)
+                         x
+                         #x00000001))))
+
+(declare-var y (BitVec 32))
+(constraint (= (hd01 y) (f y)))
+(check-synth)
+