diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-20 19:37:30 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-20 19:37:30 +0000 |
| commit | e18075c0b0aaf637b32a4bee54bff1adb6c218ee (patch) | |
| tree | f57153d9bd0d52e8b4f70fa849b4d6397570dffa /src/expr/expr.i | |
| parent | e8e85053afba60bd6060cb07c52c88c316d73b30 (diff) | |
fixes for java bindings
Diffstat (limited to 'src/expr/expr.i')
| -rw-r--r-- | src/expr/expr.i | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/expr/expr.i b/src/expr/expr.i index 9b6c55703..34f074a6d 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -30,3 +30,26 @@ namespace CVC4 { }/* CVC4 namespace */ %include "expr/expr.h" + +%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; +%template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>; +%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>; +%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>; +%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>; +%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>; +%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>; +%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>; +%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>; +%template(getConstBitVectorSignExtend) CVC4::Expr::getConst<CVC4::BitVectorSignExtend>; +%template(getConstBitVectorZeroExtend) CVC4::Expr::getConst<CVC4::BitVectorZeroExtend>; +%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>; +%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; +%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; +%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>; +%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; +%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; +%template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>; +%template(getConstString) CVC4::Expr::getConst<std::string>; +%template(getConstBoolean) CVC4::Expr::getConst<bool>; + +%include "expr/expr.h" |