Merge pull request #440 from sosy-lab/feat/improve-fp-documentation

FP theory: improve documentation and tests.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

@@ -298,8 +298,16 @@ FloatingPointFormula castFrom(
 
   FloatingPointFormula abs(FloatingPointFormula number);
 
+  /**
+   * Returns the maximum value of the two given floating-point numbers. If one of the numbers is
+   * NaN, the other number is returned.
+   */
   FloatingPointFormula max(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Returns the minimum value of the two given floating-point numbers. If one of the numbers is
+   * NaN, the other number is returned.
+   */
   FloatingPointFormula min(FloatingPointFormula number1, FloatingPointFormula number2);
 
   FloatingPointFormula sqrt(FloatingPointFormula number);
@@ -345,36 +353,118 @@ FloatingPointFormula multiply(
 
   /**
    * Create a term for assigning one floating-point term to another. This means both terms are
-   * considered equal afterwards. This method is the same as the method <code>equal</code> for other
-   * theories.
+   * considered equal afterward, based on their bit pattern (i.e., <code>0.0 != -0
+   * .0</code> and <code>NaN ==/!= NaN</code>, depending on the bit pattern of each NaN). This
+   * method is the same as the method <code>equal</code> for other theories.
    */
   BooleanFormula assignment(FloatingPointFormula number1, FloatingPointFormula number2);
 
   /**
    * Create a term for comparing the equality of two floating-point terms, according to standard
-   * floating-point semantics (i.e., NaN != NaN). Be careful to not use this method when you really
-   * need {@link #assignment(FloatingPointFormula, FloatingPointFormula)}.
+   * floating-point semantics (i.e., <code>NaN != NaN</code> and <code>0.0 == -0.0</code>). Be
+   * careful to not use this method when you really need {@link #assignment(FloatingPointFormula,
+   * FloatingPointFormula)}.
    */
   BooleanFormula equalWithFPSemantics(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Returns whether an FP number is greater than another FP number. If one of the numbers is NaN,
+   * the result is always false.
+   */
   BooleanFormula greaterThan(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Returns whether an FP number is greater or equal than another FP number. If one of the numbers
+   * is NaN, the result is always false.
+   */
   BooleanFormula greaterOrEquals(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Returns whether an FP number is less than another FP number. If one of the numbers is NaN, the
+   * result is always false.
+   */
   BooleanFormula lessThan(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Returns whether an FP number is less or equal than another FP number. If one of the numbers is
+   * NaN, the result is always false.
+   */
   BooleanFormula lessOrEquals(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  /**
+   * Check whether a floating-point number is NaN.
+   *
+   * <p>The bit patterns for NaN in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=? (irrelevant for NaN)
+   *   <li>exponent=11...11 (all bits are 1)
+   *   <li>mantissa!=00...00 (mantissa is not all 0)
+   * </ul>
+   */
   BooleanFormula isNaN(FloatingPointFormula number);
 
+  /**
+   * Checks whether a formula is positive or negative infinity.
+   *
+   * <p>The bit patterns for infinity in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=? (0 for +Inf, 1 for -Inf)
+   *   <li>exponent=11...11 (all bits are 1)
+   *   <li>mantissa=00...00 (all bits are 0)
+   * </ul>
+   */
   BooleanFormula isInfinity(FloatingPointFormula number);
 
+  /**
+   * Checks whether a formula is positive or negative zero.
+   *
+   * <p>The bit patterns for zero in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=? (0 for +0, 1 for -0)
+   *   <li>exponent=00...00 (all bits are 0)
+   *   <li>mantissa=00...00 (all bits are 0)
+   * </ul>
+   */
   BooleanFormula isZero(FloatingPointFormula number);
 
+  /**
+   * Checks whether a formula is normal FP number.
+   *
+   * <p>The bit patterns for normal FP numbers in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=? (0 for positive numbers, 1 for negative numbers)
+   *   <li>exponent!=00...00 and exponent!=11...11 (exponent is not all 0 or all 1)
+   *   <li>mantissa=? (mantissa is irrelevant)
+   * </ul>
+   */
   BooleanFormula isNormal(FloatingPointFormula number);
 
+  /**
+   * Checks whether a formula is subnormal FP number.
+   *
+   * <p>The bit patterns for subnormal FP numbers in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=? (0 for positive numbers, 1 for negative numbers)
+   *   <li>exponent=00...00 (exponent is all 0)
+   *   <li>mantissa!=00...00 (mantissa is not all 0)
+   * </ul>
+   */
   BooleanFormula isSubnormal(FloatingPointFormula number);
 
-  /** checks whether a formula is negative, including -0.0. */
+  /**
+   * Checks whether a formula is negative, including -0.0.
+   *
+   * <p>The bit patterns for negative FP numbers in SMTLIB are identical to IEEE 754:
+   *
+   * <ul>
+   *   <li>sign=1 (1 for negative numbers)
+   *   <li>number is not NaN, i.e., exponent=11...11 implies mantissa=00...00
+   * </ul>
+   */
   BooleanFormula isNegative(FloatingPointFormula number);
 }

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -190,6 +190,25 @@ public void nanAssignedNanIsTrue() throws SolverException, InterruptedException
     assertEqualsAsFormula(nan, nan);
   }
 
+  @Test
+  public void nanOrdering() throws SolverException, InterruptedException {
+    for (FloatingPointFormula other : new FloatingPointFormula[] {zero, posInf, negInf}) {
+      assertThatFormula(fpmgr.greaterThan(nan, other)).isUnsatisfiable();
+      assertThatFormula(fpmgr.greaterOrEquals(nan, other)).isUnsatisfiable();
+      assertThatFormula(fpmgr.lessThan(nan, other)).isUnsatisfiable();
+      assertThatFormula(fpmgr.lessOrEquals(nan, other)).isUnsatisfiable();
+      assertEqualsAsFormula(fpmgr.max(nan, other), other);
+      assertEqualsAsFormula(fpmgr.min(nan, other), other);
+
+      assertThatFormula(fpmgr.greaterThan(other, nan)).isUnsatisfiable();
+      assertThatFormula(fpmgr.greaterOrEquals(other, nan)).isUnsatisfiable();
+      assertThatFormula(fpmgr.lessThan(other, nan)).isUnsatisfiable();
+      assertThatFormula(fpmgr.lessOrEquals(other, nan)).isUnsatisfiable();
+      assertEqualsAsFormula(fpmgr.max(other, nan), other);
+      assertEqualsAsFormula(fpmgr.min(other, nan), other);
+    }
+  }
+
   @Test
   public void infinityOrdering() throws SolverException, InterruptedException {
     BooleanFormula order1 = fpmgr.greaterThan(posInf, zero);
@@ -320,6 +339,166 @@ public void specialValueFunctions() throws SolverException, InterruptedException
     assertThatFormula(fpmgr.isZero(minPosNormalValue)).isUnsatisfiable();
   }
 
+  @Test
+  public void specialValueFunctionsFrom32Bits() throws SolverException, InterruptedException {
+    float posInfFromBits = Float.intBitsToFloat(0x7f80_0000);
+    assertThatFormula(fpmgr.isInfinity(fpmgr.makeNumber(posInfFromBits, singlePrecType)))
+        .isTautological();
+
+    float negInfFromBits = Float.intBitsToFloat(0xff80_0000);
+    assertThatFormula(fpmgr.isInfinity(fpmgr.makeNumber(negInfFromBits, singlePrecType)))
+        .isTautological();
+
+    float zeroFromBits = Float.intBitsToFloat(0x0000_0000);
+    assertThatFormula(fpmgr.isZero(fpmgr.makeNumber(zeroFromBits, singlePrecType)))
+        .isTautological();
+
+    float negZeroFromBits = Float.intBitsToFloat(0x8000_0000);
+    assertThatFormula(fpmgr.isZero(fpmgr.makeNumber(negZeroFromBits, singlePrecType)))
+        .isTautological();
+
+    for (float nanFromBits :
+        new float[] {
+          Float.intBitsToFloat(0x7fc0_0001),
+          Float.intBitsToFloat(0x7fc0_0002),
+          Float.intBitsToFloat(0x7fc0_0003),
+          Float.intBitsToFloat(0x7fc1_2345),
+          Float.intBitsToFloat(0x7fdf_5678),
+          Float.intBitsToFloat(0x7ff0_0001),
+          // there are some more combinations for NaN, too much for one small test.
+        }) {
+      assertThatFormula(fpmgr.isNaN(fpmgr.makeNumber(nanFromBits, singlePrecType)))
+          .isTautological();
+    }
+  }
+
+  @Test
+  public void specialValueFunctionsFrom64Bits() throws SolverException, InterruptedException {
+    double posInfFromBits = Double.longBitsToDouble(0x7ff0_0000_0000_0000L);
+    assertThatFormula(fpmgr.isInfinity(fpmgr.makeNumber(posInfFromBits, doublePrecType)))
+        .isTautological();
+
+    double negInfFromBits = Double.longBitsToDouble(0xfff0_0000_0000_0000L);
+    assertThatFormula(fpmgr.isInfinity(fpmgr.makeNumber(negInfFromBits, doublePrecType)))
+        .isTautological();
+
+    double zeroFromBits = Double.longBitsToDouble(0x0000_0000_0000_0000L);
+    assertThatFormula(fpmgr.isZero(fpmgr.makeNumber(zeroFromBits, doublePrecType)))
+        .isTautological();
+
+    double negZeroFromBits = Double.longBitsToDouble(0x8000_0000_0000_0000L);
+    assertThatFormula(fpmgr.isZero(fpmgr.makeNumber(negZeroFromBits, doublePrecType)))
+        .isTautological();
+
+    for (double nanFromBits :
+        new double[] {
+          Double.longBitsToDouble(0x7ff8_0000_0000_0001L),
+          Double.longBitsToDouble(0x7ff8_0000_0000_0002L),
+          Double.longBitsToDouble(0x7ff8_0000_0000_0003L),
+          Double.longBitsToDouble(0x7ff8_1234_5678_9abcL),
+          Double.longBitsToDouble(0x7ffc_9876_5432_1001L),
+          Double.longBitsToDouble(0x7fff_ffff_ffff_fff2L),
+          // there are some more combinations for NaN, too much for one small test.
+        }) {
+      assertThatFormula(fpmgr.isNaN(fpmgr.makeNumber(nanFromBits, doublePrecType)))
+          .isTautological();
+    }
+  }
+
+  @Test
+  public void specialValueFunctionsFrom32Bits2() throws SolverException, InterruptedException {
+    requireBitvectors();
+    requireFPToBitvector();
+
+    final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
+    final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 31, 31);
+    final BitvectorFormula exponent = bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23);
+    final BitvectorFormula mantissa = bvmgr.extract(fpmgr.toIeeeBitvector(x), 22, 0);
+
+    assertThatFormula(fpmgr.isInfinity(x))
+        .isEquivalentTo(
+            bmgr.or(
+                bvmgr.equal(fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(32, 0x7f80_0000L)),
+                bvmgr.equal(fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(32, 0xff80_0000L))));
+
+    assertThatFormula(fpmgr.isZero(x))
+        .isEquivalentTo(
+            bmgr.or(
+                bvmgr.equal(fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(32, 0x0000_0000)),
+                bvmgr.equal(fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(32, 0x8000_0000L))));
+
+    assertThatFormula(fpmgr.isNormal(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))),
+                bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)))));
+
+    assertThatFormula(fpmgr.isSubnormal(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)),
+                bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))));
+
+    assertThatFormula(fpmgr.isNaN(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)),
+                bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))));
+
+    assertThatFormula(fpmgr.isNegative(x))
+        .isEquivalentTo(
+            bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))));
+  }
+
+  @Test
+  public void specialValueFunctionsFrom64Bits2() throws SolverException, InterruptedException {
+    requireBitvectors();
+    requireFPToBitvector();
+
+    final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
+    final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 63, 63);
+    final BitvectorFormula exponent = bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52);
+    final BitvectorFormula mantissa = bvmgr.extract(fpmgr.toIeeeBitvector(x), 51, 0);
+
+    assertThatFormula(fpmgr.isInfinity(x))
+        .isEquivalentTo(
+            bmgr.or(
+                bvmgr.equal(
+                    fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(64, 0x7ff0_0000_0000_0000L)),
+                bvmgr.equal(
+                    fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(64, 0xfff0_0000_0000_0000L))));
+
+    assertThatFormula(fpmgr.isZero(x))
+        .isEquivalentTo(
+            bmgr.or(
+                bvmgr.equal(
+                    fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(64, 0x0000_0000_0000_0000L)),
+                bvmgr.equal(
+                    fpmgr.toIeeeBitvector(x), bvmgr.makeBitvector(64, 0x8000_0000_0000_0000L))));
+
+    assertThatFormula(fpmgr.isNormal(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))),
+                bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)))));
+
+    assertThatFormula(fpmgr.isSubnormal(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)),
+                bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))));
+
+    assertThatFormula(fpmgr.isNaN(x))
+        .isEquivalentTo(
+            bmgr.and(
+                bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)),
+                bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))));
+
+    assertThatFormula(fpmgr.isNegative(x))
+        .isEquivalentTo(
+            bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))));
+  }
+
   @Test
   public void specialDoubles() throws SolverException, InterruptedException {
     assertThatFormula(fpmgr.assignment(fpmgr.makeNumber(Double.NaN, singlePrecType), nan))
@@ -777,10 +956,7 @@ public void fpTraversalWithRoundingMode() {
 
   @Test
   public void fpIeeeConversionTypes() {
-    assume()
-        .withMessage("FP-to-BV conversion not available for CVC4 and CVC5")
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5);
+    requireFPToBitvector();
 
     FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType);
     assertThat(mgr.getFormulaType(fpmgr.toIeeeBitvector(var)))
@@ -789,10 +965,7 @@ public void fpIeeeConversionTypes() {
 
   @Test
   public void fpIeeeConversion() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("FP-to-BV conversion not available for CVC4 and CVC5")
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5);
+    requireFPToBitvector();
 
     FloatingPointFormula var = fpmgr.makeVariable("var", singlePrecType);
     assertThatFormula(
@@ -803,10 +976,7 @@ public void fpIeeeConversion() throws SolverException, InterruptedException {
 
   @Test
   public void ieeeFpConversion() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("FP-to-BV conversion not available for CVC4 and CVC5")
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5);
+    requireFPToBitvector();
 
     BitvectorFormula var = bvmgr.makeBitvector(32, 123456789);
     assertThatFormula(
@@ -876,10 +1046,7 @@ public void checkIeeeBv2FpConversion64() throws SolverException, InterruptedExce
 
   @Test
   public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("FP-to-BV conversion not available for CVC4 and CVC5")
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5);
+    requireFPToBitvector();
 
     proveForAll(
         // makeBV(value.bits) == fromFP(makeFP(value.float))
@@ -892,10 +1059,7 @@ public void checkIeeeFp2BvConversion32() throws SolverException, InterruptedExce
 
   @Test
   public void checkIeeeFp2BvConversion64() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("FP-to-BV conversion not available for CVC4 and CVC5")
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5);
+    requireFPToBitvector();
 
     proveForAll(
         // makeBV(value.bits) == fromFP(makeFP(value.float))