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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
###############################################################################
# Top contributors (to current version):
# Daniel Larraz, Andres Noetzli, Andrew Reynolds
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2025 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.
# #############################################################################
#
# The build system configuration.
##
set(EXAMPLES_API_PYTHON
bitvectors_and_arrays
bitvectors
combination
datatypes
exceptions
extract
helloworld
id
linear_arith
parser
parser_sym_manager
quickstart
sequences
sets
strings
sygus-fun
sygus-inv
uf
)
# Examples that have a Pythonic version.
# This list should include any such example,
# even if it is only conditionally added (e.g.,
# based on CVC5_USE_COCOA or NOT CVC5_SAFE_BUILD).
set(EXAMPLES_API_PYTHON_PYTHONIC
bitvectors_and_arrays
bitvectors
combination
datatypes
exceptions
extract
floating_point
helloworld
id
linear_arith
quickstart
sequences
sets
strings
transcendentals
uf
)
find_package(Python ${CVC5_BINDINGS_PYTHON_VERSION} EXACT REQUIRED)
# Check whether the cvc5 module is already installed
execute_process(
COMMAND ${Python_EXECUTABLE} -c "import cvc5"
RESULT_VARIABLE PYTHON_CVC5_RC
ERROR_QUIET
)
if(NOT (PYTHON_CVC5_RC EQUAL 0))
# Find Python bindings in the corresponding python-*/site-packages directory.
# Lookup Python module directory and store path in PYTHON_MODULE_PATH.
execute_process(COMMAND
${Python_EXECUTABLE} -c
"import os.path; import sysconfig;\
print(os.path.dirname(os.path.dirname('${CMAKE_PREFIX_PATH}'))+\
sysconfig.get_paths()['platlib'].split(sysconfig.get_config_var('platbase'))[1])"
OUTPUT_VARIABLE PYTHON_MODULE_PATH
OUTPUT_STRIP_TRAILING_WHITESPACE)
endif()
function(_add_python_test example subdir)
string(REPLACE "/" "_" subdir_name "${subdir}") # unique test name
set(test_name example/${subdir_name}/${example})
add_test(
NAME ${test_name}
COMMAND "${Python_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/${subdir}/${example}.py"
)
set_tests_properties(${test_name} PROPERTIES
LABELS "example"
ENVIRONMENT "PYTHONPATH=${PYTHON_MODULE_PATH}"
)
endfunction()
function(create_python_example example)
# Base Python API example
_add_python_test(${example} "api/python")
# Only add the Pythonic version if it is in the list
if (example IN_LIST EXAMPLES_API_PYTHON_PYTHONIC)
_add_python_test(${example} "api/python/pythonic")
endif()
endfunction()
foreach(example ${EXAMPLES_API_PYTHON})
create_python_example(${example})
endforeach()
if((NOT CVC5_SAFE_BUILD) AND (NOT CVC5_STABLE_BUILD))
create_python_example("floating_point")
create_python_example("bags")
create_python_example("relations")
create_python_example("transcendentals")
endif()
if(CVC5_USE_COCOA)
create_python_example("finite_field")
endif()
|
