From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 22 Jun 2014 22:22:16 +0000 (-0400)
Subject: make emptyset construction with no arguments private
X-Git-Tag: cvc5-1.0.0~6712^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb9df6c45dbc74b7bed51c2fcfc98294f80bb5c4;p=cvc5.git

make emptyset construction with no arguments private
---

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() {