Generalize conflict clauses in sygus sym break, merge caches, refactor. Preparation for single invocation properties. Set output lang to SMT2 for sygus.

7 files changed, 619 insertions, 362 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c011671f8..c3372d2c8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -202,6 +202,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         opts.set(options::inputLanguage, language::input::LANG_SYGUS);
+        //since there is no sygus output language, set this to SMT lib 2
+        opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0);
       }
     }
   }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 4e7aaad53..3063e85bb 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -30,73 +30,6 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-bool SygusSplit::isRegistered( TypeNode tn ) {
-  return d_register.find( tn )!=d_register.end();
-}
-
-int SygusSplit::getKindArg( TypeNode tn, Kind k ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
-  if( itt!=d_kinds.end() ){
-    std::map< Kind, int >::iterator it = itt->second.find( k );
-    if( it!=itt->second.end() ){
-      return it->second;
-    }
-  }
-  return -1;
-}
-
-int SygusSplit::getConstArg( TypeNode tn, Node n ){
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
-  if( itt!=d_consts.end() ){
-    std::map< Node, int >::iterator it = itt->second.find( n );
-    if( it!=itt->second.end() ){
-      return it->second;
-    }
-  }
-  return -1;
-}
-
-int SygusSplit::getOpArg( TypeNode tn, Node n ) {
-  std::map< Node, int >::iterator it = d_ops[tn].find( n );
-  if( it!=d_ops[tn].end() ){
-    return it->second;
-  }else{
-    return -1;
-  }
-}
-
-bool SygusSplit::hasKind( TypeNode tn, Kind k ) {
-  return getKindArg( tn, k )!=-1;
-}
-bool SygusSplit::hasConst( TypeNode tn, Node n ) {
-  return getConstArg( tn, n )!=-1;
-}
-bool SygusSplit::hasOp( TypeNode tn, Node n ) {
-  return getOpArg( tn, n )!=-1;
-}
-
-bool SygusSplit::isKindArg( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
-  if( itt!=d_arg_kind.end() ){
-    return itt->second.find( i )!=itt->second.end();
-  }else{
-    return false;
-  }
-}
-
-bool SygusSplit::isConstArg( TypeNode tn, int i ) {
-  Assert( isRegistered( tn ) );
-  std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
-  if( itt!=d_arg_const.end() ){
-    return itt->second.find( i )!=itt->second.end();
-  }else{
-    return false;
-  }
-}
-
 void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits, std::vector< Node >& lemmas ) {
   Assert( dt.isSygus() );
   if( d_splits.find( n )==d_splits.end() ){
@@ -123,7 +56,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
       //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt
       registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex );
 
-      if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
+      if( options::sygusNormalFormArg() && sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
         arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
         tn1 = arg1.getType();
         if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){
@@ -221,35 +154,18 @@ void SygusSplit::registerSygusType( TypeNode tn ) {
       if( d_register[tn].isNull() ){
         Trace("sygus-split") << "...not sygus." << std::endl;
       }else{
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          Expr sop = dt[i].getSygusOp();
-          Assert( !sop.isNull() );
-          Node n = Node::fromExpr( sop );
-          Trace("sygus-split") << "  Operator #" << i << " : " << sop;
-          if( sop.getKind() == kind::BUILTIN ){
-            Kind sk = NodeManager::operatorToKind( n );
-            Trace("sygus-split") << ", kind = " << sk;
-            d_kinds[tn][sk] = i;
-            d_arg_kind[tn][i] = sk;
-          }else if( sop.isConst() ){
-            Trace("sygus-split") << ", constant";
-            d_consts[tn][n] = i;
-            d_arg_const[tn][i] = n;
-          }
-          d_ops[tn][n] = i;
-          Trace("sygus-split") << std::endl;
-        }
+        d_util->registerSygusType( tn );
 
         //compute the redundant operators
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
           bool nred = true;
           if( options::sygusNormalForm() ){
             Trace("sygus-split-debug") << "Is " << dt[i].getName() << " a redundant operator?" << std::endl;
-            std::map< int, Kind >::iterator it = d_arg_kind[tn].find( i );
-            if( it!=d_arg_kind[tn].end() ){
+            std::map< int, Kind >::iterator it = d_util->d_arg_kind[tn].find( i );
+            if( it!=d_util->d_arg_kind[tn].end() ){
               Kind dk;
-              if( isAntisymmetric( it->second, dk ) ){
-                int j = getKindArg( tn, dk );
+              if( d_util->isAntisymmetric( it->second, dk ) ){
+                int j = d_util->getKindArg( tn, dk );
                 if( j!=-1 ){
                   Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
                   //check for type mismatches
@@ -265,14 +181,11 @@ void SygusSplit::registerSygusType( TypeNode tn ) {
                     }
                   }
                   if( success ){
-                    Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl;
+                    Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_util->d_arg_kind[tn][i] << " terms." << std::endl;
                     nred = false;
                   }
                 }
               }
-              //if( it->second==MINUS || it->second==BITVECTOR_SUB ){
-              //}
-              //NAND,NOR
             }
             if( nred ){
               Trace("sygus-split-debug") << "Check " << dt[i].getName() << " based on generic rewriting" << std::endl;
@@ -307,24 +220,24 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
       //get parent kind
       bool hasParentKind = false;
       Kind parentKind;
-      if( isKindArg( tnnp, csIndex ) ){
+      if( d_util->isKindArg( tnnp, csIndex ) ){
         hasParentKind = true;
-        parentKind = d_arg_kind[tnnp][csIndex];
+        parentKind = d_util->d_arg_kind[tnnp][csIndex];
       }
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
         bool addSplit = d_sygus_nred[tnn][i];
         if( addSplit && hasParentKind ){
-          if( d_arg_kind.find( tnn )!=d_arg_kind.end() && d_arg_kind[tnn].find( i )!=d_arg_kind[tnn].end() ){
-            addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_arg_kind[tnn][i], parentKind, sIndex );
+          if( d_util->d_arg_kind.find( tnn )!=d_util->d_arg_kind.end() && d_util->d_arg_kind[tnn].find( i )!=d_util->d_arg_kind[tnn].end() ){
+            addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_util->d_arg_kind[tnn][i], parentKind, sIndex );
             if( !addSplit ){
-              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_arg_kind[tnn][i];
+              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_util->d_arg_kind[tnn][i];
               Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
             }
-          }else if( d_arg_const.find( tnn )!=d_arg_const.end() && d_arg_const[tnn].find( i )!=d_arg_const[tnn].end() ){
-            addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_arg_const[tnn][i], parentKind, sIndex );
+          }else if( d_util->d_arg_const.find( tnn )!=d_util->d_arg_const.end() && d_util->d_arg_const[tnn].find( i )!=d_util->d_arg_const[tnn].end() ){
+            addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_util->d_arg_const[tnn][i], parentKind, sIndex );
             if( !addSplit ){
-              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_arg_const[tnn][i];
+              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_util->d_arg_const[tnn][i];
               Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
             }
           }
@@ -343,83 +256,81 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
         }
         d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
       }
-      if( options::sygusNormalFormArg() ){
-        //compute argument relationships for 2-arg constructors
-        if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
-          int osIndex = sIndex==0 ? 1 : 0;
-          TypeNode tnno = getArgType( pdt[csIndex], osIndex );
-          if( DatatypesRewriter::isTypeDatatype( tnno ) ){
-            const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype();
-            registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex );
-            //compute relationships when doing 0-arg
-            if( sIndex==0 ){
-              Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
-              Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() );
+      //compute argument relationships for 2-arg constructors
+      if( d_util->isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
+        int osIndex = sIndex==0 ? 1 : 0;
+        TypeNode tnno = getArgType( pdt[csIndex], osIndex );
+        if( DatatypesRewriter::isTypeDatatype( tnno ) ){
+          const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype();
+          registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex );
+          //compute relationships when doing 0-arg
+          if( sIndex==0 ){
+            Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
+            Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() );
 
-              Kind parentKind = d_arg_kind[tnnp][csIndex];
-              bool isPComm = isComm( parentKind );
-              std::map< int, bool > larg_consider;
-              for( unsigned i=0; i<dto.getNumConstructors(); i++ ){
-                if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
-                  //arguments that can be removed
-                  std::map< int, bool > rem_arg;
-                  //collect information about this index
-                  bool isSingularConst = isConstArg( tnno, i ) && isSingularArg( d_arg_const[tnno][i], parentKind, 1 );
-                  bool argConsider = false;
-                  for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-                    if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
-                      Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl;
-                      bool rem = false;
-                      if( isPComm && j>i && tnn==tnno ){
-                        //based on commutativity
-                        // use term ordering : constructor index of first argument is not greater than constructor index of second argument
-                        rem = true;
-                        Trace("sygus-nf") << "* Sygus norm : commutativity of " << parentKind << " : consider " << dt[j].getSygusOp() << " before " << dto[i].getSygusOp() << std::endl;
-                      }else if( isSingularConst && argConsider ){
-                        rem = true;
-                        Trace("sygus-nf") << "* Sygus norm : RHS singularity arg " << dto[i].getSygusOp() << " of " << parentKind;
-                        Trace("sygus-nf") << " : do not consider " << dt[j].getSygusOp() << " as first arg." << std::endl;
-                      }else if( isConstArg( tnn, j ) && isSingularArg( d_arg_const[tnn][j], parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){
-                        rem = true;
-                        Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind;
-                        Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl;
-                      }else{
-                        if( parentKind!=UNDEFINED_KIND ){
-                          //&& dto[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){
-                          std::map< TypeNode, int > var_count;
-                          std::map< int, Node > pre;
-                          Node g1 = d_util->mkGeneric( dt, j, var_count, pre );
-                          Node g2 = d_util->mkGeneric( dto, i, var_count, pre );
-                          Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 );
-                          if( isGenericRedundant( tnnp, g ) ){
-                            rem = true;
-                          }
+            Kind parentKind = d_util->d_arg_kind[tnnp][csIndex];
+            bool isPComm = d_util->isComm( parentKind );
+            std::map< int, bool > larg_consider;
+            for( unsigned i=0; i<dto.getNumConstructors(); i++ ){
+              if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
+                //arguments that can be removed
+                std::map< int, bool > rem_arg;
+                //collect information about this index
+                bool isSingularConst = d_util->isConstArg( tnno, i ) && d_util->isSingularArg( d_util->d_arg_const[tnno][i], parentKind, 1 );
+                bool argConsider = false;
+                for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+                  if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
+                    Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl;
+                    bool rem = false;
+                    if( isPComm && j>i && tnn==tnno ){
+                      //based on commutativity
+                      // use term ordering : constructor index of first argument is not greater than constructor index of second argument
+                      rem = true;
+                      Trace("sygus-nf") << "* Sygus norm : commutativity of " << parentKind << " : consider " << dt[j].getSygusOp() << " before " << dto[i].getSygusOp() << std::endl;
+                    }else if( isSingularConst && argConsider ){
+                      rem = true;
+                      Trace("sygus-nf") << "* Sygus norm : RHS singularity arg " << dto[i].getSygusOp() << " of " << parentKind;
+                      Trace("sygus-nf") << " : do not consider " << dt[j].getSygusOp() << " as first arg." << std::endl;
+                    }else if( d_util->isConstArg( tnn, j ) && d_util->isSingularArg( d_util->d_arg_const[tnn][j], parentKind, 0 ) && larg_consider.find( j )!=larg_consider.end() ){
+                      rem = true;
+                      Trace("sygus-nf") << "* Sygus norm : LHS singularity arg " << dt[j].getSygusOp() << " of " << parentKind;
+                      Trace("sygus-nf") << " : do not consider " << dto[i].getSygusOp() << " as second arg." << std::endl;
+                    }else{
+                      if( parentKind!=UNDEFINED_KIND ){
+                        //&& dto[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){
+                        std::map< TypeNode, int > var_count;
+                        std::map< int, Node > pre;
+                        Node g1 = d_util->mkGeneric( dt, j, var_count, pre );
+                        Node g2 = d_util->mkGeneric( dto, i, var_count, pre );
+                        Node g = NodeManager::currentNM()->mkNode( parentKind, g1, g2 );
+                        if( isGenericRedundant( tnnp, g ) ){
+                          rem = true;
                         }
                       }
-                      if( rem ){
-                        rem_arg[j] = true;
-                      }else{
-                        argConsider = true;
-                        larg_consider[j] = true;
-                      }
                     }
-                  }
-                  if( !rem_arg.empty() ){
-                    d_sygus_pc_arg_pos[tnno][csIndex][i].clear();
-                    Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dto[i].getName() << " : " << std::endl;
-                    for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-                      if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
-                        d_sygus_pc_arg_pos[tnno][csIndex][i].push_back( j );
-                        Trace("sygus-split-debug") << "  " << dt[j].getName() << std::endl;
-                      }
+                    if( rem ){
+                      rem_arg[j] = true;
+                    }else{
+                      argConsider = true;
+                      larg_consider[j] = true;
                     }
-                    //if there are no possibilities for first argument, then this child is redundant
-                    if( d_sygus_pc_arg_pos[tnno][csIndex][i].empty() ){
-                      Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dto[i].getName();
-                      Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
-                      d_sygus_pc_nred[tnno][csIndex][osIndex][i] = false;
+                  }
+                }
+                if( !rem_arg.empty() ){
+                  d_sygus_pc_arg_pos[tnno][csIndex][i].clear();
+                  Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dto[i].getName() << " : " << std::endl;
+                  for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+                    if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
+                      d_sygus_pc_arg_pos[tnno][csIndex][i].push_back( j );
+                      Trace("sygus-split-debug") << "  " << dt[j].getName() << std::endl;
                     }
                   }
+                  //if there are no possibilities for first argument, then this child is redundant
+                  if( d_sygus_pc_arg_pos[tnno][csIndex][i].empty() ){
+                    Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dto[i].getName();
+                    Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
+                    d_sygus_pc_nred[tnno][csIndex][osIndex][i] = false;
+                  }
                 }
               }
             }
@@ -430,129 +341,16 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
   }
 }
 
-bool SygusSplit::isAssoc( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
-}
-
-bool SygusSplit::isComm( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
-}
-
-bool SygusSplit::isAntisymmetric( Kind k, Kind& dk ) {
-  if( k==GT ){
-    dk = LT;
-    return true;
-  }else if( k==GEQ ){
-    dk = LEQ;
-    return true;
-  }else if( k==BITVECTOR_UGT ){
-    dk = BITVECTOR_ULT;
-    return true;
-  }else if( k==BITVECTOR_UGE ){
-    dk = BITVECTOR_ULE;
-    return true;
-  }else if( k==BITVECTOR_SGT ){
-    dk = BITVECTOR_SLT;
-    return true;
-  }else if( k==BITVECTOR_SGE ){
-    dk = BITVECTOR_SLE;
-    return true;
-  }else{
-    return false;
-  }
-}
-
-bool SygusSplit::isIdempotentArg( Node n, Kind ik, int arg ) {
-  TypeNode tn = n.getType();
-  if( n==getTypeValue( tn, 0 ) ){
-    if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){
-      return true;
-    }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){
-      return arg==1;
-    }
-  }else if( n==getTypeValue( tn, 1 ) ){
-    if( ik==MULT || ik==BITVECTOR_MULT ){
-      return true;
-    }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
-      return arg==1;
-    }
-  }else if( n==getTypeMaxValue( tn ) ){
-    if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
-      return true;
-    }
-  }
-  return false;
-}
-
-
-bool SygusSplit::isSingularArg( Node n, Kind ik, int arg ) {
-  TypeNode tn = n.getType();
-  if( n==getTypeValue( tn, 0 ) ){
-    if( ik==AND || ik==MULT || ik==BITVECTOR_AND || ik==BITVECTOR_MULT ){
-      return true;
-    }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
-      return arg==0;
-    }
-  }else if( n==getTypeMaxValue( tn ) ){
-    if( ik==OR || ik==BITVECTOR_OR ){
-      return true;
-    }
-  }
-  return false;
-}
-
-
-Node SygusSplit::getTypeValue( TypeNode tn, int val ) {
-  std::map< int, Node >::iterator it = d_type_value[tn].find( val );
-  if( it==d_type_value[tn].end() ){
-    Node n;
-    if( tn.isInteger() || tn.isReal() ){
-      Rational c(val);
-      n = NodeManager::currentNM()->mkConst( c );
-    }else if( tn.isBitVector() ){
-      unsigned int uv = val;
-      BitVector bval(tn.getConst<BitVectorSize>(), uv);
-      n = NodeManager::currentNM()->mkConst<BitVector>(bval);
-    }else if( tn.isBoolean() ){
-      if( val==0 ){
-        n = NodeManager::currentNM()->mkConst( false );
-      }
-    }
-    d_type_value[tn][val] = n;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
-Node SygusSplit::getTypeMaxValue( TypeNode tn ) {
-  std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn );
-  if( it==d_type_max_value.end() ){
-    Node n;
-    if( tn.isBitVector() ){
-      n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
-    }else if( tn.isBoolean() ){
-      n = NodeManager::currentNM()->mkConst( true );
-    }
-    d_type_max_value[tn] = n;
-    return n;
-  }else{
-    return it->second;
-  }
-}
-
 //this function gets all easy redundant cases, before consulting rewriters
 bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) {
-  Assert( hasKind( tn, k ) );
-  Assert( hasKind( tnp, parent ) );
+  Assert( d_util->hasKind( tn, k ) );
+  Assert( d_util->hasKind( tnp, parent ) );
   Trace("sygus-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
-  int c = getKindArg( tn, k );
-  int pc = getKindArg( tnp, parent );
+  int c = d_util->getKindArg( tn, k );
+  int pc = d_util->getKindArg( tnp, parent );
   if( k==parent ){
     //check for associativity
-    if( isAssoc( k ) ){
+    if( d_util->isAssoc( k ) ){
       //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
       int firstArg = getFirstArgOccurrence( pdt[pc], dt );
       Assert( firstArg!=-1 );
@@ -607,7 +405,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
         Trace("sygus-split-debug") << ", reqk = " << reqk;
       }
       Trace("sygus-split-debug") << "?" << std::endl;
-      int pcr = getKindArg( tnp, nk );
+      int pcr = d_util->getKindArg( tnp, nk );
       if( pcr!=-1 ){
         Assert( pcr<(int)pdt.getNumConstructors() );
         //must have same number of arguments
@@ -619,7 +417,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
             Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) );
             if( reqk!=UNDEFINED_KIND ){
               //child must have a NOT
-              int nindex = getKindArg( tna, reqk );
+              int nindex = d_util->getKindArg( tna, reqk );
               if( nindex!=-1 ){
                 const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype();
                 childTypes[i] = getArgType( adt[nindex], 0 );
@@ -662,11 +460,11 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
 
 //this function gets all easy redundant cases, before consulting rewriters
 bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg ) {
-  Assert( hasConst( tn, c ) );
-  Assert( hasKind( tnp, parent ) );
-  int pc = getKindArg( tnp, parent );
+  Assert( d_util->hasConst( tn, c ) );
+  Assert( d_util->hasKind( tnp, parent ) );
+  int pc = d_util->getKindArg( tnp, parent );
   Trace("sygus-split") << "Consider sygus split const " << c << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
-  if( isIdempotentArg( c, parent, arg ) ){
+  if( d_util->isIdempotentArg( c, parent, arg ) ){
     Trace("sygus-split-debug") << "  " << c << " is idempotent arg " << arg << " of " << parent << "..." << std::endl;
     if( pdt[pc].getNumArgs()==2 ){
       int oarg = arg==0 ? 1 : 0;
@@ -675,9 +473,9 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd
         return false;
       }
     }
-  }else if( isSingularArg( c, parent, arg ) ){
+  }else if( d_util->isSingularArg( c, parent, arg ) ){
     Trace("sygus-split-debug") << "  " << c << " is singular arg " << arg << " of " << parent << "..." << std::endl;
-    if( hasConst( tnp, c ) ){
+    if( d_util->hasConst( tnp, c ) ){
       return false;
     }
   }
@@ -714,11 +512,7 @@ bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
   std::map< Node, bool >::iterator it = d_gen_redundant[tn].find( g );
   if( it==d_gen_redundant[tn].end() ){
     Trace("sygus-gnf") << "Register generic for " << tn << " : " << g << std::endl;
-    Node gr = Rewriter::rewrite( g );
-    //replace variables in order left to right
-    std::map< TypeNode, int > var_count;
-    std::map< Node, Node > subs;
-    gr = d_util->getSygusNormalized( gr, var_count, subs );
+    Node gr = d_util->getNormalized( tn, g, false );
     Trace("sygus-gnf-debug") << "Generic " << g << " rewrites to " << gr << std::endl;
     std::map< Node, Node >::iterator itg = d_gen_terms[tn].find( gr );
     bool red = true;
@@ -839,10 +633,11 @@ bool SygusSymBreak::ProgSearch::processProgramDepth( int depth ){
       Trace("sygus-sym-break-debug") << "Program is set for depth " << depth << std::endl;
       std::map< TypeNode, int > var_count;
       std::vector< Node > testers;
+      std::map< Node, std::vector< Node > > testers_u;
       //now have entire information about candidate program at given depth
-      Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers );
+      Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, Node::null(), var_count, testers, testers_u );
       if( !prog.isNull() ){
-        if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers ) ){
+        if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers, testers_u ) ){
           return false;
         }
       }else{
@@ -862,10 +657,11 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept
     Assert( n.getKind()==APPLY_SELECTOR_TOTAL );
     std::map< TypeNode, int > var_count;
     std::vector< Node > testers;
+    std::map< Node, std::vector< Node > > testers_u;
     //now have entire information about candidate program at given depth
-    Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, var_count, testers );
+    Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, Node::null(), var_count, testers, testers_u );
     if( !prog.isNull() ){
-      if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers ) ){
+      if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers, testers_u ) ){
         return false;
       }
       //also try higher levels
@@ -877,13 +673,15 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept
   return true;
 }
 
-Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) {
+Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count,
+                                                            std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
   Assert( depth>=curr_depth );
   Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
   NodeMap::const_iterator it = d_testers.find( prog );
   if( it!=d_testers.end() ){
     Node tst = (*it).second;
     testers.push_back( tst );
+    testers_u[parent].push_back( tst );
     Assert( tst[0]==prog );
     int tindex = Datatype::indexOf( tst.getOperator().toExpr() );
     TypeNode tn = prog.getType();
@@ -893,7 +691,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog
     if( curr_depth<depth ){
       for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
         Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog );
-        pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers );
+        pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, prog, var_count, testers, testers_u );
         if( pre[i].isNull() ){
           return Node::null();
         }
@@ -906,39 +704,164 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog
   }
 }
 
-bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ) {
-  std::map< Node, Node >::iterator it = d_normalized[at].find( prog );
-  if( it==d_normalized[at].end() ){
+bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog,
+                                           std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
+  Assert( a.getType()==at );
+  std::map< Node, bool >::iterator it = d_redundant[at].find( prog );
+  bool red;
+  if( it==d_redundant[at].end() ){
     Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl;
-    Node progr = Rewriter::rewrite( prog );
-    std::map< TypeNode, int > var_count;
-    std::map< Node, Node > subs;
-    progr = d_util->getSygusNormalized( progr, var_count, subs );
-    Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
-    d_normalized[at][prog] = progr;
+    Node progr = d_util->getNormalized( at, prog );
     std::map< Node, Node >::iterator it = d_normalized_to_orig[at].find( progr );
     if( it==d_normalized_to_orig[at].end() ){
       d_normalized_to_orig[at][progr] = prog;
-      d_redundant[at][prog] = false;
+      if( progr.getKind()==SKOLEM && d_util->getSygusType( progr )==at ){
+        Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl;
+        d_redundant[at][prog] = true;
+        red = true;
+      }else{
+        d_redundant[at][prog] = false;
+        red = false;
+      }
     }else{
       d_redundant[at][prog] = true;
-      Assert( !testers.empty() );
+      red = true;
       Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl;
     }
+    if( red ){
+      Assert( !testers.empty() );
+      Assert( prog!=it->second );
+      bool conflict_gen_set = false;
+      if( options::sygusNormalFormGlobalGen() ){
+        //generalize conflict
+        if( prog.getNumChildren()>0 ){
+          Assert( !testers.empty() );
+          d_util->registerSygusType( at );
+          //Trace("sygus-nf-gen-debug") << "Testers are : " << std::endl;
+          //for( unsigned i=0; i<testers.size(); i++ ){
+          //  Trace("sygus-nf-gen-debug") << "* " << testers[i] << std::endl;
+          //}
+          Trace("sygus-nf-gen-debug2") << "Tester tree is : " << std::endl;
+          for( std::map< Node, std::vector< Node > >::iterator it = testers_u.begin(); it != testers_u.end(); ++it ){
+            Trace("sygus-nf-gen-debug2") << "  " << it->first << " -> " << std::endl;
+            for( unsigned i=0; i<it->second.size(); i++ ){
+              Trace("sygus-nf-gen-debug2") << "    " << it->second[i] << std::endl;
+            }
+          }
+          Trace("sygus-nf-gen-debug2") << std::endl;
+          Assert( testers[0][0]==a );
+          Assert( prog.getNumChildren()==testers_u[a].size() );
+          //get the normal form for each child
+          Kind parentKind = prog.getKind();
+          Kind parentOpKind = prog.getOperator().getKind();
+          Trace("sygus-nf-gen-debug") << "Parent kind is " << parentKind << " " << parentOpKind << std::endl;
+          std::map< int, Node > norm_children;
+          std::map< int, bool > rlv;
+          for( unsigned i=0; i<testers_u[a].size(); i++ ){
+            TypeNode tn = testers_u[a][i][0].getType();
+            norm_children[i] = d_util->getNormalized( tn, prog[i], true );
+            rlv[i] = true;
+            Trace("sygus-nf-gen") << "- child " << i << " normalizes to " << norm_children[i] << std::endl;
+          }
+          //now, determine a minimal subset of the arguments that the rewriting depended on
+          if( testers_u[a].size()>1 ){
+            const Datatype & pdt = ((DatatypeType)(at).toType()).getDatatype();
+            int pc = Datatype::indexOf( testers[0].getOperator().toExpr() );
+            //quick checks based on constants
+            for( std::map< int, Node >::iterator it = norm_children.begin(); it != norm_children.end(); ++it ){
+              if( it->second.isConst() ){
+                if( parentOpKind==kind::BUILTIN ){
+                  Trace("sygus-nf-gen") << "-- constant arg " << it->first << " under builtin operator." << std::endl;
+                  if( !processConstantArg( at, pdt, pc, parentKind, it->first, it->second, rlv ) ){
+                    for( std::map< int, bool >::iterator itr = rlv.begin(); itr != rlv.end(); ++itr ){
+                      if( itr->first!=it->first ){
+                        rlv[itr->first] = false;
+                      }
+                    }
+                    break;
+                  }
+                }
+              }
+            }
+            //relevant testers : root + recursive collection of relevant children
+            Trace("sygus-nf-gen-debug") << "Collect relevant testers..." << std::endl;
+            std::vector< Node > rlv_testers;
+            rlv_testers.push_back( testers[0] );
+            for( unsigned i=0; i<testers_u[a].size(); i++ ){
+              if( rlv[i] ){
+                collectTesters( testers_u[a][i], testers_u, rlv_testers );
+              }else{
+                Trace("sygus-nf") << "  - argument " << i << " is not relevant." << std::endl;
+              }
+            }
+            Trace("sygus-nf-gen-debug") << "Relevant testers : " << std::endl;
+            conflict_gen_set = true;
+            for( unsigned i=0; i<testers.size(); i++ ){
+              bool rl = std::find( rlv_testers.begin(), rlv_testers.end(), testers[i] )!=rlv_testers.end();
+              Trace("sygus-nf-gen-debug") << "* " << testers[i] << " -> " << rl << std::endl;
+              d_conflict_gen[at][prog].push_back( rl );
+            }
+          }
+        }
+      }
+      if( !conflict_gen_set ){
+        for( unsigned i=0; i<testers.size(); i++ ){
+          d_conflict_gen[at][prog].push_back( true );
+        }
+      }
+    }
+  }else{
+    red = it->second;
   }
-  Assert( d_redundant[at].find( prog )!=d_redundant[at].end() );
-  if( d_redundant[at][prog] ){
-    d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers );
+  if( red ){
+    Assert( d_conflict_gen[at][prog].size()==testers.size() );
+    std::vector< Node > gtesters;
+    for( unsigned i=0; i<testers.size(); i++ ){
+      if( d_conflict_gen[at][prog][i] ){
+        gtesters.push_back( testers[i] );
+      }
+    }
+    d_util->d_conflictNode = gtesters.size()==1 ? gtesters[0] : NodeManager::currentNM()->mkNode( AND, gtesters );
     Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl;
     d_util->d_conflict = true;
-    d_redundant[at][prog] = true;
-    // TODO : generalize conflict
     return false;
   }else{
     return true;
   }
 }
 
+bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc,
+                                        Kind k, int i, Node arg, std::map< int, bool >& rlv ) {
+  Assert( d_util->hasKind( tnp, k ) );
+  if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){
+    return false;
+  }else if( d_util->isIdempotentArg( arg, k, i ) ){
+    if( pdt[pc].getNumArgs()==2 ){
+      int oi = i==0 ? 1 : 0;
+      TypeNode otn = TypeNode::fromType( ((SelectorType)pdt[pc][oi].getType()).getRangeType() );
+      if( otn==tnp ){
+        return false;
+      }
+    }
+  }else if( d_util->isSingularArg( arg, k, i ) ){
+    if( d_util->hasConst( tnp, arg ) ){
+      return false;
+    }
+  }
+  TypeNode tn = arg.getType();
+  return true;
+}
+
+void SygusSymBreak::collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers ) {
+  testers.push_back( tst );
+  std::map< Node, std::vector< Node > >::iterator it = testers_u.find( tst[0] );
+  if( it!=testers_u.end() ){
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      collectTesters( it->second[i], testers_u, testers );
+    }
+  }
+}
+
 SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) {
   d_split = new SygusSplit( this );
   d_sym_break = new SygusSymBreak( this, c );
@@ -977,6 +900,11 @@ Node SygusUtil::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ) {
   }
 }
 
+TypeNode SygusUtil::getSygusType( Node v ) {
+  Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
+  return d_fv_stype[v];
+}
+
 Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ) {
   Assert( c>=0 && c<(int)dt.getNumConstructors() );
   Assert( dt.isSygus() );
@@ -1004,11 +932,14 @@ Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >&
     if( children.size()==1 ){
       return children[0];
     }else{
+      return NodeManager::currentNM()->mkNode( APPLY, children );
+      /*
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
       Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
       Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
       return ne;
+      */
     }
   }
 }
@@ -1048,3 +979,244 @@ Node SygusUtil::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count
     return n;
   }
 }
+
+Node SygusUtil::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
+  if( do_pre_norm ){
+    std::map< TypeNode, int > var_count;
+    std::map< Node, Node > subs;
+    prog = getSygusNormalized( prog, var_count, subs );
+  }
+  std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
+  if( itn==d_normalized[t].end() ){
+    Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
+    progr = Rewriter::rewrite( progr );
+    std::map< TypeNode, int > var_count;
+    std::map< Node, Node > subs;
+    progr = getSygusNormalized( progr, var_count, subs );
+    Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
+    d_normalized[t][prog] = progr;
+    return progr;
+  }else{
+    return itn->second;
+  }
+}
+
+
+bool SygusUtil::isAssoc( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
+}
+
+bool SygusUtil::isComm( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+}
+
+bool SygusUtil::isAntisymmetric( Kind k, Kind& dk ) {
+  if( k==GT ){
+    dk = LT;
+    return true;
+  }else if( k==GEQ ){
+    dk = LEQ;
+    return true;
+  }else if( k==BITVECTOR_UGT ){
+    dk = BITVECTOR_ULT;
+    return true;
+  }else if( k==BITVECTOR_UGE ){
+    dk = BITVECTOR_ULE;
+    return true;
+  }else if( k==BITVECTOR_SGT ){
+    dk = BITVECTOR_SLT;
+    return true;
+  }else if( k==BITVECTOR_SGE ){
+    dk = BITVECTOR_SLE;
+    return true;
+  }else{
+    return false;
+  }
+}
+
+bool SygusUtil::isIdempotentArg( Node n, Kind ik, int arg ) {
+  TypeNode tn = n.getType();
+  if( n==getTypeValue( tn, 0 ) ){
+    if( ik==PLUS || ik==OR || ik==XOR || ik==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==BITVECTOR_XOR ){
+      return true;
+    }else if( ik==MINUS || ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR || ik==BITVECTOR_SUB ){
+      return arg==1;
+    }
+  }else if( n==getTypeValue( tn, 1 ) ){
+    if( ik==MULT || ik==BITVECTOR_MULT ){
+      return true;
+    }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
+      return arg==1;
+    }
+  }else if( n==getTypeMaxValue( tn ) ){
+    if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){
+      return true;
+    }
+  }
+  return false;
+}
+
+
+bool SygusUtil::isSingularArg( Node n, Kind ik, int arg ) {
+  TypeNode tn = n.getType();
+  if( n==getTypeValue( tn, 0 ) ){
+    if( ik==AND || ik==MULT || ik==BITVECTOR_AND || ik==BITVECTOR_MULT ){
+      return true;
+    }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
+      return arg==0;
+    }
+  }else if( n==getTypeMaxValue( tn ) ){
+    if( ik==OR || ik==BITVECTOR_OR ){
+      return true;
+    }
+  }
+  return false;
+}
+
+
+Node SygusUtil::getTypeValue( TypeNode tn, int val ) {
+  std::map< int, Node >::iterator it = d_type_value[tn].find( val );
+  if( it==d_type_value[tn].end() ){
+    Node n;
+    if( tn.isInteger() || tn.isReal() ){
+      Rational c(val);
+      n = NodeManager::currentNM()->mkConst( c );
+    }else if( tn.isBitVector() ){
+      unsigned int uv = val;
+      BitVector bval(tn.getConst<BitVectorSize>(), uv);
+      n = NodeManager::currentNM()->mkConst<BitVector>(bval);
+    }else if( tn.isBoolean() ){
+      if( val==0 ){
+        n = NodeManager::currentNM()->mkConst( false );
+      }
+    }
+    d_type_value[tn][val] = n;
+    return n;
+  }else{
+    return it->second;
+  }
+}
+
+Node SygusUtil::getTypeMaxValue( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator it = d_type_max_value.find( tn );
+  if( it==d_type_max_value.end() ){
+    Node n;
+    if( tn.isBitVector() ){
+      n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
+    }else if( tn.isBoolean() ){
+      n = NodeManager::currentNM()->mkConst( true );
+    }
+    d_type_max_value[tn] = n;
+    return n;
+  }else{
+    return it->second;
+  }
+}
+
+void SygusUtil::registerSygusType( TypeNode tn ){
+  if( d_register.find( tn )==d_register.end() ){
+    if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+      d_register[tn] = TypeNode::null();
+    }else{
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+      d_register[tn] = TypeNode::fromType( dt.getSygusType() );
+      if( d_register[tn].isNull() ){
+        Trace("sygus-util") << "...not sygus." << std::endl;
+      }else{
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          Expr sop = dt[i].getSygusOp();
+          Assert( !sop.isNull() );
+          Node n = Node::fromExpr( sop );
+          Trace("sygus-util") << "  Operator #" << i << " : " << sop;
+          if( sop.getKind() == kind::BUILTIN ){
+            Kind sk = NodeManager::operatorToKind( n );
+            Trace("sygus-util") << ", kind = " << sk;
+            d_kinds[tn][sk] = i;
+            d_arg_kind[tn][i] = sk;
+          }else if( sop.isConst() ){
+            Trace("sygus-util") << ", constant";
+            d_consts[tn][n] = i;
+            d_arg_const[tn][i] = n;
+          }
+          d_ops[tn][n] = i;
+          Trace("sygus-util") << std::endl;
+        }
+      }
+    }
+  }
+}
+
+bool SygusUtil::isRegistered( TypeNode tn ) {
+  return d_register.find( tn )!=d_register.end();
+}
+
+int SygusUtil::getKindArg( TypeNode tn, Kind k ) {
+  Assert( isRegistered( tn ) );
+  std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
+  if( itt!=d_kinds.end() ){
+    std::map< Kind, int >::iterator it = itt->second.find( k );
+    if( it!=itt->second.end() ){
+      return it->second;
+    }
+  }
+  return -1;
+}
+
+int SygusUtil::getConstArg( TypeNode tn, Node n ){
+  Assert( isRegistered( tn ) );
+  std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
+  if( itt!=d_consts.end() ){
+    std::map< Node, int >::iterator it = itt->second.find( n );
+    if( it!=itt->second.end() ){
+      return it->second;
+    }
+  }
+  return -1;
+}
+
+int SygusUtil::getOpArg( TypeNode tn, Node n ) {
+  std::map< Node, int >::iterator it = d_ops[tn].find( n );
+  if( it!=d_ops[tn].end() ){
+    return it->second;
+  }else{
+    return -1;
+  }
+}
+
+bool SygusUtil::hasKind( TypeNode tn, Kind k ) {
+  return getKindArg( tn, k )!=-1;
+}
+bool SygusUtil::hasConst( TypeNode tn, Node n ) {
+  return getConstArg( tn, n )!=-1;
+}
+bool SygusUtil::hasOp( TypeNode tn, Node n ) {
+  return getOpArg( tn, n )!=-1;
+}
+
+bool SygusUtil::isKindArg( TypeNode tn, int i ) {
+  Assert( isRegistered( tn ) );
+  std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
+  if( itt!=d_arg_kind.end() ){
+    return itt->second.find( i )!=itt->second.end();
+  }else{
+    return false;
+  }
+}
+
+bool SygusUtil::isConstArg( TypeNode tn, int i ) {
+  Assert( isRegistered( tn ) );
+  std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
+  if( itt!=d_arg_const.end() ){
+    return itt->second.find( i )!=itt->second.end();
+  }else{
+    return false;
+  }
+}
+
+
+
+
+
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index cf43b0a31..f30a0fd0a 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -42,16 +42,7 @@ private:
   std::map< TypeNode, std::vector< bool > > d_sygus_nred;
   std::map< TypeNode, std::map< int, std::map< int, std::vector< bool > > > > d_sygus_pc_nred;
   std::map< TypeNode, std::map< int, std::map< int, std::vector< int > > > > d_sygus_pc_arg_pos;
-  //information for builtin types
-  std::map< TypeNode, std::map< int, Node > > d_type_value;
-  std::map< TypeNode, Node > d_type_max_value;
-  //information for sygus types
   std::map< TypeNode, TypeNode > d_register;  //stores sygus type
-  std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
-  std::map< TypeNode, std::map< Kind, int > > d_kinds;
-  std::map< TypeNode, std::map< int, Node > > d_arg_const;
-  std::map< TypeNode, std::map< Node, int > > d_consts;
-  std::map< TypeNode, std::map< Node, int > > d_ops;
   // type to (rewritten) to original
   std::map< TypeNode, std::map< Node, Node > > d_gen_terms;
   std::map< TypeNode, std::map< Node, bool > > d_gen_redundant;
@@ -76,20 +67,6 @@ private:
   /** consider sygus split */
   bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg );
   bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Node c, Kind parent, int arg );
-  /** is assoc */
-  bool isAssoc( Kind k );
-  /** is comm */
-  bool isComm( Kind k );
-  /** isAntisymmetric */
-  bool isAntisymmetric( Kind k, Kind& dk );
-  /** is idempotent arg */
-  bool isIdempotentArg( Node n, Kind ik, int arg );
-  /** is singular arg */
-  bool isSingularArg( Node n, Kind ik, int arg );
-  /** get value */
-  Node getTypeValue( TypeNode tn, int val );
-  /** get value */
-  Node getTypeMaxValue( TypeNode tn );
   /** get first occurrence */
   int getFirstArgOccurrence( const DatatypeConstructor& c, const Datatype& dt );
   /** is arg datatype */
@@ -119,12 +96,13 @@ private:
     typedef context::CDHashMap< int, int > IntIntMap;
   private:
     SygusSymBreak * d_parent;
-    Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers );
+    Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count,
+                                     std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u );
     bool processProgramDepth( int depth );
     bool processSubprograms( Node n, int depth, int odepth );
     bool assignTester( Node tst, int depth );
   public:
-    ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) : 
+    ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) :
       d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) {
       d_anchor_type = d_anchor.getType();
     }
@@ -137,11 +115,14 @@ private:
     void addTester( Node tst );
   };
   std::map< Node, ProgSearch * > d_prog_search;
-  std::map< TypeNode, std::map< Node, Node > > d_normalized;
   std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig;
   std::map< TypeNode, std::map< Node, bool > > d_redundant;
+  std::map< TypeNode, std::map< Node, std::vector< bool > > > d_conflict_gen;
   Node getAnchor( Node n );
-  bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers );
+  bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog,
+                              std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u );
+  bool processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, Kind k, int i, Node arg, std::map< int, bool >& rlv );
+  void collectTesters( Node tst, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& testers );
 public:
   SygusSymBreak( SygusUtil * util, context::Context* c );
   /** add tester */
@@ -157,11 +138,51 @@ private:
   std::map< Node, TypeNode > d_fv_stype;
   SygusSplit * d_split;
   SygusSymBreak * d_sym_break;
+  std::map< TypeNode, std::map< Node, Node > > d_normalized;
+private:
+  //information for sygus types
+  std::map< TypeNode, TypeNode > d_register;  //stores sygus type
+  std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
+  std::map< TypeNode, std::map< Kind, int > > d_kinds;
+  std::map< TypeNode, std::map< int, Node > > d_arg_const;
+  std::map< TypeNode, std::map< Node, int > > d_consts;
+  std::map< TypeNode, std::map< Node, int > > d_ops;
+private:
+  bool isRegistered( TypeNode tn );
+  int getKindArg( TypeNode tn, Kind k );
+  int getConstArg( TypeNode tn, Node n );
+  int getOpArg( TypeNode tn, Node n );
+  bool hasKind( TypeNode tn, Kind k );
+  bool hasConst( TypeNode tn, Node n );
+  bool hasOp( TypeNode tn, Node n );
+  bool isKindArg( TypeNode tn, int i );
+  bool isConstArg( TypeNode tn, int i );
+  void registerSygusType( TypeNode tn );
+private:
+  //information for builtin types
+  std::map< TypeNode, std::map< int, Node > > d_type_value;
+  std::map< TypeNode, Node > d_type_max_value;
+  /** is assoc */
+  bool isAssoc( Kind k );
+  /** is comm */
+  bool isComm( Kind k );
+  /** isAntisymmetric */
+  bool isAntisymmetric( Kind k, Kind& dk );
+  /** is idempotent arg */
+  bool isIdempotentArg( Node n, Kind ik, int arg );
+  /** is singular arg */
+  bool isSingularArg( Node n, Kind ik, int arg );
+  /** get value */
+  Node getTypeValue( TypeNode tn, int val );
+  /** get value */
+  Node getTypeMaxValue( TypeNode tn );
 private:
   Node getVar( TypeNode tn, int i );
   Node getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count );
+  TypeNode getSygusType( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
+  Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false );
 public:
   SygusUtil( context::Context* c );
   SygusSplit * getSplit() { return d_split; }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 264158ed4..42d06cdb5 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -368,10 +368,13 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
     if( !d_conflict && polarity ){
       Trace("dt-tester") << "Assert tester : " << atom << std::endl;
       if( d_sygus_util ){
+        Assert( !d_sygus_util->d_conflict );
         d_sygus_util->getSymBreak()->addTester( atom );
         if( d_sygus_util->d_conflict ){
           d_conflict = true;
-          d_conflictNode = d_sygus_util->d_conflictNode;
+          std::vector< TNode > assumptions;
+          explain( d_sygus_util->d_conflictNode, assumptions );
+          d_conflictNode = mkAnd( assumptions );
           Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl;
           d_out->conflict( d_conflictNode );
           return;
@@ -599,8 +602,17 @@ bool TheoryDatatypes::propagate(TNode literal){
 
 void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) {
   for( unsigned i=0; i<tassumptions.size(); i++ ){
-    if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
-      assumptions.push_back( tassumptions[i] );
+    //flatten AND
+    if( tassumptions[i].getKind()==AND ){
+      for( unsigned j=0; j<tassumptions[i].getNumChildren(); j++ ){
+        if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i][j] )==assumptions.end() ){
+          assumptions.push_back( tassumptions[i][j] );
+        }
+      }
+    }else{
+      if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
+        assumptions.push_back( tassumptions[i] );
+      }
     }
   }
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index a034bb8c1..f9b7c4fdc 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -139,6 +139,7 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
         invc.push_back( prog );
         Node pv = NodeManager::currentNM()->mkBoundVar( "F", inv.getType() );
         d_single_inv_map[prog] = pv;
+        d_single_inv_map_to_prog[pv] = prog;
         pbvs.push_back( pv );
         Trace("cegqi-analyze-debug2") << "Make variable " << pv << " for " << prog << std::endl;
         for( unsigned k=1; k<inv.getNumChildren(); k++ ){
@@ -176,9 +177,9 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
       //std::vector< Node > si_conj;
       Assert( !pbvs.empty() );
       Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
-      Node si;
       for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
-        Assert( si.isNull() );
+        //should hold since we prevent miniscoping
+        Assert( d_single_inv.isNull() );
         std::vector< Node > tmp;
         for( unsigned i=0; i<it->second.size(); i++ ){
           Node c = it->second[i];
@@ -237,15 +238,54 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() {
           
           Trace("cegqi-analyze-debug") << "    -> " << bd << std::endl;
         }
-        si = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+        d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+        //equality resolution
+        for( unsigned j=0; j<tmp.size(); j++ ){
+          Node conj = tmp[j];
+          std::map< Node, std::vector< Node > > case_vals;
+          bool exh = processSingleInvLiteral( conj, false, case_vals );
+          Trace("cegqi-analyze-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
+          for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
+            Trace("cegqi-analyze-er") << "  " << it->first << " -> ";
+            for( unsigned k=0; k<it->second.size(); k++ ){
+              Trace("cegqi-analyze-er") << it->second[k] << " ";
+            }
+            Trace("cegqi-analyze-er") << std::endl;
+          }
+
+        }
       }
-      Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl;
-      d_single_inv = si;
+      Trace("cegqi-analyze-debug") << "...formula is : " << d_single_inv << std::endl;
     }else{
       Trace("cegqi-analyze") << "Property is not single invocation." << std::endl;
     }
   }
 }
+
+bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
+  if( lit.getKind()==NOT ){
+    return processSingleInvLiteral( lit[0], !pol, case_vals );
+  }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
+    bool exh = true;
+    for( unsigned k=0; k<lit.getNumChildren(); k++ ){
+      exh = exh && processSingleInvLiteral( lit[k], pol, case_vals );
+    }
+    return exh;
+  }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+    if( pol ){
+      for( unsigned r=0; r<2; r++ ){
+        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[0] );
+        if( it!=d_single_inv_map_to_prog.end() ){
+          if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
+            case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
+            return true;
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
   
 bool CegInstantiation::CegConjecture::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
                                                             std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, 
@@ -615,7 +655,13 @@ bool CegInstantiation::getModelValues( CegConjecture * conj, std::vector< Node >
   for( unsigned i=0; i<n.size(); i++ ){
     Node nv = getModelValue( n[i] );
     v.push_back( nv );
-    Trace("cegqi-engine") << n[i] << " -> " << nv << " ";
+    if( Trace.isOn("cegqi-engine") ){
+      TypeNode tn = nv.getType();
+      Trace("cegqi-engine") << n[i] << " -> ";
+      std::stringstream ss;
+      printSygusTerm( ss, nv );
+      Trace("cegqi-engine") << ss.str() << " ";
+    }
     if( nv.isNull() ){
       success = false;
     }
@@ -752,7 +798,7 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
       return;
     }
   }
-  out << n << std::endl;
+  out << n;
 }
 
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index ad94b51a5..aa553fb58 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -78,10 +78,12 @@ private:
                               std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, 
                               std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol );
     bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains );
+    bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
   public:
     Node d_single_inv;
     //map from programs to variables in single invocation property
     std::map< Node, Node > d_single_inv_map;
+    std::map< Node, Node > d_single_inv_map_to_prog;
     //map from programs to evaluator term representing the above variable
     std::map< Node, Node > d_single_inv_app_map;
     //list of skolems for each argument of programs
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 9d4281186..4a093b617 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -204,6 +204,8 @@ option sygusNormalFormArg --sygus-nf-arg bool :default true
   account for relationship between arguments of operations in sygus normal form
 option sygusNormalFormGlobal --sygus-nf-global bool :default true
   narrow sygus search space based on global state of current candidate program
+option sygusNormalFormGlobalGen --sygus-nf-global-gen bool :default true
+  generalize conflict lemmas for global search space narrowing
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions