diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-22 18:22:16 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-25 13:42:38 -0400 |
commit | bb9df6c45dbc74b7bed51c2fcfc98294f80bb5c4 (patch) | |
tree | 95949af309e6527a9d3ed01bdbddf7b8e6d1020b /src | |
parent | 2a734a31217cd17bd1d51abb621b0cb409973285 (diff) |
make emptyset construction with no arguments private
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/util/emptyset.h | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8590229a2..457c9c82f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1115,7 +1115,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } | EMPTYSET_TOK - { expr = MK_CONST( ::CVC4::EmptySet()); } + { expr = MK_CONST( ::CVC4::EmptySet(Type())); } // NOTE: Theory constants go here ; diff --git a/src/util/emptyset.h b/src/util/emptyset.h index 2f6c54173..43a868e42 100644 --- a/src/util/emptyset.h +++ b/src/util/emptyset.h @@ -35,10 +35,14 @@ class CVC4_PUBLIC EmptySet { const SetType d_type; + EmptySet() { } public: - EmptySet() { } /* Null typed */ - EmptySet(SetType t):d_type(t) { } + /** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ + EmptySet(SetType setType):d_type(setType) { } ~EmptySet() throw() { |