Exception Handling
examples/api/cpp/exceptions.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Daniel Larraz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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 C++ API.
14 *
15 * A simple demonstration of catching cvc5 exceptions via the C++ API.
16 */
17
18#include <cvc5/cvc5.h>
19#include <iostream>
20
21int main()
22{
23 cvc5::TermManager tm;
24 cvc5::Solver solver(tm);
25
26 solver.setOption("produce-models", "true");
27
28 // Setting an invalid option
29 try
30 {
31 solver.setOption("non-existing", "true");
32 return 1;
33 }
34 catch (const std::exception& e)
35 {
36 std::cout << e.what() << std::endl;
37 }
38
39 // Creating a term with an invalid type
40 try
41 {
42 cvc5::Sort integer = tm.getIntegerSort();
43 cvc5::Term x = tm.mkVar(integer, "x");
44 cvc5::Term invalidTerm = tm.mkTerm(cvc5::Kind::AND, {x, x});
45 solver.checkSatAssuming(invalidTerm);
46 return 1;
47 }
48 catch (const std::exception& e)
49 {
50 std::cout << e.what() << std::endl;
51 }
52
53 // Asking for a model after unsat result
54 try
55 {
56 solver.checkSatAssuming(tm.mkBoolean(false));
57 solver.getModel({}, {});
58 return 1;
59 }
60 catch (const std::exception& e)
61 {
62 std::cout << e.what() << std::endl;
63 }
64
65 return 0;
66}
examples/api/java/Exceptions.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andres Noetzli, Daniel Larraz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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 TermManager tm = new TermManager();
25 Solver solver = new Solver(tm);
26 {
27 solver.setOption("produce-models", "true");
28
29 // Setting an invalid option
30 try
31 {
32 solver.setOption("non-existing", "true");
33 System.exit(1);
34 }
35 catch (Exception e)
36 {
37 System.out.println(e.toString());
38 }
39
40 // Creating a term with an invalid type
41 try
42 {
43 Sort integer = tm.getIntegerSort();
44 Term x = tm.mkVar(integer, "x");
45 Term invalidTerm = tm.mkTerm(Kind.AND, x, x);
46 solver.checkSatAssuming(invalidTerm);
47 System.exit(1);
48 }
49 catch (Exception e)
50 {
51 System.out.println(e.toString());
52 }
53
54 // Asking for a model after unsat result
55 try
56 {
57 solver.checkSatAssuming(tm.mkBoolean(false));
58 solver.getModel(new Sort[] {}, new Term[] {});
59 System.exit(1);
60 }
61 catch (Exception e)
62 {
63 System.out.println(e.toString());
64 }
65 }
66 Context.deletePointers();
67 }
68}
examples/api/python/exceptions.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Andres Noetzli, Aina Niemetz, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2025 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