Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)

2 files changed, 11 insertions, 0 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index bcd3a0784..d697a6aaf 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1141,6 +1141,12 @@ Expr DatatypeConstructor::getSelector(std::string name) const {
   return (*this)[name].getSelector();
 }
 
+Type DatatypeConstructor::getArgType(unsigned index) const
+{
+  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+  return static_cast<SelectorType>((*this)[index].getType()).getRangeType();
+}
+
 bool DatatypeConstructor::involvesExternalType() const{
   for(const_iterator i = begin(); i != end(); ++i) {
     if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index fffabac77..826711897 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -390,6 +390,11 @@ class CVC4_PUBLIC DatatypeConstructor {
    * is returned.
    */
   Expr getSelector(std::string name) const;
+  /**
+   * Get argument type. Returns the return type of the i^th selector of this
+   * constructor.
+   */
+  Type getArgType(unsigned i) const;
 
   /** get selector internal
    *