Final preparations for changing API to use the Node-level datatype (#4863)

This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.

After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 91ae9d158445e8226b6fe285f4d5c789d2c99845..bfc33ef8774daaf1b93a715ba70734bf35438134 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -220,6 +220,28 @@ void DType::addConstructor(std::shared_ptr<DTypeConstructor> c)
   d_constructors.push_back(c);
 }
 
+void DType::addSygusConstructor(Node op,
+                                const std::string& cname,
+                                const std::vector<TypeNode>& cargs,
+                                int weight)
+{
+  // avoid name clashes
+  std::stringstream ss;
+  ss << getName() << "_" << getNumConstructors() << "_" << cname;
+  std::string name = ss.str();
+  unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
+  std::shared_ptr<DTypeConstructor> c =
+      std::make_shared<DTypeConstructor>(name, cweight);
+  c->setSygus(op);
+  for (size_t j = 0, nargs = cargs.size(); j < nargs; j++)
+  {
+    std::stringstream sname;
+    sname << name << "_" << j;
+    c->addArg(sname.str(), cargs[j]);
+  }
+  addConstructor(c);
+}
+
 void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll)
 {
   Assert(!d_resolved);

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 1682614d0b1b9ec156cd357686b3a9c86e87491d..f48997748dbbabff7fe2eb8cdd5442c440de3418 100644 (file)
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -77,7 +77,6 @@ typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
 class NodeManager;
-
 class Datatype;
 
 /**
@@ -191,6 +190,31 @@ class DType
    * be unique; they are for convenience and pretty-printing only.
    */
   void addConstructor(std::shared_ptr<DTypeConstructor> c);
+  /** add sygus constructor
+   *
+   * This adds a sygus constructor to this datatype, where
+   * this datatype should be currently unresolved. Note this method is
+   * syntactic sugar for adding a normal constructor and setting it to be a
+   * sygus constructor, and following a naming convention that avoids
+   * constructors with the same name.
+   *
+   * @param op : the builtin operator, constant, or variable that this
+   * constructor encodes
+   * @param cname the name of the constructor (for printing only)
+   * @param cargs the arguments of the constructor.
+   * It should be the case that cargs are sygus datatypes that
+   * encode the arguments of op. For example, a sygus constructor
+   * with op = PLUS should be such that cargs.size()>=2 and
+   * the sygus type of cargs[i] is Real/Int for each i.
+   * @param weight denotes the value added by the constructor when computing the
+   * size of datatype terms. Passing a value < 0 denotes the default weight for
+   * the constructor, which is 0 for nullary constructors and 1 for non-nullary
+   * constructors.
+   */
+  void addSygusConstructor(Node op,
+                           const std::string& cname,
+                           const std::vector<TypeNode>& cargs,
+                           int weight = -1);
 
   /** set sygus
    *

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index c64814ed6b250bfbea13f11ecf48607ee5522b43..05daae1b85dc1e1ce6d4cf046dc7edbb050f032a 100644 (file)
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -70,7 +70,7 @@ void DTypeConstructor::addArgSelf(std::string selectorName)
   addArg(a);
 }
 
-std::string DTypeConstructor::getName() const { return d_name; }
+const std::string& DTypeConstructor::getName() const { return d_name; }
 
 Node DTypeConstructor::getConstructor() const
 {
@@ -115,7 +115,10 @@ TypeNode DTypeConstructor::getSpecializedConstructorType(
     TypeNode returnType) const
 {
   Assert(isResolved());
-  Assert(returnType.isDatatype());
+  Assert(returnType.isDatatype())
+      << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
+         "got "
+      << returnType;
   const DType& dt = DType::datatypeOf(d_constructor);
   Assert(dt.isParametric());
   TypeNode dtt = dt.getTypeNode();
@@ -577,6 +580,13 @@ bool DTypeConstructor::resolve(
     arg->d_selector.setAttribute(DTypeIndexAttr(), index++);
     arg->d_resolved = true;
     argTypes.push_back(range);
+    // We use \0 as a distinguished marker for unresolved selectors for doing
+    // name resolutions. We now can remove \0 from name if necessary.
+    const size_t nul = arg->d_name.find('\0');
+    if (nul != std::string::npos)
+    {
+      arg->d_name.resize(nul);
+    }
   }
 
   Assert(index == getNumArgs());

diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index 2553309f15d75fbf10c48e1040505639b4d6d181..ee85d5f25537cf0f994ccb3f963ee692d75f2f14 100644 (file)
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -76,7 +76,7 @@ class DTypeConstructor
   void addArgSelf(std::string selectorName);
 
   /** Get the name of this constructor. */
-  std::string getName() const;
+  const std::string& getName() const;
 
   /**
    * Get the constructor operator of this constructor.  The

diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index 302e6c51f2925adf40e488c504d83c3d17ce1f84..e29d229aff0bca6390d60ed702cfbe6c7c10b84b 100644 (file)
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -26,7 +26,7 @@ DTypeSelector::DTypeSelector(std::string name, Node selector)
   Assert(name != "");
 }
 
-std::string DTypeSelector::getName() const { return d_name; }
+const std::string& DTypeSelector::getName() const { return d_name; }
 
 Node DTypeSelector::getSelector() const
 {
@@ -55,7 +55,11 @@ void DTypeSelector::toStream(std::ostream& out) const
   TypeNode t;
   if (d_resolved)
   {
-    t = getRangeType();
+    // don't try to print the range type of null, instead we print null itself.
+    if (!getType().isNull())
+    {
+      t = getRangeType();
+    }
   }
   else if (d_selector.isNull())
   {

diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
index bd0271d9033fcf3d3b3a9cf4e02e3d799c740432..6a3a7b268e3d73d1a991230b6a7b9b64c70c7e21 100644 (file)
--- a/src/expr/dtype_selector.h
+++ b/src/expr/dtype_selector.h
@@ -41,7 +41,7 @@ class DTypeSelector
   DTypeSelector(std::string name, Node selector);
 
   /** Get the name of this constructor argument. */
-  std::string getName() const;
+  const std::string& getName() const;
 
   /**
    * Get the selector for this constructor argument; this call is

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c72de95644987069d93b93f962d98afdc8b08159..bcddc23f5180843ac9262aa110778b79acc4baa6 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -582,6 +582,33 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
                                      paramTypes,
                                      paramReplacements);
     }
+    // Check the datatype has been resolved properly.
+    for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+    {
+      const DTypeConstructor& c = dt[i];
+      TypeNode testerType CVC4_UNUSED = c.getTester().getType();
+      Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut)
+          << "malformed tester in datatype post-resolution";
+      TypeNode ctorType CVC4_UNUSED = c.getConstructor().getType();
+      Assert(ctorType.isConstructor()
+            && ctorType.getNumChildren() == c.getNumArgs() + 1
+            && ctorType.getRangeType() == ut)
+          << "malformed constructor in datatype post-resolution";
+      // for all selectors...
+      for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+      {
+        const DTypeSelector& a = c[j];
+        TypeNode selectorType = a.getType();
+        Assert(a.isResolved() && selectorType.isSelector()
+              && selectorType[0] == ut)
+            << "malformed selector in datatype post-resolution";
+        // This next one's a "hard" check, performed in non-debug builds
+        // as well; the other ones should all be guaranteed by the
+        // CVC4::DType class, but this actually needs to be checked.
+        AlwaysAssert(!selectorType.getRangeType().isFunctionLike())
+            << "cannot put function-like things in datatypes";
+      }
+    }
   }
 
   for (NodeManagerListener* nml : d_listeners)