2 files changed, 39 insertions, 0 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 7813626a7..c15e103f9 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -140,6 +140,14 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
   d_constructors.push_back(c);
 }
 
+
+void Datatype::setSygusType( Type st ){
+  CheckArgument(!d_resolved, this,
+                "cannot set sygus type to a finalized Datatype");
+  d_sygus_type = st;
+}
+
+
 Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
 
@@ -543,6 +551,15 @@ DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
   CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }
 
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester, Expr sygus_op) :
+  d_name(name + '\0' + tester),
+  d_tester(),
+  d_args(),
+  d_sygus_op(sygus_op) {
+  CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+  CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+}
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
@@ -611,6 +628,11 @@ Expr DatatypeConstructor::getTester() const {
   return d_tester;
 }
 
+Expr DatatypeConstructor::getSygusOp() const {
+  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  return d_sygus_op;
+}
+
 Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 32fae8235..084202956 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -185,6 +185,8 @@ private:
   Expr d_constructor;
   Expr d_tester;
   std::vector<DatatypeConstructorArg> d_args;
+  /** the operator associated with this constructor (for sygus) */
+  Expr d_sygus_op;
 
   void resolve(ExprManager* em, DatatypeType self,
                const std::map<std::string, DatatypeType>& resolutions,
@@ -223,6 +225,7 @@ public:
    * constructor and tester aren't created until resolution time.
    */
   DatatypeConstructor(std::string name, std::string tester);
+  DatatypeConstructor(std::string name, std::string tester, Expr sygus_op);
 
   /**
    * Add an argument (i.e., a data field) of the given name and type
@@ -268,6 +271,9 @@ public:
    * Datatype must be resolved.
    */
   Expr getTester() const;
+  
+  /** get sygus op */
+  Expr getSygusOp() const;
 
   /**
    * Get the tester name for this Datatype constructor.
@@ -453,6 +459,7 @@ private:
   bool d_resolved;
   Type d_self;
   bool d_involvesExt;
+  Type d_sygus_type;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -510,6 +517,9 @@ public:
    */
   void addConstructor(const DatatypeConstructor& c);
 
+  /** set the sygus type of this datatype */
+  void setSygusType( Type st );
+  
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
 
@@ -530,6 +540,9 @@ public:
 
   /** is this a co-datatype? */
   inline bool isCodatatype() const;
+  
+  /** is this a sygus datatype? */
+  inline bool isSygus() const;
 
   /**
    * Return the cardinality of this datatype (the sum of the
@@ -720,6 +733,10 @@ inline bool Datatype::isCodatatype() const {
   return d_isCo;
 }
 
+inline bool Datatype::isSygus() const {
+  return !d_sygus_type.isNull();
+}
+
 inline bool Datatype::operator!=(const Datatype& other) const throw() {
   return !(*this == other);
 }