make emptyset construction with no arguments private

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8590229a2017407e8abd7aec9a1212be8b4446ba..457c9c82f2e90ba6064d8e3a30a54e654acd89b5 100644 (file)
--- 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 2f6c54173e6cc763026e6dc95eda459779e0294a..43a868e423cfbd9c0214315db3cac05d402bdb37 100644 (file)
--- 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() {