Add missing methods involving datatype sorts to the API (#5290)

This is required for migrating the parser's symbol table from Expr -> Term.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 9b34b07cd44d99b6565807063412318e2346a595..bda88c53995a11888699fe40692f9c9d24691dd5 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1098,6 +1098,37 @@ Sort Sort::getConstructorCodomainSort() const
   return Sort(d_solver, ConstructorType(*d_type).getRangeType());
 }
 
+/* Selector sort ------------------------------------------------------- */
+
+Sort Sort::getSelectorDomainSort() const
+{
+  CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
+  TypeNode typeNode = TypeNode::fromType(*d_type);
+  return Sort(d_solver, typeNode.getSelectorDomainType().toType());
+}
+
+Sort Sort::getSelectorCodomainSort() const
+{
+  CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
+  TypeNode typeNode = TypeNode::fromType(*d_type);
+  return Sort(d_solver, typeNode.getSelectorRangeType().toType());
+}
+
+/* Tester sort ------------------------------------------------------- */
+
+Sort Sort::getTesterDomainSort() const
+{
+  CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
+  TypeNode typeNode = TypeNode::fromType(*d_type);
+  return Sort(d_solver, typeNode.getTesterDomainType().toType());
+}
+
+Sort Sort::getTesterCodomainSort() const
+{
+  CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
+  return d_solver->getBooleanSort();
+}
+
 /* Function sort ------------------------------------------------------- */
 
 size_t Sort::getFunctionArity() const

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 99e67dd2ae93176e33f254a11eb7a5b47a30023f..646695c648bc71c3a78ae32398def0ef44041fec 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -506,6 +506,30 @@ class CVC4_PUBLIC Sort
    */
   Sort getConstructorCodomainSort() const;
 
+  /* Selector sort ------------------------------------------------------- */
+
+  /**
+   * @return the domain sort of a selector sort
+   */
+  Sort getSelectorDomainSort() const;
+
+  /**
+   * @return the codomain sort of a selector sort
+   */
+  Sort getSelectorCodomainSort() const;
+
+  /* Tester sort ------------------------------------------------------- */
+
+  /**
+   * @return the domain sort of a tester sort
+   */
+  Sort getTesterDomainSort() const;
+
+  /**
+   * @return the codomain sort of a tester sort, which is the Boolean sort
+   */
+  Sort getTesterCodomainSort() const;
+
   /* Function sort ------------------------------------------------------- */
 
   /**

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e917a9d0d75261a81680a2b0613f10201a37fd73..b9b72e0c5b6b8f7450f648d2b0fa3595b74c690c 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -347,6 +347,12 @@ bool TypeNode::isComparableTo(TypeNode t) const {
   return false;
 }
 
+TypeNode TypeNode::getTesterDomainType() const
+{
+  Assert(isTester());
+  return (*this)[0];
+}
+
 TypeNode TypeNode::getSequenceElementType() const
 {
   Assert(isSequence());

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9ed952369838119d59fe410444eba2f83a6dd46a..57cdfc43bc7275e8d037d23dd5280a63aa0c98f7 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -539,6 +539,9 @@ public:
   /** Get the return type (for selector types) */
   TypeNode getSelectorRangeType() const;
 
+  /** Get the domain type (for tester types) */
+  TypeNode getTesterDomainType() const;
+
   /** Get the element type (for set types) */
   TypeNode getSetElementType() const;
 

diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 02e5d814da2e2f9e5942d9f415566a7d787d6c3a..60b2dd299f58fddb120417e21de633f551d15a8b 100644 (file)
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -114,11 +114,20 @@ void SortBlack::testDatatypeSorts()
   // get tester
   Term isConsTerm = dcons.getTesterTerm();
   TS_ASSERT(isConsTerm.getSort().isTester());
+  TS_ASSERT(isConsTerm.getSort().getTesterDomainSort() == dtypeSort);
+  Sort booleanSort = d_solver.getBooleanSort();
+  TS_ASSERT(isConsTerm.getSort().getTesterCodomainSort() == booleanSort);
+  TS_ASSERT_THROWS(booleanSort.getTesterDomainSort(), CVC4ApiException&);
+  TS_ASSERT_THROWS(booleanSort.getTesterCodomainSort(), CVC4ApiException&);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
   Term tailTerm = dselTail.getSelectorTerm();
   TS_ASSERT(tailTerm.getSort().isSelector());
+  TS_ASSERT(tailTerm.getSort().getSelectorDomainSort() == dtypeSort);
+  TS_ASSERT(tailTerm.getSort().getSelectorCodomainSort() == dtypeSort);
+  TS_ASSERT_THROWS(booleanSort.getSelectorDomainSort(), CVC4ApiException&);
+  TS_ASSERT_THROWS(booleanSort.getSelectorCodomainSort(), CVC4ApiException&);
 }
 
 void SortBlack::testInstantiate()