Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.

8 files changed, 850 insertions, 252 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index ac93114b7..8a6d5d4a3 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -145,6 +145,23 @@ void Datatype::resolve(ExprManager* em,
     }
     d_record = new Record(fields);
   }
+  
+  //make the sygus evaluation function
+  if( isSygus() ){
+    PrettyCheckArgument(d_params.empty(), this, "sygus types cannot be parametric");
+    NodeManager* nm = NodeManager::fromExprManager(em);
+    std::string name = "eval_" + getName();
+    std::vector<TypeNode> evalType;
+    evalType.push_back(TypeNode::fromType(d_self));
+    if( !d_sygus_bvl.isNull() ){
+      for(size_t j = 0; j < d_sygus_bvl.getNumChildren(); ++j) {
+        evalType.push_back(TypeNode::fromType(d_sygus_bvl[j].getType()));
+      }
+    }
+    evalType.push_back(TypeNode::fromType(d_sygus_type));
+    TypeNode eval_func_type = nm->mkFunctionType(evalType);
+    d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr();    
+  }  
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -156,7 +173,7 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 
 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   PrettyCheckArgument(!d_resolved, this,
-                "cannot set sygus type to a finalized Datatype");
+                      "cannot set sygus type to a finalized Datatype");        
   d_sygus_type = st;
   d_sygus_bvl = bvl;
   d_sygus_allow_const = allow_const || allow_all;
@@ -394,9 +411,7 @@ bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw
 Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   ExprManagerScope ems(d_self);
-
   Debug("datatypes") << "mkGroundTerm of type " << t << std::endl;
-
   // is this already in the cache ?
   std::map< Type, Expr >::iterator it = d_ground_term.find( t );
   if( it != d_ground_term.end() ){
@@ -589,6 +604,10 @@ bool Datatype::getSygusAllowAll() const {
   return d_sygus_allow_const;
 }
 
+Expr Datatype::getSygusEvaluationFunc() const {
+  return d_sygus_eval;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 5a09730d0..88c72ea59 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -491,6 +491,7 @@ private:
   Expr d_sygus_bvl;
   bool d_sygus_allow_const;
   bool d_sygus_allow_all;
+  Expr d_sygus_eval;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -744,6 +745,8 @@ public:
   bool getSygusAllowConst() const;
   /** does it allow constants */
   bool getSygusAllowAll() const;
+  /** get the evaluation function for this datatype for the deep embedding */
+  Expr getSygusEvaluationFunc() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cf8fca2fa..585ef3dc2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -253,6 +253,8 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
+option cegqiUnifCondSol --cegqi-unif-csol bool :default false
+  enable approach which unifies conditional solutions
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 15495265e..33674770d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -730,19 +730,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd]
       for(size_t i = 0; i < datatypeTypes.size(); ++i) {
         DatatypeType dtt = datatypeTypes[i];
         const Datatype& dt = dtt.getDatatype();
-        name = "eval_" + dt.getName();
-        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-        std::vector<Type> evalType;
-        evalType.push_back(dtt);
-        if( !terms[0].isNull() ){
-          for(size_t j = 0; j < terms[0].getNumChildren(); ++j) {
-            evalType.push_back(terms[0][j].getType());
-          }
-        }
-        evalType.push_back(sorts[i]);
-        const FunctionType eval_func_type =
-            EXPR_MANAGER->mkFunctionType(evalType);
-        Expr eval = PARSER_STATE->mkVar(name, eval_func_type);
+        Expr eval = dt.getSygusEvaluationFunc();
         Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName()
                               << std::endl;
         evals.insert(std::make_pair(dtt, eval));
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 9903f14aa..999c554b5 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -32,9 +32,9 @@ namespace quantifiers {
 
 
 CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c )
-    : d_qe( qe ), d_curr_lit( c, 0 )
-{
+    : d_qe( qe ), d_curr_lit( c, 0 ) {
   d_refine_count = 0;
+  d_incomplete_candidate_values = false;
   d_ceg_si = new CegConjectureSingleInv( qe, this );
 }
 
@@ -71,6 +71,7 @@ void CegConjecture::assign( Node q ) {
     Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
     //store the inner variables for each disjunct
     for( unsigned j=0; j<d_base_disj.size(); j++ ){
+      Trace("cegqi") << "  " << j << " : " << d_base_disj[j] << std::endl;
       d_inner_vars_disj.push_back( std::vector< Node >() );
       //if the disjunct is an existential, store it
       if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){
@@ -80,6 +81,12 @@ void CegConjecture::assign( Node q ) {
         }
       }
     }
+    if( options::cegqiUnifCondSol() ){
+      // 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;
@@ -88,25 +95,64 @@ void CegConjecture::assign( Node q ) {
   }
 }
 
-void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
+void CegConjecture::registerCandidateConditional( Node v ) {
+  TypeNode tn = v.getType();
+  bool type_valid = false;
+  if( tn.isDatatype() ){
+    const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype();
+    if( dt.isSygus() ){
+      type_valid = true;
+      for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+        Node op = Node::fromExpr( dt[j].getSygusOp() );
+        if( op.getKind() == kind::BUILTIN ){
+          Kind sk = NodeManager::operatorToKind( op );
+          if( sk==kind::ITE ){
+            // we can do unification
+            d_cinfo[v].d_csol_op = Node::fromExpr( dt[j].getConstructor() );
+            Trace("cegqi") << "Can do synthesis unification for variable " << v << ", based on operator " << d_cinfo[v].d_csol_op << std::endl;
+            Assert( dt[j].getNumArgs()==3 );
+            for( unsigned k=0; k<3; k++ ){
+              Type t = dt[j][k].getRangeType();
+              if( k==0 ){
+                d_cinfo[v].d_csol_cond = NodeManager::currentNM()->mkSkolem( "c", TypeNode::fromType( t ) );
+              }else{
+                d_cinfo[v].d_csol_var[k-1] = NodeManager::currentNM()->mkSkolem( "e", TypeNode::fromType( t ) );
+              }
+            }
+            break;
+          }
+        }
+      }
+    }
+  }
+  //mark active
+  if( d_cinfo[v].d_csol_cond.isNull() ){
+    d_cinfo[v].d_csol_status = 0;
+  }
+  if( !type_valid ){
+    Assert( false );
+  }
+}
+
+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 = qe->getValuation().ensureLiteral( d_nsg_guard );
+        d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
         AlwaysAssert( !d_nsg_guard.isNull() );
-        qe->getOutputChannel().requirePhase( d_nsg_guard, true );
+        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;
-        qe->getOutputChannel().lemma( lem );
+        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;
-        qe->getOutputChannel().lemma( lems[i] );
+        d_qe->getOutputChannel().lemma( lems[i] );
         if( Trace.isOn("cegqi-debug") ){
           Node rlem = Rewriter::rewrite( lems[i] );
           Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
@@ -117,7 +163,25 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
   }
 }
 
-Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+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 );
+    }
+  }
+  //TODO
+  Assert( ret.isNull() || ret.getType().isInteger() );
+  return ret;
+}
+  
+  
+Node CegConjecture::getFairnessLiteral( int i ) {
   if( d_measure_term.isNull() ){
     return Node::null();
   }else{
@@ -131,8 +195,8 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
 
       Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
       Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl;
-      qe->getOutputChannel().lemma( lem );
-      qe->getOutputChannel().requirePhase( lit, true );
+      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
@@ -146,7 +210,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
         }
         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;
-        qe->getOutputChannel().lemma( hlem );
+        d_qe->getOutputChannel().lemma( hlem );
       }
       return lit;
     }else{
@@ -219,10 +283,563 @@ bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
   }
 }
 
+
+void CegConjecture::doCegConjectureSingleInvCheck(std::vector< Node >& lems) {
+  if( d_ceg_si!=NULL ){
+    d_ceg_si->check(lems);
+  }
+}
+
+bool CegConjecture::needsRefinement() { 
+  return !d_ce_sk.empty() || d_incomplete_candidate_values;
+}
+
+void CegConjecture::getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd ){
+  Assert( options::cegqiUnifCondSol() );
+  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 ){
+        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{
+        //otherwise, yet to explore 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::cegqiUnifCondSol() && !forceOrig ){
+    for( unsigned i=0; i<d_candidates.size(); i++ ){
+      getConditionalCandidateList( clist, d_candidates[i], true );
+    }
+  }else{
+    clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() );
+  }
+}
+
+Node CegConjecture::constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr ) {
+  Assert( options::cegqiUnifCondSol() );
+  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 ){
+          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 ) {
+  Assert( clist.size()==model_values.size() );
+  if( options::cegqiUnifCondSol() ){
+    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() ){
+        return false;
+      }
+    }
+  }else{
+    Assert( model_values.size()==d_candidates.size() );
+    candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() );
+  }
+  return true;
+}
+
+void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values) {
+  std::vector< Node > clist;
+  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 ) ){
+    d_incomplete_candidate_values = false;
+    Assert( c_model_values.size()==d_candidates.size() );
+    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::cegqiUnifCondSol() ){
+      //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 ){
+      d_ce_sk.push_back( std::vector< Node >() );
+    }
+    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 ){
+        ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+        if( sk_refine ){
+          d_ce_sk.back().push_back( dr[0] );
+        }
+      }else{
+        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;
+        }
+      }
+    }
+    Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+    lem = Rewriter::rewrite( lem );
+    lems.push_back( lem );
+    recordInstantiation( c_model_values );
+  }else{
+    d_incomplete_candidate_values = true;
+    Assert( false );
+  }
+}
+
+Node CegConjecture::getActiveConditional( Node curr ) {
+  Assert( options::cegqiUnifCondSol() );
+  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{
+      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::getContextConditionals( Node curr, Node x, std::vector< Node >& conds, std::vector< Node >& rets, std::map< Node, bool >& cpols ) {
+  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 ){
+        conds.push_back( it->second.d_csol_cond );
+        rets.push_back( it->second.d_csol_var[it->second.d_csol_status] );
+        cpols[it->second.d_csol_cond] = ( it->second.d_csol_status==1  );
+        getContextConditionals( it->second.d_csol_var[1-it->second.d_csol_status], x, conds, rets, cpols );
+      }
+    }
+  }
+}
+
+Node CegConjecture::mkConditional( Node c, std::vector< Node >& args, bool pol ) {
+  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] );
+  }
+  Node ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, condc );
+  if( !pol ){
+    ret = ret.negate();
+  }
+  return ret;
+}
+  
+  
+Node CegConjecture::purifyConditionalEvaluations( Node n, std::map< Node, Node >& csol_cond, 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_cond.find( n[0] );
+      if( itc!=csol_cond.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_cond, 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;
+  }
+}
+        
+void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
+  Assert( lems.empty() );
+  std::map< Node, Node > csol_cond;
+  std::map< Node, std::vector< Node > > csol_ccond;
+  std::map< Node, std::vector< Node > > csol_ccond_ret;
+  std::map< Node, std::map< Node, bool > > csol_cpol;
+  std::vector< Node > csol_vals;
+  if( options::cegqiUnifCondSol() ){
+    std::vector< Node > new_active_measure_sum;
+    Trace("cegqi-unif") << "Conditional solution refinement, expand active conditional nodes" << std::endl;
+    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
+      getContextConditionals( v, ac, csol_ccond[v], csol_ccond_ret[v], csol_cpol[v] );
+      if( !csol_ccond[v].empty() ){
+        //it will be conditionally evaluated, this is a placeholder
+        csol_cond[v] = Node::null();
+      }
+      //if it is a conditional
+      if( !d_cinfo[ac].d_csol_cond.isNull() ){
+        //activate
+        Trace("cegqi-unif") << "****** For " << v << ", expanding an active conditional node : " << ac << std::endl;
+        d_cinfo[ac].d_csol_status = 0;  //TODO
+        Trace("cegqi-unif") << "...expanded to " << d_cinfo[ac].d_csol_op << "( ";
+        Trace("cegqi-unif") << d_cinfo[ac].d_csol_cond << ", " << d_cinfo[ac].d_csol_var[0] << ", ";
+        Trace("cegqi-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_cond[v] = d_cinfo[ac].d_csol_cond;
+        csol_vals.push_back( d_cinfo[ac].d_csol_var[d_cinfo[ac].d_csol_status] );
+      }else{
+        Trace("cegqi-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==0 ){
+          Node acf = getMeasureTermFactor( ac );
+          if( !acf.isNull() ){
+            new_active_measure_sum.push_back( acf );
+          }
+          d_cinfo[ac].d_csol_status = 1;
+        }
+        csol_vals.push_back( ac );
+      }
+      if( !csol_ccond[v].empty() ){
+        Trace("cegqi-unif") << "...it is nested under " << csol_ccond[v].size() << " other conditionals" << std::endl;
+      }
+    }
+    // must add to active measure
+    if( !new_active_measure_sum.empty() ){
+      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;
+    }
+  }
+  Trace("cegqi-refine") << "Refine " << d_ce_sk.size() << " points." << std::endl;
+  //for conditional evaluation
+  std::map< Node, Node > psubs_visited;
+  std::map< Node, Node > psubs;
+  //skolem substitution
+  std::vector< Node > sk_vars;
+  std::vector< Node > sk_subs;
+  for( unsigned j=0; j<d_ce_sk.size(); j++ ){
+    bool success = true;
+    std::vector< Node > lem_c;
+    Assert( d_ce_sk[j].size()==d_base_disj.size() );
+    std::vector< Node > inst_cond_c;
+    for( unsigned k=0; k<d_ce_sk[j].size(); k++ ){
+      Node ce_q = d_ce_sk[j][k];
+      Trace("cegqi-refine") << "  For counterexample point " << j << ", disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl;
+      Node c_disj;
+      if( !ce_q.isNull() ){
+        Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL );
+        c_disj = d_base_disj[k][0][1];
+      }else{
+        if( d_inner_vars_disj[k].empty() ){
+          c_disj = d_base_disj[k].negate();
+        }else{
+          //denegrate case : quantified disjunct was trivially true and does not need to be refined
+          Trace("cegqi-refine") << "*** skip " << d_base_disj[k] << std::endl;
+          //add trivial substitution (in case we need substitution for previous cex's)
+          for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){
+            sk_vars.push_back( d_inner_vars_disj[k][i] );
+            sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value
+          }
+        }
+      }
+      //compute the body, inst_cond
+      if( options::cegqiUnifCondSol() && !c_disj.isNull() ){
+        Trace("cegqi-unif") << "Process " << c_disj << std::endl;
+        c_disj = purifyConditionalEvaluations( c_disj, csol_cond, psubs, psubs_visited );
+        Trace("cegqi-unif") << "Purified to : " << c_disj << std::endl;
+        Trace("cegqi-unif") << "...now with " << psubs.size() << " definitions." << std::endl;
+      }else{
+        //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
+      }
+      //collect the substitution over all disjuncts
+      if( !ce_q.isNull() ){
+        Assert( !d_inner_vars_disj[k].empty() );
+        Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() );
+        std::vector< Node > model_values;
+        if( getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
+          sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
+          sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
+        }else{
+          success = false;
+          break;
+        }
+      }
+      //add to the lemma
+      if( !c_disj.isNull() ){
+        lem_c.push_back( c_disj );
+      }
+    }
+    if( success ){
+      Trace("cegqi-unif") << "Add conditional assumptions for " << psubs.size() << " evaluations." << std::endl;
+      //add conditional correctness assumptions
+      std::map< Node, Node > psubs_condc;
+      std::map< Node, std::vector< Node > > psubs_apply;
+      std::vector< Node > paux_vars;
+      for( std::map< Node, Node >::iterator itp = psubs.begin(); itp != psubs.end(); ++itp ){
+        Assert( csol_cond.find( itp->first[0] )!=csol_cond.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 c = csol_cond[itp->first[0]];
+        psubs_apply[ c ].push_back( itp->first );
+        Trace("cegqi-unif") << "   process assumption " << itp->first << " == " << itp->second << ", with current condition " << c;
+        Trace("cegqi-unif") << ", and " << csol_ccond[itp->first[0]].size() << " context conditionals." << std::endl;
+        std::vector< Node> assm;
+        if( !c.isNull() ){
+          assm.push_back( mkConditional( c, args ) );
+        }
+        for( unsigned j=0; j<csol_ccond[itp->first[0]].size(); j++ ){
+          Node cc = csol_ccond[itp->first[0]][j];
+          assm.push_back( mkConditional( cc, args, csol_cpol[itp->first[0]][cc] ) );
+        }
+        Assert( !assm.empty() );
+        Node condn = assm.size()==1 ? assm[0] : NodeManager::currentNM()->mkNode( kind::AND, assm );
+        Node cond = NodeManager::currentNM()->mkNode( kind::IMPLIES, condn, itp->first.eqNode( itp->second ) );
+        psubs_condc[itp->first] = cond;
+        Trace("cegqi-unif") << "   ...made conditional correctness assumption : " << cond << std::endl;
+      }
+      for( std::map< Node, Node >::iterator itp = psubs_condc.begin(); itp != psubs_condc.end(); ++itp ){
+        lem_c.push_back( itp->second );
+      }
+      
+      Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
+      //substitute the actual return values
+      if( options::cegqiUnifCondSol() ){
+        Assert( d_candidates.size()==csol_vals.size() );
+        lem = lem.substitute( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+      }
+      
+      //previous non-ground conditional refinement lemmas must satisfy the current point
+      for( unsigned i=0; i<d_refinement_lemmas.size(); i++ ){
+        Node prev_lem = d_refinement_lemmas[i];
+        prev_lem = prev_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+        //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 );
+        prev_lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), prev_lem );
+        Trace("cegqi-unif") << "...previous conditional refinement lemma with new counterexample : " << prev_lem << std::endl;
+        lems.push_back( prev_lem );
+      }
+      if( !isGround() && !csol_cond.empty() ){
+        Trace("cegqi-unif") << "Lemma " << lem << " is a non-ground conditional refinement lemma, store it for future instantiation." << std::endl;
+        d_refinement_lemmas.push_back( lem );
+        d_refinement_lemmas_aux_vars.push_back( paux_vars );
+      }
+      
+      if( options::cegqiUnifCondSol() ){
+        Trace("cegqi-unif") << "We have lemma : " << lem << std::endl;
+        Trace("cegqi-unif") << "Now add progress assertions..." << std::endl;
+        std::vector< Node > prgr_conj;
+        std::map< Node, bool > cprocessed;
+        for( std::map< Node, Node >::iterator itc = csol_cond.begin(); itc !=csol_cond.end(); ++itc ){
+          Node x = itc->first;
+          Node c = itc->second;          
+          if( !c.isNull() ){
+            Trace("cegqi-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" ) );
+            }
+            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
+                Node pdlem = prgr_domain_d.size()==1 ? prgr_domain_d[0] : NodeManager::currentNM()->mkNode( OR, prgr_domain_d );
+                prgr_conj.push_back( pdlem );
+              }
+            }
+            //the condition holds for the point
+            prgr_conj.push_back( mkConditional( c, prgr_pt ) );
+            // ...and not for its context, if this return point is different from them
+            //for( unsigned j=0; j<csol_ccond[x].size(); j++ ){
+            //  Node cc = csol_ccond[x][j];
+            //  prgr_conj.push_back( mkConditional( cc, prgr_pt, csol_cpol[x][cc] ) );
+            //}
+            //FIXME
+          }
+        }
+        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( d_candidates.begin(), d_candidates.end(), csol_vals.begin(), csol_vals.end() );
+          Trace("cegqi-unif") << "Progress lemma is " << prgr_lem << std::endl;
+          lem = NodeManager::currentNM()->mkNode( kind::AND, lem, prgr_lem );
+        }
+        //make in terms of new values
+        Assert( csol_vals.size()==d_candidates.size() );
+        Trace("cegqi-unif") << "Now rewrite in terms of new evaluation branches...got " << lem << std::endl;
+      }
+      //apply the substitution
+      Assert( sk_vars.size()==sk_subs.size() );
+      lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+      lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
+      lem = Rewriter::rewrite( lem );
+      lems.push_back( lem );
+    }
+  }
+  d_ce_sk.clear();
+  d_incomplete_candidate_values = false;
+}
+
 void CegConjecture::preregisterConjecture( Node q ) {
   d_ceg_si->preregisterConjecture( q );
 }
 
+bool CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+  bool success = true;
+  Trace("cegqi-engine") << "  * Value is : ";
+  for( unsigned i=0; i<n.size(); i++ ){
+    Node nv = getModelValue( n[i] );
+    v.push_back( nv );
+    if( Trace.isOn("cegqi-engine") ){
+      TypeNode tn = nv.getType();
+      Trace("cegqi-engine") << n[i] << " -> ";
+      std::stringstream ss;
+      std::vector< Node > lvs;
+      TermDbSygus::printSygusTerm( ss, nv, lvs );
+      Trace("cegqi-engine") << ss.str() << " ";
+    }
+    if( nv.isNull() ){
+      Trace("cegqi-warn") << "WARNING: failed getModelValues." << std::endl;
+      success = false;
+    }
+  }
+  Trace("cegqi-engine") << std::endl;
+  return success;
+}
+
+Node CegConjecture::getModelValue( Node n ) {
+  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
+  return d_qe->getModel()->getValue( n );
+}
+
+void CegConjecture::debugPrint( const char * c ) {
+  Trace(c) << "Synthesis conjecture : " << d_quant << std::endl;
+  Trace(c) << "  * Candidate program/output symbol : ";
+  for( unsigned i=0; i<d_candidates.size(); i++ ){
+    Trace(c) << d_candidates[i] << " ";
+  }
+  Trace(c) << std::endl;
+  Trace(c) << "  * Candidate ce skolems : ";
+  for( unsigned i=0; i<d_ce_sk.size(); i++ ){
+    Trace(c) << d_ce_sk[i] << " ";
+  }
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe, qe->getSatContext() );
   d_last_inst_si = false;
@@ -315,26 +932,32 @@ void CegInstantiation::registerQuantifier( Node q ) {
       //fairness
       if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
         std::vector< Node > mc;
-        for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
-          TypeNode tn = d_conj->d_candidates[j].getType();
-          if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE ){
-            if( tn.isDatatype() ){
-              mc.push_back( NodeManager::currentNM()->mkNode( DT_SIZE, d_conj->d_candidates[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, d_conj->d_candidates[j] ) );
+        if( options::cegqiUnifCondSol() || 
+            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] ) );
+              }
             }
-          }else if( 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() ) );
           }
         }
         if( !mc.empty() ){
-          d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
-          Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
+          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{
@@ -351,7 +974,7 @@ void CegInstantiation::assertNode( Node n ) {
 Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
   //enforce fairness
   if( d_conj->isAssigned() ){
-    d_conj->initializeGuard( d_quantEngine );
+    d_conj->initializeGuard();
     std::vector< Node > req_dec;
     const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
     if( ! ceg_si->d_full_guard.isNull() ){
@@ -374,12 +997,12 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
     }
 
     if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-      Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+      Node lit = d_conj->getFairnessLiteral( d_conj->getCurrentTermSize() );
       bool value;
       if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
         if( !value ){
-          d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
-          lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+          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;
@@ -398,47 +1021,43 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   Node q = conj->d_quant;
   Node aq = conj->d_assert_quant;
-  Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
-  Trace("cegqi-engine-debug") << "  * Candidate program/output symbol : ";
-  for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
-    Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
-  }
-  Trace("cegqi-engine-debug") << std::endl;
-  Trace("cegqi-engine-debug") << "  * Candidate ce skolems : ";
-  for( unsigned i=0; i<conj->d_ce_sk.size(); i++ ){
-    Trace("cegqi-engine-debug") << conj->d_ce_sk[i] << " ";
+  if( Trace.isOn("cegqi-engine-debug") ){
+    conj->debugPrint("cegqi-engine-debug");
+    Trace("cegqi-engine-debug") << std::endl;
   }
-  Trace("cegqi-engine-debug") << std::endl;
   if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-    Trace("cegqi-engine") << "  * Current term size : " << conj->d_curr_lit.get() << std::endl;
-  }
+    Trace("cegqi-engine") << "  * Current term size : " << conj->getCurrentTermSize() << std::endl;
+  }  
 
-  if( conj->d_ce_sk.empty() ){
-    Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+  if( !conj->needsRefinement() ){
     if( conj->d_syntax_guided ){
-      if( conj->getCegConjectureSingleInv() != NULL ){
-        std::vector< Node > lems;
-        if( conj->doCegConjectureCheck( lems ) ){
-          if( !lems.empty() ){
-            d_last_inst_si = true;
-            for( unsigned j=0; j<lems.size(); j++ ){
-              Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << lems[j] << std::endl;
-              d_quantEngine->addLemma( lems[j] );
-            }
-            d_statistics.d_cegqi_si_lemmas += lems.size();
-            Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
-          }
-          return;
+      std::vector< Node > clems;
+      conj->doCegConjectureSingleInvCheck( clems );
+      if( !clems.empty() ){
+        d_last_inst_si = true;
+        for( unsigned j=0; j<clems.size(); j++ ){
+          Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << clems[j] << std::endl;
+          d_quantEngine->addLemma( clems[j] );
         }
+        d_statistics.d_cegqi_si_lemmas += clems.size();
+        Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
+        return;
       }
+      //ignore return value here
+      std::vector< Node > clist;
+      conj->getCandidateList( clist );
       std::vector< Node > model_values;
-      if( getModelValues( conj, conj->d_candidates, model_values ) ){
+      if( conj->getModelValues( clist, model_values ) ){
         if( options::sygusDirectEval() ){
+          Trace("cegqi-debug") << "Do direct evaluation..." << std::endl;
           std::vector< Node > eager_eval_lem;
-          for( unsigned j=0; j<conj->d_candidates.size(); j++ ){
-            d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem );
+          for( unsigned j=0; j<clist.size(); j++ ){
+          Trace("cegqi-debug") << "  register " << clist[j] << " -> " << model_values[j] << std::endl;
+            d_quantEngine->getTermDatabaseSygus()->registerModelValue( clist[j], model_values[j], eager_eval_lem );
           }
+          Trace("cegqi-debug") << "...produced " << eager_eval_lem.size()  << " eager evaluation lemmas." << std::endl;
           if( !eager_eval_lem.empty() ){
+            Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
             for( unsigned j=0; j<eager_eval_lem.size(); j++ ){
               Node lem = eager_eval_lem[j];
               if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
@@ -453,11 +1072,15 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         }
         //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<conj->d_candidates.size(); j++ ){
-            getMeasureLemmas( conj->d_candidates[j], model_values[j], 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] );
@@ -466,156 +1089,75 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
             return;
           }
         }
-        //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 );
-        if( sk_refine ){
-          conj->d_ce_sk.push_back( std::vector< Node >() );
-        }
-        std::vector< Node > ic;
-        ic.push_back( aq.negate() );
-        std::vector< Node > d;
-        collectDisjuncts( inst, d );
-        Assert( d.size()==conj->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 ){
-            ic.push_back( getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
-            if( sk_refine ){
-              conj->d_ce_sk.back().push_back( dr[0] );
-            }
+        
+        Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
+        std::vector< Node > cclems;
+        conj->doCegConjectureCheck( cclems, model_values );
+        bool addedLemma = false;
+        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);
+            addedLemma = true;
           }else{
-            ic.push_back( dr );
-            if( sk_refine ){
-              conj->d_ce_sk.back().push_back( Node::null() );
-            }
-            if( !conj->d_inner_vars_disj[i].empty() ){
-              Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
+            //this may happen if we eagerly unfold, simplify to true
+            if( !options::sygusDirectEval() ){
+              Trace("cegqi-warn") << "  ...FAILED to add candidate!" << std::endl;
+            }else{
+              Trace("cegqi-engine-debug") << "  ...FAILED to add candidate!" << std::endl;
             }
           }
         }
-        Node lem = NodeManager::currentNM()->mkNode( OR, ic );
-        lem = Rewriter::rewrite( lem );
-        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);
-          Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
+        if( addedLemma ){
+          Trace("cegqi-engine") << "  ...check for counterexample." << std::endl;
         }else{
-          //this may happen if we eagerly unfold, simplify to true
-          if( !options::sygusDirectEval() ){
-            Trace("cegqi-engine") << "  ...FAILED to add candidate!" << std::endl;
-          }else{
-            Trace("cegqi-engine-debug") << "  ...FAILED to add candidate!" << std::endl;
-          }
-          if( conj->d_refine_count==0  ){
+          if( conj->needsRefinement() ){
             //immediately go to refine candidate
             checkCegConjecture( conj );
             return;
           }
-        }
+        } 
       }
-
     }else{
       Assert( aq==q );
       std::vector< Node > model_terms;
-      if( getModelValues( conj, conj->d_candidates, model_terms ) ){
+      std::vector< Node > clist;
+      conj->getCandidateList( clist, true );
+      Assert( clist.size()==q[0].getNumChildren() );
+      if( conj->getModelValues( clist, model_terms ) ){
+        conj->recordInstantiation( model_terms );
         d_quantEngine->addInstantiation( q, model_terms );
       }
     }
   }else{
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
-    for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){
-      bool success = true;
-      std::vector< Node > lem_c;
-      Assert( conj->d_ce_sk[j].size()==conj->d_base_disj.size() );
-      for( unsigned k=0; k<conj->d_ce_sk[j].size(); k++ ){
-        Node ce_q = conj->d_ce_sk[j][k];
-        Node c_disj = conj->d_base_disj[k];
-        if( !ce_q.isNull() ){
-          Assert( !conj->d_inner_vars_disj[k].empty() );
-          Assert( conj->d_inner_vars_disj[k].size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
-          std::vector< Node > model_values;
-          if( getModelValues( NULL, getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
-            //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
-            Node inst_ce_refine = conj->d_base_disj[k][0][1].substitute( conj->d_inner_vars_disj[k].begin(), conj->d_inner_vars_disj[k].end(),
-                                                                         model_values.begin(), model_values.end() );
-            lem_c.push_back( inst_ce_refine );
-          }else{
-            success = false;
-            break;
-          }
-        }else{
-          if( conj->d_inner_vars_disj[k].empty() ){
-            lem_c.push_back( conj->d_base_disj[k].negate() );
-          }else{
-            //denegrate case : quantified disjunct was trivially true and does not need to be refined
-            Trace("cegqi-debug") << "*** skip " << conj->d_base_disj[k] << std::endl;
-          }
-        }
-      }
-      if( success ){
-        Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
-        lem = NodeManager::currentNM()->mkNode( OR, conj->getGuard().negate(), lem );
-        lem = Rewriter::rewrite( lem );
-        Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
-        Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
-        bool res = d_quantEngine->addLemma( lem );
-        if( res ){
-          ++(d_statistics.d_cegqi_lemmas_refine);
-          conj->d_refine_count++;
-        }else{
-          Trace("cegqi-engine") << "  ...FAILED to add refinement!" << std::endl;
-        }
+    std::vector< Node > rlems;
+    conj->doCegConjectureRefine( rlems );
+    bool addedLemma = false;
+    for( unsigned i=0; i<rlems.size(); i++ ){
+      Node lem = rlems[i];
+      Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl;
+      bool res = d_quantEngine->addLemma( lem );
+      if( res ){
+        ++(d_statistics.d_cegqi_lemmas_refine);
+        conj->d_refine_count++;
+        addedLemma = true;
+      }else{
+        Trace("cegqi-warn") << "  ...FAILED to add refinement!" << std::endl;
       }
     }
-    conj->d_ce_sk.clear();
-  }
-}
-
-bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v ) {
-  bool success = true;
-  Trace("cegqi-engine") << "  * Value is : ";
-  for( unsigned i=0; i<n.size(); i++ ){
-    Node nv = getModelValue( n[i] );
-    v.push_back( nv );
-    if( Trace.isOn("cegqi-engine") ){
-      TypeNode tn = nv.getType();
-      Trace("cegqi-engine") << n[i] << " -> ";
-      std::stringstream ss;
-      std::vector< Node > lvs;
-      TermDbSygus::printSygusTerm( ss, nv, lvs );
-      Trace("cegqi-engine") << ss.str() << " ";
-    }
-    if( nv.isNull() ){
-      success = false;
-    }
-    if( conj ){
-      conj->d_candidate_inst[i].push_back( nv );
+    if( addedLemma ){
+      Trace("cegqi-engine") << "  ...refine candidate." << std::endl;
     }
   }
-  Trace("cegqi-engine") << std::endl;
-  return success;
-}
-
-Node CegInstantiation::getModelValue( Node n ) {
-  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
-  return d_quantEngine->getModel()->getValue( n );
-}
-
-Node CegInstantiation::getModelTerm( Node n ){
-  //TODO
-  return getModelValue( n );
 }
 
 void CegInstantiation::registerMeasuredType( TypeNode tn ) {
@@ -710,13 +1252,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited )
           }
           for( unsigned j=1; j<n.getNumChildren(); j++ ){
             Node nc = getEagerUnfold( n[j], visited );
-            //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));
-            //  subs.push_back( nc.eqNode( c ) );
-            //}else{
             subs.push_back( nc );
-            //}
             Assert( subs[j-1].getType()==var_list[j-1].getType() );
           }
           Assert( vars.size()==subs.size() );
@@ -763,6 +1299,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
     //}
     for( unsigned i=0; i<d_conj->d_quant[0].getNumChildren(); i++ ){
       Node prog = d_conj->d_quant[0][i];
+      Trace("cegqi-debug") << "  print solution for " << prog << std::endl;
       std::stringstream ss;
       ss << prog;
       std::string f(ss.str());
@@ -779,8 +1316,9 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
         sol = sol.getKind()==LAMBDA ? sol[1] : sol;
       }else{
-        if( !d_conj->d_candidate_inst[i].empty() ){
-          sol = d_conj->d_candidate_inst[i].back();
+        Node cprog = d_conj->getCandidate( i );
+        if( !d_conj->d_cinfo[cprog].d_inst.empty() ){
+          sol = d_conj->d_cinfo[cprog].d_inst.back();
           // Check if this was based on a template, if so, we must do
           // Reconstruction
           if( d_conj->d_assert_quant!=d_conj->d_quant ){
@@ -844,6 +1382,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
           }else{
             status = 1;
           }
+        }else{
+          Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl;
         }
       }
       if( !(Trace.isOn("cegqi-stats")) ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 7f36f4d25..f49298411 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -31,6 +31,37 @@ namespace quantifiers {
 class CegConjecture {
 private:
   QuantifiersEngine * d_qe;
+  /** list of constants for quantified formula */
+  std::vector< Node > d_candidates;
+  /** base instantiation */
+  Node d_base_inst;
+  /** expand base inst to disjuncts */
+  std::vector< Node > d_base_disj;
+  /** list of variables on inner quantification */
+  std::vector< Node > d_inner_vars;
+  std::vector< std::vector< Node > > d_inner_vars_disj;
+  /** current extential quantifeirs whose couterexamples we must refine */
+  std::vector< std::vector< Node > > d_ce_sk;
+  /** the cardinality literals */
+  std::map< int, Node > d_lits;
+  /** current cardinality */
+  context::CDO< int > d_curr_lit;
+  /** active measure term */
+  Node d_active_measure_term;
+  /** refinement lemmas */
+  std::vector< Node > d_refinement_lemmas;
+  std::vector< std::vector< Node > > d_refinement_lemmas_aux_vars;
+private: //for condition solutions
+  /** get candidate list recursively for conditional solutions */
+  void getConditionalCandidateList( std::vector< Node >& clist, Node curr, bool reqAdd );
+  Node constructConditionalCandidate( std::map< Node, Node >& cmv, Node curr );
+  Node getActiveConditional( Node curr );
+  void getContextConditionals( Node curr, Node x, std::vector< Node >& conds, std::vector< Node >& rets, std::map< Node, bool >& cpols );
+  Node mkConditional( Node c, std::vector< Node >& args, bool pol = true );
+  Node purifyConditionalEvaluations( Node n, std::map< Node, Node >& csol_cond, std::map< Node, Node >& psubs, 
+                                     std::map< Node, Node >& visited );
+  /** register candidate conditional */
+  void registerCandidateConditional( Node v );
 public:
   CegConjecture( QuantifiersEngine * qe, context::Context* c );
   ~CegConjecture();
@@ -39,33 +70,41 @@ public:
   Node d_assert_quant;
   /** quantified formula (after processing) */
   Node d_quant;
-  /** base instantiation */
-  Node d_base_inst;
-  /** expand base inst to disjuncts */
-  std::vector< Node > d_base_disj;
-  /** list of constants for quantified formula */
-  std::vector< Node > d_candidates;
-  /** list of variables on inner quantification */
-  std::vector< Node > d_inner_vars;
-  std::vector< std::vector< Node > > d_inner_vars_disj;
-  /** list of terms we have instantiated candidates with */
-  std::map< int, std::vector< Node > > d_candidate_inst;
+
+  class CandidateInfo {
+  public:
+    CandidateInfo() : d_csol_status(-1){}
+    /** list of terms we have instantiated candidates with */
+    std::vector< Node > d_inst;
+    /** conditional solutions */
+    Node d_csol_op;
+    Node d_csol_cond;
+    Node d_csol_var[2];
+    /** solution status */
+    int d_csol_status;
+  };
+  std::map< Node, CandidateInfo > d_cinfo;
+  
   /** measure term */
   Node d_measure_term;
   /** measure sum size */
   int d_measure_term_size;
   /** refine count */
   unsigned d_refine_count;
-  /** current extential quantifeirs whose couterexamples we must refine */
-  std::vector< std::vector< Node > > d_ce_sk;
+  /** incomplete candidate values */
+  bool d_incomplete_candidate_values;
 
   const CegConjectureSingleInv* getCegConjectureSingleInv() const {
     return d_ceg_si;
   }
+  
+  bool needsRefinement();
+  void getCandidateList( std::vector< Node >& clist, bool forceOrig = false );
+  bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values );
 
-  bool doCegConjectureCheck(std::vector< Node >& lems) {
-    return d_ceg_si->check(lems);
-  }
+  void doCegConjectureSingleInvCheck(std::vector< Node >& lems);
+  void doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values);
+  void doCegConjectureRefine(std::vector< Node >& lems);
 
   Node getSingleInvocationSolution(unsigned sol_index, TypeNode stn,
                                    int& reconstructed, bool rconsSygus=true){
@@ -80,21 +119,36 @@ public:
   std::vector<Node>& getProgTempVars(Node prog) {
     return d_ceg_si->d_prog_templ_vars[prog];
   }
+  
+  void recordInstantiation( std::vector< Node >& vs ) {
+    Assert( vs.size()==d_candidates.size() );
+    for( unsigned i=0; i<vs.size(); i++ ){
+      d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
+    }
+  }
+  Node getCandidate( unsigned int i ) { return d_candidates[i]; }
+  
+  void debugPrint( const char * c );
 
- private:
+private:
   /** single invocation utility */
   CegConjectureSingleInv * d_ceg_si;
 public: //non-syntax guided (deprecated)
   /** guard */
   bool d_syntax_guided;
   Node d_nsg_guard;
-public:  //for fairness
-  /** the cardinality literals */
-  std::map< int, Node > d_lits;
-  /** current cardinality */
-  context::CDO< int > d_curr_lit;
+public:
+  /** get current term size */
+  int getCurrentTermSize() { return d_curr_lit.get(); }
+  /** increment current term size */
+  void incrementCurrentTermSize() { d_curr_lit.set( d_curr_lit.get() + 1 ); }
+  /** set measure term */
+  void setMeasureTerm( Node mt );
+  /** get measure term */
+  Node getMeasureTermFactor( Node v );
+  Node getMeasureTerm() { return d_measure_term; }
   /** allocate literal */
-  Node getLiteral( QuantifiersEngine * qe, int i );
+  Node getFairnessLiteral( int i );
   /** get guard */
   Node getGuard();
   /** is ground */
@@ -110,11 +164,15 @@ public:  //for fairness
   /** preregister conjecture */
   void preregisterConjecture( Node q );
   /** initialize guard */
-  void initializeGuard( QuantifiersEngine * qe );
+  void initializeGuard();
   /** assign */
   void assign( Node q );
   /** is assigned */
   bool isAssigned() { return !d_quant.isNull(); }
+  /** get model values */
+  bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
+  /** get model value */
+  Node getModelValue( Node n );
 };
 
 
@@ -146,12 +204,6 @@ private: //for enforcing fairness
 private:
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
-  /** get model values */
-  bool getModelValues( CegConjecture * conj, std::vector< Node >& n, std::vector< Node >& v );
-  /** get model value */
-  Node getModelValue( Node n );
-  /** get model term */
-  Node getModelTerm( Node n );
 public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
   ~CegInstantiation();
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 92d62a177..84743fc1d 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -758,13 +758,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
     for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
       Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
-      //if( varList[i].getType().isBoolean() ){
-      //  //TODO force boolean term conversion mode
-      //  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-      //  vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
-      //}else{
       vars.push_back( d_single_inv_arg_sk[i] );
-      //}
       d_sol->d_varList.push_back( varList[i] );
     }
     Trace("csi-sol") << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index d93898a1e..8ecd32ab1 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -215,7 +215,7 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) {
       if( n0.getKind()==ITE ){
         n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
                                                    NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
-      }else if( n0.getKind()==EQUAL ){
+      }else if( n0.getKind()==EQUAL && n0[0].getType().isBoolean() ){
         n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
                                                    NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
       }else{