[floating-point] 두 개의 같지 않은 부동 소수점 숫자를 빼서 0을 얻을 수 있습니까?

여기서 0으로 나누기가 발생할 수있는 경우는 없습니다.

SMT 해결사 Z3는 소수점 연산 부동 정확한 IEEE을 지원합니다. Z3에게 숫자 a와 b같은 것을 찾도록 요청합시다 a != b && (a - b) == 0.

(set-info :status unknown)
(set-logic QF_FP)
(declare-fun b () (FloatingPoint 8 24))
(declare-fun a () (FloatingPoint 8 24))
(declare-fun rm () RoundingMode)
(assert
(and (not (fp.eq a b)) (fp.eq (fp.sub rm a b) +zero) true))
(check-sat)

결과는 UNSAT입니다. 그런 숫자는 없습니다.

위의 SMTLIB 문자열은 또한 Z3가 임의의 반올림 모드 ( rm) 를 선택할 수 있도록합니다 . 즉, 결과는 가능한 모든 반올림 모드 (5 개가 있음)에 적용됩니다. 그 결과 재생중인 변수가 NaN무한대 일 수도 있습니다 .

a == b로 구현됩니다 fp.eq있도록 품질 +0f과 -0f동등 비교합니다. 0과의 비교도 사용 fp.eq됩니다. 문제는 0으로 나누기를 피하는 것을 목표로하기 때문에 이것은 적절한 비교입니다.

평등 테스트는 비트 평등를 사용하여 구현 된, 경우 +0f와 -0f만드는 방법이었을 것 a - b제로. 이 답변의 잘못된 이전 버전에는 궁금한 점에 대한 모드 세부 정보가 포함되어 있습니다.

Z3 온라인 은 아직 FPA 이론을 지원하지 않습니다. 이 결과는 최신 불안정한 분기를 사용하여 얻었습니다. 다음과 같이 .NET 바인딩을 사용하여 재생할 수 있습니다.

var fpSort = context.MkFPSort32();
var aExpr = (FPExpr)context.MkConst("a", fpSort);
var bExpr = (FPExpr)context.MkConst("b", fpSort);
var rmExpr = (FPRMExpr)context.MkConst("rm", context.MkFPRoundingModeSort());
var fpZero = context.MkFP(0f, fpSort);
var subExpr = context.MkFPSub(rmExpr, aExpr, bExpr);
var constraintExpr = context.MkAnd(
        context.MkNot(context.MkFPEq(aExpr, bExpr)),
        context.MkFPEq(subExpr, fpZero),
        context.MkTrue()
    );

var smtlibString = context.BenchmarkToSMTString(null, "QF_FP", null, null, new BoolExpr[0], constraintExpr);

var solver = context.MkSimpleSolver();
solver.Assert(constraintExpr);

var status = solver.Check();
Console.WriteLine(status);

(예 : 사례를 간과 어렵 기 때문에 IEEE 부동의 질문에 대답 Z3를 사용하는 것은 좋은 NaN, -0f, +-inf) 당신이 임의의 질문을 할 수 있습니다. 사양을 해석하고 인용 할 필요가 없습니다. “이 특정 int log2(float)알고리즘이 맞습니까?” 와 같은 혼합 부동 소수점 및 정수 질문을 할 수도 있습니다 .

답변

public class Test {
    public static double calculation(double a, double b)
    {
         if (a == b)
         {
             return 0;
         }
         else
         {
             return 2 / (a - b);
         }
    }

    /**
     * @param args
     */
    public static void main(String[] args) {
        double d1 = Double.MIN_VALUE;
        double d2 = 2.0 * Double.MIN_VALUE;
        System.out.println("Result: " + calculation(d1, d2));
    }
}