1 files changed, 28 insertions, 0 deletions
diff --git a/src/util/cardinality.i b/src/util/cardinality.i
index 760f746c0..82f67382b 100644
--- a/src/util/cardinality.i
+++ b/src/util/cardinality.i
@@ -20,4 +20,32 @@
 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
 %ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
 
+  class Beth {
+    Integer d_index;
+
+  public:
+    Beth(const Integer& beth) : d_index(beth) {
+      CheckArgument(beth >= 0, beth,
+                    "Beth index must be a nonnegative integer, not %s.",
+                    beth.toString().c_str());
+    }
+
+    const Integer& getNumber() const throw() {
+      return d_index;
+    }
+  };/* class Cardinality::Beth */
+
+  class Unknown {
+  public:
+    Unknown() throw() {}
+    ~Unknown() throw() {}
+  };/* class Cardinality::Unknown */
+
 %include "util/cardinality.h"
+
+%{
+namespace CVC4 {
+  typedef CVC4::Cardinality::Beth Beth;
+  typedef CVC4::Cardinality::Unknown Unknown;
+}
+%}