diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 22:29:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-21 22:29:01 -0700 |
commit | 252a8fb4323fed6eb621a4f88a06abfc39307b76 (patch) | |
tree | 1858636286f1c657c2fd03ec4c788db8602d1489 /src/expr/expr.i | |
parent | be33ac9656bf7feafa3715d6623749f6afd962b5 (diff) |
Add floating-point support in the Java API (#3063)
This commit adds support for the theory of floating-point numbers in the
Java API. Previously, floating-point related classes were missing in the
JAR. The commit also provides an example that showcases how to work with
the theory of floating-point numbers through the API.
Diffstat (limited to 'src/expr/expr.i')
-rw-r--r-- | src/expr/expr.i | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/expr/expr.i b/src/expr/expr.i index b172f60ed..fba1e8858 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -133,23 +133,25 @@ namespace CVC4 { %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; #endif %template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>; -%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>; %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>; +%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; %template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>; -%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>; %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(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>; -%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; -%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; +%template(getConstBoolean) CVC4::Expr::getConst<bool>; %template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>; +%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>; +%template(getConstFloatingPoint) CVC4::Expr::getConst<CVC4::FloatingPoint>; +%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; %template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; -%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; +%template(getConstRoundingMode) CVC4::Expr::getConst<CVC4::RoundingMode>; %template(getConstString) CVC4::Expr::getConst<CVC4::String>; -%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>; -%template(getConstBoolean) CVC4::Expr::getConst<bool>; +%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; #ifdef SWIGJAVA |