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 | |
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')
-rw-r--r-- | src/expr/expr.i | 18 | ||||
-rw-r--r-- | src/expr/expr_manager.i | 22 |
2 files changed, 21 insertions, 19 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 diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index df99af56d..2736e9135 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -51,17 +51,17 @@ %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::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::DatatypeIndexConstant>; |