blob: 42633e803a3ddd7e53895fe4d5286da338d1ffe8 (
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
|
/******************************************************************************
* 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);
}
}
}
|