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
|
%{
#include "expr/expr_manager.h"
%}
%typemap(javacode) CVC4::ExprManager %{
// a ref is kept here to keep Java GC from collecting the Options
// before the ExprManager
private Object options;
%}
%typemap(javaconstruct) ExprManager {
this($imcall, true);
this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
}
%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::ExprManager {
SmtEngine.dlRef(options);
options = null;
if (swigCPtr != 0) {
if (swigCMemOwn) {
swigCMemOwn = false;
CVC4JNI.delete_ExprManager(swigCPtr);
}
swigCPtr = 0;
}
}
#ifdef SWIGOCAML
/* OCaml bindings cannot deal with this degree of overloading */
%ignore CVC4::ExprManager::mkExpr(Kind, const std::vector<Expr>&);
%ignore CVC4::ExprManager::mkExpr(Kind, Expr, const std::vector<Expr>&);
%ignore CVC4::ExprManager::mkExpr(Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr, Expr);
%ignore CVC4::ExprManager::mkExpr(Expr, const std::vector<Expr>&);
#endif /* SWIGOCAML */
%ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
%include "expr/expr_manager.h"
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::SubrangeBounds>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSignExtend>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorZeroExtend>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::IntToBitVector>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>;
//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Predicate>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RegExp>;
%template(mkConst) CVC4::ExprManager::mkConst<bool>;
%include "expr/expr_manager.h"
|
