(Context ctx)
| 2134 | } |
| 2135 | |
| 2136 | public void floatingPointExample1(Context ctx) throws TestFailedException |
| 2137 | { |
| 2138 | System.out.println("FloatingPointExample1"); |
| 2139 | Log.append("FloatingPointExample1"); |
| 2140 | |
| 2141 | FPSort s = ctx.mkFPSort(11, 53); |
| 2142 | System.out.println("Sort: " + s); |
| 2143 | |
| 2144 | FPNum x = (FPNum)ctx.mkNumeral("-1e1", s); /* -1 * 10^1 = -10 */ |
| 2145 | FPNum y = (FPNum)ctx.mkNumeral("-10", s); /* -10 */ |
| 2146 | FPNum z = (FPNum)ctx.mkNumeral("-1.25p3", s); /* -1.25 * 2^3 = -1.25 * 8 = -10 */ |
| 2147 | System.out.println("x=" + x.toString() + |
| 2148 | "; y=" + y.toString() + |
| 2149 | "; z=" + z.toString()); |
| 2150 | |
| 2151 | BoolExpr a = ctx.mkAnd(ctx.mkFPEq(x, y), ctx.mkFPEq(y, z)); |
| 2152 | check(ctx, ctx.mkNot(a), Status.UNSATISFIABLE); |
| 2153 | |
| 2154 | /* nothing is equal to NaN according to floating-point |
| 2155 | * equality, so NaN == k should be unsatisfiable. */ |
| 2156 | FPExpr k = (FPExpr)ctx.mkConst("x", s); |
| 2157 | FPExpr nan = ctx.mkFPNaN(s); |
| 2158 | |
| 2159 | /* solver that runs the default tactic for QF_FP. */ |
| 2160 | Solver slvr = ctx.mkSolver("QF_FP"); |
| 2161 | slvr.add(ctx.mkFPEq(nan, k)); |
| 2162 | if (slvr.check() != Status.UNSATISFIABLE) |
| 2163 | throw new TestFailedException(); |
| 2164 | System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr); |
| 2165 | |
| 2166 | /* NaN is equal to NaN according to normal equality. */ |
| 2167 | slvr = ctx.mkSolver("QF_FP"); |
| 2168 | slvr.add(ctx.mkEq(nan, nan)); |
| 2169 | if (slvr.check() != Status.SATISFIABLE) |
| 2170 | throw new TestFailedException(); |
| 2171 | System.out.println("OK, sat:" + System.getProperty("line.separator") + slvr); |
| 2172 | |
| 2173 | /* Let's prove -1e1 * -1.25e3 == +100 */ |
| 2174 | x = (FPNum)ctx.mkNumeral("-1e1", s); |
| 2175 | y = (FPNum)ctx.mkNumeral("-1.25p3", s); |
| 2176 | FPExpr x_plus_y = (FPExpr)ctx.mkConst("x_plus_y", s); |
| 2177 | FPNum r = (FPNum)ctx.mkNumeral("100", s); |
| 2178 | slvr = ctx.mkSolver("QF_FP"); |
| 2179 | |
| 2180 | slvr.add(ctx.mkEq(x_plus_y, ctx.mkFPMul(ctx.mkFPRoundNearestTiesToAway(), x, y))); |
| 2181 | slvr.add(ctx.mkNot(ctx.mkFPEq(x_plus_y, r))); |
| 2182 | if (slvr.check() != Status.UNSATISFIABLE) |
| 2183 | throw new TestFailedException(); |
| 2184 | System.out.println("OK, unsat:" + System.getProperty("line.separator") + slvr); |
| 2185 | } |
| 2186 | |
| 2187 | public void floatingPointExample2(Context ctx) throws TestFailedException |
| 2188 | { |
no test coverage detected