Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

1 files changed, 304 insertions, 1183 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e82af63e4..63e8aa365 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/datatype.h"
 #include "options/quantifiers_options.h"
+#include "options/datatypes_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
@@ -32,19 +33,142 @@ namespace quantifiers {
 
 
 CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c )
-    : d_qe( qe ), d_curr_lit( c, 0 ) {
+    : d_qe( qe ) {
   d_refine_count = 0;
   d_ceg_si = new CegConjectureSingleInv( qe, this );
+  d_ceg_pbe = new CegConjecturePbe( qe, this );
 }
 
 CegConjecture::~CegConjecture() {
   delete d_ceg_si;
+  delete d_ceg_pbe;
+}
+
+Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    
+    std::vector< Node > children;
+    bool childChanged = false;
+    bool madeOp = false;
+    Kind ret_k = n.getKind();
+    Node op;
+    if( n.getNumChildren()>0 ){
+      if( n.getKind()==kind::APPLY_UF ){
+        op = n.getOperator();
+      }
+    }else{
+      op = n;
+    }
+    // is it a synth function?
+    std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
+    if( its!=synth_fun_vars.end() ){
+      Assert( its->second.getType().isDatatype() );
+      // make into evaluation function
+      const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
+      Assert( dt.isSygus() );
+      children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
+      children.push_back( its->second );
+      madeOp = true;
+      childChanged = true;
+      ret_k = kind::APPLY_UF;
+    }
+    if( n.getNumChildren()>0 || childChanged ){
+      if( !madeOp ){
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.push_back( n.getOperator() );
+        }
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = convertToEmbedding( n[i], synth_fun_vars, visited ); 
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( ret_k, children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
+void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.isConst() ){
+      TypeNode tn = n.getType();
+      Node nc = n;
+      if( tn.isReal() ){
+        nc = NodeManager::currentNM()->mkConst( n.getConst<Rational>().abs() );
+      }
+      if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){
+        Trace("cegqi-debug") << "...consider const : " << nc << std::endl;
+        consts[tn].push_back( nc );
+      }
+    }
+    
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectConstants( n[i], consts, visited );
+    }
+  }
 }
 
 void CegConjecture::assign( Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
+  Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
   d_assert_quant = q;
+  std::map< TypeNode, std::vector< Node > > extra_cons;
+  
+  Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
+  if( options::sygusAddConstGrammar() ){
+    std::map< Node, bool > cvisited;
+    collectConstants( q[1], extra_cons, cvisited );
+  } 
+  
+  Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
+  //convert to deep embedding
+  std::vector< Node > qchildren;
+  std::map< Node, Node > visited;
+  std::map< Node, Node > synth_fun_vars;
+  std::vector< Node > ebvl;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    Node v = q[0][i];
+    Node sf = v.getAttribute(SygusSynthFunAttribute());
+    Assert( !sf.isNull() );
+    Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
+    // sfvl may be null for constant synthesis functions
+    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+    TypeNode tn;
+    if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
+      tn = v.getType();
+    }else{
+      // make the default grammar
+      std::stringstream ss;
+      ss << sf;
+      tn = d_qe->getTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
+    }
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    // ev is the first-order variable corresponding to this synth fun
+    std::stringstream ss;
+    ss << "f" << sf;
+    Node ev = NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); 
+    ebvl.push_back( ev );
+    synth_fun_vars[sf] = ev;
+    Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl;
+  }
+  qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
+  qchildren.push_back( convertToEmbedding( q[1], synth_fun_vars, visited ) );
+  if( q.getNumChildren()==3 ){
+    qchildren.push_back( q[2] );
+  }
+  q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
+  Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl;
+
   //register with single invocation if applicable
   if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){
     d_ceg_si->initialize( q );
@@ -52,18 +176,44 @@ void CegConjecture::assign( Node q ) {
       //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );
       //may have rewritten quantified formula (for invariant synthesis)
       q = d_ceg_si->d_quant;
+      Assert( q.getKind()==kind::FORALL );
     }
   }
+
   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() ) );
+    Node e = NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() );
+    d_candidates.push_back( e );
   }
   Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
   //construct base instantiation
   d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
+  
+  // register this term with sygus database
+  std::vector< Node > guarded_lemmas;
+  if( !isSingleInvocation() ){
+    if( options::sygusPbe() ){
+      d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
+    }
+    for( unsigned i=0; i<d_candidates.size(); i++ ){
+      Node e = d_candidates[i];
+      if( options::sygusPbe() ){
+        std::vector< std::vector< Node > > exs;
+        std::vector< Node > exos;
+        std::vector< Node > exts;
+        // use the PBE examples, regardless of the search algorith, since these help search space pruning
+        if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){
+          d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts );
+        }
+      }else{
+        d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e );
+      }
+    }
+  }
+  
   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 );
@@ -80,269 +230,50 @@ void CegConjecture::assign( Node q ) {
         }
       }
     }
-    if( options::sygusUnifCondSol() ){
-      // for each variable, determine whether we can do conditional counterexamples
-      for( unsigned i=0; i<d_candidates.size(); i++ ){
-        registerCandidateConditional( d_candidates[i] );
-      }
-    }
     d_syntax_guided = true;
   }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
     d_syntax_guided = false;
   }else{
     Assert( false );
   }
-}
-
-void CegConjecture::registerCandidateConditional( Node v ) {
-  TypeNode tn = v.getType();
-  bool type_valid = false;
-  bool success = false;
-  std::vector< TypeNode > unif_types;
-  if( tn.isDatatype() ){
-    const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
-    if( dt.isSygus() ){
-      type_valid = true;
-      if( d_candidates.size()==1 ){  // conditional solutions for multiple function conjectures TODO?
-        for( unsigned r=0; r<2; r++ ){
-          for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-            Node op = Node::fromExpr( dt[j].getSygusOp() );
-            if( r==0 ){
-              if( op.getKind() == kind::BUILTIN ){
-                Kind sk = NodeManager::operatorToKind( op );
-                if( sk==kind::ITE ){
-                  // we can do unification
-                  success = true;
-                  d_cinfo[v].d_csol_op = Node::fromExpr( dt[j].getConstructor() );
-                  Assert( dt[j].getNumArgs()==3 );
-                  for( unsigned k=0; k<3; k++ ){
-                    unif_types.push_back( TypeNode::fromType( dt[j][k].getRangeType() ) );
-                  }
-                  break;
-                }
-              }
-            }else{
-              if( dt[j].getNumArgs()>=3 ){
-                // could be a defined ITE (this is a hack for ICFP benchmarks)
-                std::vector< Node > utchildren;
-                utchildren.push_back( Node::fromExpr( dt[j].getConstructor() ) );
-                std::vector< Node > sks;
-                for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-                  Type t = dt[j][k].getRangeType();
-                  Node kv = NodeManager::currentNM()->mkSkolem( "ut", TypeNode::fromType( t ) );
-                  sks.push_back( kv );
-                  utchildren.push_back( kv );
-                }
-                Node ut = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, utchildren );
-                std::vector< Node > echildren;
-                echildren.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
-                echildren.push_back( ut );
-                Node sbvl = Node::fromExpr( dt.getSygusVarList() );
-                for( unsigned k=0; k<sbvl.getNumChildren(); k++ ){
-                  echildren.push_back( sbvl[k] );
-                }
-                Node eut = NodeManager::currentNM()->mkNode( kind::APPLY_UF, echildren );
-                Trace("sygus-unif-debug") << "Test evaluation of " << eut << "..." << std::endl;
-                eut = d_qe->getTermDatabaseSygus()->unfold( eut );
-                Trace("sygus-unif-debug") << "...got " << eut << std::endl;
-                if( eut.getKind()==kind::ITE ){
-                  success = true;
-                  std::vector< Node > vs;
-                  std::vector< Node > ss;
-                  std::map< Node, unsigned > templ_var_index;
-                  for( unsigned k=0; k<sks.size(); k++ ){
-                    echildren[1] = sks[k];
-                    Node esk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, echildren );
-                    vs.push_back( esk );
-                    Node tvar = NodeManager::currentNM()->mkSkolem( "templ", esk.getType() );
-                    templ_var_index[tvar] = k;
-                    ss.push_back( tvar );
-                  }
-                  eut = eut.substitute( vs.begin(), vs.end(), ss.begin(), ss.end() );
-                  Trace("sygus-unif") << "Defined constructor " << j << ", base term is " << eut << std::endl;
-                  //success if we can find a injection from ITE args to sygus args
-                  std::map< unsigned, unsigned > templ_injection;
-                  for( unsigned k=0; k<3; k++ ){
-                    if( !inferIteTemplate( k, eut[k], templ_var_index, templ_injection ) ){
-                      Trace("sygus-unif") << "...failed to find injection (range)." << std::endl;
-                      success = false;
-                      break;
-                    }
-                    if( templ_injection.find( k )==templ_injection.end() ){
-                      Trace("sygus-unif") << "...failed to find injection (domain)." << std::endl;
-                      success = false;
-                      break;
-                    }
-                  }
-                  if( success ){
-                    d_cinfo[v].d_csol_op = Node::fromExpr( dt[j].getConstructor() );
-                    for( unsigned k=0; k<3; k++ ){
-                      Assert( templ_injection.find( k )!=templ_injection.end() );
-                      unsigned sk_index = templ_injection[k];
-                      unif_types.push_back( sks[sk_index].getType() );
-                      //also store the template information, if necessary
-                      Node teut = eut[k];
-                      if( !teut.isVar() ){
-                        d_cinfo[v].d_template[k] = teut;
-                        d_cinfo[v].d_template_arg[k] = ss[sk_index];
-                        Trace("sygus-unif") << "  Arg " << k << " : template : " << teut << ", arg " << ss[sk_index] << std::endl;
-                      }else{
-                        Assert( teut==ss[sk_index] );
-                      }
-                    }
-                  }
-                }
-              }
-            }
-          }
-          if( success ){
-            break;
-          }
-        }
-      }
-    }
-  }
-  //mark active
-  if( !success ){
-    d_cinfo[v].d_csol_status = -1;
-  }else{     
-    //make progress guard
-    Node pg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "P", NodeManager::currentNM()->booleanType(), "Progress guard for conditional solution." ) );
-    Node pglem = NodeManager::currentNM()->mkNode( kind::OR, pg.negate(), pg );
-    Trace("cegqi-lemma") << "Cegqi::Lemma : progress split : " << pglem << std::endl;
-    d_qe->getOutputChannel().lemma( pglem );
-    d_qe->getOutputChannel().requirePhase( pg, true );
-              
-    Assert( unif_types.size()==3 ); 
-    d_cinfo[v].d_csol_cond = NodeManager::currentNM()->mkSkolem( "c", unif_types[0] );
-    for( unsigned k=0; k<2; k++ ){
-      d_cinfo[v].d_csol_var[k] = NodeManager::currentNM()->mkSkolem( "e", unif_types[k+1] );
-      // optimization : need not be an ITE if types are equivalent  TODO
-    }
-    d_cinfo[v].d_csol_progress_guard = pg;
-    Trace("sygus-unif") << "Can do synthesis unification for variable " << v << ", based on operator " << d_cinfo[v].d_csol_op << std::endl;
-  }
-  if( !type_valid ){
-    Assert( false );
-  }
-}
-
-bool CegConjecture::inferIteTemplate( unsigned k, Node n, std::map< Node, unsigned >& templ_var_index, std::map< unsigned, unsigned >& templ_injection ){
-  if( n.getNumChildren()==0 ){
-    std::map< Node, unsigned >::iterator itt = templ_var_index.find( n );
-    if( itt!=templ_var_index.end() ){
-      unsigned kk = itt->second;
-      std::map< unsigned, unsigned >::iterator itti = templ_injection.find( k );
-      if( itti==templ_injection.end() ){
-        templ_injection[k] = kk;
-      }else if( itti->second!=kk ){
-        return false;
-      }
-    }
-    return true;
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !inferIteTemplate( k, n[i], templ_var_index, templ_injection ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-void CegConjecture::initializeGuard(){
-  if( isAssigned() ){
-    if( !d_syntax_guided ){
-      if( d_nsg_guard.isNull() ){
-        d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-        d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
-        AlwaysAssert( !d_nsg_guard.isNull() );
-        d_qe->getOutputChannel().requirePhase( d_nsg_guard, true );
-        //add immediate lemma
-        Node lem = NodeManager::currentNM()->mkNode( OR, d_nsg_guard.negate(), d_base_inst.negate() );
-        Trace("cegqi-lemma") << "Cegqi::Lemma : non-syntax-guided : " << lem << std::endl;
-        d_qe->getOutputChannel().lemma( lem );
-      }
-    }else if( d_ceg_si->d_si_guard.isNull() ){
-      std::vector< Node > lems;
-      d_ceg_si->getInitialSingleInvLemma( lems );
-      for( unsigned i=0; i<lems.size(); i++ ){
-        Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
-        d_qe->getOutputChannel().lemma( lems[i] );
-        if( Trace.isOn("cegqi-debug") ){
-          Node rlem = Rewriter::rewrite( lems[i] );
-          Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
-        }
+  
+  // initialize the guard
+  if( !d_syntax_guided ){
+    if( d_nsg_guard.isNull() ){
+      d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+      d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
+      AlwaysAssert( !d_nsg_guard.isNull() );
+      d_qe->getOutputChannel().requirePhase( d_nsg_guard, true );
+      // negated base as a guarded lemma
+      guarded_lemmas.push_back( d_base_inst.negate() );
+    }
+  }else if( d_ceg_si->d_si_guard.isNull() ){
+    std::vector< Node > lems;
+    d_ceg_si->getInitialSingleInvLemma( lems );
+    for( unsigned i=0; i<lems.size(); i++ ){
+      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
+      d_qe->getOutputChannel().lemma( lems[i] );
+      if( Trace.isOn("cegqi-debug") ){
+        Node rlem = Rewriter::rewrite( lems[i] );
+        Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
       }
     }
-    Assert( !getGuard().isNull() );
   }
-}
-
-void CegConjecture::setMeasureTerm( Node mt ){ 
-  d_measure_term = mt;
-  d_active_measure_term = mt;
-}
-
-Node CegConjecture::getMeasureTermFactor( Node v ) {
-  Node ret;
-  if( getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){
-    if( v.getType().isDatatype() ){
-      ret = NodeManager::currentNM()->mkNode( DT_SIZE, v );
-    }
+  Assert( !getGuard().isNull() );
+  Node gneg = getGuard().negate();
+  for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
+    Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
+    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
+    d_qe->getOutputChannel().lemma( lem );
   }
-  //TODO
-  Assert( ret.isNull() || ret.getType().isInteger() );
-  return ret;
-}
-  
   
-Node CegConjecture::getFairnessLiteral( int i ) {
-  if( d_measure_term.isNull() ){
-    return Node::null();
-  }else{
-    std::map< int, Node >::iterator it = d_lits.find( i );
-    if( it==d_lits.end() ){
-      Trace("cegqi-engine") << "******* CEGQI : allocate size literal " << i << std::endl;
-      Node c = NodeManager::currentNM()->mkConst( Rational( i ) );
-      Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, c );
-      lit = Rewriter::rewrite( lit );
-      d_lits[i] = lit;
-
-      Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
-      Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl;
-      d_qe->getOutputChannel().lemma( lem );
-      d_qe->getOutputChannel().requirePhase( lit, true );
-
-      if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){
-        //implies height bounds on each candidate variable
-        std::vector< Node > lem_c;
-        for( unsigned j=0; j<d_candidates.size(); j++ ){
-          if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){
-            lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) );
-          }else{
-            //lem_c.push_back( NodeManager::currentNM()->mkNode( DT_SIZE_BOUND, d_candidates[j], c ) );
-          }
-        }
-        Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) );
-        Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (pred) : " << hlem << std::endl;
-        d_qe->getOutputChannel().lemma( hlem );
-      }
-      return lit;
-    }else{
-      return it->second;
-    }
-  }
+  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
 }
 
 Node CegConjecture::getGuard() {
   return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard;
 }
 
-CegqiFairMode CegConjecture::getCegqiFairMode() {
-  return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair();
-}
-
 bool CegConjecture::isSingleInvocation() const {
   return d_ceg_si->isSingleInvocation();
 }
@@ -410,99 +341,21 @@ bool CegConjecture::needsRefinement() {
   return !d_ce_sk.empty();
 }
 
-void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){
-  Assert( options::sygusUnifCondSol() );
-  std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
-  if( it!=d_cinfo.end() ){
-    if( !it->second.d_csol_cond.isNull() ){
-      if( it->second.d_csol_status!=-1 ){
-        int pstatus = getProgressStatus( curr );
-        if( pstatus!=-1 ){
-          Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 );
-          //interested in model value for condition and branched variables
-          clist.push_back( it->second.d_csol_cond );
-          //assume_flat_ITEs
-          clist.push_back( it->second.d_csol_var[it->second.d_csol_status] );
-          //conditionally get the other branch
-          getConditionalCandidateList( clist, it->second.d_csol_var[1-it->second.d_csol_status], false );
-          return;
-        }else{
-          // it is progress-inactive, will not be included
-        }
-      }
-      //otherwise, yet to expand branch
-      if( !reqAdd ){
-        // if we are not top-level, we can ignore this (it won't be part of solution)
-        return;
-      }
-    }else{
-      // a standard variable not handlable by unification
-    }
-    clist.push_back( curr );
-  }
-}
-
 void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
-  if( options::sygusUnifCondSol() && !forceOrig ){
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      getConditionalCandidateList( clist, d_candidates[i], true );
-    }
+  if( d_ceg_pbe->isPbe() && !forceOrig ){
+    //Assert( isGround() );
+    d_ceg_pbe->getCandidateList( d_candidates, clist );
   }else{
     clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() );
   }
 }
 
-Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ) {
-  Assert( options::sygusUnifCondSol() );
-  std::map< Node, Node >::iterator itc = cmv.find( curr );
-  if( itc!=cmv.end() ){
-    return itc->second;
-  }else{
-    std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
-    if( it!=d_cinfo.end() ){
-      if( !it->second.d_csol_cond.isNull() ){
-        if( it->second.d_csol_status!=-1 ){
-          int pstatus = getProgressStatus( curr );
-          if( pstatus!=-1 ){
-            Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 );
-            Node v_curr = constructConditionalCandidate( cmv, it->second.d_csol_var[it->second.d_csol_status] );
-            Node v_next = constructConditionalCandidate( cmv, it->second.d_csol_var[1-it->second.d_csol_status] );
-            if( v_next.isNull() ){
-              // try taking current branch as a leaf
-              return v_curr;
-            }else{
-              Node v_cond = constructConditionalCandidate( cmv, it->second.d_csol_cond );
-              std::vector< Node > args;
-              args.push_back( it->second.d_csol_op );
-              args.push_back( v_cond );
-              args.push_back( it->second.d_csol_status==0 ? v_curr : v_next );
-              args.push_back( it->second.d_csol_status==0 ? v_next : v_curr );
-              return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, args );
-            }
-          }
-        }
-      }
-    }
-  }
-  return Node::null();
-}
-
-bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values ) {
+bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, 
+                                         std::vector< Node >& lems ) {
   Assert( clist.size()==model_values.size() );
-  if( options::sygusUnifCondSol() ){
-    std::map< Node, Node > cmv;
-    for( unsigned i=0; i<clist.size(); i++ ){
-      cmv[ clist[i] ] = model_values[i];
-    }
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      Node n = constructConditionalCandidate( cmv, d_candidates[i] );
-      Trace("cegqi-candidate") << "...constructed conditional candidate " << n << " for " << d_candidates[i] << std::endl;
-      candidate_values.push_back( n );
-      if( n.isNull() ){
-        Assert( false ); //currently should never happen
-        return false;
-      }
-    }
+  if( d_ceg_pbe->isPbe() ){
+    //Assert( isGround() );
+    return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems );
   }else{
     Assert( model_values.size()==d_candidates.size() );
     candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() );
@@ -515,175 +368,73 @@ void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector<
   getCandidateList( clist );
   std::vector< Node > c_model_values;
   Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
-  if( constructCandidates( clist, model_values, c_model_values ) ){
-    Assert( c_model_values.size()==d_candidates.size() );
+  bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems );
+
+  //must get a counterexample to the value of the current candidate
+  Node inst;
+  if( constructed_cand ){
     if( Trace.isOn("cegqi-check")  ){
       Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl;
       for( unsigned i=0; i<c_model_values.size(); i++ ){
         Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl;
       }
     }
-    //must get a counterexample to the value of the current candidate
-    Node inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
-    bool hasActiveConditionalNode = false;
-    if( options::sygusUnifCondSol() ){
-      //TODO
-      hasActiveConditionalNode = true;
-    }
-    //check whether we will run CEGIS on inner skolem variables
-    bool sk_refine = ( !isGround() || d_refine_count==0 || hasActiveConditionalNode );
-    if( sk_refine ){
-      Assert( d_ce_sk.empty() );
-      d_ce_sk.push_back( std::vector< Node >() );
+    Assert( c_model_values.size()==d_candidates.size() );
+    inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
+  }else{
+    inst = d_base_inst;
+  }
+  
+  //check whether we will run CEGIS on inner skolem variables
+  bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand );
+  if( sk_refine ){
+    Assert( d_ce_sk.empty() );
+    d_ce_sk.push_back( std::vector< Node >() );
+  }else{
+    if( !constructed_cand ){
+      return;
     }
-    std::vector< Node > ic;
-    ic.push_back( d_assert_quant.negate() );
-    std::vector< Node > d;
-    CegInstantiation::collectDisjuncts( inst, d );
-    Assert( d.size()==d_base_disj.size() );
-    //immediately skolemize inner existentials
-    for( unsigned i=0; i<d.size(); i++ ){
-      Node dr = Rewriter::rewrite( d[i] );
-      if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+  }
+  
+  std::vector< Node > ic;
+  ic.push_back( d_assert_quant.negate() );
+  std::vector< Node > d;
+  CegInstantiation::collectDisjuncts( inst, d );
+  Assert( d.size()==d_base_disj.size() );
+  //immediately skolemize inner existentials
+  for( unsigned i=0; i<d.size(); i++ ){
+    Node dr = Rewriter::rewrite( d[i] );
+    if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+      if( constructed_cand ){
         ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
-        if( sk_refine ){
-          d_ce_sk.back().push_back( dr[0] );
-        }
-      }else{
+      }
+      if( sk_refine ){
+        Assert( !isGround() );
+        d_ce_sk.back().push_back( dr[0] );
+      }
+    }else{
+      if( constructed_cand ){
         ic.push_back( dr );
-        if( sk_refine ){
-          d_ce_sk.back().push_back( Node::null() );
-        }
         if( !d_inner_vars_disj[i].empty() ){
           Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
         }
       }
+      if( sk_refine ){
+        d_ce_sk.back().push_back( Node::null() );
+      }
     }
+  }
+  if( constructed_cand ){
     Node lem = NodeManager::currentNM()->mkNode( OR, ic );
     lem = Rewriter::rewrite( lem );
+    //eagerly unfold applications of evaluation function
+    if( options::sygusDirectEval() ){
+      Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
+      std::map< Node, Node > visited_n;
+      lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n );
+    }
     lems.push_back( lem );
     recordInstantiation( c_model_values );
-  }else{
-    Assert( false );
-  }
-}
-
-Node CegConjecture::getActiveConditional( Node curr ) {
-  Assert( options::sygusUnifCondSol() );
-  std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
-  Assert( it!=d_cinfo.end() );
-  if( !it->second.d_csol_cond.isNull() ){
-    if( it->second.d_csol_status==-1 ){
-      //yet to branch, this is the one
-      return curr;
-    }else{
-      int pstatus = getProgressStatus( curr );
-      if( pstatus==-1 ){
-        // it is progress-inactive
-        return curr;
-      }else{
-        Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 );
-        return getActiveConditional( it->second.d_csol_var[1-it->second.d_csol_status] );
-      }
-    }
-  }else{
-    //not a conditional
-    return curr;
-  }
-}
-
-void CegConjecture::getContextConditionalNodes( Node curr, Node x, std::vector< Node >& nodes ) {
-  if( curr!=x ){
-    std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( curr );
-    if( !it->second.d_csol_cond.isNull() ){
-      if( it->second.d_csol_status!=-1 ){
-        nodes.push_back( curr );
-        getContextConditionalNodes( it->second.d_csol_var[1-it->second.d_csol_status], x, nodes );
-      }
-    }
-  }
-}
-
-Node CegConjecture::mkConditionalEvalNode( Node c, std::vector< Node >& args ) {
-  Assert( !c.isNull() );
-  std::vector< Node > condc;
-  //get evaluator
-  Assert( c.getType().isDatatype() );
-  const Datatype& cd = ((DatatypeType)c.getType().toType()).getDatatype();
-  Assert( cd.isSygus() );
-  condc.push_back( Node::fromExpr( cd.getSygusEvaluationFunc() ) );
-  condc.push_back( c );
-  for( unsigned a=0; a<args.size(); a++ ){
-    condc.push_back( args[a] );
-  }
-  return NodeManager::currentNM()->mkNode( kind::APPLY_UF, condc );
-}
-
-Node CegConjecture::mkConditionalNode( Node v, std::vector< Node >& args, unsigned eindex ) {
-  std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
-  if( it!=d_cinfo.end() ){
-    Assert( eindex<=2 );
-    Node en = eindex==0 ? it->second.d_csol_cond : it->second.d_csol_var[eindex-1];
-    if( !en.isNull() ){
-      Node ret = mkConditionalEvalNode( en, args );
-      //consider template
-      std::map< unsigned, Node >::iterator itt = it->second.d_template.find( eindex );
-      if( itt!=it->second.d_template.end() ){
-        Assert( it->second.d_template_arg.find( eindex )!=it->second.d_template_arg.end() );
-        TNode var = it->second.d_template_arg[eindex];
-        TNode subs = ret;
-        Node rret = itt->second.substitute( var, subs );
-        ret = rret;
-      }
-      return ret;
-    }
-  }
-  Assert( false );
-  return Node::null();
-}
-
-Node CegConjecture::mkConditional( Node v, std::vector< Node >& args, bool pol ) {
-  Node ret = mkConditionalNode( v, args, 0 );
-  if( !pol ){
-    ret = ret.negate();
-  }
-  return ret;
-}
-  
-Node CegConjecture::purifyConditionalEvaluations( Node n, std::map< Node, Node >& csol_active, std::map< Node, Node >& psubs, std::map< Node, Node >& visited ){
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  if( itv!=visited.end() ){
-    return itv->second;
-  }else{
-    Node ret;
-    if( n.getKind()==APPLY_UF ){
-      std::map< Node, Node >::iterator itc = csol_active.find( n[0] );
-      if( itc!=csol_active.end() ){
-        //purify it with a variable
-        ret = NodeManager::currentNM()->mkSkolem( "y", n.getType(), "purification variable for sygus conditional solution" );
-        psubs[n] = ret;
-      }
-    }
-    if( ret.isNull() ){
-      ret = n;
-      if( n.getNumChildren()>0 ){
-        std::vector< Node > children;
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.push_back( n.getOperator() );
-        }
-        bool childChanged = false;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node nc = purifyConditionalEvaluations( n[i], csol_active, psubs, visited );
-          childChanged = childChanged || nc!=n[i];
-          children.push_back( nc );
-        }
-        if( childChanged ){
-          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-        }
-      }
-    }
-    visited[n] = ret;
-    return ret;
   }
 }
         
@@ -717,119 +468,9 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
     }
   }
   
-  
   std::map< Node, Node > csol_active;
   std::map< Node, std::vector< Node > > csol_ccond_nodes;
   std::map< Node, std::map< Node, bool > > csol_cpol;    
-  if( options::sygusUnifCondSol() ){
-    //previous non-ground conditional refinement lemmas must satisfy the current point
-    if( !isGround() ){
-      Trace("cegqi-refine") << "doCegConjectureRefine : check for new refinements of previous lemmas..." << std::endl;
-      for( unsigned i=0; i<d_refinement_lemmas_ngr.size(); i++ ){
-        Node prev_lem = d_refinement_lemmas_ngr[i];
-        prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-        if( d_refinement_lemmas_reproc.find( prev_lem )==d_refinement_lemmas_reproc.end() ){
-          d_refinement_lemmas_reproc[prev_lem] = true;
-          //do auxiliary variable substitution
-          std::vector< Node > subs;
-          for( unsigned ii=0; ii<d_refinement_lemmas_aux_vars[i].size(); ii++ ){
-            subs.push_back( NodeManager::currentNM()->mkSkolem( "y", d_refinement_lemmas_aux_vars[i][ii].getType(), 
-                                                                "purification variable for non-ground sygus conditional solution" ) );
-          }
-          prev_lem = prev_lem.substitute( d_refinement_lemmas_aux_vars[i].begin(), d_refinement_lemmas_aux_vars[i].end(), subs.begin(), subs.end() );
-          prev_lem = Rewriter::rewrite( prev_lem );
-          Trace("sygus-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
-          lems.push_back( prev_lem );
-        }
-      }
-      if( !lems.empty() ){  
-        Trace("cegqi-refine") << "...added lemmas, abort further refinement." << std::endl;
-        d_ce_sk.clear();
-        return;
-      }
-    }
-    Trace("cegqi-refine") << "doCegConjectureRefine : conditional solution refinement, expand active conditional nodes" << std::endl;
-    std::vector< Node > new_active_measure_sum;
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      Node v = d_candidates[i];
-      Node ac = getActiveConditional( v );
-      Assert( !ac.isNull() );
-      //compute the contextual conditions
-      getContextConditionalNodes( v, ac, csol_ccond_nodes[v] );
-      if( !csol_ccond_nodes[v].empty() ){
-        //it will be conditionally evaluated, this is a placeholder
-        csol_active[v] = Node::null();
-      }
-      Trace("sygus-unif") << "Active conditional for " << v << " is : " << ac << std::endl;
-      //if it is a conditional
-      bool is_active_conditional = false;
-      if( !d_cinfo[ac].d_csol_cond.isNull() ){
-        int pstatus = getProgressStatus( ac );
-        Assert( pstatus!=0 );
-        if( pstatus==-1 ){
-          //inject new progress point TODO?
-          Trace("sygus-unif") << "...progress status is " << pstatus << ", do not expand." << std::endl;
-          Assert( false );
-        }else{
-          is_active_conditional = true;
-          //expand this conditional
-          Trace("sygus-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
-          d_cinfo[ac].d_csol_status = 0;  //TODO: prefer some branches more than others based on the grammar?
-          Trace("sygus-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
-          Trace("sygus-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
-          Trace("sygus-unif") << d_cinfo[ac].d_csol_var[1] << " )" << std::endl;
-          registerCandidateConditional( d_cinfo[ac].d_csol_var[1-d_cinfo[ac].d_csol_status] );
-          //add to measure sum
-          Node acfc = getMeasureTermFactor( d_cinfo[ac].d_csol_cond );
-          if( !acfc.isNull() ){
-            new_active_measure_sum.push_back( acfc );
-          }
-          Node acfv = getMeasureTermFactor( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] );
-          if( !acfv.isNull() ){
-            new_active_measure_sum.push_back( acfv );
-          }
-          csol_active[v] = ac;
-        }
-      }
-      if( !is_active_conditional ){
-        Trace("sygus-unif") << "* For " << v << ", its active node " << ac << " is not a conditional node." << std::endl;
-        //if we have not already included this in the measure, do so
-        if( d_cinfo[ac].d_csol_status==-1 ){
-          Node acf = getMeasureTermFactor( ac );
-          if( !acf.isNull() ){
-            new_active_measure_sum.push_back( acf );
-          }
-          d_cinfo[ac].d_csol_status = 2;
-        }
-      }
-      if( !csol_ccond_nodes[v].empty() ){
-        Trace("sygus-unif") << "...it is nested under " << csol_ccond_nodes[v].size() << " other conditionals" << std::endl;
-      }
-    }
-    // must add to active measure
-    if( !new_active_measure_sum.empty() ){
-      Node mcsum = new_active_measure_sum.size()==1 ? new_active_measure_sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, new_active_measure_sum );
-      Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, mcsum, d_active_measure_term );
-      Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
-      d_qe->getOutputChannel().lemma( mclem );
-      /*    
-      for( unsigned i=0; i<new_active_measure_sum.size(); i++ ){
-        Node mclem = NodeManager::currentNM()->mkNode( kind::LEQ, new_active_measure_sum[i], d_active_measure_term );
-        Trace("cegqi-lemma") << "Cegqi::Lemma : Measure component lemma : " << mclem << std::endl;
-        d_qe->getOutputChannel().lemma( mclem );
-      }
-      
-      Node new_active_measure = NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() );
-      new_active_measure_sum.push_back( new_active_measure );
-      Node namlem = NodeManager::currentNM()->mkNode( kind::GEQ, new_active_measure, NodeManager::currentNM()->mkConst(Rational(0)));
-      Node ramlem = d_active_measure_term.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, new_active_measure_sum ) );
-      namlem = NodeManager::currentNM()->mkNode( kind::AND, ramlem, namlem );
-      Trace("cegqi-lemma") << "Cegqi::Lemma : Measure expansion : " << namlem << std::endl;
-      d_qe->getOutputChannel().lemma( namlem );
-      d_active_measure_term = new_active_measure;
-      */
-    }
-  }
   
   //for conditional evaluation
   std::map< Node, Node > psubs_visited;
@@ -855,14 +496,7 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
     }
     if( !c_disj.isNull() ){
       //compute the body, inst_cond
-      if( options::sygusUnifCondSol() ){
-        Trace("sygus-unif") << "Process " << c_disj << std::endl;
-        c_disj = purifyConditionalEvaluations( c_disj, csol_active, psubs, psubs_visited );
-        Trace("sygus-unif") << "Purified to : " << c_disj << std::endl;
-        Trace("sygus-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
-      }else{
-        //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
-      }
+      //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
       lem_c.push_back( c_disj );
     }
   }
@@ -872,118 +506,10 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
   std::vector< Node > psubs_cond_conc;
   std::map< Node, std::vector< Node > > psubs_apply;
   std::vector< Node > paux_vars;
-  if( options::sygusUnifCondSol() ){
-    Trace("cegqi-refine") << "doCegConjectureRefine : add conditional assumptions for " << psubs.size() << " evaluations..." << std::endl;
-    for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){
-      Assert( csol_active.find( itp->first[0] )!=csol_active.end() );
-      paux_vars.push_back( itp->second );
-      std::vector< Node > args;
-      for( unsigned a=1; a<itp->first.getNumChildren(); a++ ){
-        args.push_back( itp->first[a] );
-      }
-      Node ac = csol_active[itp->first[0]];
-      Assert( d_cinfo.find( ac )!=d_cinfo.end() );
-      Node c = d_cinfo[ac].d_csol_cond;
-      psubs_apply[ c ].push_back( itp->first );
-      Trace("sygus-unif") << "   process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
-      Trace("sygus-unif") << ", and " << csol_ccond_nodes[itp->first[0]].size() << " context conditionals." << std::endl;
-      std::vector< Node> assm;
-      if( !c.isNull() ){
-        assm.push_back( mkConditional( ac, args, true ) );
-      }
-      for( unsigned j=0; j<csol_ccond_nodes[itp->first[0]].size(); j++ ){
-        Node acc = csol_ccond_nodes[itp->first[0]][j];
-        bool pol = ( d_cinfo[acc].d_csol_status==1 );
-        assm.push_back( mkConditional( acc, args, pol ) );
-      }
-      Assert( !assm.empty() );
-      Node c_ant = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm );
-      psubs_cond_ant.push_back( c_ant );
-      // make the evaluation node
-      Node eret = mkConditionalNode( ac, args, d_cinfo[ac].d_csol_status+1 );
-      Node c_conc = eret.eqNode( itp->second );
-      psubs_cond_conc.push_back( c_conc );
-      Trace("sygus-unif") << "   ...made conditional correctness assumption : " << c_ant << " => " << c_conc << std::endl;
-    }
-  }else{
-    Assert( psubs.empty() );
-  }
+  Assert( psubs.empty() );
   
   Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
   
-  if( options::sygusUnifCondSol() ){
-    Trace("sygus-unif-debug") << "We have base lemma : " << base_lem << std::endl;
-    //progress lemmas
-    Trace("cegqi-refine") << "doCegConjectureRefine : add progress lemmas..." << std::endl;
-    std::map< Node, bool > cprocessed;
-    for( std::map< Node, Node >::iterator itc = csol_active.begin(); itc !=csol_active.end(); ++itc ){
-      Node x = itc->first;
-      Node ac = itc->second;
-      Assert( d_cinfo.find( ac )!=d_cinfo.end() );
-      Node c = d_cinfo[ac].d_csol_cond;    
-      if( !c.isNull() ){
-        Trace("sygus-unif") << "  process conditional " << c << " for " << x << ", which was applied " << psubs_apply[c].size() << " times." << std::endl;
-        //make the progress point
-        Assert( x.getType().isDatatype() );
-        const Datatype& dx = ((DatatypeType)x.getType().toType()).getDatatype();
-        Node sbvl = Node::fromExpr( dx.getSygusVarList() );
-        std::vector< Node > prgr_pt;
-        for( unsigned a=0; a<sbvl.getNumChildren(); a++ ){
-          prgr_pt.push_back( NodeManager::currentNM()->mkSkolem( "kp", sbvl[a].getType(), "progress point for sygus conditional" ) );
-        }
-        Node pdlem;    
-        if( !psubs_apply[c].empty() ){
-          std::vector< Node > prgr_domain_d;
-          for( unsigned j=0; j<psubs_apply[c].size(); j++ ){
-            std::vector< Node > prgr_domain;
-            for( unsigned a=1; a<psubs_apply[c][j].getNumChildren(); a++ ){
-              Assert( a<=prgr_pt.size() );
-              prgr_domain.push_back( prgr_pt[a-1].eqNode( psubs_apply[c][j][a] ) );
-            }
-            if( !prgr_domain.empty() ){
-              //the point is in the domain of this function application
-              Node pdc = prgr_domain.size()==1 ? prgr_domain[0] : NodeManager::currentNM()->mkNode( AND, prgr_domain );
-              prgr_domain_d.push_back( pdc );
-            }
-          }
-          if( !prgr_domain_d.empty() ){
-            //the progress point is in the domain of some function application
-            pdlem = prgr_domain_d.size()==1 ? prgr_domain_d[0] : NodeManager::currentNM()->mkNode( OR, prgr_domain_d );
-            pdlem = pdlem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-            Trace("sygus-unif") << "Progress domain point lemma is " << pdlem << std::endl;
-            lems.push_back( pdlem );
-          }
-        }
-        //the condition holds for the point, if this is an active condition
-        Node cplem = mkConditional( ac, prgr_pt );
-        if( !csol_ccond_nodes[x].empty() ){
-          std::vector< Node > prgr_conj;
-          prgr_conj.push_back( cplem );
-          // ...and not for its context
-          for( unsigned j=0; j<csol_ccond_nodes[x].size(); j++ ){
-            Node acc = csol_ccond_nodes[x][j];
-            bool pol = ( d_cinfo[acc].d_csol_status==1 );
-            prgr_conj.push_back( mkConditional( acc, prgr_pt, pol ) );
-          }
-          cplem = NodeManager::currentNM()->mkNode( kind::AND, prgr_conj );
-        }
-        Assert( !d_cinfo[x].d_csol_progress_guard.isNull() );
-        cplem = NodeManager::currentNM()->mkNode( kind::OR, d_cinfo[x].d_csol_progress_guard.negate(), cplem );
-        Trace("sygus-unif") << "Progress lemma is " << cplem << std::endl;
-        lems.push_back( cplem );
-      }
-    }
-    /*
-    if( !prgr_conj.empty() ){
-      Node prgr_lem = prgr_conj.size()==1 ? prgr_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, prgr_conj );
-      prgr_lem = prgr_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-      prgr_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prgr_lem );
-      Trace("sygus-unif") << "Progress lemma is " << prgr_lem << std::endl;
-      lems.push_back( prgr_lem );
-    }
-    */
-  }
-  
   Trace("cegqi-refine") << "doCegConjectureRefine : construct and finalize lemmas..." << std::endl;
   
   Node lem = base_lem;
@@ -992,37 +518,8 @@ void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
   base_lem = Rewriter::rewrite( base_lem );
   d_refinement_lemmas_base.push_back( base_lem );
   
-  if( options::sygusUnifCondSol() ){
-    //add the conditional evaluation
-    if( !psubs_cond_ant.empty() ){
-      std::vector< Node > children;
-      children.push_back( base_lem );
-      std::vector< Node > pav;
-      std::vector< Node > pcv;
-      for( unsigned i=0; i<psubs_cond_ant.size(); i++ ){
-        children.push_back( NodeManager::currentNM()->mkNode( kind::OR, psubs_cond_ant[i].negate(), psubs_cond_conc[i] ) );
-        Node pa = psubs_cond_ant[i].substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-        pav.push_back( pa );
-        Node pc = psubs_cond_conc[i].substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-        pcv.push_back( pc );
-      }
-      d_refinement_lemmas_ceval_ant.push_back( pav );
-      d_refinement_lemmas_ceval_conc.push_back( pcv );
-      lem = NodeManager::currentNM()->mkNode( AND, children );
-    }
-  }
-
   lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
   
-  if( options::sygusUnifCondSol() ){
-    if( !isGround() ){
-      //store the non-ground version of the lemma
-      lem = Rewriter::rewrite( lem );
-      d_refinement_lemmas_ngr.push_back( lem );
-      d_refinement_lemmas_aux_vars.push_back( paux_vars );
-    }
-  }
-  
   lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
   lem = Rewriter::rewrite( lem );
   d_refinement_lemmas.push_back( lem );
@@ -1071,62 +568,6 @@ void CegConjecture::debugPrint( const char * c ) {
   }
 }
 
-int CegConjecture::getProgressStatus( Node v ) {
-  Assert( options::sygusUnifCondSol() );
-  std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
-  if( it!=d_cinfo.end() ){
-    if( !it->second.d_csol_cond.isNull() ){
-      if( it->second.d_csol_status!=-1 ){
-        Node plit = it->second.d_csol_progress_guard;
-        Assert( !plit.isNull() );
-        //check SAT value of plit
-        bool value;
-        if( d_qe->getValuation().hasSatValue( plit, value ) ) {
-          if( !value ){
-            return -1;
-          }else{
-            return 1;
-          }
-        }else{
-          return 0;
-        }
-      }
-    }
-  }
-  return -2;
-}
-
-Node CegConjecture::getNextDecisionRequestConditional( Node v, unsigned& priority ) {
-  Assert( options::sygusUnifCondSol() );
-  int pstatus = getProgressStatus( v );
-  if( pstatus>=0 ){
-    std::map< Node, CandidateInfo >::iterator it = d_cinfo.find( v );
-    Assert( it!=d_cinfo.end() );
-    if( pstatus==1 ){
-      //active, recurse
-      Assert( it->second.d_csol_status==0 || it->second.d_csol_status==1 );
-      return getNextDecisionRequestConditional( it->second.d_csol_var[1-it->second.d_csol_status], priority );
-    }else if( pstatus==0 ){
-      //needs decision
-      priority = 1;
-      return it->second.d_csol_progress_guard;
-    }
-  }
-  return Node::null();
-}
-
-Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
-  if( options::sygusUnifCondSol() ){
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      Node lit = getNextDecisionRequestConditional( d_candidates[i], priority );
-      if( !lit.isNull() ){
-        return lit;
-      }
-    }
-  }
-  return Node::null();
-}
-
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe, qe->getSatContext() );
   d_last_inst_si = false;
@@ -1174,6 +615,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
 }
 
 void CegInstantiation::preRegisterQuantifier( Node q ) {
+/*
   if( options::sygusDirectEval() ){
     if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){  
       //check whether it is an evaluation axiom
@@ -1207,46 +649,15 @@ void CegInstantiation::preRegisterQuantifier( Node q ) {
         }
       }
     }
-  }  
+  } 
+  */ 
 }
 
 void CegInstantiation::registerQuantifier( Node q ) {
-  if( d_quantEngine->getOwner( q )==this && d_eval_axioms.find( q )==d_eval_axioms.end() ){
+  if( d_quantEngine->getOwner( q )==this ){ // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
     if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
       d_conj->assign( q );
-
-      //fairness
-      if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-        std::vector< Node > mc;
-        if( options::sygusUnifCondSol() || 
-            d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED  ){
-          //measure term is a fresh constant
-          mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) );
-        }else{
-          std::vector< Node > clist;
-          d_conj->getCandidateList( clist, true );
-          for( unsigned j=0; j<clist.size(); j++ ){
-            TypeNode tn = clist[j].getType();
-            if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){
-              if( tn.isDatatype() ){
-                mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, clist[j] ) );
-              }
-            }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
-              registerMeasuredType( tn );
-              std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
-              if( it!=d_uf_measure.end() ){
-                mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, clist[j] ) );
-              }
-            }
-          }
-        }
-        if( !mc.empty() ){
-          Node mt = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
-          Trace("cegqi") << "Measure term is : " << mt << std::endl;
-          d_conj->setMeasureTerm( mt );
-        }
-      }
     }else{
       Assert( d_conj->d_quant==q );
     }
@@ -1259,10 +670,7 @@ void CegInstantiation::assertNode( Node n ) {
 }
 
 Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
-  //enforce fairness
   if( d_conj->isAssigned() ){
-    d_conj->initializeGuard();
-    // 
     std::vector< Node > req_dec;
     const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
     if( ! ceg_si->d_full_guard.isNull() ){
@@ -1283,32 +691,7 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
         Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl;
       }
     }
-    
-    //ask the conjecture directly
-    Node lit = d_conj->getNextDecisionRequest( priority );
-    if( !lit.isNull() ){
-      return lit;
-    }
-
-    if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-      Node lit = d_conj->getFairnessLiteral( d_conj->getCurrentTermSize() );
-      bool value;
-      if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
-        if( !value ){
-          d_conj->incrementCurrentTermSize();
-          lit = d_conj->getFairnessLiteral( d_conj->getCurrentTermSize() );
-          Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
-          priority = 1;
-          return lit;
-        }
-      }else{
-        Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
-        priority = 1;
-        return lit;
-      }
-    }
   }
-
   return Node::null();
 }
 
@@ -1319,11 +702,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     conj->debugPrint("cegqi-engine-debug");
     Trace("cegqi-engine-debug") << std::endl;
   }
-  if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-    Trace("cegqi-engine") << "  * Current term size : " << conj->getCurrentTermSize() << std::endl;
-  }  
 
   if( !conj->needsRefinement() ){
+    Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
     if( conj->d_syntax_guided ){
       std::vector< Node > clems;
       conj->doCegConjectureSingleInvCheck( clems );
@@ -1345,25 +726,24 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       if( options::sygusDirectEval() ){
         bool addedEvalLemmas = false;
         if( options::sygusCRefEval() ){
-          Trace("cegqi-debug") << "Do cref evaluation..." << std::endl;
+          Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..." << std::endl;
           // see if any refinement lemma is refuted by evaluation
           std::vector< Node > cre_lems;
           getCRefEvaluationLemmas( conj, clist, model_values, cre_lems );
           if( !cre_lems.empty() ){
-            Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..." << std::endl;
             for( unsigned j=0; j<cre_lems.size(); j++ ){
               Node lem = cre_lems[j];
-              Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
               if( d_quantEngine->addLemma( lem ) ){
+                Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem << std::endl;
                 addedEvalLemmas = true;
               }
             }
             if( addedEvalLemmas ){
-              return;
+              //return;
             }
           }
         }
-        Trace("cegqi-debug") << "Do direct evaluation..." << std::endl;
+        Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
         std::vector< Node > eager_terms; 
         std::vector< Node > eager_vals; 
         std::vector< Node > eager_exps;
@@ -1373,15 +753,14 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         }
         Trace("cegqi-debug") << "...produced " << eager_terms.size()  << " eager evaluation lemmas." << std::endl;
         if( !eager_terms.empty() ){
-          Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
           for( unsigned j=0; j<eager_terms.size(); j++ ){
             Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[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;
             if( d_quantEngine->addLemma( lem ) ){
+              Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl;
               addedEvalLemmas = true;
             }
           }
@@ -1390,25 +769,6 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           return;
         }
       }
-      //check if we must apply fairness lemmas
-      if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){
-        Trace("cegqi-debug") << "Get measure lemmas..." << std::endl;
-        std::vector< Node > lems;
-        for( unsigned j=0; j<clist.size(); j++ ){
-          Trace("cegqi-debug") << "  get measure lemmas for " << clist[j] << " -> " << model_values[j] << std::endl;
-          getMeasureLemmas( clist[j], model_values[j], lems );
-        }
-        Trace("cegqi-debug") << "...produced " << lems.size() << " measure lemmas." << std::endl;
-        if( !lems.empty() ){
-          Trace("cegqi-engine") << "  *** Do measure refinement..." << std::endl;
-          for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Cegqi::Lemma : measure : " << lems[j] << std::endl;
-            d_quantEngine->addLemma( lems[j] );
-          }
-          Trace("cegqi-engine") << "  ...refine size." << std::endl;
-          return;
-        }
-      }
       
       Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
       std::vector< Node > cclems;
@@ -1417,12 +777,6 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       for( unsigned i=0; i<cclems.size(); i++ ){
         Node lem = cclems[i];
         d_last_inst_si = false;
-        //eagerly unfold applications of evaluation function
-        if( options::sygusDirectEval() ){
-          Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl;
-          std::map< Node, Node > visited_n;
-          lem = getEagerUnfold( lem, visited_n );
-        }
         Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl;
         if( d_quantEngine->addLemma( lem ) ){
           ++(d_statistics.d_cegqi_lemmas_ce);
@@ -1482,308 +836,68 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 }
 
 void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems ) {
+  Trace("sygus-cref-eval") << "Cref eval : conjecture has " << conj->getNumRefinementLemmas() << " refinement lemmas." << std::endl;
   if( conj->getNumRefinementLemmas()>0 ){
     Assert( vs.size()==ms.size() );
-    std::map< Node, Node > vtm;
-    for( unsigned i=0; i<vs.size(); i++ ){
-      vtm[vs[i]] = ms[i];
-    }
-    /*
-    if( options::sygusUnifCondSol() ){
-      // first, check progress lemmas  TODO?
-      for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){
-        Node plem = conj->getConditionalProgressLemma( i );
-        std::vector< Node > pp;
-        conj->
-        std::map< Node, Node > visitedp;
-        std::map< Node, std::vector< Node > > expp;
-        conj->getModelValues
-      }
-    }
-    */
+
+    Node neg_guard = conj->getGuard().negate();
     for( unsigned i=0; i<conj->getNumRefinementLemmas(); i++ ){
       Node lem;
       std::map< Node, Node > visited;
       std::map< Node, std::vector< Node > > exp;
-      if( options::sygusUnifCondSol() ){
-        for( unsigned j=0; j<conj->getNumConditionalEvaluations( i ); j++ ){
-          std::map< Node, Node > visitedc;
-          std::map< Node, std::vector< Node > > expc;
-          Node ce = conj->getConditionalEvaluationAntec( i, j );
-          Node cee = crefEvaluate( ce, vtm, visitedc, expc );
-          Trace("sygus-cref-eval") << "Check conditional evaluation condition : " << ce << ", evaluates to " << cee << std::endl;
-          if( !cee.isNull() && cee==d_quantEngine->getTermDatabase()->d_true  ){
-            Node conc = conj->getConditionalEvaluationConc( i, j );
-            // the conditional holds, we will apply this as a substitution
-            for( unsigned r=0; r<2; r++ ){
-              if( conc[r].isVar() ){
-                Node v = conc[r];
-                Node c = conc[1-r];
-                Assert( exp.find( v )==exp.end() );
-                visited[v] = c;
-                //exp[v].insert( exp[v].end(), expc[ce].begin(), expc[ce].end() );
-                exp[v].push_back( ce );
-                Trace("sygus-cref-eval") << "   consider " << v << " -> " << c << " with expanation " << ce << std::endl;
-                break;
-              }
-            }
-          }
-        }
-        //if at least one conditional fires
-        if( !visited.empty() ){
-          lem = conj->getRefinementBaseLemma( i );
-        }
-      }else{
-        lem = conj->getRefinementBaseLemma( i );
-      }
+      lem = conj->getRefinementBaseLemma( i );
       if( !lem.isNull() ){
-        Trace("sygus-cref-eval") << "Check refinement lemma " << lem << " against current model." << std::endl;
-        Node elem = crefEvaluate( lem, vtm, visited, exp );
-        Trace("sygus-cref-eval") << "...evaluated to " << elem << ", exp size = " << exp[lem].size() << std::endl;
-        if( !elem.isNull() && elem==d_quantEngine->getTermDatabase()->d_false ){
-          elem = conj->getGuard().negate();
-          Node cre_lem;
-          if( !exp[lem].empty() ){
-            Node en = exp[lem].size()==1 ? exp[lem][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[lem] );
-            cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), elem );
-          }else{
-            cre_lem = elem;
-          }
-          if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
-            Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
-            lems.push_back( cre_lem );
+        std::vector< Node > lem_conj;
+        //break into conjunctions
+        if( lem.getKind()==kind::AND ){
+          for( unsigned i=0; i<lem.getNumChildren(); i++ ){
+            lem_conj.push_back( lem[i] );
           }
+        }else{
+          lem_conj.push_back( lem );
         }
-      }
-    }
-  }
-}
-
-Node CegInstantiation::crefEvaluate( Node n, std::map< Node, Node >& vtm, std::map< Node, Node >& visited, std::map< Node, std::vector< Node > >& exp ){
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  Node ret;
-  std::vector< Node > exp_c;
-  if( itv!=visited.end() ){
-    if( !itv->second.isConst() ){
-      //we stored a partially evaluated node, actually evaluate the result now
-      ret = crefEvaluate( itv->second, vtm, visited, exp );
-      exp_c.push_back( itv->second );
-    }else{
-      return itv->second;
-    }
-  }else{
-    if( n.getKind()==kind::APPLY_UF ){
-      //it is an evaluation function
-      Trace("sygus-cref-eval-debug") << "Compute evaluation for : " << n << std::endl;
-      //unfold by one step 
-      Node nn = d_quantEngine->getTermDatabaseSygus()->unfold( n, vtm, exp[n] );
-      Trace("sygus-cref-eval-debug") << "...unfolded once to " << nn << std::endl;
-      Assert( nn!=n );
-      //it is the result of evaluating the unfolding
-      ret = crefEvaluate( nn, vtm, visited, exp );
-      //carry explanation
-      exp_c.push_back( nn );
-    }
-    if( ret.isNull() ){
-      if( n.getNumChildren()>0 ){
-        std::vector< Node > children;
-        bool childChanged = false;
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.push_back( n.getOperator() );
-        }
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node nc = crefEvaluate( n[i], vtm, visited, exp );
-          childChanged = nc!=n[i] || childChanged;
-          children.push_back( nc );
-          //Boolean short circuiting
-          if( n.getKind()==kind::AND ){
-            if( nc==d_quantEngine->getTermDatabase()->d_false ){
-              ret = nc;
-              exp_c.clear();
-            }
-          }else if( n.getKind()==kind::OR ){
-            if( nc==d_quantEngine->getTermDatabase()->d_true ){
-              ret = nc;
-              exp_c.clear();
-            }
-          }else if( n.getKind()==kind::ITE && i==0 ){
-            int index = -1;
-            if( nc==d_quantEngine->getTermDatabase()->d_true ){
-              index = 1;
-            }else if( nc==d_quantEngine->getTermDatabase()->d_false ){
-              index = 2;
+        EvalSygusInvarianceTest vsit;
+        vsit.d_result = d_quantEngine->getTermDatabase()->d_false;
+        for( unsigned j=0; j<lem_conj.size(); j++ ){
+          Node lemc = lem_conj[j];
+          Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
+          Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lemc << " against current model." << std::endl;
+          Node cre_lem;
+          Node lemcs = lemc.substitute( vs.begin(), vs.end(), ms.begin(), ms.end() );
+          Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl;
+          Node lemcsu = d_quantEngine->getTermDatabaseSygus()->evaluateWithUnfolding( lemcs, vsit.d_visited );
+          Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl;
+          if( lemcsu==d_quantEngine->getTermDatabase()->d_false ){
+            std::vector< Node > msu;
+            std::vector< Node > mexp;
+            msu.insert( msu.end(), ms.begin(), ms.end() );
+            for( unsigned k=0; k<vs.size(); k++ ){
+              vsit.d_var = vs[k];
+              vsit.d_update_nvn = msu[k];
+              msu[k] = vs[k];
+              // substitute for everything except this
+              vsit.d_conj = lemc.substitute( vs.begin(), vs.end(), msu.begin(), msu.end() );
+              // get minimal explanation for this
+              Trace("sygus-cref-eval2-debug") << "  compute min explain of : " << vs[k] << " = " << vsit.d_update_nvn << std::endl;
+              d_quantEngine->getTermDatabaseSygus()->getExplanationFor( vs[k], vsit.d_update_nvn, mexp, vsit );
+              msu[k] = vsit.d_update_nvn;
             }
-            if( index!=-1 ){
-              ret = crefEvaluate( n[index], vtm, visited, exp );
-              exp_c.push_back( n[index] );
+            if( !mexp.empty() ){
+              Node en = mexp.size()==1 ? mexp[0] : NodeManager::currentNM()->mkNode( kind::AND, mexp );
+              cre_lem = NodeManager::currentNM()->mkNode( kind::OR, en.negate(), neg_guard );
+            }else{
+              cre_lem = neg_guard;
             }
           }
-          //carry explanation
-          exp_c.push_back( n[i] );
-          if( !ret.isNull() ){
-            break;
-          }
-        }
-        if( ret.isNull() ){
-          if( childChanged ){
-            ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-            ret = Rewriter::rewrite( ret );
-          }else{
-            ret = n;
-          }
-        }
-      }else{
-        ret = n;
-      }
-    }
-  }
-  //carry explanation from children
-  for( unsigned i=0; i<exp_c.size(); i++ ){
-    Node nn = exp_c[i];
-    std::map< Node, std::vector< Node > >::iterator itx = exp.find( nn );
-    if( itx!=exp.end() ){
-      for( unsigned j=0; j<itx->second.size(); j++ ){
-        if( std::find( exp[n].begin(), exp[n].end(), itx->second[j] )==exp[n].end() ){
-          exp[n].push_back( itx->second[j] );
-        }
-      }
-    }
-  }
-  Trace("sygus-cref-eval-debug") << "... evaluation of " << n << " is (" << ret.getKind() << ") " << ret << std::endl;
-  Trace("sygus-cref-eval-debug") << "...... exp size = " << exp[n].size() << std::endl;
-  Assert( ret.isNull() || ret.isConst() );
-  visited[n] = ret;
-  return ret;
-}
-
-void CegInstantiation::registerMeasuredType( TypeNode tn ) {
-  std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
-  if( it==d_uf_measure.end() ){
-    if( tn.isDatatype() ){
-      TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->integerType() );
-      Node op = NodeManager::currentNM()->mkSkolem( "tsize", op_tn, "was created by ceg instantiation to enforce fairness." );
-      d_uf_measure[tn] = op;
-    }
-  }
-}
-
-Node CegInstantiation::getSizeTerm( Node n, TypeNode tn, std::vector< Node >& lems ) {
-  std::map< Node, Node >::iterator itt = d_size_term.find( n );
-  if( itt==d_size_term.end() ){
-    registerMeasuredType( tn );
-    Node sn = NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], n );
-    lems.push_back( NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), sn ) );
-    d_size_term[n] = sn;
-    return sn;
-  }else{
-    return itt->second;
-  }
-}
-
-void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& lems ) {
-  Trace("cegqi-lemma-debug") << "Get measure lemma " << n << " " << v << std::endl;
-  Assert( n.getType()==v.getType() );
-  TypeNode tn = n.getType();
-  if( tn.isDatatype() ){
-    Assert( v.getKind()==APPLY_CONSTRUCTOR );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    int index = Datatype::indexOf( v.getOperator().toExpr() );
-    std::map< int, Node >::iterator it = d_size_term_lemma[n].find( index );
-    if( it==d_size_term_lemma[n].end() ){
-      Node lhs = getSizeTerm( n, tn, lems );
-      //add measure lemma
-      std::vector< Node > sumc;
-      for( unsigned j=0; j<dt[index].getNumArgs(); j++ ){
-        TypeNode tnc = v[j].getType();
-        if( tnc.isDatatype() ){
-          Node seln = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][j].getSelector() ), n );
-          sumc.push_back( getSizeTerm( seln, tnc, lems ) );
-        }
-      }
-      Node rhs;
-      if( !sumc.empty() ){
-        sumc.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
-        rhs = NodeManager::currentNM()->mkNode( PLUS, sumc );
-      }else{
-        rhs = NodeManager::currentNM()->mkConst( Rational(0) );
-      }
-      Node lem = lhs.eqNode( rhs );
-      Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[index].getTester() ), n );
-      lem = NodeManager::currentNM()->mkNode( OR, cond.negate(), lem );
-
-      d_size_term_lemma[n][index] = lem;
-      Trace("cegqi-lemma-debug") << "...constructed lemma " << lem << std::endl;
-      lems.push_back( lem );
-      //return;
-    }
-    //get lemmas for children
-    for( unsigned i=0; i<v.getNumChildren(); i++ ){
-      Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
-      getMeasureLemmas( nn, v[i], lems );
-    }
-
-  }
-}
-
-Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  if( itv==visited.end() ){
-    Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
-    Node ret;
-    if( n.getKind()==APPLY_UF ){
-      TypeNode tn = n[0].getType();
-      Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
-      if( tn.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        if( dt.isSygus() ){ 
-          Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
-          Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn );
-          Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
-          std::vector< Node > vars;
-          std::vector< Node > subs;
-          Node var_list = Node::fromExpr( dt.getSygusVarList() );
-          Assert( var_list.getNumChildren()+1==n.getNumChildren() );
-          for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
-            vars.push_back( var_list[j] );
-          }
-          for( unsigned j=1; j<n.getNumChildren(); j++ ){
-            Node nc = getEagerUnfold( n[j], visited );
-            subs.push_back( nc );
-            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;
-          Assert( n.getType()==bTerm.getType() );
-          ret = bTerm; 
-        }
-      }
-    }
-    if( ret.isNull() ){
-      if( n.getKind()!=FORALL ){
-        bool childChanged = false;
-        std::vector< Node > children;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node nc = getEagerUnfold( n[i], visited );
-          childChanged = childChanged || n[i]!=nc;
-          children.push_back( nc );
-        }
-        if( childChanged ){
-          if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-            children.insert( children.begin(), n.getOperator() );
+          if( !cre_lem.isNull() ){
+            if( std::find( lems.begin(), lems.end(), cre_lem )==lems.end() ){
+              Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem << std::endl;
+              lems.push_back( cre_lem );
+            }
           }
-          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
         }
       }
-      if( ret.isNull() ){
-        ret = n;
-      }
     }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return itv->second;
   }
 }
 
@@ -1826,8 +940,10 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
             for( unsigned j=0; j<svl.getNumChildren(); j++ ){
               subs.push_back( Node::fromExpr( svl[j] ) );
             }
-            bool templIsPost = false;
-            Node templ;
+            //bool templIsPost = false;
+            const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
+            Node templ = ceg_si->getTemplate( prog );
+            /*
             if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
               const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
               if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){
@@ -1841,8 +957,11 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
                 templIsPost = true;
               }
             }
+            */
             Trace("cegqi-inv") << "Template is " << templ << std::endl;
             if( !templ.isNull() ){
+              TNode templa = ceg_si->getTemplateArg( prog );
+              Assert( !templa.isNull() );
               std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
               std::vector< Node > vars;
               vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() );
@@ -1860,7 +979,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
               Trace("cegqi-inv") << "Builtin version of solution is : "
                                  << sol << ", type : " << sol.getType()
                                  << std::endl;
-              sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ );
+              //sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ );
+              TNode tsol = sol;
+              sol = templ.substitute( templa, tsol );
             }
             if( sol==sygus_sol ){
               sol = sygus_sol;