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.

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>;