mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
b056bd2446
This adds `stable` as a build type, which is similar to `safe` but permits incomplete proofs in regressions and the use of regular options with `no-support:` fields.
120 lines
3.1 KiB
CMake
120 lines
3.1 KiB
CMake
###############################################################################
|
|
# 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()
|