Add missing functions to new C++ API (#3769)

2 files changed, 395 insertions, 36 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index b16e5afc5..41a374283 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -827,6 +827,14 @@ bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
 
 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
 
+bool Sort::operator<(const Sort& s) const { return *d_type < *s.d_type; }
+
+bool Sort::operator>(const Sort& s) const { return *d_type > *s.d_type; }
+
+bool Sort::operator<=(const Sort& s) const { return *d_type <= *s.d_type; }
+
+bool Sort::operator>=(const Sort& s) const { return *d_type >= *s.d_type; }
+
 bool Sort::isNull() const { return isNullHelper(); }
 
 bool Sort::isBoolean() const { return d_type->isBoolean(); }
@@ -853,6 +861,10 @@ bool Sort::isParametricDatatype() const
   return DatatypeType(*d_type).isParametric();
 }
 
+bool Sort::isConstructor() const { return d_type->isConstructor(); }
+bool Sort::isSelector() const { return d_type->isSelector(); }
+bool Sort::isTester() const { return d_type->isTester(); }
+
 bool Sort::isFunction() const { return d_type->isFunction(); }
 
 bool Sort::isPredicate() const { return d_type->isPredicate(); }
@@ -873,6 +885,13 @@ bool Sort::isFirstClass() const { return d_type->isFirstClass(); }
 
 bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); }
 
+bool Sort::isSubsortOf(Sort s) const { return d_type->isSubtypeOf(*s.d_type); }
+
+bool Sort::isComparableTo(Sort s) const
+{
+  return d_type->isComparableTo(*s.d_type);
+}
+
 Datatype Sort::getDatatype() const
 {
   CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
@@ -902,6 +921,27 @@ std::string Sort::toString() const { return d_type->toString(); }
 // to the new API. !!!
 CVC4::Type Sort::getType(void) const { return *d_type; }
 
+/* Constructor sort ------------------------------------------------------- */
+
+size_t Sort::getConstructorArity() const
+{
+  CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+  return ConstructorType(*d_type).getArity();
+}
+
+std::vector<Sort> Sort::getConstructorDomainSorts() const
+{
+  CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+  std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
+  return typeVectorToSorts(types);
+}
+
+Sort Sort::getConstructorCodomainSort() const
+{
+  CVC4_API_CHECK(isConstructor()) << "Not a function sort.";
+  return ConstructorType(*d_type).getRangeType();
+}
+
 /* Function sort ------------------------------------------------------- */
 
 size_t Sort::getFunctionArity() const
@@ -1290,6 +1330,44 @@ bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
 
+bool Term::operator<(const Term& t) const { return *d_expr < *t.d_expr; }
+
+bool Term::operator>(const Term& t) const { return *d_expr > *t.d_expr; }
+
+bool Term::operator<=(const Term& t) const { return *d_expr <= *t.d_expr; }
+
+bool Term::operator>=(const Term& t) const { return *d_expr >= *t.d_expr; }
+
+size_t Term::getNumChildren() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  // special case for apply kinds
+  if (isApplyKind(d_expr->getKind()))
+  {
+    return d_expr->getNumChildren() + 1;
+  }
+  return d_expr->getNumChildren();
+}
+
+Term Term::operator[](size_t index) const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  // special cases for apply kinds
+  if (isApplyKind(d_expr->getKind()))
+  {
+    CVC4_API_CHECK(d_expr->hasOperator())
+        << "Expected apply kind to have operator when accessing child of Term";
+    if (index == 0)
+    {
+      // return the operator
+      return api::Term(d_expr->getOperator());
+    }
+    // otherwise we are looking up child at (index-1)
+    index--;
+  }
+  return api::Term((*d_expr)[index]);
+}
+
 uint64_t Term::getId() const
 {
   CVC4_API_CHECK_NOT_NULL;
@@ -1308,6 +1386,37 @@ Sort Term::getSort() const
   return Sort(d_expr->getType());
 }
 
+Term Term::substitute(Term e, Term replacement) const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(!e.isNull())
+      << "Expected non-null term to replace in substitute";
+  CVC4_API_CHECK(!replacement.isNull())
+      << "Expected non-null term as replacement in substitute";
+  CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort()))
+      << "Expecting terms of comparable sort in substitute";
+  return api::Term(d_expr->substitute(e.getExpr(), replacement.getExpr()));
+}
+
+Term Term::substitute(const std::vector<Term> es,
+                      const std::vector<Term>& replacements) const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(es.size() == replacements.size())
+      << "Expecting vectors of the same arity in substitute";
+  for (unsigned i = 0, nterms = es.size(); i < nterms; i++)
+  {
+    CVC4_API_CHECK(!es[i].isNull())
+        << "Expected non-null term to replace in substitute";
+    CVC4_API_CHECK(!replacements[i].isNull())
+        << "Expected non-null term as replacement in substitute";
+    CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort()))
+        << "Expecting terms of comparable sort in substitute";
+  }
+  return api::Term(d_expr->substitute(termVectorToExprs(es),
+                                      termVectorToExprs(replacements)));
+}
+
 bool Term::hasOp() const
 {
   CVC4_API_CHECK_NOT_NULL;
@@ -1344,6 +1453,12 @@ Op Term::getOp() const
 
 bool Term::isNull() const { return isNullHelper(); }
 
+bool Term::isConst() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return d_expr->isConst();
+}
+
 Term Term::notTerm() const
 {
   CVC4_API_CHECK_NOT_NULL;
@@ -1775,15 +1890,15 @@ DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
 DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
     : d_stor(new CVC4::DatatypeConstructorArg(stor))
 {
+  CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
 }
 
 DatatypeSelector::~DatatypeSelector() {}
 
-bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
+std::string DatatypeSelector::getName() const { return d_stor->getName(); }
 
 Term DatatypeSelector::getSelectorTerm() const
 {
-  CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
   Term sel = d_stor->getSelector();
   return sel;
 }
@@ -1816,39 +1931,55 @@ DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; }
 DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
     : d_ctor(new CVC4::DatatypeConstructor(ctor))
 {
+  CVC4_API_CHECK(d_ctor->isResolved())
+      << "Expected resolved datatype constructor";
 }
 
 DatatypeConstructor::~DatatypeConstructor() {}
 
-bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
+std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
 
 Term DatatypeConstructor::getConstructorTerm() const
 {
-  CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
   Term ctor = d_ctor->getConstructor();
   return ctor;
 }
 
+Term DatatypeConstructor::getTesterTerm() const
+{
+  Term tst = d_ctor->getTester();
+  return tst;
+}
+
+std::string DatatypeConstructor::getTesterName() const
+{
+  return d_ctor->getTesterName();
+}
+
+size_t DatatypeConstructor::getNumSelectors() const
+{
+  return d_ctor->getNumArgs();
+}
+
+DatatypeSelector DatatypeConstructor::operator[](size_t index) const
+{
+  return (*d_ctor)[index];
+}
+
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
 {
-  // CHECK: selector with name exists?
-  // CHECK: is resolved?
-  return (*d_ctor)[name];
+  return getSelectorForName(name);
 }
 
 DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
 {
-  // CHECK: cons with name exists?
-  // CHECK: is resolved?
-  return (*d_ctor)[name];
+  return getSelectorForName(name);
 }
 
 Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
 {
-  // CHECK: cons with name exists?
-  // CHECK: is resolved?
-  Term sel = d_ctor->getSelector(name);
-  return sel;
+  DatatypeSelector sel = getSelector(name);
+  return sel.getSelectorTerm();
 }
 
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
@@ -1940,6 +2071,25 @@ const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor(
   return *d_ctor;
 }
 
+DatatypeSelector DatatypeConstructor::getSelectorForName(
+    const std::string& name) const
+{
+  bool foundSel = false;
+  size_t index = 0;
+  for (size_t i = 0, nsels = getNumSelectors(); i < nsels; i++)
+  {
+    if ((*d_ctor)[i].getName() == name)
+    {
+      index = i;
+      foundSel = true;
+      break;
+    }
+  }
+  CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
+                           << getName() << " exists";
+  return (*d_ctor)[index];
+}
+
 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 {
   out << ctor.toString();
@@ -1951,6 +2101,7 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 Datatype::Datatype(const CVC4::Datatype& dtype)
     : d_dtype(new CVC4::Datatype(dtype))
 {
+  CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
 }
 
 // Nullary constructor for Cython
@@ -1960,39 +2111,42 @@ Datatype::~Datatype() {}
 
 DatatypeConstructor Datatype::operator[](size_t idx) const
 {
-  // CHECK (maybe): is resolved?
   CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
   return (*d_dtype)[idx];
 }
 
 DatatypeConstructor Datatype::operator[](const std::string& name) const
 {
-  // CHECK: cons with name exists?
-  // CHECK: is resolved?
-  return (*d_dtype)[name];
+  return getConstructorForName(name);
 }
 
 DatatypeConstructor Datatype::getConstructor(const std::string& name) const
 {
-  // CHECK: cons with name exists?
-  // CHECK: is resolved?
-  return (*d_dtype)[name];
+  return getConstructorForName(name);
 }
 
 Term Datatype::getConstructorTerm(const std::string& name) const
 {
-  // CHECK: cons with name exists?
-  // CHECK: is resolved?
-  Term ctor = d_dtype->getConstructor(name);
-  return ctor;
+  DatatypeConstructor ctor = getConstructor(name);
+  return ctor.getConstructorTerm();
 }
 
+std::string Datatype::getName() const { return d_dtype->getName(); }
+
 size_t Datatype::getNumConstructors() const
 {
   return d_dtype->getNumConstructors();
 }
 
 bool Datatype::isParametric() const { return d_dtype->isParametric(); }
+bool Datatype::isCodatatype() const { return d_dtype->isCodatatype(); }
+
+bool Datatype::isTuple() const { return d_dtype->isTuple(); }
+
+bool Datatype::isRecord() const { return d_dtype->isRecord(); }
+
+bool Datatype::isFinite() const { return d_dtype->isFinite(); }
+bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); }
 
 std::string Datatype::toString() const { return d_dtype->getName(); }
 
@@ -2010,6 +2164,25 @@ Datatype::const_iterator Datatype::end() const
 // to the new API. !!!
 const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; }
 
+DatatypeConstructor Datatype::getConstructorForName(
+    const std::string& name) const
+{
+  bool foundCons = false;
+  size_t index = 0;
+  for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
+  {
+    if ((*d_dtype)[i].getName() == name)
+    {
+      index = i;
+      foundCons = true;
+      break;
+    }
+  }
+  CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
+                            << getName() << " exists";
+  return (*d_dtype)[index];
+}
+
 Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
                                          bool begin)
 {
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 9820aeb19..103637a7d 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -230,6 +230,34 @@ class CVC4_PUBLIC Sort
   bool operator!=(const Sort& s) const;
 
   /**
+   * Comparison for ordering on sorts.
+   * @param s the sort to compare to
+   * @return true if this sort is less than s
+   */
+  bool operator<(const Sort& s) const;
+
+  /**
+   * Comparison for ordering on sorts.
+   * @param s the sort to compare to
+   * @return true if this sort is greater than s
+   */
+  bool operator>(const Sort& s) const;
+
+  /**
+   * Comparison for ordering on sorts.
+   * @param s the sort to compare to
+   * @return true if this sort is less than or equal to s
+   */
+  bool operator<=(const Sort& s) const;
+
+  /**
+   * Comparison for ordering on sorts.
+   * @param s the sort to compare to
+   * @return true if this sort is greater than or equal to s
+   */
+  bool operator>=(const Sort& s) const;
+
+  /**
    * @return true if this Sort is a null sort.
    */
   bool isNull() const;
@@ -295,6 +323,23 @@ class CVC4_PUBLIC Sort
   bool isParametricDatatype() const;
 
   /**
+   * Is this a constructor sort?
+   * @return true if the sort is a constructor sort
+   */
+  bool isConstructor() const;
+
+  /**
+   * Is this a selector sort?
+   * @return true if the sort is a selector sort
+   */
+  bool isSelector() const;
+
+  /**
+   * Is this a tester sort?
+   * @return true if the sort is a tester sort
+   */
+  bool isTester() const;
+  /**
    * Is this a function sort?
    * @return true if the sort is a function sort
    */
@@ -373,6 +418,19 @@ class CVC4_PUBLIC Sort
   bool isFunctionLike() const;
 
   /**
+   * Is this sort a subsort of the given sort?
+   * @return true if this sort is a subsort of s
+   */
+  bool isSubsortOf(Sort s) const;
+
+  /**
+   * Is this sort comparable to the given sort (i.e., do they share
+   * a common ancestor in the subsort tree)?
+   * @return true if this sort is comparable to s
+   */
+  bool isComparableTo(Sort s) const;
+
+  /**
    * @return the underlying datatype of a datatype sort
    */
   Datatype getDatatype() const;
@@ -399,10 +457,27 @@ class CVC4_PUBLIC Sort
   // to the new API. !!!
   CVC4::Type getType(void) const;
 
+  /* Constructor sort ------------------------------------------------------- */
+
+  /**
+   * @return the arity of a constructor sort
+   */
+  size_t getConstructorArity() const;
+
+  /**
+   * @return the domain sorts of a constructor sort
+   */
+  std::vector<Sort> getConstructorDomainSorts() const;
+
+  /**
+   * @return the codomain sort of a constructor sort
+   */
+  Sort getConstructorCodomainSort() const;
+
   /* Function sort ------------------------------------------------------- */
 
   /**
-   * @return the arity  of a function sort
+   * @return the arity of a function sort
    */
   size_t getFunctionArity() const;
 
@@ -722,6 +797,48 @@ class CVC4_PUBLIC Term
   bool operator!=(const Term& t) const;
 
   /**
+   * Comparison for ordering on terms.
+   * @param t the term to compare to
+   * @return true if this term is less than t
+   */
+  bool operator<(const Term& t) const;
+
+  /**
+   * Comparison for ordering on terms.
+   * @param t the term to compare to
+   * @return true if this term is greater than t
+   */
+  bool operator>(const Term& t) const;
+
+  /**
+   * Comparison for ordering on terms.
+   * @param t the term to compare to
+   * @return true if this term is less than or equal to t
+   */
+  bool operator<=(const Term& t) const;
+
+  /**
+   * Comparison for ordering on terms.
+   * @param t the term to compare to
+   * @return true if this term is greater than or equal to t
+   */
+  bool operator>=(const Term& t) const;
+
+  /**
+   * Returns the number of children of this term.
+   *
+   * @return the number of term
+   */
+  size_t getNumChildren() const;
+
+  /**
+   * Get the child term at a given index.
+   * @param index the index of the child term to return
+   * @return the child term with the given index
+   */
+  Term operator[](size_t index) const;
+
+  /**
    * @return the id of this term
    */
   uint64_t getId() const;
@@ -737,6 +854,18 @@ class CVC4_PUBLIC Term
   Sort getSort() const;
 
   /**
+   * @return the result of replacing "e" by "replacement" in this term
+   */
+  Term substitute(Term e, Term replacement) const;
+
+  /**
+   * @return the result of simulatenously replacing "es" by "replacements" in
+   * this term
+   */
+  Term substitute(const std::vector<Term> es,
+                  const std::vector<Term>& replacements) const;
+
+  /**
    * @return true iff this term has an operator
    */
   bool hasOp() const;
@@ -753,6 +882,13 @@ class CVC4_PUBLIC Term
   bool isNull() const;
 
   /**
+   * Check if this is a Term representing a constant.
+   *
+   * @return true if a constant Term
+   */
+  bool isConst() const;
+
+  /**
    * Boolean negation.
    * @return the Boolean negation of this term
    */
@@ -1205,10 +1341,8 @@ class CVC4_PUBLIC DatatypeSelector
    */
   ~DatatypeSelector();
 
-  /**
-   * @return true if this datatype selector has been resolved.
-   */
-  bool isResolved() const;
+  /** @return the name of this Datatype selector. */
+  std::string getName() const;
 
   /**
    * Get the selector operator of this datatype selector.
@@ -1262,10 +1396,8 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   ~DatatypeConstructor();
 
-  /**
-   * @return true if this datatype constructor has been resolved.
-   */
-  bool isResolved() const;
+  /** @return the name of this Datatype constructor. */
+  std::string getName() const;
 
   /**
    * Get the constructor operator of this datatype constructor.
@@ -1274,6 +1406,24 @@ class CVC4_PUBLIC DatatypeConstructor
   Term getConstructorTerm() const;
 
   /**
+   * Get the tester operator of this datatype constructor.
+   * @return the tester operator
+   */
+  Term getTesterTerm() const;
+
+  /**
+   * @return the tester name for this Datatype constructor.
+   */
+  std::string getTesterName() const;
+
+  /**
+   * @return the number of selectors (so far) of this Datatype constructor.
+   */
+  size_t getNumSelectors() const;
+
+  /** @return the i^th DatatypeSelector. */
+  DatatypeSelector operator[](size_t index) const;
+  /**
    * Get the datatype selector with the given name.
    * This is a linear search through the selectors, so in case of
    * multiple, similarly-named selectors, the first is returned.
@@ -1387,6 +1537,12 @@ class CVC4_PUBLIC DatatypeConstructor
 
  private:
   /**
+   * Return selector for name.
+   * @param name The name of selector to find
+   * @return the selector object for the name
+   */
+  DatatypeSelector getSelectorForName(const std::string& name) const;
+  /**
    * The internal datatype constructor wrapped by this datatype constructor.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
    * not ref counted.
@@ -1445,12 +1601,36 @@ class CVC4_PUBLIC Datatype
    */
   Term getConstructorTerm(const std::string& name) const;
 
-  /** Get the number of constructors for this Datatype. */
+  /** @return the name of this Datatype. */
+  std::string getName() const;
+
+  /** @return the number of constructors for this Datatype. */
   size_t getNumConstructors() const;
 
-  /** Is this Datatype parametric? */
+  /** @return true if this datatype is parametric */
   bool isParametric() const;
 
+  /** @return true if this datatype corresponds to a co-datatype */
+  bool isCodatatype() const;
+
+  /** @return true if this datatype corresponds to a tuple */
+  bool isTuple() const;
+
+  /** @return true if this datatype corresponds to a record */
+  bool isRecord() const;
+
+  /** @return true if this datatype is finite */
+  bool isFinite() const;
+
+  /**
+   * Is this datatype well-founded? If this datatype is not a codatatype,
+   * this returns false if there are no values of this datatype that are of
+   * finite size.
+   *
+   * @return true if this datatype is well-founded
+   */
+  bool isWellFounded() const;
+
   /**
    * @return a string representation of this datatype
    */
@@ -1545,6 +1725,12 @@ class CVC4_PUBLIC Datatype
 
  private:
   /**
+   * Return constructor for name.
+   * @param name The name of constructor to find
+   * @return the constructor object for the name
+   */
+  DatatypeConstructor getConstructorForName(const std::string& name) const;
+  /**
    * The internal datatype wrapped by this datatype.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
    * not ref counted.