Exception Handling

examples/api/java/Exceptions.java

 1/******************************************************************************
 2 * Top contributors (to current version):
 3 *   Mudathir Mohamed, Andres Noetzli
 4 *
 5 * This file is part of the cvc5 project.
 6 *
 7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
 8 * in the top-level source directory and their institutional affiliations.
 9 * All rights reserved.  See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Catching cvc5 exceptions via the Java API.
14 *
15 * A simple demonstration of catching cvc5 execptions via the Java API.
16 */
17
18import io.github.cvc5.*;
19
20public class Exceptions
21{
22  public static void main(String[] args)
23  {
24    Solver solver = new Solver();
25    {
26      solver.setOption("produce-models", "true");
27
28      // Setting an invalid option
29      try
30      {
31        solver.setOption("non-existing", "true");
32        System.exit(1);
33      }
34      catch (Exception e)
35      {
36        System.out.println(e.toString());
37      }
38
39      // Creating a term with an invalid type
40      try
41      {
42        Sort integer = solver.getIntegerSort();
43        Term x = solver.mkVar(integer, "x");
44        Term invalidTerm = solver.mkTerm(Kind.AND, x, x);
45        solver.checkSatAssuming(invalidTerm);
46        System.exit(1);
47      }
48      catch (Exception e)
49      {
50        System.out.println(e.toString());
51      }
52
53      // Asking for a model after unsat result
54      try
55      {
56        solver.checkSatAssuming(solver.mkBoolean(false));
57        solver.getModel(new Sort[] {}, new Term[] {});
58        System.exit(1);
59      }
60      catch (Exception e)
61      {
62        System.out.println(e.toString());
63      }
64    }
65    Context.deletePointers();
66  }
67}