From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Oct 2020 16:46:20 +0000 (-0500)
Subject: Add missing methods involving datatype sorts to the API (#5290)
X-Git-Tag: cvc5-1.0.0~2657
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=88025001599c7e5ced8d55c3769e728758434f69;p=cvc5.git

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 9b34b07cd..bda88c539 100644
--- 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 99e67dd2a..646695c64 100644
--- 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 e917a9d0d..b9b72e0c5 100644
--- 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 9ed952369..57cdfc43b 100644
--- 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 02e5d814d..60b2dd299 100644
--- 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()