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}
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-2022 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 slv = cvc5.Solver()
26
27 slv.setOption("produce-models", "true")
28
29 # Setting an invalid option
30 try:
31 slv.setOption("non-existing", "true")
32 return 1
33 except:
34 pass
35
36 # Creating a term with an invalid type
37 try:
38 integer = slv.getIntegerSort()
39 x = slv.mkConst("x", integer)
40 invalidTerm = em.mkTerm(AND, x, x)
41 slv.checkSat(invalidTerm)
42 return 1
43 except:
44 pass
45
46 # Asking for a model after unsat result
47 try:
48 slv.checkSat(slv.mkBoolean(False))
49 slv.getModel()
50 return 1
51 except:
52 pass
53
54 return 0
55
56
57if __name__ == '__main__':
58 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