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

1 files changed, 198 insertions, 25 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)
 {