examples/api/java/UnsatCores.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * An example of interacting with unsat cores using CVC4's Java API.
 */

import edu.stanford.CVC4.*;
import java.util.Iterator;

public class UnsatCores {
  public static void main(String[] args) {
    System.loadLibrary("cvc4jni");

    ExprManager em = new ExprManager();
    SmtEngine smt = new SmtEngine(em);

    // Enable the production of unsat cores
    smt.setOption("produce-unsat-cores", new SExpr(true));

    Type boolType = em.booleanType();
    Expr a = em.mkVar("A", boolType);
    Expr b = em.mkVar("B", boolType);

    // A ^ B
    smt.assertFormula(em.mkExpr(Kind.AND, a, b));
    // ~(A v B)
    smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.OR, a, b)));

    Result res = smt.checkSat(); // result is unsat

    // Retrieve the unsat core
    UnsatCore unsatCore = smt.getUnsatCore();
    
    // Print the unsat core
    System.out.println("Unsat Core: " + unsatCore);

    // Iterate over expressions in the unsat core. The `UnsatCore` class
    // implements the `Iterable<Expr>` interface.
    System.out.println("--- Unsat Core ---");
    for (Expr e : unsatCore) {
      System.out.println(e);
    }
  }
}