| 1415 | // / Find x and y such that: x ^ y - 103 == x * y |
| 1416 | |
| 1417 | public void bitvectorExample2(Context ctx) throws TestFailedException |
| 1418 | { |
| 1419 | System.out.println("BitvectorExample2"); |
| 1420 | Log.append("BitvectorExample2"); |
| 1421 | |
| 1422 | /* construct x ^ y - 103 == x * y */ |
| 1423 | BitVecSort bv_type = ctx.mkBitVecSort(32); |
| 1424 | BitVecExpr x = ctx.mkBVConst("x", 32); |
| 1425 | BitVecExpr y = ctx.mkBVConst("y", 32); |
| 1426 | BitVecExpr x_xor_y = ctx.mkBVXOR(x, y); |
| 1427 | BitVecExpr c103 = (BitVecNum) ctx.mkNumeral("103", bv_type); |
| 1428 | BitVecExpr lhs = ctx.mkBVSub(x_xor_y, c103); |
| 1429 | BitVecExpr rhs = ctx.mkBVMul(x, y); |
| 1430 | BoolExpr ctr = ctx.mkEq(lhs, rhs); |
| 1431 | |
| 1432 | System.out |
| 1433 | .println("find values of x and y, such that x ^ y - 103 == x * y"); |
| 1434 | |
| 1435 | /* find a model (i.e., values for x an y that satisfy the constraint */ |
| 1436 | Model m = check(ctx, ctr, Status.SATISFIABLE); |
| 1437 | System.out.println(m); |
| 1438 | } |
| 1439 | |
| 1440 | // / Demonstrates how to use the SMTLIB parser. |
| 1441 | |