| 1293 | // / <remarks>This example also demonstrates how big numbers can be |
| 1294 | // / created in ctx.</remarks> |
| 1295 | public void pushPopExample1(Context ctx) throws TestFailedException |
| 1296 | { |
| 1297 | System.out.println("PushPopExample1"); |
| 1298 | Log.append("PushPopExample1"); |
| 1299 | |
| 1300 | /* create a big number */ |
| 1301 | IntSort int_type = ctx.getIntSort(); |
| 1302 | IntExpr big_number = ctx |
| 1303 | .mkInt("1000000000000000000000000000000000000000000000000000000"); |
| 1304 | |
| 1305 | /* create number 3 */ |
| 1306 | IntExpr three = (IntExpr) ctx.mkNumeral("3", int_type); |
| 1307 | |
| 1308 | /* create x */ |
| 1309 | IntExpr x = ctx.mkIntConst("x"); |
| 1310 | |
| 1311 | Solver solver = ctx.mkSolver(); |
| 1312 | |
| 1313 | /* assert x >= "big number" */ |
| 1314 | BoolExpr c1 = ctx.mkGe(x, big_number); |
| 1315 | System.out.println("assert: x >= 'big number'"); |
| 1316 | solver.add(c1); |
| 1317 | |
| 1318 | /* create a backtracking point */ |
| 1319 | System.out.println("push"); |
| 1320 | solver.push(); |
| 1321 | |
| 1322 | /* assert x <= 3 */ |
| 1323 | BoolExpr c2 = ctx.mkLe(x, three); |
| 1324 | System.out.println("assert: x <= 3"); |
| 1325 | solver.add(c2); |
| 1326 | |
| 1327 | /* context is inconsistent at this point */ |
| 1328 | if (solver.check() != Status.UNSATISFIABLE) |
| 1329 | throw new TestFailedException(); |
| 1330 | |
| 1331 | /* |
| 1332 | * backtrack: the constraint x <= 3 will be removed, since it was |
| 1333 | * asserted after the last ctx.Push. |
| 1334 | */ |
| 1335 | System.out.println("pop"); |
| 1336 | solver.pop(1); |
| 1337 | |
| 1338 | /* the context is consistent again. */ |
| 1339 | if (solver.check() != Status.SATISFIABLE) |
| 1340 | throw new TestFailedException(); |
| 1341 | |
| 1342 | /* new constraints can be asserted... */ |
| 1343 | |
| 1344 | /* create y */ |
| 1345 | IntExpr y = ctx.mkIntConst("y"); |
| 1346 | |
| 1347 | /* assert y > x */ |
| 1348 | BoolExpr c3 = ctx.mkGt(y, x); |
| 1349 | System.out.println("assert: y > x"); |
| 1350 | solver.add(c3); |
| 1351 | |
| 1352 | /* the context is still consistent. */ |