Support for arbitrary constants/variables in Sygus grammars.

2 files changed, 11 insertions, 2 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 1e310251c..18ef25e7f 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -134,11 +134,12 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 }
 
 
-void Datatype::setSygus( Type st, Expr bvl ){
+void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){
   CheckArgument(!d_resolved, this,
                 "cannot set sygus type to a finalized Datatype");
   d_sygus_type = st;
   d_sygus_bvl = bvl;
+  d_sygus_allow_const = allow_const;
 }
 
 
@@ -470,6 +471,10 @@ Expr Datatype::getSygusVarList() const {
   return d_sygus_bvl;
 }
 
+bool Datatype::getSygusAllowConst() const {
+  return d_sygus_allow_const;
+}
+
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 6e7e09fa0..79e7bf7d7 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -456,6 +456,7 @@ private:
   /** information for sygus */
   Type d_sygus_type;
   Expr d_sygus_bvl;  
+  bool d_sygus_allow_const;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -534,8 +535,9 @@ public:
   /** set the sygus information of this datatype
    *    st : the builtin type for this grammar
    *    bvl : the list of arguments for the synth-fun
+   *    allow_const : whether all constants are (implicitly) included in the grammar
    */
-  void setSygus( Type st, Expr bvl );
+  void setSygus( Type st, Expr bvl, bool allow_const );
   
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
@@ -664,6 +666,8 @@ public:
   Type getSygusType() const;
   /** get sygus var list */
   Expr getSygusVarList() const;
+  /** does it allow constants */
+  bool getSygusAllowConst() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,