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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
%{
#include "expr/expr.h"
%}
%ignore CVC4::Expr::Expr(const Expr&);
// This is currently the only function that would require bindings for
// `std::unordered_map<Expr, Expr, ExprHashFunction>` and is better implemented
// at the Java/Python level if needed. Thus, we ignore it here.
%ignore CVC4::Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
%ignore CVC4::operator<<(std::ostream&, const Expr&);
%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
// Ignore because we would not know which ExprManager the Expr belongs to
%ignore CVC4::TypeCheckingException::getExpression() const;
%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth);
%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes);
%ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
%ignore CVC4::Expr::operator=(const Expr&);
%ignore CVC4::Expr::operator!=(const Expr&) const;
%ignore CVC4::Expr::operator bool() const;// can just use isNull()
%rename(equals) CVC4::Expr::operator==(const Expr&) const;
%rename(less) CVC4::Expr::operator<(const Expr&) const;
%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const;
%rename(greater) CVC4::Expr::operator>(const Expr&) const;
%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const;
%rename(getChild) CVC4::Expr::operator[](unsigned i) const;
#ifdef SWIGJAVA
// For the Java bindings, we implement `getExprManager()` at the Java level
// because we can't map back the C++ point to the Java object
%ignore CVC4::Expr::getExprManager() const;
%rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
%typemap(javabody) CVC4::Expr %{
private long swigCPtr;
protected boolean swigCMemOwn;
private ExprManager em;
protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
swigCMemOwn = cMemoryOwn;
swigCPtr = cPtr;
this.em = em; // keep ref to em in SWIG proxy class
}
protected static long getCPtr($javaclassname obj) {
return (obj == null) ? 0 : obj.swigCPtr;
}
public ExprManager getExprManager() throws edu.stanford.CVC4.Exception {
return this.em;
}
public JavaIteratorAdapter_Expr iterator() {
return new JavaIteratorAdapter_Expr(this.em, this);
}
%}
// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
%typemap(javaconstruct) Expr {
this(null, $imcall, true);
}
%typemap(javaconstruct) CVC4::Expr {
this(null, $imcall, true);
}
%typemap(javaout) CVC4::Expr {
return new Expr(this.em, $jnicall, true);
}
SWIG_STD_VECTOR_EM(CVC4::Expr, const CVC4::Expr&)
SWIG_STD_VECTOR_EM(std::vector<CVC4::Expr>, const std::vector<CVC4::Expr>&)
%template(vectorExpr) std::vector<CVC4::Expr>;
%typemap(javaout) std::vector<CVC4::Expr> {
return new vectorExpr(this.em, $jnicall, true);
}
%typemap(javaout) const std::vector<CVC4::Expr>& {
return new vectorExpr(this.em, $jnicall, false);
}
%template(vectorVectorExpr) std::vector<std::vector<CVC4::Expr>>;
%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected";
%typemap(javaout) const CVC4::AscriptionType& {
return new AscriptionType(this.em, $jnicall, $owner);
}
%typemap(javaout) const CVC4::EmptySet& {
return new EmptySet(this.em, $jnicall, $owner);
}
%typemap(javaout) const CVC4::ExprSequence& {
return new ExprSequence(this.em, $jnicall, $owner);
}
// Instead of Expr::begin() and end(), create an
// iterator() method on the Java side that returns a Java-style
// Iterator.
%ignore CVC4::Expr::begin() const;
%ignore CVC4::Expr::end() const;
%ignore CVC4::Expr::const_iterator;
// Expr is "iterable" on the Java side
%typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.stanford.CVC4.Expr>";
// the JavaIteratorAdapter should not be public, and implements Iterator
%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "class";
%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "java.util.Iterator<edu.stanford.CVC4.Expr>";
// add some functions to the Java side (do it here because there's no way to do these in C++)
%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "
public void remove() {
throw new java.lang.UnsupportedOperationException();
}
public edu.stanford.CVC4.Expr next() {
if(hasNext()) {
return getNext();
} else {
throw new java.util.NoSuchElementException();
}
}
"
// getNext() just allows C++ iterator access from Java-side next(), make it private
%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>::getNext() "private";
#endif /* SWIGJAVA */
#ifdef SWIGPYTHON
%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
#endif /* SWIGPYTHON */
%include "expr/expr.h"
#ifdef SWIGPYTHON
/* The python bindings on Mac OS X have trouble with this one - leave it
* out for now. */
//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
#else
%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
#endif
%template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>;
%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>;
%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>;
%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>;
%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>;
%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>;
%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>;
%template(getConstBitVectorSignExtend) CVC4::Expr::getConst<CVC4::BitVectorSignExtend>;
%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
%template(getConstBitVectorZeroExtend) CVC4::Expr::getConst<CVC4::BitVectorZeroExtend>;
%template(getConstBoolean) CVC4::Expr::getConst<bool>;
%template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>;
%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>;
%template(getConstExprSequence) CVC4::Expr::getConst<CVC4::ExprSequence>;
%template(getConstFloatingPoint) CVC4::Expr::getConst<CVC4::FloatingPoint>;
%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>;
%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
%template(getConstRoundingMode) CVC4::Expr::getConst<CVC4::RoundingMode>;
%template(getConstString) CVC4::Expr::getConst<CVC4::String>;
%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>;
#ifdef SWIGJAVA
SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Expr, CVC4::Expr)
%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>;
#endif /* SWIGJAVA */
|
