From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 24 Feb 2020 17:35:37 +0000 (-0600)
Subject: Add missing functions to new C++ API (#3769)
X-Git-Tag: cvc5-1.0.0~3613
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90fe2a057cdcdaea34f0a03f837159d9adb45914;p=cvc5.git

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

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
@@ -229,6 +229,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.
    */
@@ -294,6 +322,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
@@ -372,6 +417,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
    */
@@ -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;
 
@@ -721,6 +796,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
    */
@@ -736,6 +853,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
    */
@@ -752,6 +881,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.
@@ -1273,6 +1405,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
@@ -1386,6 +1536,12 @@ class CVC4_PUBLIC DatatypeConstructor
   const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
 
  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
@@ -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
    */
@@ -1544,6 +1724,12 @@ class CVC4_PUBLIC Datatype
   const CVC4::Datatype& getDatatype(void) const;
 
  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
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index b9c671a30..2d7a9c12b 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -28,6 +28,9 @@ class DatatypeBlack : public CxxTest::TestSuite
 
   void testMkDatatypeSort();
 
+  void testDatatypeStructs();
+  void testDatatypeNames();
+
  private:
   Solver d_solver;
 };
@@ -50,8 +53,117 @@ void DatatypeBlack::testMkDatatypeSort()
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
   TS_ASSERT_THROWS(d[2], CVC4ApiException&);
-  TS_ASSERT(consConstr.isResolved());
-  TS_ASSERT(nilConstr.isResolved());
   TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm());
   TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
 }
+
+void DatatypeBlack::testDatatypeStructs()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(!dt.isCodatatype());
+  TS_ASSERT(!dt.isTuple());
+  TS_ASSERT(!dt.isRecord());
+  TS_ASSERT(!dt.isFinite());
+  TS_ASSERT(dt.isWellFounded());
+  // get constructor
+  DatatypeConstructor dcons = dt[0];
+  Term consTerm = dcons.getConstructorTerm();
+  TS_ASSERT(dcons.getNumSelectors() == 2);
+  // get tester name: notice this is only to support the Z3-style datatypes
+  // prior to SMT-LIB 2.6 where testers where changed to indexed symbols.
+  TS_ASSERT_THROWS_NOTHING(dcons.getTesterName());
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
+  DatatypeConstructorDecl ca("A");
+  dtypeSpecEnum.addConstructor(ca);
+  DatatypeConstructorDecl cb("B");
+  dtypeSpecEnum.addConstructor(cb);
+  DatatypeConstructorDecl cc("C");
+  dtypeSpecEnum.addConstructor(cc);
+  Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
+  Datatype dtEnum = dtypeSortEnum.getDatatype();
+  TS_ASSERT(!dtEnum.isTuple());
+  TS_ASSERT(dtEnum.isFinite());
+
+  // create codatatype
+  DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
+  DatatypeConstructorDecl consStream("cons");
+  DatatypeSelectorDecl headStream("head", intSort);
+  consStream.addSelector(headStream);
+  DatatypeSelectorDecl tailStream("tail", DatatypeDeclSelfSort());
+  consStream.addSelector(tailStream);
+  dtypeSpecStream.addConstructor(consStream);
+  Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
+  Datatype dtStream = dtypeSortStream.getDatatype();
+  TS_ASSERT(dtStream.isCodatatype());
+  TS_ASSERT(!dtStream.isFinite());
+  // codatatypes may be well-founded
+  TS_ASSERT(dtStream.isWellFounded());
+
+  // create tuple
+  Sort tupSort = d_solver.mkTupleSort({boolSort});
+  Datatype dtTuple = tupSort.getDatatype();
+  TS_ASSERT(dtTuple.isTuple());
+  TS_ASSERT(!dtTuple.isRecord());
+  TS_ASSERT(dtTuple.isFinite());
+  TS_ASSERT(dtTuple.isWellFounded());
+
+  // create record
+  std::vector<std::pair<std::string, Sort>> fields = {
+      std::make_pair("b", boolSort), std::make_pair("i", intSort)};
+  Sort recSort = d_solver.mkRecordSort(fields);
+  TS_ASSERT(recSort.isDatatype());
+  Datatype dtRecord = recSort.getDatatype();
+  TS_ASSERT(!dtRecord.isTuple());
+  TS_ASSERT(dtRecord.isRecord());
+  TS_ASSERT(!dtRecord.isFinite());
+  TS_ASSERT(dtRecord.isWellFounded());
+}
+
+void DatatypeBlack::testDatatypeNames()
+{
+  Sort intSort = d_solver.getIntegerSort();
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(dt.getName() == std::string("list"));
+  TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil"));
+  TS_ASSERT_THROWS_NOTHING(dt["cons"]);
+  TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&);
+  TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&);
+
+  DatatypeConstructor dcons = dt[0];
+  TS_ASSERT(dcons.getName() == std::string("cons"));
+  TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head"));
+  TS_ASSERT_THROWS_NOTHING(dcons["tail"]);
+  TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&);
+
+  // get selector
+  DatatypeSelector dselTail = dcons[1];
+  TS_ASSERT(dselTail.getName() == std::string("tail"));
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 4ea29b8d7..1bac8a283 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -27,6 +27,7 @@ class SortBlack : public CxxTest::TestSuite
   void tearDown() override;
 
   void testGetDatatype();
+  void testDatatypeSorts();
   void testInstantiate();
   void testGetFunctionArity();
   void testGetFunctionDomainSorts();
@@ -47,6 +48,9 @@ class SortBlack : public CxxTest::TestSuite
   void testGetTupleLength();
   void testGetTupleSorts();
 
+  void testSortCompare();
+  void testSortSubtyping();
+
  private:
   Solver d_solver;
 };
@@ -72,6 +76,49 @@ void SortBlack::testGetDatatype()
   TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
 }
 
+void SortBlack::testDatatypeSorts()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(!dtypeSort.isConstructor());
+  TS_ASSERT_THROWS(dtypeSort.getConstructorCodomainSort(), CVC4ApiException&);
+  TS_ASSERT_THROWS(dtypeSort.getConstructorDomainSorts(), CVC4ApiException&);
+  TS_ASSERT_THROWS(dtypeSort.getConstructorArity(), CVC4ApiException&);
+
+  // get constructor
+  DatatypeConstructor dcons = dt[0];
+  Term consTerm = dcons.getConstructorTerm();
+  Sort consSort = consTerm.getSort();
+  TS_ASSERT(consSort.isConstructor());
+  TS_ASSERT(!consSort.isTester());
+  TS_ASSERT(!consSort.isSelector());
+  TS_ASSERT(consSort.getConstructorArity() == 2);
+  std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts();
+  TS_ASSERT(consDomSorts[0] == intSort);
+  TS_ASSERT(consDomSorts[1] == dtypeSort);
+  TS_ASSERT(consSort.getConstructorCodomainSort() == dtypeSort);
+
+  // get tester
+  Term isConsTerm = dcons.getTesterTerm();
+  TS_ASSERT(isConsTerm.getSort().isTester());
+
+  // get selector
+  DatatypeSelector dselTail = dcons[1];
+  Term tailTerm = dselTail.getSelectorTerm();
+  TS_ASSERT(tailTerm.getSort().isSelector());
+}
+
 void SortBlack::testInstantiate()
 {
   // instantiate parametric datatype, check should not fail
@@ -277,3 +324,37 @@ void SortBlack::testGetTupleSorts()
   Sort bvSort = d_solver.mkBitVectorSort(32);
   TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
 }
+
+void SortBlack::testSortCompare()
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort bvSort2 = d_solver.mkBitVectorSort(32);
+  TS_ASSERT(bvSort >= bvSort2);
+  TS_ASSERT(bvSort <= bvSort2);
+  TS_ASSERT((intSort > boolSort) != (intSort < boolSort));
+  TS_ASSERT((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
+}
+
+void SortBlack::testSortSubtyping()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort realSort = d_solver.getRealSort();
+  TS_ASSERT(intSort.isSubsortOf(realSort));
+  TS_ASSERT(!realSort.isSubsortOf(intSort));
+  TS_ASSERT(intSort.isComparableTo(realSort));
+  TS_ASSERT(realSort.isComparableTo(intSort));
+
+  Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
+  Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
+  TS_ASSERT(!arraySortII.isComparableTo(intSort));
+  // we do not support subtyping for arrays
+  TS_ASSERT(!arraySortII.isComparableTo(arraySortIR));
+
+  Sort setSortI = d_solver.mkSetSort(intSort);
+  Sort setSortR = d_solver.mkSetSort(realSort);
+  // we support subtyping for sets
+  TS_ASSERT(setSortI.isSubsortOf(setSortR));
+  TS_ASSERT(setSortR.isComparableTo(setSortI));
+}
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index ea619db7c..8f63c55ec 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -39,6 +39,10 @@ class TermBlack : public CxxTest::TestSuite
   void testIteTerm();
 
   void testTermAssignment();
+  void testTermCompare();
+  void testTermChildren();
+  void testSubstitute();
+  void testIsConst();
 
  private:
   Solver d_solver;
@@ -652,3 +656,101 @@ void TermBlack::testTermAssignment()
   t2 = d_solver.mkReal(2);
   TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
 }
+
+void TermBlack::testTermCompare()
+{
+  Term t1 = d_solver.mkReal(1);
+  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  TS_ASSERT(t2 >= t3);
+  TS_ASSERT(t2 <= t3);
+  TS_ASSERT((t1 > t2) != (t1 < t2));
+  TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2));
+}
+
+void TermBlack::testTermChildren()
+{
+  // simple term 2+3
+  Term two = d_solver.mkReal(2);
+  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
+  TS_ASSERT(t1[0] == two);
+  TS_ASSERT(t1.getNumChildren() == 2);
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&);
+
+  // apply term f(2)
+  Sort intSort = d_solver.getIntegerSort();
+  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+  Term f = d_solver.mkConst(fsort, "f");
+  Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
+  // due to our higher-order view of terms, we treat f as a child of APPLY_UF
+  TS_ASSERT(t2.getNumChildren() == 2);
+  TS_ASSERT_EQUALS(t2[0], f);
+  TS_ASSERT_EQUALS(t2[1], two);
+  TS_ASSERT_THROWS(tnull[0], CVC4ApiException&);
+}
+
+void TermBlack::testSubstitute()
+{
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  Term one = d_solver.mkReal(1);
+  Term ttrue = d_solver.mkTrue();
+  Term xpx = d_solver.mkTerm(PLUS, x, x);
+  Term onepone = d_solver.mkTerm(PLUS, one, one);
+
+  TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone);
+  TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx);
+  // incorrect due to type
+  TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&);
+
+  // simultaneous substitution
+  Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
+  Term xpy = d_solver.mkTerm(PLUS, x, y);
+  Term xpone = d_solver.mkTerm(PLUS, y, one);
+  std::vector<Term> es;
+  std::vector<Term> rs;
+  es.push_back(x);
+  rs.push_back(y);
+  es.push_back(y);
+  rs.push_back(one);
+  TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone);
+
+  // incorrect substitution due to arity
+  rs.pop_back();
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+
+  // incorrect substitution due to types
+  rs.push_back(ttrue);
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+
+  // null cannot substitute
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&);
+  rs.pop_back();
+  rs.push_back(tnull);
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+  es.clear();
+  rs.clear();
+  es.push_back(x);
+  rs.push_back(y);
+  TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&);
+  es.push_back(tnull);
+  rs.push_back(one);
+  TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
+}
+
+void TermBlack::testIsConst()
+{
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  Term one = d_solver.mkReal(1);
+  Term xpone = d_solver.mkTerm(PLUS, x, one);
+  Term onepone = d_solver.mkTerm(PLUS, one, one);
+  TS_ASSERT(!x.isConst());
+  TS_ASSERT(one.isConst());
+  TS_ASSERT(!xpone.isConst());
+  TS_ASSERT(!onepone.isConst());
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&);
+}