Some cleanup, fix warnings raised by Debian packager.

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 427282490979406af15a2fa295aee64f76afb08a..dd9fcdfbdcbf0ee88361676e186d0256f6c18da4 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -341,6 +341,14 @@ bool Expr::isBoundVar() const {
   return getKind() == CVC4::kind::BOUND_VARIABLE;
 }
 
+bool Expr::isForall() const {
+  return getKind() == CVC4::kind::FORALL;
+}
+
+bool Expr::isExists() const {
+  return getKind() == CVC4::kind::EXISTS;
+}
+
 bool Expr::isLambda() const {
   // when implemented, also fix isClosure() below
   Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");

diff --git a/src/expr/expr.i b/src/expr/expr.i
index c649a5ebbc7880ced816b954c7dae770a01f92d4..31788f06b0a4630592efc9941a3c7b7493fe4b50 100644 (file)
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -104,7 +104,9 @@ namespace CVC4 {
 %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
 %template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>;
 %template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>;
-%template(getConstString) CVC4::Expr::getConst<std::string>;
+%template(getConstString) CVC4::Expr::getConst<CVC4::String>;
+%template(getConstRegExp) CVC4::Expr::getConst<CVC4::RegExp>;
+%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>;
 %template(getConstBoolean) CVC4::Expr::getConst<bool>;
 
 #ifdef SWIGJAVA

diff --git a/src/util/emptyset.h b/src/util/emptyset.h
index 2d307b2d44392a4ff4d1e33e2ec1e02e2e9566a6..2f6c54173e6cc763026e6dc95eda459779e0294a 100644 (file)
--- a/src/util/emptyset.h
+++ b/src/util/emptyset.h
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file emptyset.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "cvc4_public.h"
 
@@ -30,36 +46,34 @@ public:
 
   SetType getType() const { return d_type; }
 
-  bool operator==(const EmptySet& asa) const throw() {
-    return d_type == asa.d_type;
+  bool operator==(const EmptySet& es) const throw() {
+    return d_type == es.d_type;
   }
-  bool operator!=(const EmptySet& asa) const throw() {
-    return !(*this == asa);
+  bool operator!=(const EmptySet& es) const throw() {
+    return !(*this == es);
   }
 
-  bool operator<(const EmptySet& asa) const throw() {
-    return d_type < asa.d_type;
+  bool operator<(const EmptySet& es) const throw() {
+    return d_type < es.d_type;
   }
-  bool operator<=(const EmptySet& asa) const throw() {
-    return d_type <= asa.d_type;
+  bool operator<=(const EmptySet& es) const throw() {
+    return d_type <= es.d_type;
   }
-  bool operator>(const EmptySet& asa) const throw() {
-    return !(*this <= asa);
+  bool operator>(const EmptySet& es) const throw() {
+    return !(*this <= es);
   }
-  bool operator>=(const EmptySet& asa) const throw() {
-    return !(*this < asa);
+  bool operator>=(const EmptySet& es) const throw() {
+    return !(*this < es);
   }
 
-
 };/* class EmptySet */
 
-std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC;
 
 struct CVC4_PUBLIC EmptySetHashFunction {
-  inline size_t operator()(const EmptySet& asa) const {
-    return TypeHashFunction()(asa.getType());
+  inline size_t operator()(const EmptySet& es) const {
+    return TypeHashFunction()(es.getType());
   }
-};/* struct EmptysetHashFunction */
-
+};/* struct EmptySetHashFunction */
 
-}
+}/* CVC4 namespace */