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, 120 insertions, 0 deletions

diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 108ab8614..dd7d6566f 100644
--- 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
index 000000000..fe2e3747e
--- /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;
+  }
+}