Allow sygus with no syntactic restrictions for LIA. Add regressions.

2 files changed, 11 insertions, 3 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 18ef25e7f..948bad56c 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -134,12 +134,13 @@ void Datatype::addConstructor(const DatatypeConstructor& c) {
 }
 
 
-void Datatype::setSygus( Type st, Expr bvl, bool allow_const ){
+void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
   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;
+  d_sygus_allow_const = allow_const || allow_all;
+  d_sygus_allow_const = allow_all;
 }
 
 
@@ -475,6 +476,10 @@ bool Datatype::getSygusAllowConst() const {
   return d_sygus_allow_const;
 }
 
+bool Datatype::getSygusAllowAll() 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 79e7bf7d7..224ac89ad 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -457,6 +457,7 @@ private:
   Type d_sygus_type;
   Expr d_sygus_bvl;  
   bool d_sygus_allow_const;
+  bool d_sygus_allow_all;
 
   // "mutable" because computing the cardinality can be expensive,
   // and so it's computed just once, on demand---this is the cache
@@ -537,7 +538,7 @@ public:
    *    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, bool allow_const );
+  void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all );
   
   /** Get the name of this Datatype. */
   inline std::string getName() const throw();
@@ -668,6 +669,8 @@ public:
   Expr getSygusVarList() const;
   /** does it allow constants */
   bool getSygusAllowConst() const;
+  /** does it allow constants */
+  bool getSygusAllowAll() const;
 
   /**
    * Get whether this datatype involves an external type.  If so,