// [ؖ̓T^IȋLq(ؖp^[)]
// An example, refering unsatCoreAndProofExample2
import java.util.*;
import com.microsoft.z3.*;
public class unsatCoreAndProofExample2 extends Object
{
	// RXgN^
	public Z3Application(){ test(); }
	// ړȈ̃\bh
	public void test()
	{
		// ReLXg̐Ap[^ݒ
		HashMap<String, String> cfg = new HashMap<String, String>();
		cfg.put("model", "true");
		cfg.put("proof", "true");
		cfg.put("auto-config", "false");
		Context ctx = new Context(cfg);
		// ϐA̕\
		BoolExpr pa = ctx.mkBoolConst("PredA");
		BoolExpr pb = ctx.mkBoolConst("PredB");
		BoolExpr pc = ctx.mkBoolConst("PredC");
		BoolExpr pd = ctx.mkBoolConst("PredD");
		BoolExpr f1 = ctx.mkAnd(new BoolExpr[]{pa, pb, pc});
		BoolExpr f2 = ctx.mkAnd(new BoolExpr[]{pa, ctx.mkNot(pb), pc});
		BoolExpr f3 = ctx.mkOr(ctx.mkNot(pa), ctx.mkNot(pc));
		BoolExpr f4 = pd;
		BoolExpr p1 = ctx.mkBoolConst("P1");
		BoolExpr p2 = ctx.mkBoolConst("P2");
		BoolExpr p3 = ctx.mkBoolConst("P3");
		BoolExpr p4 = ctx.mkBoolConst("P4");
		// \o̐ASAT Aؖ擾
		Solver solver = ctx.mkSolver();
		solver.assertAndTrack(f1, p1);
		solver.assertAndTrack(f2, p2);
		solver.assertAndTrack(f3, p3);
		solver.assertAndTrack(f4, p4);
		Status result = solver.check();
		if(result==Status.UNSATISFIABLE){
			System.out.println("unsat");
			System.out.println("proof: " + solver.getProof());
			System.out.println("core: ");
			for(Expr c: solver.getUnsatCore()) System.out.println(c);
		}
	}
	// C\bh
	public static void main(String... args)
	{
		Z3Application app = new Z3Application();
	}
}