Skip to content

Commit 005d6b0

Browse files
kfriedbergerkfriedberger
committed
FP theory: improve documentation and tests.
1 parent 2010088 commit 005d6b0

File tree

2 files changed

+23
-51
lines changed

2 files changed

+23
-51
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -438,7 +438,7 @@ FloatingPointFormula multiply(
438438
* <ul>
439439
* <li>sign=? (0 for positive numbers, 1 for negative numbers)
440440
* <li>exponent!=00...00 and exponent!=11...11 (exponent is not all 0 or all 1)
441-
* <li>mantissa!=00...00 (mantissa is not all 0)
441+
* <li>mantissa=? (mantissa is irrelevant)
442442
* </ul>
443443
*/
444444
BooleanFormula isNormal(FloatingPointFormula number);

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

+22-50
Original file line numberDiff line numberDiff line change
@@ -410,7 +410,10 @@ public void specialValueFunctionsFrom32Bits2() throws SolverException, Interrupt
410410
requireBitvectors();
411411
requireFPToBitvector();
412412

413-
FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
413+
final FloatingPointFormula x = fpmgr.makeVariable("x32", singlePrecType);
414+
final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 31, 31);
415+
final BitvectorFormula exponent = bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23);
416+
final BitvectorFormula mantissa = bvmgr.extract(fpmgr.toIeeeBitvector(x), 22, 0);
414417

415418
assertThatFormula(fpmgr.isInfinity(x))
416419
.isEquivalentTo(
@@ -427,49 +430,35 @@ public void specialValueFunctionsFrom32Bits2() throws SolverException, Interrupt
427430
assertThatFormula(fpmgr.isNormal(x))
428431
.isEquivalentTo(
429432
bmgr.and(
430-
bmgr.not(
431-
bvmgr.equal(
432-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23),
433-
bvmgr.makeBitvector(8, 0))),
434-
bmgr.not(
435-
bvmgr.equal(
436-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23),
437-
bvmgr.makeBitvector(8, -1)))));
433+
bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0))),
434+
bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)))));
438435

439436
assertThatFormula(fpmgr.isSubnormal(x))
440437
.isEquivalentTo(
441438
bmgr.and(
442-
bvmgr.equal(
443-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23), bvmgr.makeBitvector(8, 0)),
444-
bmgr.not(
445-
bvmgr.equal(
446-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 22, 0),
447-
bvmgr.makeBitvector(23, 0)))));
439+
bvmgr.equal(exponent, bvmgr.makeBitvector(8, 0)),
440+
bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))));
448441

449442
assertThatFormula(fpmgr.isNaN(x))
450443
.isEquivalentTo(
451444
bmgr.and(
452-
bvmgr.equal(
453-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 30, 23), bvmgr.makeBitvector(8, -1)),
454-
bmgr.not(
455-
bvmgr.equal(
456-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 22, 0),
457-
bvmgr.makeBitvector(23, 0)))));
445+
bvmgr.equal(exponent, bvmgr.makeBitvector(8, -1)),
446+
bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(23, 0)))));
458447

459448
assertThatFormula(fpmgr.isNegative(x))
460449
.isEquivalentTo(
461-
bmgr.and(
462-
bmgr.not(fpmgr.isNaN(x)),
463-
bvmgr.equal(
464-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 31, 31), bvmgr.makeBitvector(1, 1))));
450+
bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))));
465451
}
466452

467453
@Test
468454
public void specialValueFunctionsFrom64Bits2() throws SolverException, InterruptedException {
469455
requireBitvectors();
470456
requireFPToBitvector();
471457

472-
FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
458+
final FloatingPointFormula x = fpmgr.makeVariable("x64", doublePrecType);
459+
final BitvectorFormula signBit = bvmgr.extract(fpmgr.toIeeeBitvector(x), 63, 63);
460+
final BitvectorFormula exponent = bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52);
461+
final BitvectorFormula mantissa = bvmgr.extract(fpmgr.toIeeeBitvector(x), 51, 0);
473462

474463
assertThatFormula(fpmgr.isInfinity(x))
475464
.isEquivalentTo(
@@ -490,41 +479,24 @@ public void specialValueFunctionsFrom64Bits2() throws SolverException, Interrupt
490479
assertThatFormula(fpmgr.isNormal(x))
491480
.isEquivalentTo(
492481
bmgr.and(
493-
bmgr.not(
494-
bvmgr.equal(
495-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52),
496-
bvmgr.makeBitvector(11, 0))),
497-
bmgr.not(
498-
bvmgr.equal(
499-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52),
500-
bvmgr.makeBitvector(11, -1)))));
482+
bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0))),
483+
bmgr.not(bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)))));
501484

502485
assertThatFormula(fpmgr.isSubnormal(x))
503486
.isEquivalentTo(
504487
bmgr.and(
505-
bvmgr.equal(
506-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52), bvmgr.makeBitvector(11, 0)),
507-
bmgr.not(
508-
bvmgr.equal(
509-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 51, 0),
510-
bvmgr.makeBitvector(52, 0)))));
488+
bvmgr.equal(exponent, bvmgr.makeBitvector(11, 0)),
489+
bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))));
511490

512491
assertThatFormula(fpmgr.isNaN(x))
513492
.isEquivalentTo(
514493
bmgr.and(
515-
bvmgr.equal(
516-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 62, 52), bvmgr.makeBitvector(11, -1)),
517-
bmgr.not(
518-
bvmgr.equal(
519-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 51, 0),
520-
bvmgr.makeBitvector(52, 0)))));
494+
bvmgr.equal(exponent, bvmgr.makeBitvector(11, -1)),
495+
bmgr.not(bvmgr.equal(mantissa, bvmgr.makeBitvector(52, 0)))));
521496

522497
assertThatFormula(fpmgr.isNegative(x))
523498
.isEquivalentTo(
524-
bmgr.and(
525-
bmgr.not(fpmgr.isNaN(x)),
526-
bvmgr.equal(
527-
bvmgr.extract(fpmgr.toIeeeBitvector(x), 63, 63), bvmgr.makeBitvector(1, 1))));
499+
bmgr.and(bmgr.not(fpmgr.isNaN(x)), bvmgr.equal(signBit, bvmgr.makeBitvector(1, 1))));
528500
}
529501

530502
@Test

0 commit comments

Comments
 (0)