blob: 4e1382f87c4a691fce99531aee78faf94f7a6029 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
%{
#include "util/cardinality.h"
%}
%feature("valuewrapper") CVC4::Cardinality::Beth;
%rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&);
%rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&);
%rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&);
%rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const;
%rename(times) CVC4::Cardinality::operator*(const Cardinality&) const;
%rename(power) CVC4::Cardinality::operator^(const Cardinality&) const;
%rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const;
%ignore CVC4::Cardinality::operator!=(const Cardinality&) const;
%rename(less) CVC4::Cardinality::operator<(const Cardinality&) const;
%rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const;
%rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const;
%rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const;
%ignore CVC4::operator<<(std::ostream&, const Cardinality&);
%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
namespace CVC4 {
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;
}
%}
|