Reestablishing support for define-sort (#5810)

Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.

This fixes issue #5809.

2 files changed, 39 insertions, 0 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e845bf876..abec4d8dd 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1082,6 +1082,30 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams));
 }
 
+Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
+{
+  NodeManagerScope scope(d_solver->getNodeManager());
+  return Sort(
+      d_solver,
+      d_type->substitute(sort.getTypeNode(), replacement.getTypeNode()));
+}
+
+Sort Sort::substitute(const std::vector<Sort>& sorts,
+                      const std::vector<Sort>& replacements) const
+{
+  NodeManagerScope scope(d_solver->getNodeManager());
+
+  std::vector<CVC4::TypeNode> tSorts = sortVectorToTypeNodes(sorts),
+                              tReplacements =
+                                  sortVectorToTypeNodes(replacements);
+
+  return Sort(d_solver,
+              d_type->substitute(tSorts.begin(),
+                                 tSorts.end(),
+                                 tReplacements.begin(),
+                                 tReplacements.end()));
+}
+
 std::string Sort::toString() const
 {
   if (d_solver != nullptr)
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 98752c697..66ba4f23b 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -477,6 +477,21 @@ class CVC4_PUBLIC Sort
   Sort instantiate(const std::vector<Sort>& params) const;
 
   /**
+   * Substitution of Sorts.
+   * @param sort the subsort to be substituted within this sort.
+   * @param replacement the sort replacing the substituted subsort.
+   */
+  Sort substitute(const Sort& sort, const Sort& replacement) const;
+
+  /**
+   * Simultaneous substitution of Sorts.
+   * @param sorts the subsorts to be substituted within this sort.
+   * @param replacements the sort replacing the substituted subsorts.
+   */
+  Sort substitute(const std::vector<Sort>& sorts,
+                  const std::vector<Sort>& replacements) const;
+
+  /**
    * Output a string representation of this sort to a given stream.
    * @param out the output stream
    */