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 /examples | |
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 'examples')
-rw-r--r-- | examples/api/java/CMakeLists.txt | 2 | ||||
-rw-r--r-- | examples/api/java/FloatingPointArith.java | 118 |
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; + } +} |