Improve interface for sygus datatype, fix utilities (#3473)

2 files changed, 64 insertions, 34 deletions

diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index d8ee2e1ea..73f7c5769 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -26,15 +26,16 @@ std::string SygusDatatype::getName() const { return d_dt.getName(); }
 
 void SygusDatatype::addConstructor(Node op,
                                    const std::string& name,
-                                   const std::vector<TypeNode>& consTypes,
+                                   const std::vector<TypeNode>& argTypes,
                                    std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
-  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);
+  d_cons.push_back(SygusDatatypeConstructor());
+  d_cons.back().d_op = op;
+  d_cons.back().d_name = name;
+  d_cons.back().d_argTypes = argTypes;
+  d_cons.back().d_pc = spc;
+  d_cons.back().d_weight = weight;
 }
 
 void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
@@ -53,15 +54,21 @@ void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
       av, cname, builtinArg, printer::SygusEmptyPrintCallback::getEmptyPC(), 0);
 }
 void SygusDatatype::addConstructor(Kind k,
-                                   const std::vector<TypeNode>& consTypes,
+                                   const std::vector<TypeNode>& argTypes,
                                    std::shared_ptr<SygusPrintCallback> spc,
                                    int weight)
 {
   NodeManager* nm = NodeManager::currentNM();
-  addConstructor(nm->operatorOf(k), kindToString(k), consTypes, spc, weight);
+  addConstructor(nm->operatorOf(k), kindToString(k), argTypes, spc, weight);
 }
 
-size_t SygusDatatype::getNumConstructors() const { return d_ops.size(); }
+size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); }
+
+const SygusDatatypeConstructor& SygusDatatype::getConstructor(unsigned i) const
+{
+  Assert(i < d_cons.size());
+  return d_cons[i];
+}
 
 void SygusDatatype::initializeDatatype(TypeNode sygusType,
                                        Node sygusVars,
@@ -69,21 +76,26 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
                                        bool allowAll)
 {
   // should not have initialized (set sygus) yet
-  Assert(!d_dt.isSygus());
+  Assert(!isInitialized());
+  // should have added a constructor
+  Assert(!d_cons.empty());
   /* 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)
+  for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i)
   {
     // must convert to type now
     std::vector<Type> cargs;
-    for (TypeNode& ct : d_consArgs[i])
+    for (TypeNode& ct : d_cons[i].d_argTypes)
     {
       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]);
+    d_dt.addSygusConstructor(d_cons[i].d_op.toExpr(),
+                             d_cons[i].d_name,
+                             cargs,
+                             d_cons[i].d_pc,
+                             d_cons[i].d_weight);
   }
   Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
 }
@@ -91,8 +103,10 @@ void SygusDatatype::initializeDatatype(TypeNode sygusType,
 const Datatype& SygusDatatype::getDatatype() const
 {
   // should have initialized by this point
-  Assert(d_dt.isSygus());
+  Assert(isInitialized());
   return d_dt;
 }
 
+bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); }
+
 }  // namespace CVC4
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 132406c69..e7b60f3a3 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -33,6 +33,25 @@ struct SygusAnyConstAttributeId
 typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
 
 /**
+ * Information necessary to specify a sygus constructor. Further detail on these
+ * fields can be found in SygusDatatype below.
+ */
+class SygusDatatypeConstructor
+{
+ public:
+  /** The operator that the constructor encodes. */
+  Node d_op;
+  /** Name of the constructor. */
+  std::string d_name;
+  /** List of argument types. */
+  std::vector<TypeNode> d_argTypes;
+  /** Print callback of the constructor. */
+  std::shared_ptr<SygusPrintCallback> d_pc;
+  /** Weight of the constructor. */
+  int d_weight;
+};
+
+/**
  * Keeps the necessary information for initializing a sygus datatype, which
  * includes the operators, names, print callbacks and list of argument types
  * for each constructor.
@@ -57,28 +76,28 @@ class SygusDatatype
    *
    * 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
+   * argTypes: the argument types of the constructor (typically other sygus
    * datatype types).
+   * spc: the print callback (for custom printing of this node),
+   * weight: the weight of this constructor.
    *
-   * It should be the case that consTypes are sygus datatype types (possibly
+   * It should be the case that argTypes are sygus datatype types (possibly
    * unresolved) that encode the arguments of the builtin operator. That is,
-   * if op is the builtin PLUS operator, then consTypes could contain 2+
+   * if op is the builtin PLUS operator, then argTypes could contain 2+
    * sygus datatype types that encode integer.
    */
   void addConstructor(Node op,
                       const std::string& name,
-                      const std::vector<TypeNode>& consTypes,
+                      const std::vector<TypeNode>& argTypes,
                       std::shared_ptr<SygusPrintCallback> spc = nullptr,
                       int weight = -1);
   /**
    * Add constructor that encodes an application of builtin kind k. Like above,
-   * the arguments consTypes should correspond to sygus datatypes that encode
+   * the arguments argTypes should correspond to sygus datatypes that encode
    * the types of the arguments of the kind.
    */
   void addConstructor(Kind k,
-                      const std::vector<TypeNode>& consTypes,
+                      const std::vector<TypeNode>& argTypes,
                       std::shared_ptr<SygusPrintCallback> spc = nullptr,
                       int weight = -1);
   /**
@@ -90,6 +109,9 @@ class SygusDatatype
   /** Get the number of constructors added to this class so far */
   size_t getNumConstructors() const;
 
+  /** Get constructor at index i */
+  const SygusDatatypeConstructor& getConstructor(unsigned i) const;
+
   /** builds a datatype with the information in the type object
    *
    * sygusType: the builtin type that this datatype encodes,
@@ -106,18 +128,12 @@ class SygusDatatype
   /** Get the sygus datatype initialized by this class */
   const Datatype& getDatatype() const;
 
+  /** is initialized */
+  bool isInitialized() 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;
+  /** Information for each constructor. */
+  std::vector<SygusDatatypeConstructor> d_cons;
   /** Datatype to represent type's structure */
   Datatype d_dt;
 };