4 files changed, 75 insertions, 7 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 5f43fb24f..dd5f12b28 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -223,6 +223,41 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   PrettyCheckArgument(
       !isResolved(), this, "cannot set sygus type to a finalized Datatype");
+  // We can be in a case where the only rule specified was
+  // (Constant T), in which case we have not yet added a constructor. We
+  // ensure an arbitrary constant is added in this case. We additionally
+  // add a constant if the grammar has only non-nullary constructors, since this
+  // ensures the datatype is well-founded (see 3423).
+  // Notice we only want to do this for sygus datatypes that are user-provided.
+  // At the moment, the condition !allow_all implies the grammar is
+  // user-provided and hence may require a default constant.
+  // TODO (https://github.com/CVC4/cvc4-projects/issues/38):
+  // In an API for SyGuS, it probably makes more sense for the user to
+  // explicitly add the "any constant" constructor with a call instead of
+  // passing a flag. This would make the block of code unnecessary.
+  if (allow_const && !allow_all)
+  {
+    // if i don't already have a constant (0-ary constructor)
+    bool hasConstant = false;
+    for (unsigned i = 0, ncons = getNumConstructors(); i < ncons; i++)
+    {
+      if ((*this)[i].getNumArgs() == 0)
+      {
+        hasConstant = true;
+        break;
+      }
+    }
+    if (!hasConstant)
+    {
+      // add an arbitrary one
+      Expr op = st.mkGroundTerm();
+      std::stringstream cname;
+      cname << op;
+      std::vector<Type> cargs;
+      addSygusConstructor(op, cname.str(), cargs);
+    }
+  }
+
   TypeNode stn = TypeNode::fromType(st);
   Node bvln = Node::fromExpr(bvl);
   d_internal->setSygus(stn, bvln, allow_const, allow_all);
diff --git a/src/expr/node.h b/src/expr/node.h
index 4bef8db74..e07499b69 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1368,15 +1368,15 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
       nb << getOperator().substitute(node, replacement, cache);
     }
   }
-  for (const Node& n : *this)
+  for (const_iterator it = begin(), iend = end(); it != iend; ++it)
   {
-    if (n == node)
+    if (*it == node)
     {
       nb << replacement;
     }
     else
     {
-      nb << n.substitute(node, replacement, cache);
+      nb << (*it).substitute(node, replacement, cache);
     }
   }
 
@@ -1435,9 +1435,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                      replacementsBegin, replacementsEnd,
                                      cache);
     }
-    for (const Node& n : *this)
+    for (const_iterator it = begin(), iend = end(); it != iend; ++it)
     {
-      nb << n.substitute(
+      nb << (*it).substitute(
           nodesBegin, nodesEnd, replacementsBegin, replacementsEnd, cache);
     }
     Node n = nb;
@@ -1483,9 +1483,9 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
       // push the operator
       nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache);
     }
-    for (const Node& n : *this)
+    for (const_iterator it = begin(), iend = end(); it != iend; ++it)
     {
-      nb << n.substitute(substitutionsBegin, substitutionsEnd, cache);
+      nb << (*it).substitute(substitutionsBegin, substitutionsEnd, cache);
     }
     Node n = nb;
     cache[*this] = n;
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 9619e69d1..595adda55 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -129,6 +129,32 @@ bool hasSubtermMulti(TNode n, TNode t)
   return false;
 }
 
+bool hasSubtermKind(Kind k, Node n)
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getKind() == k)
+      {
+        return true;
+      }
+      for (const Node& cn : cur)
+      {
+        visit.push_back(cn);
+      }
+    }
+  } while (!visit.empty());
+  return false;
+}
+
 bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
 {
   if (t.empty())
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 929e1c5ef..e47029284 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -45,6 +45,13 @@ bool hasSubterm(TNode n, TNode t, bool strict = false);
 bool hasSubtermMulti(TNode n, TNode t);
 
 /**
+ * @param k The kind of node to check
+ * @param n The node to search in.
+ * @return true iff there is a term in n that has kind k
+ */
+bool hasSubtermKind(Kind k, Node n);
+
+/**
  * Check if the node n has a subterm that occurs in t.
  * @param n The node to search in
  * @param t The set of subterms to search for