moves-rwth · volkm · Mar 19, 2025 · Jul 24, 2017 · Jul 26, 2017 · Jul 26, 2017
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -1 +1 @@
-534f29c9e329007d67428da3ef7be84141140fe2
+534f29c9e329007d67428da3ef7be84141140fe2
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -203,3 +203,105 @@ Version 0.9.x
 
 ### Version 0.9 (2017/03)
 - Start of this changelog
+
+
+# Appendix: Pycarl Changelog
+=============
+
+Version 2.3.x
+-------------
+
+### Version 2.3.0 (2024/08)
+Requires carl-storm version >= 14.23
+
+- Added support for intervals with different number types
+- Automated code formatting
+- Developer: improved build and CMake support
+- Developer: improved CI
+
+
+Version 2.2.x
+-------------
+
+### Version 2.2.0 (2023/06)
+Requires carl-storm version >= 14.23
+
+- Upgraded repo / version for carl, requires [carl-storm](https://github.com/moves-rwth/carl-storm) from now on
+- Developer: added Dockerfile
+- Developer: improved build process
+- Developer: updated pybind11 to version 2.10.0
+
+
+Version 2.1.x
+-------------
+
+### Version 2.1.0 (2022/07)
+Requires carl with branch `master14`
+
+- Developer: updated pybind11 to version 2.8.1 and adapted bindings accordingly
+- Improved continuous integration with Github Actions
+
+
+Version 2.0.x
+-------------
+
+### Version 2.0.5 (2022/01)
+Requires carl with branch `master14`
+
+- Added support for continuous integration with Github Actions
+
+### Version 2.0.4 (2019/11)
+Requires carl with branch `master14`
+
+- Extended conversion of number types to formulae
+- (minor) changed `constant_part` to function for `Polynomial`
+- (minor) added an additional operator on polynomials
+- Fix for compilation with Xcode 11
+
+### Version 2.0.3 (2019/01)
+Requires carl with branch `master14` or a carl version between 17.12 and 18.08
+
+- Extended bindings for arithmetic operations
+- Fixed negation comparison
+- Improved error output in installation
+- Extended documentation
+- Improved and extended setup
+
+### Version 2.0.2 (2017/12)
+Requires carl version >= 17.12
+
+- Adaptions to changes in carl
+- Extended bindings for rational functions and factorized rational functions
+- `Variable` constructor no longer returns an existing variable if a variable with that name exists
+- `expand()` allows to obtain the expanded polynomial and rational function
+- Added methods for getting information about pycarl configuration
+- Extended build script:
+    * uses config file
+    * support for disabling build of CLN and parser bindings
+    * fixed debug build type
+
+### Version 2.0.1 (2017/08)
+Requires carl version >= 17.08
+
+- Added conversions between CLN and GMP
+- Added variable and integer pickling support. Throw errors if pickling is not supported
+- Added hash functions
+- Hide factorization caches for user
+- Depend on [carl-parser](https://github.com/ths-rwth/carl-parser) for parsing routines
+- Check for carl version
+- Fixed issues when CLN is not available
+
+### Version 2.0.0 (2017/05)
+- First version with support for CLN and GMP.
+  This means that no longer all operators are supported as it would be ambiguous
+- Using bigint
+
+
+Version 1.2.x
+-------------
+
+### Version 1.2.1 (2017/04)
+- Arbitrary-size integers (CLN and GMP)
+
+### Version 1.2.0 (2017/03)
+- Start of this changelog
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -2,17 +2,38 @@ cmake_minimum_required(VERSION 3.15)
 
 project(stormpy)
 
+# include(FetchContent)
+
+# FetchContent_Declare(
+#     storm
+#     GIT_REPOSITORY https://github.com/moves-rwth/storm.git
+#     GIT_BRANCH     master
+#     OVERRIDE_FIND_PACKAGE
+# )
+# message(Callign make available)
+# FetchContent_MakeAvailable(storm)
+# message(Done with make)
+
+
 option(USE_STORM_DFT "Enable support for DFTs" ON)
 option(USE_STORM_GSPN "Enable support for GSPNs" ON)
 option(USE_STORM_PARS "Enable support for parametric models" ON)
 option(USE_STORM_POMDP "Enable support for POMDPs" ON)
 option(STORMPY_DISABLE_SIGNATURE_DOC "Disable the signature in the documentation" OFF)
+
+option(USE_CLN_NUMBERS "Make cln numbers available in pycarl" ON)
+option(USE_PARSER "Make carlparser available in pycarl" ON)
+
 MARK_AS_ADVANCED(STORMPY_DISABLE_SIGNATURE_DOC)
 set(PYBIND_VERSION "" CACHE STRING "Pybind11 version to use")
 MARK_AS_ADVANCED(PYBIND_VERSION)
 set(STORM_DIR_HINT "" CACHE STRING "A hint where the Storm library can be found.")
+set(CARL_DIR_HINT "" CACHE STRING "A hint where the Carl library can be found.")
+set(CARLPARSER_DIR_HINT "" CACHE STRING "A hint where the Carl-parser library can be found.")
 
 find_package(storm REQUIRED HINTS ${STORM_DIR_HINT})
+find_package(carl REQUIRED HINTS ${CARL_DIR_HINT})
+find_package(carlparser QUIET HINTS ${CARLPARSER_DIR_HINT})
 
 find_package(Python COMPONENTS Interpreter Development REQUIRED)
 include(resources/include_pybind11.cmake)
@@ -53,12 +74,26 @@ if (STORM_USE_CLN_RF)
 else()
     set(PYCARL_RF_PACKAGE "gmp")
 endif()
-set(PYCARL_IMPORTS "import pycarl")
+set(PYCARL_IMPORTS "from stormpy import pycarl")
 if (STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
-    set(PYCARL_IMPORTS "${PYCARL_IMPORTS}\nimport pycarl.cln")
+    set(PYCARL_IMPORTS "${PYCARL_IMPORTS}\nfrom stormpy.pycarl import cln")
 endif()
 if (NOT STORM_USE_CLN_EA OR NOT STORM_USE_CLN_RF)
-    set(PYCARL_IMPORTS "${PYCARL_IMPORTS}\nimport pycarl.gmp")
+    set(PYCARL_IMPORTS "${PYCARL_IMPORTS}\nfrom stormpy.pycarl import gmp")
+endif()
+
+set(CARL_VERSION ${carl_VERSION})
+if ((USE_PARSER) AND (carlparser_FOUND))
+    set(CARL_WITH_PARSER "True")
+else()
+    set(CARL_WITH_PARSER "False")
+endif()
+if ((USE_CLN_NUMBERS) AND (CARL_USE_CLN_NUMBERS))
+    set(CARL_WITH_CLN "True")
+    set(PYCARL_HAS_CLN TRUE)
+else()
+    set(CARL_WITH_CLN "False")
+    set(PYCARL_HAS_CLN FALSE)
 endif()
 
 # Set dependency variables
@@ -95,9 +130,10 @@ function(stormpy_optional_module NAME ADDITIONAL_LIBS ADDITIONAL_INCLUDES)
     set_target_properties(${NAME} PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/${NAME}")
 endfunction(stormpy_optional_module)
 
-# Generate definitions used during compilation
+# Generate stormpy definitions used during compilation
 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/config.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/config.h)
-
+# Generate pycarl definitions used during compilation
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/definitions.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/pycarl/definitions.h)
 
 stormpy_module(core)
 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/core_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/_config.py @ONLY)
@@ -107,6 +143,15 @@ stormpy_module(logic)
 stormpy_module(storage)
 stormpy_module(utility)
 
+# Pycarl Core
+######
+file(GLOB_RECURSE pycarl_core_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/pycarl_core/*.cpp)
+pybind11_add_module(pycarl_core ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_core.cpp ${pycarl_core_SOURCES})
+target_include_directories(pycarl_core PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src/)
+target_link_libraries(pycarl_core PRIVATE lib_carl)
+set_target_properties(pycarl_core PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl" OUTPUT_NAME "pycarl_core")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_core_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/_config.py @ONLY)
+
 # Optional modules
 if(HAVE_STORM_DFT)
     stormpy_optional_module(dft storm-dft "${storm-dft_INCLUDE_DIR}")
@@ -121,3 +166,68 @@ if(HAVE_STORM_POMDP)
     stormpy_optional_module(pomdp storm-pomdp "${storm-pomdp_INCLUDE_DIR}")
 endif()
 
+# Typed core
+file(GLOB_RECURSE PYCARL_TYPED_CORE_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/typed_core/*.cpp)
+# GMP
+pybind11_add_module(pycarl.gmp ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_gmp.cpp ${PYCARL_TYPED_CORE_SOURCES})
+target_include_directories(pycarl.gmp PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.gmp PRIVATE lib_carl)
+set_target_properties(pycarl.gmp PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/gmp" OUTPUT_NAME "gmp")
+# CLN
+pybind11_add_module(pycarl.cln ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_cln.cpp ${PYCARL_TYPED_CORE_SOURCES})
+target_include_directories(pycarl.cln PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.cln PRIVATE lib_carl)
+target_compile_definitions(pycarl.cln PUBLIC "PYCARL_USE_CLN=ON")
+set_target_properties(pycarl.cln PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln" OUTPUT_NAME "cln")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_cln_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln/_config.py @ONLY)
+
+
+# Formula
+#########
+file(GLOB_RECURSE PYCARL_FORMULA_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/formula/*.cpp)
+pybind11_add_module(pycarl.formula ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_formula.cpp ${PYCARL_FORMULA_SOURCES})
+target_include_directories(pycarl.formula PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}  ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.formula PRIVATE lib_carl)
+set_target_properties(pycarl.formula PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/formula" OUTPUT_NAME "formula")
+
+# Typed formula
+file(GLOB_RECURSE PYCARL_TYPED_FORMULA_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/typed_formula/*.cpp)
+# GMP
+pybind11_add_module(pycarl.formula-gmp ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_typed_formula.cpp ${PYCARL_TYPED_FORMULA_SOURCES})
+target_include_directories(pycarl.formula-gmp PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}  ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.formula-gmp PRIVATE lib_carl)
+set_target_properties(pycarl.formula-gmp PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/gmp/formula" OUTPUT_NAME "formula")
+# CLN
+pybind11_add_module(pycarl.formula-cln ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_typed_formula.cpp ${PYCARL_TYPED_FORMULA_SOURCES})
+target_include_directories(pycarl.formula-cln PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}  ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.formula-cln PRIVATE lib_carl)
+target_compile_definitions(pycarl.formula-cln PUBLIC "PYCARL_USE_CLN=ON")
+set_target_properties(pycarl.formula-cln PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln/formula" OUTPUT_NAME "formula")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_cln_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln/formula/_config.py @ONLY)
+
+
+# Parse
+# #######
+file(GLOB_RECURSE PYCARL_PARSE_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/parse/*.cpp)
+
+pybind11_add_module(pycarl.parse ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_parse.cpp ${PYCARL_PARSE_SOURCES})
+target_include_directories(pycarl.parse PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}  ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.parse PRIVATE lib_carl carl-parser)
+set_target_properties(pycarl.parse PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/parse" OUTPUT_NAME "parse")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_parser_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/parse/_config.py @ONLY)
+
+# Typed parse
+file(GLOB_RECURSE PYCARL_TYPED_PARSE_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/typed_parse/*.cpp)
+# GMP
+pybind11_add_module(pycarl.parse-gmp ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_typed_parse.cpp ${PYCARL_TYPED_PARSE_SOURCES})
+target_include_directories(pycarl.parse-gmp PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.parse-gmp PRIVATE lib_carl carl-parser)
+set_target_properties(pycarl.parse-gmp PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/gmp/parse" OUTPUT_NAME "parse")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_parser_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/gmp/parse/_config.py @ONLY)
+# CLN
+pybind11_add_module(pycarl.parse-cln ${CMAKE_CURRENT_SOURCE_DIR}/src/pycarl/mod_typed_parse.cpp ${PYCARL_TYPED_PARSE_SOURCES})
+target_include_directories(pycarl.parse-cln PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${CMAKE_CURRENT_BINARY_DIR}/src)
+target_link_libraries(pycarl.parse-cln PRIVATE lib_carl carl-parser)
+target_compile_definitions(pycarl.parse-cln PUBLIC "PYCARL_USE_CLN=ON")
+set_target_properties(pycarl.parse-cln PROPERTIES LIBRARY_OUTPUT_DIRECTORY "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln/parse" OUTPUT_NAME "parse")
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/cmake/pycarl_parser_config.py.in ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/pycarl/cln/parse/_config.py @ONLY)
diff --git a/Dockerfile b/Dockerfile
@@ -20,8 +20,6 @@ MAINTAINER Matthias Volk <[email protected]>
 ARG build_type=Release
 # Additional arguments for compiling stormpy
 ARG setup_args=""
-# Additional arguments for compiling pycarl
-ARG setup_args_pycarl=""
 # Number of threads to use for parallel compilation
 ARG no_threads=2
 
@@ -37,7 +35,6 @@ RUN apt-get install -y --no-install-recommends \
     python3-venv
 # Packages maven and uuid-dev are required for carl-parser
 
-
 # Build carl-parser
 ###################
 WORKDIR /opt/
@@ -64,20 +61,6 @@ ENV PATH="$VIRTUAL_ENV/bin:$PATH"
 
 RUN pip install setuptools
 
-# Build pycarl
-##############
-WORKDIR /opt/
-
-# Obtain latest version of pycarl from public repository
-RUN git clone https://github.com/moves-rwth/pycarl.git
-
-# Switch to pycarl directory
-WORKDIR /opt/pycarl
-
-# Build pycarl
-RUN python setup.py build_ext $setup_args_pycarl -j $no_threads develop
-
-
 # Build stormpy
 ###############
 RUN mkdir /opt/stormpy

diff --git a/README.md b/README.md
@@ -23,3 +23,7 @@ Stormpy depends on [pycarl](https://github.com/moves-rwth/pycarl/).
 
 - Sebastian Junges
 - Matthias Volk
+Stormpy includes Pycarl, the Python Bindings for [CArL](https://github.com/moves-rwth/carl-storm).
+
+The development of pycarl received significant contributions from:
+- Harold Bruintjes
diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt
@@ -1,26 +1,35 @@
 cmake_minimum_required(VERSION 3.15)
 
 project(storm-version)
+
+include(FetchContent)
+
+set(INSTALL_STORM TRUE CACHE BOOL "Whether to install storm from scratch.")
 set(STORM_DIR_HINT "" CACHE STRING "A hint where the Storm library can be found.")
+set(CARL_DIR_HINT "" CACHE STRING "A hint where the Carl library can be found.")
+set(CARLPARSER_DIR_HINT "" CACHE STRING "A hint where the Carl-parser library can be found.")
+
+if(INSTALL_STORM)
+    message(STATUS "Installing Storm from scratch")
+endif()
 
 find_package(storm REQUIRED HINTS ${STORM_DIR_HINT})
+find_package(carl REQUIRED HINTS ${CARL_DIR_HINT})
+find_package(carlparser QUIET HINTS ${CARLPARSER_DIR_HINT})
 
 include(${CMAKE_CURRENT_SOURCE_DIR}/macros.cmake)
 
-
 # Set configuration
 set(STORM_DIR ${storm_DIR})
 set(STORM_VERSION ${storm_VERSION})
 set(STORM_LIBS ${storm_LIBRARIES})
 
-
 # Check for optional Storm libraries
 storm_with_lib(DFT)
 storm_with_lib(GSPN)
 storm_with_lib(PARS)
 storm_with_lib(POMDP)
 
-
 # Set variables
 set_variable_string(STORM_CLN_EA_BOOL ${STORM_USE_CLN_EA})
 set_variable_string(STORM_CLN_RF_BOOL ${STORM_USE_CLN_RF})
@@ -33,6 +42,21 @@ set_variable_string(HAVE_STORM_GSPN_BOOL ${HAVE_STORM_GSPN})
 set_variable_string(HAVE_STORM_PARS_BOOL ${HAVE_STORM_PARS})
 set_variable_string(HAVE_STORM_POMDP_BOOL ${HAVE_STORM_POMDP})
 
+# Set configuration
+set(CARL_DIR ${carl_DIR})
+set(CARL_VERSION ${carl_VERSION})
+if(carlparser_FOUND)
+    set(CARL_PARSER_DIR ${carlparser_DIR})
+    set_variable_string(CARL_WITH_PARSER "True")
+else()
+    set(CARL_PARSER_DIR "")
+    set_variable_string(CARL_WITH_PARSER "False")
+endif()
+if(CARL_USE_CLN_NUMBERS)
+    set_variable_string(CARL_WITH_CLN "True")
+else()
+    set_variable_string(CARL_WITH_CLN "False")
+endif()
 
 # Write configuration file
 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/config.py.in ${CMAKE_CURRENT_BINARY_DIR}/generated/config.py @ONLY)
diff --git a/cmake/config.py.in b/cmake/config.py.in
@@ -10,3 +10,8 @@ HAVE_STORM_DFT = @HAVE_STORM_DFT_BOOL@
 HAVE_STORM_GSPN = @HAVE_STORM_GSPN_BOOL@
 HAVE_STORM_PARS = @HAVE_STORM_PARS_BOOL@
 HAVE_STORM_POMDP = @HAVE_STORM_POMDP_BOOL@
+CARL_DIR = "@CARL_DIR@"
+CARL_VERSION = "@CARL_VERSION@"
+CARL_PARSER_DIR = "@CARL_PARSER_DIR@"
+CARL_WITH_PARSER = @CARL_WITH_PARSER@
+CARL_WITH_CLN = @CARL_WITH_CLN@
diff --git a/cmake/pycarl_cln_config.py.in b/cmake/pycarl_cln_config.py.in
@@ -0,0 +1,3 @@
+# Auto-generated by CMake.
+
+CARL_WITH_CLN = @CARL_WITH_CLN@
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		534f29c9e329007d67428da3ef7be84141140fe2
		534f29c9e329007d67428da3ef7be84141140fe2
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# Auto-generated by CMake.

		CARL_WITH_CLN = @CARL_WITH_CLN@