Introduce SyGuS datatype API (#3465)

11 files changed, 279 insertions, 117 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 479b28cfb..0c1044e74 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -48,6 +48,8 @@ libcvc4_add_sources(
   datatype.cpp
   record.cpp
   record.h
+  sygus_datatype.cpp
+  sygus_datatype.h
   uninterpreted_constant.cpp
   uninterpreted_constant.h
 )
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
new file mode 100644
index 000000000..be2b04402
--- /dev/null
+++ b/src/expr/sygus_datatype.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file sygus_datatype.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of class for constructing SyGuS datatypes.
+ **/
+
+#include "expr/sygus_datatype.h"
+
+#include "printer/sygus_print_callback.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+SygusDatatype::SygusDatatype(const std::string& name) : d_dt(Datatype(name)) {}
+
+std::string SygusDatatype::getName() const { return d_dt.getName(); }
+
+void SygusDatatype::addConstructor(Node op,
+                                   const std::string& name,
+                                   std::shared_ptr<SygusPrintCallback> spc,
+                                   int weight,
+                                   const std::vector<TypeNode>& consTypes)
+{
+  d_ops.push_back(op);
+  d_cons_names.push_back(std::string(name));
+  d_pc.push_back(spc);
+  d_weight.push_back(weight);
+  d_consArgs.push_back(consTypes);
+}
+
+void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
+{
+  // add an "any constant" proxy variable
+  Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+  // mark that it represents any constant
+  SygusAnyConstAttribute saca;
+  av.setAttribute(saca, true);
+  std::stringstream ss;
+  ss << getName() << "_any_constant";
+  std::string cname(ss.str());
+  std::vector<TypeNode> builtinArg;
+  builtinArg.push_back(tn);
+  addConstructor(
+      av, cname, printer::SygusEmptyPrintCallback::getEmptyPC(), 0, builtinArg);
+}
+
+void SygusDatatype::initializeDatatype(TypeNode sygusType,
+                                       Node sygusVars,
+                                       bool allowConst,
+                                       bool allowAll)
+{
+  /* Use the sygus type to not lose reference to the original types (Bool,
+   * Int, etc) */
+  d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll);
+  for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+  {
+    // must convert to type now
+    std::vector<Type> cargs;
+    for (TypeNode& ct : d_consArgs[i])
+    {
+      cargs.push_back(ct.toType());
+    }
+    // add (sygus) constructor
+    d_dt.addSygusConstructor(
+        d_ops[i].toExpr(), d_cons_names[i], cargs, d_pc[i], d_weight[i]);
+  }
+  Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
+}
+
+const Datatype& SygusDatatype::getDatatype() const { return d_dt; }
+
+}  // namespace CVC4
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
new file mode 100644
index 000000000..d7b18644a
--- /dev/null
+++ b/src/expr/sygus_datatype.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file sygus_datatype.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for constructing SyGuS datatypes.
+ **/
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__SYGUS_DATATYPE_H
+#define CVC4__EXPR__SYGUS_DATATYPE_H
+
+#include <string>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
+/**
+ * Keeps the necessary information for initializing a sygus datatype, which
+ * includes the operators, names, print callbacks and list of argument types
+ * for each constructor.
+ *
+ * It also maintains a datatype to represent the structure of the type node.
+ *
+ * Notice that this class is only responsible for setting SyGuS-related
+ * information regarding the datatype. It is still required that the user
+ * of this class construct the datatype type corresponding to the datatype
+ * e.g. via a call to ExprManager::mkMutualDatatypeTypes().
+ */
+class SygusDatatype
+{
+ public:
+  /** constructor */
+  SygusDatatype(const std::string& name);
+  ~SygusDatatype() {}
+  /** get the name of this datatype */
+  std::string getName() const;
+  /**
+   * Add constructor that encodes an application of builtin operator op.
+   *
+   * op: the builtin operator,
+   * name: the name of the constructor,
+   * spc: the print callback (for custom printing of this node),
+   * weight: the weight of this constructor,
+   * consTypes: the argument types of the constructor (typically other sygus
+   * datatype types).
+   */
+  void addConstructor(Node op,
+                      const std::string& name,
+                      std::shared_ptr<SygusPrintCallback> spc,
+                      int weight,
+                      const std::vector<TypeNode>& consTypes);
+  /**
+   * This adds a constructor that corresponds to the any constant constructor
+   * for the given (builtin) type tn.
+   */
+  void addAnyConstantConstructor(TypeNode tn);
+
+  /** builds a datatype with the information in the type object
+   *
+   * sygusType: the builtin type that this datatype encodes,
+   * sygusVars: the formal argument list of the function-to-synthesize,
+   * allowConst: whether the grammar corresponding to this datatype allows
+   * any constant,
+   * allowAll: whether the grammar corresponding to this datatype allows
+   * any term.
+   */
+  void initializeDatatype(TypeNode sygusType,
+                          Node sygusVars,
+                          bool allowConst,
+                          bool allowAll);
+  /** Get the sygus datatype initialized by this class */
+  const Datatype& getDatatype() const;
+
+ private:
+  //---------- information to build normalized type node
+  /** Operators for each constructor. */
+  std::vector<Node> d_ops;
+  /** Names for each constructor. */
+  std::vector<std::string> d_cons_names;
+  /** Print callbacks for each constructor */
+  std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
+  /** Weights for each constructor */
+  std::vector<int> d_weight;
+  /** List of argument types for each constructor */
+  std::vector<std::vector<TypeNode>> d_consArgs;
+  /** Datatype to represent type's structure */
+  Datatype d_dt;
+};
+
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 572ddbac2..be4226f69 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/sygus_datatype.h"
 #include "options/datatypes_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 7e5a3ae98..ceb5d2dab 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -15,6 +15,7 @@
 #include "theory/datatypes/sygus_extension.h"
 
 #include "expr/node_manager.h"
+#include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index bb62ab8ae..5bf0ca036 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/sygus_datatype.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index 92783c2f7..2ac288c4c 100644
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -34,12 +34,6 @@ struct SygusVarNumAttributeId
 };
 typedef expr::Attribute<SygusVarNumAttributeId, uint64_t> SygusVarNumAttribute;
 
-/** Attribute true for variables that represent any constant */
-struct SygusAnyConstAttributeId
-{
-};
-typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
-
 /**
  * Attribute true for enumerators whose current model values were registered by
  * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 5e8c9c411..68445fca0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 
 #include "expr/datatype.h"
+#include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
 #include "printer/sygus_print_callback.h"
 #include "smt/smt_engine.h"
@@ -73,6 +74,12 @@ SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe)
 {
 }
 
+SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
+    : d_tn(src_tn),
+      d_unres_tn(unres_tn),
+      d_sdt(unres_tn.getAttribute(expr::VarNameAttr()))
+{
+}
 Kind SygusGrammarNorm::TypeObject::getEliminateKind(Kind ok)
 {
   Kind nk = ok;
@@ -200,47 +207,40 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
     exp_sop_n = Rewriter::rewrite(exp_sop_n);
   }
 
-  d_ops.push_back(exp_sop_n);
-  Trace("sygus-grammar-normalize-defs")
-      << "\tOriginal op: " << cons.getSygusOp()
-      << "\n\tExpanded one: " << exp_sop_n
-      << "\n\tRewritten one: " << d_ops.back() << "\n\n";
-  d_cons_names.push_back(cons.getName());
-  d_pc.push_back(cons.getSygusPrintCallback());
-  d_weight.push_back(cons.getWeight());
-  d_cons_args_t.push_back(std::vector<Type>());
+  std::vector<TypeNode> consTypes;
   for (const DatatypeConstructorArg& arg : cons)
   {
-    /* Collect unresolved type nodes corresponding to the typenode of the
-     * arguments */
-    d_cons_args_t.back().push_back(
-        sygus_norm
-            ->normalizeSygusRec(TypeNode::fromType(
-                static_cast<SelectorType>(arg.getType()).getRangeType()))
-            .toType());
+    // Collect unresolved type nodes corresponding to the typenode of the
+    // arguments.
+    TypeNode atype = TypeNode::fromType(arg.getRangeType());
+    // normalize it recursively
+    atype = sygus_norm->normalizeSygusRec(atype);
+    consTypes.push_back(atype);
   }
+
+  Trace("sygus-type-cons-defs") << "\tOriginal op: " << cons.getSygusOp()
+                                << "\n\tExpanded one: " << exp_sop_n << "\n\n";
+  d_sdt.addConstructor(exp_sop_n,
+                       cons.getName(),
+                       cons.getSygusPrintCallback(),
+                       cons.getWeight(),
+                       consTypes);
 }
 
-void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
-                                                 const Datatype& dt)
+void SygusGrammarNorm::TypeObject::initializeDatatype(
+    SygusGrammarNorm* sygus_norm, const Datatype& dt)
 {
   /* Use the sygus type to not lose reference to the original types (Bool,
    * Int, etc) */
-  d_dt.setSygus(dt.getSygusType(),
-                sygus_norm->d_sygus_vars.toExpr(),
-                dt.getSygusAllowConst(),
-                dt.getSygusAllowAll());
-  for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
-  {
-    d_dt.addSygusConstructor(d_ops[i].toExpr(),
-                             d_cons_names[i],
-                             d_cons_args_t[i],
-                             d_pc[i],
-                             d_weight[i]);
-  }
-  Trace("sygus-grammar-normalize") << "...built datatype " << d_dt << " ";
+  TypeNode sygusType = TypeNode::fromType(dt.getSygusType());
+  d_sdt.initializeDatatype(sygusType,
+                           sygus_norm->d_sygus_vars.toExpr(),
+                           dt.getSygusAllowConst(),
+                           dt.getSygusAllowAll());
+  Trace("sygus-grammar-normalize")
+      << "...built datatype " << d_sdt.getDatatype() << " ";
   /* Add to global accumulators */
-  sygus_norm->d_dt_all.push_back(d_dt);
+  sygus_norm->d_dt_all.push_back(d_sdt.getDatatype());
   sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
   Trace("sygus-grammar-normalize") << "---------------------------------\n";
 }
@@ -334,27 +334,25 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
     /* creates type for element */
     std::vector<unsigned> tmp;
     tmp.push_back(d_elem_pos.back());
-    Type t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp).toType();
+    TypeNode t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp);
     /* consumes element */
     d_elem_pos.pop_back();
     /* adds to Root: "type" */
-    to.d_ops.push_back(iden_op);
-    to.d_cons_names.push_back("id");
-    to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
-    /* Identity operators should not increase the size of terms */
-    to.d_weight.push_back(0);
-    to.d_cons_args_t.push_back(std::vector<Type>());
-    to.d_cons_args_t.back().push_back(t);
+    std::vector<TypeNode> ctypes;
+    ctypes.push_back(t);
+    to.d_sdt.addConstructor(iden_op,
+                            "id",
+                            printer::SygusEmptyPrintCallback::getEmptyPC(),
+                            0,
+                            ctypes);
     Trace("sygus-grammar-normalize-chain")
         << "\tAdding  " << t << " to " << to.d_unres_tn << "\n";
     /* adds to Root: "type + Root" */
-    to.d_ops.push_back(nm->operatorOf(PLUS));
-    to.d_cons_names.push_back(kindToString(PLUS));
-    to.d_pc.push_back(nullptr);
-    to.d_weight.push_back(-1);
-    to.d_cons_args_t.push_back(std::vector<Type>());
-    to.d_cons_args_t.back().push_back(t);
-    to.d_cons_args_t.back().push_back(to.d_unres_tn.toType());
+    std::vector<TypeNode> ctypesp;
+    ctypesp.push_back(t);
+    ctypesp.push_back(to.d_unres_tn);
+    to.d_sdt.addConstructor(
+        nm->operatorOf(PLUS), kindToString(PLUS), nullptr, -1, ctypesp);
     Trace("sygus-grammar-normalize-chain")
         << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
         << to.d_unres_tn << " and " << t << "\n";
@@ -383,13 +381,13 @@ void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
     Trace("sygus-grammar-normalize-chain") << "\n";
   }
   /* adds to Root: (\lambda x. x ) Next */
-  to.d_ops.push_back(iden_op);
-  to.d_cons_names.push_back("id_next");
-  to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
-  to.d_weight.push_back(0);
-  to.d_cons_args_t.push_back(std::vector<Type>());
-  to.d_cons_args_t.back().push_back(
-      sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType());
+  std::vector<TypeNode> ctypes;
+  ctypes.push_back(sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos));
+  to.d_sdt.addConstructor(iden_op,
+                          "id_next",
+                          printer::SygusEmptyPrintCallback::getEmptyPC(),
+                          0,
+                          ctypes);
 }
 
 std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
@@ -541,21 +539,6 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
   /* Creates type object for normalization */
   TypeObject to(tn, unres_tn);
 
-  /* Determine normalization transformation based on sygus type and given
-    * operators */
-  std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
-  /* If a transformation was selected, apply it */
-  if (transformation != nullptr)
-  {
-    transformation->buildType(this, to, dt, op_pos);
-  }
-
-  /* Remaining operators are rebuilt as they are */
-  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
-  {
-    Assert(op_pos[i] < dt.getNumConstructors());
-    to.addConsInfo(this, dt[op_pos[i]]);
-  }
   if (dt.getSygusAllowConst())
   {
     TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
@@ -568,29 +551,31 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
         && !sygus_type.isBoolean())
     {
       Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
-      // add an "any constant" proxy variable
-      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
-      // mark that it represents any constant
-      SygusAnyConstAttribute saca;
-      av.setAttribute(saca, true);
-      std::stringstream ss;
-      ss << to.d_unres_tn << "_any_constant";
-      std::string cname(ss.str());
-      std::vector<Type> builtin_arg;
-      builtin_arg.push_back(dt.getSygusType());
+      TypeNode dtn = TypeNode::fromType(dt.getSygusType());
       // we add this constructor first since we use left associative chains
       // and our symmetry breaking should group any constants together
       // beneath the same application
       // we set its weight to zero since it should be considered at the
       // same level as constants.
-      to.d_ops.insert(to.d_ops.begin(), av.toExpr());
-      to.d_cons_names.insert(to.d_cons_names.begin(), cname);
-      to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg);
-      to.d_pc.insert(to.d_pc.begin(),
-                     printer::SygusEmptyPrintCallback::getEmptyPC());
-      to.d_weight.insert(to.d_weight.begin(), 0);
+      to.d_sdt.addAnyConstantConstructor(dtn);
     }
   }
+
+  /* Determine normalization transformation based on sygus type and given
+    * operators */
+  std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
+  /* If a transformation was selected, apply it */
+  if (transformation != nullptr)
+  {
+    transformation->buildType(this, to, dt, op_pos);
+  }
+
+  /* Remaining operators are rebuilt as they are */
+  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
+  {
+    Assert(op_pos[i] < dt.getNumConstructors());
+    to.addConsInfo(this, dt[op_pos[i]]);
+  }
   /* Build normalize datatype */
   if (Trace.isOn("sygus-grammar-normalize"))
   {
@@ -601,8 +586,8 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
     }
     Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
   }
-  to.buildDatatype(this, dt);
-  return to.d_unres_tn;
+  to.initializeDatatype(this, dt);
+  return unres_tn;
 }
 
 TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 00c501cfe..f9c53c4ad 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -24,7 +24,7 @@
 
 #include "expr/datatype.h"
 #include "expr/node.h"
-#include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "expr/sygus_datatype.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
@@ -178,20 +178,15 @@ class SygusGrammarNorm
    * the unresolved type node used as placeholder for references of the yet to
    * be built normalized type
    *
-   * a datatype to represent the structure of the type node for the normalized
-   * type
+   * A (SyGuS) datatype to represent the structure of the type node for the
+   * normalized type.
    */
   class TypeObject
   {
    public:
     /* Stores the original type node and the unresolved placeholder. The
      * datatype for the latter is created with the respective name. */
-    TypeObject(TypeNode src_tn, TypeNode unres_tn)
-        : d_tn(src_tn),
-          d_unres_tn(unres_tn),
-          d_dt(Datatype(unres_tn.getAttribute(expr::VarNameAttr())))
-    {
-    }
+    TypeObject(TypeNode src_tn, TypeNode unres_tn);
     ~TypeObject() {}
 
     /** adds information in "cons" (operator, name, print callback, argument
@@ -215,16 +210,16 @@ class SygusGrammarNorm
      */
     static Node eliminatePartialOperators(Node n);
 
-    /** builds a datatype with the information in the type object
+    /** initializes a datatype with the information in the type object
      *
      * "dt" is the datatype of the original typenode. It is necessary for
      * retrieving ancillary information during the datatype building, such as
      * its sygus type (e.g. Int)
      *
-     * The built datatype and its unresolved type are saved in the global
+     * The initialized datatype and its unresolved type are saved in the global
      * accumulators of "sygus_norm"
      */
-    void buildDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
+    void initializeDatatype(SygusGrammarNorm* sygus_norm, const Datatype& dt);
 
     //---------- information stored from original type node
 
@@ -233,20 +228,10 @@ class SygusGrammarNorm
 
     //---------- information to build normalized type node
 
-    /* Operators for each constructor. */
-    std::vector<Node> d_ops;
-    /* Names for each constructor. */
-    std::vector<std::string> d_cons_names;
-    /* Print callbacks for each constructor */
-    std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
-    /* Weights for each constructor */
-    std::vector<int> d_weight;
-    /* List of argument types for each constructor */
-    std::vector<std::vector<Type>> d_cons_args_t;
     /* Unresolved type node placeholder */
     TypeNode d_unres_tn;
-    /* Datatype to represent type's structure */
-    Datatype d_dt;
+    /** A sygus datatype */
+    SygusDatatype d_sdt;
   }; /* class TypeObject */
 
   /** Transformation abstract class
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 84a9c2405..79b4c9caa 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include "base/check.h"
+#include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 5f51d8dec..1ff0457c4 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/type_info.h"
 
 #include "base/check.h"
+#include "expr/sygus_datatype.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"