From: Tim King <taking@cs.nyu.edu>
Date: Wed, 15 Nov 2017 15:22:08 +0000 (-0800)
Subject: Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 and 136293... 
X-Git-Tag: cvc5-1.0.0~5473
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35b57e733af6e1588cd3b8625db932fb1d66a9a2;p=cvc5.git

Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 and 1362931. (#1373)
---

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4f1fc82b1..a8cd83215 100644
--- 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 3e6d13046..da0a9813f 100644
--- 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;