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
54

/*********************                                                        */
/*! \file UnsatCore.java
 ** \verbatim
 ** Top contributors (to current version):
 **   Andres Noetzli
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2019 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.\endverbatim
 **
 ** \brief An example of interacting with unsat cores using CVC4's Java API
 **
 ** An example of interacting with unsat cores using CVC4's Java API.
 **/

import edu.nyu.acsys.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);
    }
  }
}