| 1080 | // / <remarks>This example also demonstrates how big numbers can be |
| 1081 | // / created in ctx.</remarks> |
| 1082 | public void pushPopExample1(Context ctx) throws TestFailedException |
| 1083 | { |
| 1084 | System.out.println("PushPopExample1"); |
| 1085 | Log.append("PushPopExample1"); |
| 1086 | |
| 1087 | /* create a big number */ |
| 1088 | IntSort int_type = ctx.getIntSort(); |
| 1089 | IntNum big_number = ctx.mkInt("1000000000000000000000000000000000000000000000000000000"); |
| 1090 | |
| 1091 | /* create number 3 */ |
| 1092 | IntExpr three = (IntExpr) ctx.mkNumeral("3", int_type); |
| 1093 | |
| 1094 | /* create x */ |
| 1095 | IntExpr x = ctx.mkIntConst("x"); |
| 1096 | |
| 1097 | Solver solver = ctx.mkSolver(); |
| 1098 | |
| 1099 | /* assert x >= "big number" */ |
| 1100 | BoolExpr c1 = ctx.mkGe(x, big_number); |
| 1101 | System.out.println("assert: x >= 'big number'"); |
| 1102 | solver.add(c1); |
| 1103 | |
| 1104 | /* create a backtracking point */ |
| 1105 | System.out.println("push"); |
| 1106 | solver.push(); |
| 1107 | |
| 1108 | /* assert x <= 3 */ |
| 1109 | BoolExpr c2 = ctx.mkLe(x, three); |
| 1110 | System.out.println("assert: x <= 3"); |
| 1111 | solver.add(c2); |
| 1112 | |
| 1113 | /* context is inconsistent at this point */ |
| 1114 | if (solver.check() != Status.UNSATISFIABLE) |
| 1115 | throw new TestFailedException(); |
| 1116 | |
| 1117 | /* |
| 1118 | * backtrack: the constraint x <= 3 will be removed, since it was |
| 1119 | * asserted after the last ctx.Push. |
| 1120 | */ |
| 1121 | System.out.println("pop"); |
| 1122 | solver.pop(1); |
| 1123 | |
| 1124 | /* the context is consistent again. */ |
| 1125 | if (solver.check() != Status.SATISFIABLE) |
| 1126 | throw new TestFailedException(); |
| 1127 | |
| 1128 | /* new constraints can be asserted... */ |
| 1129 | |
| 1130 | /* create y */ |
| 1131 | IntExpr y = ctx.mkIntConst("y"); |
| 1132 | |
| 1133 | /* assert y > x */ |
| 1134 | BoolExpr c3 = ctx.mkGt(y, x); |
| 1135 | System.out.println("assert: y > x"); |
| 1136 | solver.add(c3); |
| 1137 | |
| 1138 | /* the context is still consistent. */ |
| 1139 | if (solver.check() != Status.SATISFIABLE) |