| 1202 | // / Find x and y such that: x ^ y - 103 == x * y |
| 1203 | |
| 1204 | public void bitvectorExample2(Context ctx) throws TestFailedException |
| 1205 | { |
| 1206 | System.out.println("BitvectorExample2"); |
| 1207 | Log.append("BitvectorExample2"); |
| 1208 | |
| 1209 | /* construct x ^ y - 103 == x * y */ |
| 1210 | BitVecSort bv_type = ctx.mkBitVecSort(32); |
| 1211 | BitVecExpr x = ctx.mkBVConst("x", 32); |
| 1212 | BitVecExpr y = ctx.mkBVConst("y", 32); |
| 1213 | BitVecExpr x_xor_y = ctx.mkBVXOR(x, y); |
| 1214 | Expr<BitVecSort> c103 = ctx.mkNumeral("103", bv_type); |
| 1215 | BitVecExpr lhs = ctx.mkBVSub(x_xor_y, c103); |
| 1216 | BitVecExpr rhs = ctx.mkBVMul(x, y); |
| 1217 | BoolExpr ctr = ctx.mkEq(lhs, rhs); |
| 1218 | |
| 1219 | System.out.println("find values of x and y, such that x ^ y - 103 == x * y"); |
| 1220 | |
| 1221 | /* find a model (i.e., values for x an y that satisfy the constraint */ |
| 1222 | Model m = check(ctx, ctr, Status.SATISFIABLE); |
| 1223 | System.out.println(m); |
| 1224 | } |
| 1225 | |
| 1226 | // / Demonstrates how to use the SMTLIB parser. |
| 1227 | |