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

[cvc5.git] / src / expr / datatype.h

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index fffabac7787dc934ff914e4f13c2a3d5387efe2b..82671189778b14bc7c96e3aa17eca09f425097d6 100644 (file)
--- 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
    *