From e908abc0e8a7a7d61a4d6e25821042a8e860e873 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 21 Jan 2015 11:34:55 +0100
Subject: [PATCH] Initial work on sygusNormalForm.

---
 src/Makefile.am                           |   2 +
 src/parser/smt2/smt2.cpp                  |   2 -
 src/theory/datatypes/datatypes_sygus.cpp  | 309 ++++++++++++++++++++++
 src/theory/datatypes/datatypes_sygus.h    |  69 +++++
 src/theory/datatypes/theory_datatypes.cpp |  49 +---
 src/theory/datatypes/theory_datatypes.h   |  38 ++-
 src/theory/quantifiers/options            |   2 -
 src/util/datatype.cpp                     |   4 +
 src/util/datatype.h                       |   3 +
 9 files changed, 429 insertions(+), 49 deletions(-)
 create mode 100644 src/theory/datatypes/datatypes_sygus.cpp
 create mode 100644 src/theory/datatypes/datatypes_sygus.h

diff --git a/src/Makefile.am b/src/Makefile.am
index e66d590dc..c72e11809 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -235,6 +235,8 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/theory_datatypes.h \
 	theory/datatypes/datatypes_rewriter.h \
 	theory/datatypes/theory_datatypes.cpp \
+	theory/datatypes/datatypes_sygus.h \
+	theory/datatypes/datatypes_sygus.cpp \
 	theory/sets/expr_patterns.h \
 	theory/sets/normal_form.h \
 	theory/sets/options_handlers.h \
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c6c3a896c..3db2e252d 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -526,8 +526,6 @@ void Smt2::includeFile(const std::string& filename) {
 
 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs ) {
-  //minimize grammar goes here
-
   for( unsigned i=0; i<cnames.size(); i++ ){
     std::string name = dt.getName() + "_" + cnames[i];
     std::string testerId("is-");
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
new file mode 100644
index 000000000..af855e166
--- /dev/null
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -0,0 +1,309 @@
+/*********************                                                        */
+/*! \file theory_datatypes.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of sygus utilities for theory of datatypes
+ **
+ ** Implementation of sygus utilities for theory of datatypes
+ **/
+
+
+#include "theory/datatypes/datatypes_sygus.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "expr/node_manager.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::datatypes;
+
+void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) {
+  Assert( dt.isSygus() );
+  Trace("sygus-split") << "Get sygus splits " << n << std::endl;
+  TypeNode typ, ptyp;
+  std::map< int, Kind > arg_kind, parg_kind;
+  std::map< Kind, int > kinds, pkinds;
+  std::map< int, Node > arg_const, parg_const;
+  std::map< Node, int > consts, pconsts;
+
+  //get the kinds for child datatype
+  Trace("sygus-split") << "Operations for child : " << std::endl;
+  getSygusKinds( dt, arg_kind, kinds, arg_const, consts );
+  typ = TypeNode::fromType(dt.getSygusType());
+
+  //compute the redundant operators
+  TypeNode tnn = n.getType();
+  if( d_sygus_nred.find( tnn )==d_sygus_nred.end() ){
+    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+      bool nred = true;
+      std::map< int, Kind >::iterator it = arg_kind.find( i );
+      if( it!=arg_kind.end() ){
+        Kind dk;
+        if( isAntisymmetric( it->second, dk ) ){
+          std::map< Kind, int >::iterator ita = kinds.find( dk );
+          if( ita!=kinds.end() ){
+            Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
+            //check for type mismatches
+            bool success = true;
+            unsigned j = ita->second;
+            for( unsigned k=0; k<2; k++ ){
+              unsigned ko = k==0 ? 1 : 0;
+              TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
+              TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
+              if( tni!=tnj ){
+                Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
+                success = false;
+                break;
+              }
+            }
+            if( success ){
+              Trace("sygus-split") << "* Sygus norm " << dt.getName() << " : do not consider any " << arg_kind[i] << " terms." << std::endl;
+              nred = false;
+            }
+          }
+        }
+      }
+      d_sygus_nred[tnn].push_back( nred );
+    }
+  }
+
+
+  //get parent information, if possible
+  Node op;
+  int csIndex;
+  int sIndex;
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    op = n.getOperator();
+    Expr selectorExpr = op.toExpr();
+    const Datatype& pdt = Datatype::datatypeOf(selectorExpr);
+    Assert( pdt.isSygus() );
+    csIndex = Datatype::cindexOf(selectorExpr);
+    sIndex = Datatype::indexOf(selectorExpr);
+
+    std::map< int, std::vector< bool > >::iterator it = d_sygus_pc_nred[op].find( sIndex );
+    if( it==d_sygus_pc_nred[op].end() ){
+      Trace("sygus-split") << "  Constructor, selector index : " << csIndex << " " << sIndex << std::endl;
+
+      Trace("sygus-split") << "Operations for parent : " << std::endl;
+      getSygusKinds( pdt, parg_kind, pkinds, parg_const, pconsts );
+      ptyp = TypeNode::fromType(pdt.getSygusType());
+      bool parentKind = parg_kind.find( csIndex )!=parg_kind.end();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        bool addSplit = d_sygus_nred[tnn][i];
+        if( addSplit && parentKind ){
+          if( arg_kind.find( i )!=arg_kind.end() ){
+            addSplit = considerSygusSplitKind( dt, pdt, arg_kind[i], parg_kind[csIndex], sIndex, kinds, pkinds, consts, pconsts );
+            if( !addSplit ){
+              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << arg_kind[i];
+              Trace("sygus-nf") << " as argument " << sIndex << " of " << arg_kind[csIndex] << "." << std::endl;
+            }
+          }else if( arg_const.find( i )!=arg_const.end() ){
+            addSplit = considerSygusSplitConst( dt, pdt, arg_const[i], parg_kind[csIndex], sIndex, kinds, pkinds, consts, pconsts );
+          }
+        }
+        d_sygus_pc_nred[op][sIndex].push_back( addSplit );
+      }
+    }
+  }
+
+  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+    bool addSplit = d_sygus_nred[tnn][i];
+    if( addSplit ){
+      if( !op.isNull() ){
+        addSplit = d_sygus_pc_nred[op][sIndex][i];
+      }
+      if( addSplit ){
+        Node test = DatatypesRewriter::mkTester( n, i, dt );
+        splits.push_back( test );
+      }
+    }
+  }
+  Assert( !splits.empty() );
+}
+
+void SygusSplit::getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds,
+                                                    std::map< int, Node >& arg_const, std::map< Node, int >& consts ) {
+  for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+    Expr sop = dt[i].getSygusOp();
+    Assert( !sop.isNull() );
+    Trace("sygus-split") << "  Operator #" << i << " : " << sop;
+    if( sop.getKind() == kind::BUILTIN ){
+      Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) );
+      Trace("sygus-split") << ", kind = " << sk;
+      kinds[sk] = i;
+      arg_kind[i] = sk;
+    }else if( sop.isConst() ){
+      Node n = Node::fromExpr( sop );
+      Trace("sygus-split") << ", constant";
+      consts[n] = i;
+      arg_const[i] = n;
+    }
+    Trace("sygus-split") << std::endl;
+  }
+}
+
+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_CONCAT;
+}
+
+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==BITVECTOR_PLUS || ik==BITVECTOR_OR || ik==OR ){
+      return true;
+    }else if( ik==BITVECTOR_SHL || ik==BITVECTOR_LSHR ){
+      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==BITVECTOR_AND ){
+      return true;
+    }
+  }
+  return false;
+}
+
+
+bool SygusSplit::isSingularArg( Node n, Kind ik, int arg ) {
+  TypeNode tn = n.getType();
+  if( n==getTypeValue( tn, 0 ) ){
+    if( ik==MULT || ik==BITVECTOR_MULT || ik==BITVECTOR_AND || ik==AND ){
+      return true;
+    }else if( ik==DIVISION || ik==BITVECTOR_UDIV || ik==BITVECTOR_SDIV ){
+      return arg==0;
+    }
+  }else if( n==getTypeMaxValue( tn ) ){
+    if( 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 || val==1 ){
+        n = NodeManager::currentNM()->mkConst( val==1 );
+      }
+    }
+    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>());
+    }
+    d_type_max_value[tn] = n;
+    return n;
+  }else{
+    return it->second;
+  }
+}
+bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg,
+                                         std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                                         std::map< Node, int >& consts, std::map< Node, int >& pconsts ) {
+  Assert( kinds.find( k )!=kinds.end() );
+  Assert( pkinds.find( parent )!=pkinds.end() );
+  Trace("sygus-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
+  if( k==parent ){
+    //check for associativity
+    if( isAssoc( k ) ){
+      //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
+      int firstArg = -1;
+      int c = pkinds[k];
+      for( unsigned i=0; i<pdt[c].getNumArgs(); i++ ){
+        TypeNode tni = TypeNode::fromType( ((SelectorType)pdt[c][i].getType()).getRangeType() );
+        if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){
+          const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype();
+          if( adt==dt ){
+            firstArg = i;
+            break;
+          }
+        }
+      }
+      Assert( firstArg!=-1 );
+      Trace("sygus-split-debug") << "Associative, with first arg = " << firstArg << std::endl;
+      return arg==firstArg;
+    }
+  }
+  if( parent==NOT ){
+     //negation normal form
+    /*
+    if( k==NOT || k==ITE || ( k==AND && kinds.find( OR )!=kinds.end() ) || ( k==OR && kinds.find( AND )!=kinds.end() ) ||
+        ( k==IFF && kinds.find( XOR )!=kinds.end() ) || ( k==XOR && kinds.find( IFF )!=kinds.end() ) ){
+      return false;
+    }
+    */
+  }
+  /*
+  if( parent==MINUS ){
+
+  }
+  */
+  return true;
+}
+
+bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg,
+                                               std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                                               std::map< Node, int >& consts, std::map< Node, int >& pconsts ) {
+  Trace("sygus-split") << "Consider sygus split const " << c << ", parent = " << parent << ", arg = " << arg << "?" << std::endl;
+  return true;
+}
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
new file mode 100644
index 000000000..c3491b588
--- /dev/null
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file theory_datatypes.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sygus utilities for theory of datatypes
+ **
+ ** Theory of datatypes.
+ **/
+
+#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H
+#define __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H
+
+#include "expr/node.h"
+#include "util/datatype.h"
+#include <iostream>
+#include <map>
+#include "context/cdchunk_list.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+  
+class SygusSplit
+{
+private:
+  std::map< TypeNode, std::vector< bool > > d_sygus_nred;
+  std::map< Node, std::map< int, std::vector< bool > > > d_sygus_pc_nred;
+  std::map< TypeNode, std::map< int, Node > > d_type_value;
+  std::map< TypeNode, Node > d_type_max_value;
+private:
+  /** consider sygus split */
+  bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg,
+                               std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                               std::map< Node, int >& consts, std::map< Node, int >& pconsts );
+  bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg,
+                                std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                                std::map< Node, int >& consts, std::map< Node, int >& pconsts );
+  /** get sygus kinds */
+  void getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds, std::map< int, Node >& arg_const, std::map< Node, int >& consts );
+  /** is assoc */
+  bool isAssoc( 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 );
+public:
+  /** get sygus splits */
+  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
+};
+  
+  
+}
+}
+}
+
+#endif
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8db9435ed..bbc8837b9 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/datatypes/options.h"
 #include "theory/type_enumerator.h"
+#include "theory/datatypes/datatypes_sygus.h"
 
 #include <map>
 
@@ -64,6 +65,12 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 
   d_true = NodeManager::currentNM()->mkConst( true );
   d_dtfCounter = 0;
+  
+  if( options::sygusNormalForm() ){
+    d_sygus_split = new SygusSplit;
+  }else{
+    d_sygus_split = NULL;
+  }
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -238,8 +245,8 @@ void TheoryDatatypes::check(Effort e) {
                 }else{
                   Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                   std::vector< Node > children;
-                  if( dt.isSygus() && options::sygusNormalForm() ){
-                    getSygusSplits( n, dt, children );
+                  if( dt.isSygus() && d_sygus_split ){
+                    d_sygus_split->getSygusSplits( n, dt, children );
                   }else{
                     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
                       Node test = DatatypesRewriter::mkTester( n, i, dt );
@@ -248,6 +255,7 @@ void TheoryDatatypes::check(Effort e) {
                   }
                   Assert( !children.empty() );
                   Node lemma = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::OR, children );
+                  Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
                   d_out->lemma( lemma );
                 }
                 return;
@@ -1915,40 +1923,3 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
   }
   return false;
 }
-
-void TheoryDatatypes::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits ) {
-  Assert( dt.isSygus() );
-  Trace("sygus-split") << "Get sygus splits " << n << std::endl;
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
-    Node op = n.getOperator();
-    std::map< Node, std::vector< bool > >::iterator it = d_sygus_splits.find( op );
-    if( it==d_sygus_splits.end() ){
-      Expr selectorExpr = op.toExpr();
-      int csIndex = Datatype::cindexOf(selectorExpr);
-      int sIndex = Datatype::indexOf(selectorExpr);
-      Trace("sygus-split") << "  Constructor, selector index : " << csIndex << " " << sIndex << std::endl;
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        Expr sop = dt[i].getSygusOp();
-        Kind sk = NodeManager::operatorToKind( Node::fromExpr( sop ) );
-        Trace("sygus-split") << "  Operator #" << i << " : " << sop << ", kind = " << sk << std::endl;
-        bool addSplit = true;
-        //TODO
-        
-        d_sygus_splits[op].push_back( addSplit );
-      }
-    }
-    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      if( d_sygus_splits[op][i] ){
-        Node test = DatatypesRewriter::mkTester( n, i, dt );
-        splits.push_back( test );
-      }
-    }
-    Assert( !splits.empty() );
-  }else{
-    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      Node test = DatatypesRewriter::mkTester( n, i, dt );
-      splits.push_back( test );
-    }
-  }
-}
-
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 2f0ec20ec..0421213a6 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -34,10 +34,9 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-class EqualityQueryTheory;
+class SygusSplit;
 
 class TheoryDatatypes : public Theory {
-  friend class EqualityQueryTheory;
 private:
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
@@ -180,8 +179,8 @@ private:
   unsigned d_dtfCounter;
   /** expand definition skolem functions */
   std::map< Node, Node > d_exp_def_skolem;
-  /** sygus splits */
-  std::map< Node, std::vector< bool > > d_sygus_splits;
+  /** sygus split utility */
+  SygusSplit * d_sygus_split;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -280,8 +279,6 @@ private:
   bool mustCommunicateFact( Node n, Node exp );
   /** check clash mod eq */
   bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
-  /** get sygus splits */
-  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
 private:
   //equality queries
   bool hasTerm( TNode a );
@@ -291,6 +288,35 @@ private:
 public:
   /** get equality engine */
   eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
+
+
+private:
+  /** sygus splits */
+  std::map< TypeNode, std::vector< bool > > d_sygus_nred;
+  std::map< Node, std::map< int, std::vector< bool > > > d_sygus_pc_nred;
+  std::map< TypeNode, std::map< int, Node > > d_type_value;
+private:
+  /** get sygus splits */
+  void getSygusSplits( Node n, const Datatype& dt, std::vector< Node >& splits );
+  /** consider sygus split */
+  bool considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, Kind k, Kind parent, int arg,
+                               std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                               std::map< Node, int >& consts, std::map< Node, int >& pconsts );
+  bool considerSygusSplitConst( const Datatype& dt, const Datatype& pdt, Node c, Kind parent, int arg,
+                                std::map< Kind, int >& kinds, std::map< Kind, int >& pkinds,
+                                std::map< Node, int >& consts, std::map< Node, int >& pconsts );
+  /** get sygus kinds */
+  void getSygusKinds( const Datatype& dt, std::map< int, Kind >& arg_kind, std::map< Kind, int >& kinds, std::map< int, Node >& arg_const, std::map< Node, int >& consts );
+  /** is assoc */
+  bool isAssoc( 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, bool maxVal = false );
 };/* class TheoryDatatypes */
 
 }/* CVC4::theory::datatypes namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ad1508716..cebc5f245 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -196,8 +196,6 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
-option sygusMinGrammar --sygus-min-grammar bool :default false
-  minimize sygus grammars
 option sygusDecompose --sygus-decompose bool :default false
   decompose single invocation synthesis conjectures
 option sygusNormalForm --sygus-normal-form bool :default true
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index c15e103f9..fad2719f4 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -424,6 +424,10 @@ Expr Datatype::getConstructor(std::string name) const {
   return (*this)[name].getConstructor();
 }
 
+Type Datatype::getSygusType() const {
+  return d_sygus_type;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 084202956..b91348cdb 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -632,6 +632,9 @@ public:
    * This Datatype must be resolved.
    */
   Expr getConstructor(std::string name) const;
+  
+  /** get sygus type */
+  Type getSygusType() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,
-- 
2.30.2