Initial work on sygusNormalForm.

2 files changed, 7 insertions, 0 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index c15e103f9..fad2719f4 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -424,6 +424,10 @@ Expr Datatype::getConstructor(std::string name) const {
   return (*this)[name].getConstructor();
 }
 
+Type Datatype::getSygusType() const {
+  return d_sygus_type;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 084202956..b91348cdb 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -632,6 +632,9 @@ public:
    * This Datatype must be resolved.
    */
   Expr getConstructor(std::string name) const;
+  
+  /** get sygus type */
+  Type getSygusType() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,