From 252a8fb4323fed6eb621a4f88a06abfc39307b76 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 21 Jun 2019 22:29:01 -0700 Subject: [PATCH] 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. --- examples/api/java/CMakeLists.txt | 2 + examples/api/java/FloatingPointArith.java | 118 ++++++++++++++++++++++ src/bindings/java/CMakeLists.txt | 13 +++ src/cvc4.i | 2 + src/expr/expr.i | 18 ++-- src/expr/expr_manager.i | 22 ++-- src/util/floatingpoint.i | 13 +++ 7 files changed, 169 insertions(+), 19 deletions(-) create mode 100644 examples/api/java/FloatingPointArith.java 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; + } +} 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 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; #endif %template(getConstArrayStoreAll) CVC4::Expr::getConst; -%template(getConstBitVectorSize) CVC4::Expr::getConst; %template(getConstAscriptionType) CVC4::Expr::getConst; +%template(getConstBitVector) CVC4::Expr::getConst; %template(getConstBitVectorBitOf) CVC4::Expr::getConst; -%template(getConstBitVectorRepeat) CVC4::Expr::getConst; %template(getConstBitVectorExtract) CVC4::Expr::getConst; +%template(getConstBitVectorRepeat) CVC4::Expr::getConst; %template(getConstBitVectorRotateLeft) CVC4::Expr::getConst; +%template(getConstBitVectorRotateRight) CVC4::Expr::getConst; %template(getConstBitVectorSignExtend) CVC4::Expr::getConst; +%template(getConstBitVectorSize) CVC4::Expr::getConst; %template(getConstBitVectorZeroExtend) CVC4::Expr::getConst; -%template(getConstBitVectorRotateRight) CVC4::Expr::getConst; -%template(getConstUninterpretedConstant) CVC4::Expr::getConst; -%template(getConstKind) CVC4::Expr::getConst; +%template(getConstBoolean) CVC4::Expr::getConst; %template(getConstDatatypeIndexConstant) CVC4::Expr::getConst; +%template(getConstEmptySet) CVC4::Expr::getConst; +%template(getConstFloatingPoint) CVC4::Expr::getConst; +%template(getConstKind) CVC4::Expr::getConst; %template(getConstRational) CVC4::Expr::getConst; -%template(getConstBitVector) CVC4::Expr::getConst; +%template(getConstRoundingMode) CVC4::Expr::getConst; %template(getConstString) CVC4::Expr::getConst; -%template(getConstEmptySet) CVC4::Expr::getConst; -%template(getConstBoolean) CVC4::Expr::getConst; +%template(getConstUninterpretedConstant) CVC4::Expr::getConst; #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; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; +%template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; 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 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" -- 2.30.2