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.

5 files changed, 49 insertions, 19 deletions

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 6277b2794..a94afc0a0 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -97,6 +97,18 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java
   ${CMAKE_CURRENT_BINARY_DIR}/ExprStream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToBV.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPFloatingPoint.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPGeneric.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPIEEEBitVector.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPReal.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPSignedBitVector.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPUnsignedBitVector.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToSBV.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
   ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
   ${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java
@@ -162,6 +174,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/Result.java
   ${CMAKE_CURRENT_BINARY_DIR}/RewriteRuleCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java
diff --git a/src/cvc4.i b/src/cvc4.i
index c0112c9b0..166514bc9 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -56,6 +56,7 @@ using namespace CVC4;
 #include "options/option_exception.h"
 #include "smt/command.h"
 #include "util/bitvector.h"
+#include "util/floatingpoint.h"
 #include "util/integer.h"
 #include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -313,6 +314,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/integer.i"
 %include "util/rational.i"
 %include "util/bitvector.i"
+%include "util/floatingpoint.i"
 
 // Tim: The remainder of util/.
 %include "util/bool.i"
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>;
diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i
index c66cc311d..7a57de057 100644
--- a/src/util/floatingpoint.i
+++ b/src/util/floatingpoint.i
@@ -2,4 +2,17 @@
 #include "util/floatingpoint.h"
 %}
 
+// Ignore the methods related to FloatingPointLiteral (otherwise we have to
+// wrap those classes as well)
+%ignore CVC4::FloatingPointLiteral;
+%ignore CVC4::FloatingPoint::FloatingPoint (const FloatingPointSize &oldt, const FloatingPointLiteral &oldfpl);
+%ignore CVC4::FloatingPoint::getLiteral () const;
+
+// Ignore the partial methods (otherwise we have to provide a template
+// instantiation for std::pair<FloatingPoint, bool> which is quite ugly)
+%ignore CVC4::FloatingPoint::max(const FloatingPoint &arg) const;
+%ignore CVC4::FloatingPoint::min(const FloatingPoint &arg) const;
+%ignore CVC4::FloatingPoint::convertToRational() const;
+%ignore CVC4::FloatingPoint::convertToBV(BitVectorSize width, const RoundingMode &rm, bool signedBV) const;
+
 %include "util/floatingpoint.h"