Show how push & pop can be used to create "backtracking" points. This example also demonstrates how big numbers can be created in ctx.
(Context ctx)
| 1243 | /// <remarks>This example also demonstrates how big numbers can be |
| 1244 | /// created in ctx.</remarks> |
| 1245 | public static void PushPopExample1(Context ctx) |
| 1246 | { |
| 1247 | Console.WriteLine("PushPopExample1"); |
| 1248 | |
| 1249 | /* create a big number */ |
| 1250 | IntSort int_type = ctx.IntSort; |
| 1251 | IntExpr big_number = ctx.MkInt("1000000000000000000000000000000000000000000000000000000"); |
| 1252 | |
| 1253 | /* create number 3 */ |
| 1254 | IntExpr three = (IntExpr)ctx.MkNumeral("3", int_type); |
| 1255 | |
| 1256 | /* create x */ |
| 1257 | IntExpr x = ctx.MkIntConst("x"); |
| 1258 | |
| 1259 | Solver solver = ctx.MkSolver(); |
| 1260 | |
| 1261 | /* assert x >= "big number" */ |
| 1262 | BoolExpr c1 = ctx.MkGe(x, big_number); |
| 1263 | Console.WriteLine("assert: x >= 'big number'"); |
| 1264 | solver.Assert(c1); |
| 1265 | |
| 1266 | /* create a backtracking point */ |
| 1267 | Console.WriteLine("push"); |
| 1268 | solver.Push(); |
| 1269 | |
| 1270 | /* assert x <= 3 */ |
| 1271 | BoolExpr c2 = ctx.MkLe(x, three); |
| 1272 | Console.WriteLine("assert: x <= 3"); |
| 1273 | solver.Assert(c2); |
| 1274 | |
| 1275 | /* context is inconsistent at this point */ |
| 1276 | if (solver.Check() != Status.UNSATISFIABLE) |
| 1277 | throw new TestFailedException(); |
| 1278 | |
| 1279 | /* backtrack: the constraint x <= 3 will be removed, since it was |
| 1280 | asserted after the last ctx.Push. */ |
| 1281 | Console.WriteLine("pop"); |
| 1282 | solver.Pop(1); |
| 1283 | |
| 1284 | /* the context is consistent again. */ |
| 1285 | if (solver.Check() != Status.SATISFIABLE) |
| 1286 | throw new TestFailedException(); |
| 1287 | |
| 1288 | /* new constraints can be asserted... */ |
| 1289 | |
| 1290 | /* create y */ |
| 1291 | IntExpr y = ctx.MkIntConst("y"); |
| 1292 | |
| 1293 | /* assert y > x */ |
| 1294 | BoolExpr c3 = ctx.MkGt(y, x); |
| 1295 | Console.WriteLine("assert: y > x"); |
| 1296 | solver.Assert(c3); |
| 1297 | |
| 1298 | /* the context is still consistent. */ |
| 1299 | if (solver.Check() != Status.SATISFIABLE) |
| 1300 | throw new TestFailedException(); |
| 1301 | } |
| 1302 |