blob: 6478aea5cbaa9c907c309d5a81308e3610927f02 (
plain)
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.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);
}
}
}
|