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.

diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 108ab86148f2890bb068ae159086f9739a7e1fe5..dd7d6566f5b5dfce2fdae83f933b15322d9a15e7 100644 (file)
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -8,6 +8,7 @@ set(EXAMPLES_API_JAVA
   #CVC4Streams
   Combination
   Datatypes
+  FloatingPointArith
   HelloWorld
   LinearArith
   ## disabled until bindings for the new API are in place (issue #2284)
@@ -34,5 +35,6 @@ foreach(example ${EXAMPLES_API_JAVA})
         -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/api/java/"
         ${example}
   )
+  set_tests_properties(${example_test} PROPERTIES SKIP_RETURN_CODE 77)
   set_tests_properties(${example_test} PROPERTIES LABELS "example")
 endforeach()

diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
new file mode 100644 (file)
index 0000000..fe2e374
--- /dev/null
+++ b/examples/api/java/FloatingPointArith.java
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file FloatingPointArith.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief An example of solving floating-point problems with CVC4's Java API
+ **
+ ** This example shows how to check whether CVC4 was built with floating-point
+ ** support, how to create floating-point types, variables and expressions, and
+ ** how to create rounding mode constants by solving toy problems. The example
+ ** also shows making special values (such as NaN and +oo) and converting an
+ ** IEEE 754-2008 bit-vector to a floating-point number.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.util.Iterator;
+
+public class FloatingPointArith {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    // Test whether CVC4 was built with floating-point support
+    if (!Configuration.isBuiltWithSymFPU()) {
+      System.out.println("CVC4 was built without floating-point support.");
+      System.out.println("Configure with --symfpu and rebuild CVC4 to run");
+      System.out.println("this example.");
+      System.exit(77);
+    }
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    // Enable the model production
+    smt.setOption("produce-models", new SExpr(true));
+
+    // Make single precision floating-point variables
+    FloatingPointType fpt32 = em.mkFloatingPointType(8, 24);
+    Expr a = em.mkVar("a", fpt32);
+    Expr b = em.mkVar("b", fpt32);
+    Expr c = em.mkVar("c", fpt32);
+    Expr d = em.mkVar("d", fpt32);
+    Expr e = em.mkVar("e", fpt32);
+
+    // Assert that floating-point addition is not associative:
+    // (a + (b + c)) != ((a + b) + c)
+    Expr rm = em.mkConst(RoundingMode.roundNearestTiesToEven);
+    Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS,
+        rm,
+        a,
+        em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, b, c));
+    Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS,
+        rm,
+        em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, a, b),
+        c);
+    smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, a, b)));
+
+    Result r = smt.checkSat(); // result is sat
+    assert r.isSat() == Result.Sat.SAT;
+
+    System.out.println("a = " + smt.getValue(a));
+    System.out.println("b = " + smt.getValue(b));
+    System.out.println("c = " + smt.getValue(c));
+
+    // Now, let's restrict `a` to be either NaN or positive infinity
+    FloatingPointSize fps32 = new FloatingPointSize(8, 24);
+    Expr nan = em.mkConst(FloatingPoint.makeNaN(fps32));
+    Expr inf = em.mkConst(FloatingPoint.makeInf(fps32, /* sign */ true));
+    smt.assertFormula(em.mkExpr(
+        Kind.OR, em.mkExpr(Kind.EQUAL, a, inf), em.mkExpr(Kind.EQUAL, a, nan)));
+
+    r = smt.checkSat(); // result is sat
+    assert r.isSat() == Result.Sat.SAT;
+
+    System.out.println("a = " + smt.getValue(a));
+    System.out.println("b = " + smt.getValue(b));
+    System.out.println("c = " + smt.getValue(c));
+
+    // And now for something completely different. Let's try to find a (normal)
+    // floating-point number that rounds to different integer values for
+    // different rounding modes.
+    Expr rtp = em.mkConst(RoundingMode.roundTowardPositive);
+    Expr rtn = em.mkConst(RoundingMode.roundTowardNegative);
+    Expr op = em.mkConst(new FloatingPointToSBV(16)); // (_ fp.to_sbv 16)
+    lhs = em.mkExpr(op, rtp, d);
+    rhs = em.mkExpr(op, rtn, d);
+    smt.assertFormula(em.mkExpr(Kind.FLOATINGPOINT_ISN, d));
+    smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, lhs, rhs)));
+
+    r = smt.checkSat(); // result is sat
+    assert r.isSat() == Result.Sat.SAT;
+
+    // Convert the result to a rational and print it
+    Expr val = smt.getValue(d);
+    Rational realVal =
+        val.getConstFloatingPoint().convertToRationalTotal(new Rational(0));
+    System.out.println("d = " + val + " = " + realVal);
+    System.out.println("((_ fp.to_sbv 16) RTP d) = " + smt.getValue(lhs));
+    System.out.println("((_ fp.to_sbv 16) RTN d) = " + smt.getValue(rhs));
+
+    // For our final trick, let's try to find a floating-point number between
+    // positive zero and the smallest positive floating-point number
+    Expr zero = em.mkConst(FloatingPoint.makeZero(fps32, /* sign */ true));
+    Expr smallest =
+        em.mkConst(new FloatingPoint(8, 24, new BitVector(32, 0b001)));
+    smt.assertFormula(em.mkExpr(Kind.AND,
+        em.mkExpr(Kind.FLOATINGPOINT_LT, zero, e),
+        em.mkExpr(Kind.FLOATINGPOINT_LT, e, smallest)));
+
+    r = smt.checkSat(); // result is unsat
+    assert r.isSat() == Result.Sat.UNSAT;
+  }
+}

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 6277b2794812bfc3eae46d4fe7a009fbc6b6e744..a94afc0a01ae5e6ae7527e2c7b6cbb2df525db7d 100644 (file)
--- 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 c0112c9b0e753c3bf3db5a8fd67999781c25ccb5..166514bc9ff78955b773a2411569d05850fb7f54 100644 (file)
--- 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 b172f60ed2076df9730be1de556d40835cfc3913..fba1e8858710a9153ace644ab18c1621b4906225 100644 (file)
--- 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 df99af56d7b9ac9f9a39c44695adf12adbbf795d..2736e9135a50211dc163a262480b54116355d37f 100644 (file)
--- 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 c66cc311d3bbb1e519b5705054a339c1aa6aa16e..7a57de0570bac6c7519d1030d9b0e673862498e0 100644 (file)
--- 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"