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-2024 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}
examples/api/python/exceptions.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Andres Noetzli, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# Catching cvc5 exceptions with the legacy Python API.
15#
16# A simple demonstration of catching cvc5 exceptions with the legacy Python API.
17##
18
19import cvc5
20from cvc5 import Kind
21import sys
22
23
24def main():
25 tm = cvc5.TermManager()
26 slv = cvc5.Solver(tm)
27
28 slv.setOption("produce-models", "true")
29
30 # Setting an invalid option
31 try:
32 slv.setOption("non-existing", "true")
33 return 1
34 except:
35 pass
36
37 # Creating a term with an invalid type
38 try:
39 integer = tm.getIntegerSort()
40 x = tm.mkConst("x", integer)
41 invalidTerm = em.mkTerm(AND, x, x)
42 slv.checkSat(invalidTerm)
43 return 1
44 except:
45 pass
46
47 # Asking for a model after unsat result
48 try:
49 slv.checkSat(tm.mkBoolean(False))
50 slv.getModel()
51 return 1
52 except:
53 pass
54
55 return 0
56
57
58if __name__ == '__main__':
59 sys.exit(main())
cvc5_pythonic_api:/test/pgms/example_exceptions.py
1from cvc5_pythonic_api import *
2
3if __name__ == '__main__':
4 s = Solver()
5 s.set("produce-models", True)
6 try:
7 # invalid option
8 s.set("non-existing-option", True)
9 except:
10 pass
11
12 try:
13 # type error
14 Int("x") + BitVec("a", 5)
15 except:
16 pass
17
18 s += BoolVal(False)
19 s.check()
20 try:
21 s.model()
22 except:
23 pass