(Context ctx)
| 1940 | } |
| 1941 | |
| 1942 | public void floatingPointExample1(Context ctx) throws TestFailedException |
| 1943 | { |
| 1944 | System.out.println("FloatingPointExample1"); |
| 1945 | Log.append("FloatingPointExample1"); |
| 1946 | |
| 1947 | FPSort s = ctx.mkFPSort(11, 53); |
| 1948 | System.out.printf("Sort: %s%n", s); |
| 1949 | |
| 1950 | FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */ |
| 1951 | FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */ |
| 1952 | FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */ |
| 1953 | System.out.printf("x=%s; y=%s; z=%s%n", x.toString(), y.toString(), z.toString()); |
| 1954 | |
| 1955 | BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z)); |
| 1956 | check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE); |
| 1957 | |
| 1958 | /* nothing is equal to NaN according to floating-point |
| 1959 | * equality, so NaN == k should be unsatisfiable. */ |
| 1960 | FPExpr k = (FPExpr)ctx.mkConst("x", s); |
| 1961 | FPExpr nan = ctx.mkFPNaN(s); |
| 1962 | |
| 1963 | /* solver that runs the default tactic for QF_FP. */ |
| 1964 | Solver slvr = ctx.mkSolver("QF_FP"); |
| 1965 | slvr.add(ctx.mkFPEq(nan, k)); |
| 1966 | if (slvr.check() != Status.UNSATISFIABLE) |
| 1967 | throw new TestFailedException(); |
| 1968 | System.out.printf("OK, unsat:%n%s%n", slvr); |
| 1969 | |
| 1970 | /* NaN is equal to NaN according to normal equality. */ |
| 1971 | slvr = ctx.mkSolver("QF_FP"); |
| 1972 | slvr.add(ctx.mkEq(nan, nan)); |
| 1973 | if (slvr.check() != Status.SATISFIABLE) |
| 1974 | throw new TestFailedException(); |
| 1975 | System.out.printf("OK, sat:%n%s%n", slvr); |
| 1976 | |
| 1977 | /* Let's prove -1e1 * -1.25e3 == +100 */ |
| 1978 | x = (FPNum)ctx.mkNumeral("-1e1", s); |
| 1979 | y = (FPNum)ctx.mkNumeral("-1.25p3", s); |
| 1980 | FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s); |
| 1981 | FPNum r = (FPNum)ctx.mkNumeral("100", s); |
| 1982 | slvr = ctx.mkSolver("QF_FP"); |
| 1983 | |
| 1984 | slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y))); |
| 1985 | slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r))); |
| 1986 | if (slvr.check() != Status.UNSATISFIABLE) |
| 1987 | throw new TestFailedException(); |
| 1988 | System.out.printf("OK, unsat:%n%s%n", slvr); |
| 1989 | } |
| 1990 | |
| 1991 | public void floatingPointExample2(Context ctx) throws TestFailedException |
| 1992 | { |
no test coverage detected