| 2033 | // / Extract unsatisfiable core example |
| 2034 | |
| 2035 | public void unsatCoreAndProofExample(Context ctx) |
| 2036 | { |
| 2037 | System.out.println("UnsatCoreAndProofExample"); |
| 2038 | Log.append("UnsatCoreAndProofExample"); |
| 2039 | |
| 2040 | Solver solver = ctx.mkSolver(); |
| 2041 | |
| 2042 | BoolExpr pa = ctx.mkBoolConst("PredA"); |
| 2043 | BoolExpr pb = ctx.mkBoolConst("PredB"); |
| 2044 | BoolExpr pc = ctx.mkBoolConst("PredC"); |
| 2045 | BoolExpr pd = ctx.mkBoolConst("PredD"); |
| 2046 | BoolExpr p1 = ctx.mkBoolConst("P1"); |
| 2047 | BoolExpr p2 = ctx.mkBoolConst("P2"); |
| 2048 | BoolExpr p3 = ctx.mkBoolConst("P3"); |
| 2049 | BoolExpr p4 = ctx.mkBoolConst("P4"); |
| 2050 | BoolExpr[] assumptions = new BoolExpr[] { ctx.mkNot(p1), ctx.mkNot(p2), |
| 2051 | ctx.mkNot(p3), ctx.mkNot(p4) }; |
| 2052 | BoolExpr f1 = ctx.mkAnd(pa, pb, pc); |
| 2053 | BoolExpr f2 = ctx.mkAnd(pa, ctx.mkNot(pb), pc); |
| 2054 | BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc)); |
| 2055 | BoolExpr f4 = pd; |
| 2056 | |
| 2057 | solver.add(ctx.mkOr(f1, p1)); |
| 2058 | solver.add(ctx.mkOr(f2, p2)); |
| 2059 | solver.add(ctx.mkOr(f3, p3)); |
| 2060 | solver.add(ctx.mkOr(f4, p4)); |
| 2061 | Status result = solver.check(assumptions); |
| 2062 | |
| 2063 | if (result == Status.UNSATISFIABLE) |
| 2064 | { |
| 2065 | System.out.println("unsat"); |
| 2066 | System.out.println("proof: " + solver.getProof()); |
| 2067 | System.out.println("core: "); |
| 2068 | for (Expr c : solver.getUnsatCore()) |
| 2069 | { |
| 2070 | System.out.println(c); |
| 2071 | } |
| 2072 | } |
| 2073 | } |
| 2074 | |
| 2075 | /// Extract unsatisfiable core example with AssertAndTrack |
| 2076 | |