From: Tim King 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& 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& 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;