Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 and 136293...

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4f1fc82b15c3c0aaaba7127a84e8053a9273bf71..a8cd83215ddc696b9ab3e0d36d28ebcd10075ec7 100644 (file)
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -776,25 +776,27 @@ Type DatatypeConstructor::doParametricSubstitution( Type range,
   }
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name) :
-  // 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
-  // the tester name away inside the constructor name until
-  // resolution.
-  d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
-  d_tester(),
-  d_args() {
+DatatypeConstructor::DatatypeConstructor(std::string name)
+    :  // 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
+       // the tester name away inside the constructor name until
+       // resolution.
+      d_name(name + '\0' + "is_" + name),  // default tester name is "is_FOO"
+      d_tester(),
+      d_args(),
+      d_sygus_num_let_input_args(0) {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
 }
 
-DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
-  // 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
-  // the tester name away inside the constructor name until
-  // resolution.
-  d_name(name + '\0' + tester),
-  d_tester(),
-  d_args() {
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester)
+    :  // 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
+       // the tester name away inside the constructor name until
+       // resolution.
+      d_name(name + '\0' + tester),
+      d_tester(),
+      d_args(),
+      d_sygus_num_let_input_args(0) {
   PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
   PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
 }

diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 3e6d13046f20566dc38803dbc47c359fedfffec0..da0a9813f40d7bfb9cac514c2f1b88a7fe4b4e41 100644 (file)
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -1117,37 +1117,40 @@ inline std::string DatatypeUnresolvedType::getName() const throw() {
   return d_name;
 }
 
-inline Datatype::Datatype(std::string name, bool isCo) :
-  d_name(name),
-  d_params(),
-  d_isCo(isCo),
-  d_isTuple(false),
-  d_isRecord(false),
-  d_record(NULL),
-  d_constructors(),
-  d_resolved(false),
-  d_self(),
-  d_involvesExt(false),
-  d_involvesUt(false),
-  d_card(CardinalityUnknown()),
-  d_well_founded(0) {
-}
-
-inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) :
-  d_name(name),
-  d_params(params),
-  d_isCo(isCo),
-  d_isTuple(false),
-  d_isRecord(false),
-  d_record(NULL),
-  d_constructors(),
-  d_resolved(false),
-  d_self(),
-  d_involvesExt(false),
-  d_involvesUt(false),
-  d_card(CardinalityUnknown()),
-  d_well_founded(0) {
-}
+inline Datatype::Datatype(std::string name, bool isCo)
+    : d_name(name),
+      d_params(),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_isRecord(false),
+      d_record(NULL),
+      d_constructors(),
+      d_resolved(false),
+      d_self(),
+      d_involvesExt(false),
+      d_involvesUt(false),
+      d_sygus_allow_const(false),
+      d_sygus_allow_all(false),
+      d_card(CardinalityUnknown()),
+      d_well_founded(0) {}
+
+inline Datatype::Datatype(std::string name, const std::vector<Type>& params,
+                          bool isCo)
+    : d_name(name),
+      d_params(params),
+      d_isCo(isCo),
+      d_isTuple(false),
+      d_isRecord(false),
+      d_record(NULL),
+      d_constructors(),
+      d_resolved(false),
+      d_self(),
+      d_involvesExt(false),
+      d_involvesUt(false),
+      d_sygus_allow_const(false),
+      d_sygus_allow_all(false),
+      d_card(CardinalityUnknown()),
+      d_well_founded(0) {}
 
 inline std::string Datatype::getName() const throw() {
   return d_name;