| 273 | } |
| 274 | |
| 275 | static void Disprove(Context ctx, BoolExpr f, bool useMBQI = false, params BoolExpr[] assumptions) |
| 276 | { |
| 277 | Console.WriteLine("Disproving: " + f); |
| 278 | Solver s = ctx.MkSolver(); |
| 279 | Params p = ctx.MkParams(); |
| 280 | p.Add("mbqi", useMBQI); |
| 281 | s.Parameters = p; |
| 282 | foreach (BoolExpr a in assumptions) |
| 283 | s.Assert(a); |
| 284 | s.Assert(ctx.MkNot(f)); |
| 285 | Status q = s.Check(); |
| 286 | |
| 287 | switch (q) |
| 288 | { |
| 289 | case Status.UNKNOWN: |
| 290 | Console.WriteLine("Unknown because: " + s.ReasonUnknown); |
| 291 | break; |
| 292 | case Status.SATISFIABLE: |
| 293 | Console.WriteLine("OK, model: " + s.Model); |
| 294 | break; |
| 295 | case Status.UNSATISFIABLE: |
| 296 | throw new TestFailedException(); |
| 297 | } |
| 298 | } |
| 299 | |
| 300 | static void ModelConverterTest(Context ctx) |
| 301 | { |