src/util/cardinality.i

   1 %{
   2 #include "util/cardinality.h"
   3 %}
   4
   5 %feature("valuewrapper") CVC4::Cardinality::Beth;
   6
   7 %rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&);
   8 %rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&);
   9 %rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&);
  10 %rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const;
  11 %rename(times) CVC4::Cardinality::operator*(const Cardinality&) const;
  12 %rename(power) CVC4::Cardinality::operator^(const Cardinality&) const;
  13 %rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const;
  14 %ignore CVC4::Cardinality::operator!=(const Cardinality&) const;
  15 %rename(less) CVC4::Cardinality::operator<(const Cardinality&) const;
  16 %rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const;
  17 %rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const;
  18 %rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const;
  19
  20 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
  21 %ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
  22
  23 namespace CVC4 {
  24   class Beth {
  25     Integer d_index;
  26
  27   public:
  28     Beth(const Integer& beth) : d_index(beth) {
  29       CheckArgument(beth >= 0, beth,
  30                     "Beth index must be a nonnegative integer, not %s.",
  31                     beth.toString().c_str());
  32     }
  33
  34     const Integer& getNumber() const throw() {
  35       return d_index;
  36     }
  37   };/* class Cardinality::Beth */
  38
  39   class Unknown {
  40   public:
  41     Unknown() throw() {}
  42     ~Unknown() throw() {}
  43   };/* class Cardinality::Unknown */
  44 }
  45
  46 %include "util/cardinality.h"
  47
  48 %{
  49 namespace CVC4 {
  50   typedef CVC4::Cardinality::Beth Beth;
  51   typedef CVC4::Cardinality::Unknown Unknown;
  52 }
  53 %}