From f2c6bb91fddd8de8cc22008801912eb50d24a7e8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 3 Aug 2015 14:03:03 +0200 Subject: [PATCH 1/6] Some extra methods for the Expr. Manager. Former-commit-id: b3e813280f91562ea3b071364e646125c8faaa9c --- src/storage/expressions/ExpressionManager.cpp | 16 ++++++++-- src/storage/expressions/ExpressionManager.h | 30 ++++++++++++++++++- 2 files changed, 43 insertions(+), 3 deletions(-) diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 6738a0502..2685c940c 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -200,11 +200,23 @@ namespace storm { return nameToIndexMapping.find(name) != nameToIndexMapping.end(); } - Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary) { - std::string newName = "__x" + std::to_string(freshVariableCounter++); + Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary, std::string const& prefix) { + std::string newName = prefix + std::to_string(freshVariableCounter++); return declareOrGetVariable(newName, variableType, auxiliary, false); } + Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getBooleanType(), auxiliary, prefix); + } + + Variable ExpressionManager::declareFreshIntegerVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getIntegerType(), auxiliary, prefix); + } + + Variable ExpressionManager::declareFreshRationalVariable(bool auxiliary, const std::string& prefix) { + return declareFreshVariable(this->getRationalType(), auxiliary, prefix); + } + uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const { if (variableType.isBooleanType()) { return numberOfBooleanVariables; diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index c0bda2a5c..cef581dcf 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -230,9 +230,37 @@ namespace storm { * * @param variableType The type of the variable to declare. * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. * @return The variable. */ - Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false); + Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with rational type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshRationalVariable(bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with Boolean type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshBooleanVariable(bool auxiliary = false, std::string const& prefix = "x"); + + /*! + * Declares a variable with integer type whose name is guaranteed to be unique and not yet in use. + * + * @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable. + * @param prefix The prefix which should be used. + * @return The variable. + */ + Variable declareFreshIntegerVariable(bool auxiliary = false, std::string const& prefix = "x"); /*! * Retrieves the number of variables. From ec74d015572a588760751f4490a8b60c2e646c7e Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 3 Aug 2015 14:04:23 +0200 Subject: [PATCH 2/6] Fix in the comment. Former-commit-id: fe3ff1d2a0972c573deeac85dc1493ed45a1f311 --- src/storage/SparseMatrix.h | 58 +++++++++++++++++++------------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index df682d756..35ff09658 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -385,7 +385,7 @@ namespace storm { index_type getNumberOfEntries() const; private: - // The pointer to the columnd and value of the first entry. + // The pointer to the column and value of the first entry. const_iterator beginIterator; // The number of non-zero entries in the rows. @@ -492,33 +492,33 @@ namespace storm { */ index_type getEntryCount() const; - /*! - * Returns the number of entries in the given row group of the matrix. - * - * @return The number of entries in the given row group of the matrix. - */ - uint_fast64_t getRowGroupEntryCount(uint_fast64_t const group) const; + /*! + * Returns the number of entries in the given row group of the matrix. + * + * @return The number of entries in the given row group of the matrix. + */ + uint_fast64_t getRowGroupEntryCount(uint_fast64_t const group) const; - /*! - * Returns the cached number of nonzero entries in the matrix. - * - * @see updateNonzeroEntryCount() - * - * @return The number of nonzero entries in the matrix. - */ - index_type getNonzeroEntryCount() const; + /*! + * Returns the cached number of nonzero entries in the matrix. + * + * @see updateNonzeroEntryCount() + * + * @return The number of nonzero entries in the matrix. + */ + index_type getNonzeroEntryCount() const; - /*! - * Recompute the nonzero entry count - */ - void updateNonzeroEntryCount() const; + /*! + * Recompute the nonzero entry count + */ + void updateNonzeroEntryCount() const; - /*! - * Change the nonzero entry count by the provided value. - * - * @param difference Difference between old and new nonzero entry count. - */ - void updateNonzeroEntryCount(std::make_signed::type difference); + /*! + * Change the nonzero entry count by the provided value. + * + * @param difference Difference between old and new nonzero entry count. + */ + void updateNonzeroEntryCount(std::make_signed::type difference); /*! * Returns the number of row groups in the matrix. @@ -622,13 +622,13 @@ namespace storm { /*! * Transposes the matrix. - * - * @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows. - * @param keepZeros A flag indicating whether entries with value zero should be kept. + * + * @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows. + * @param keepZeros A flag indicating whether entries with value zero should be kept. * * @return A sparse matrix that represents the transpose of this matrix. */ - storm::storage::SparseMatrix transpose(bool joinGroups = false, bool keepZeros = false) const; + storm::storage::SparseMatrix transpose(bool joinGroups = false, bool keepZeros = false) const; /*! * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). From d62539165e028328e4d58aabca76c5a8f3c08398 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 3 Aug 2015 15:36:45 +0200 Subject: [PATCH 3/6] 'Identity updates' can now be described as applying 'true' in PRISM programs. Former-commit-id: b2f70eb465618290b2bd9467bd8254ef2a49c273 --- src/parser/PrismParser.cpp | 2 +- test/functional/parser/PrismParserTest.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index a7e1f522d..bff8c71b8 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -133,7 +133,7 @@ namespace storm { assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); - assignmentDefinitionList %= +assignmentDefinition % "&"; + assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index a3fbc7526..e386b7682 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -40,6 +40,7 @@ TEST(PrismParser, SimpleTest) { [] x=3 -> 1:(x'=1); [] x=3 -> 1:(x'=4); [] x=4 -> 1:(x'=5); + [] x=5 -> 1: true; endmodule)"; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1, result.getNumberOfModules()); From ecb37ccd1d9b16186954f4fe1362da718b6d1929 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 3 Aug 2015 16:09:49 +0200 Subject: [PATCH 4/6] made compilation of ConstraintCollector in Dtmc predicated on CARL being available Former-commit-id: 8d0e3ea6365fc72ee266c1aeae49024599b895ec --- src/models/sparse/Dtmc.cpp | 2 ++ src/models/sparse/Dtmc.h | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index f2f197428..f1248af39 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -182,6 +182,7 @@ namespace storm { // return storm::models::Dtmc(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels); } +#ifdef STORM_HAVE_CARL template Dtmc::ConstraintCollector::ConstraintCollector(Dtmc const& dtmc) { process(dtmc); @@ -221,6 +222,7 @@ namespace storm { void Dtmc::ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { process(dtmc); } +#endif template bool Dtmc::checkValidityOfProbabilityMatrix() const { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 37095f05e..43ec31487 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -59,6 +59,7 @@ namespace storm { */ Dtmc getSubDtmc(storm::storage::BitVector const& states) const; +#ifdef STORM_HAVE_CARL class ConstraintCollector { private: // A set of constraints that says that the DTMC actually has valid probability distributions in all states. @@ -118,6 +119,7 @@ namespace storm { */ bool checkValidityOfProbabilityMatrix() const; }; +#endif } // namespace sparse } // namespace models From f879c608ebaa288a118395eb487b75b002e548d6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 3 Aug 2015 16:25:09 +0200 Subject: [PATCH 5/6] fix for wrong ifdef Former-commit-id: dd17e10d08a5d1daadede33e0a8ad3dfad3db08c --- src/models/sparse/Dtmc.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 43ec31487..af1d2ad3f 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -110,7 +110,8 @@ namespace storm { void operator()(storm::models::sparse::Dtmc const& dtmc); }; - +#endif + private: /*! * Checks the probability matrix for validity. @@ -119,7 +120,6 @@ namespace storm { */ bool checkValidityOfProbabilityMatrix() const; }; -#endif } // namespace sparse } // namespace models From 9c0b5b028c48950904b2ca9a5fda2b6e60ebe4af Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 3 Aug 2015 18:14:13 +0200 Subject: [PATCH 6/6] Finding z3 in system, cleaned some cmakelists. Former-commit-id: 67ab9f7a0cf81fa3adf757981097a01d75b333a1 --- CMakeLists.txt | 61 +++++++----------------------------- resources/cmake/FindZ3.cmake | 47 +++++++++++++++++++++++++++ storm-config.h.in | 8 ++--- 3 files changed, 63 insertions(+), 53 deletions(-) create mode 100644 resources/cmake/FindZ3.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 768e0d071..9925cde30 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,7 +28,6 @@ option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precom option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") -set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") set(MSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).") set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") @@ -61,6 +60,7 @@ find_package(Gurobi) find_package(TBB) find_package(Threads REQUIRED) find_package(GMP) +find_package(Z3) # If the DEBUG option was turned on, we will target a debug version and a release version otherwise. if (STORM_DEBUG) @@ -82,12 +82,6 @@ else() set(ENABLE_CUDA ON) endif() -if ("${Z3_ROOT}" STREQUAL "") - set(ENABLE_Z3 OFF) -else() - set(ENABLE_Z3 ON) - set(Z3_LIB_NAME "z3") -endif() if ("${MSAT_ROOT}" STREQUAL "") set(ENABLE_MSAT OFF) @@ -142,10 +136,6 @@ elseif(MSVC) # since nobody cares at the moment add_definitions(/wd4250) - if(ENABLE_Z3) - set(Z3_LIB_NAME "libz3") - endif() - # MSVC does not do strict-aliasing, so no option needed else(CLANG) set(STORM_COMPILED_BY "Clang (LLVM)") @@ -209,11 +199,7 @@ message(STATUS "StoRM - Version information: ${STORM_CPP_VERSION_MAJOR}.${STORM_ # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") # Gurobi Defines -if (ENABLE_GUROBI) - set(STORM_CPP_GUROBI_DEF "define") -else() - set(STORM_CPP_GUROBI_DEF "undef") -endif() +set(STORM_HAVE_GUROBI ${ENABLE_GUROBI}) # CUDA Defines if (ENABLE_CUDA) @@ -223,24 +209,16 @@ else() endif() # glpk defines -set(STORM_CPP_GLPK_DEF "define") +set(STORM_HAVE_GLPK 1) # CUDA Defines set(STORM_CPP_CUDAFORSTORM_DEF "undef") # Z3 Defines -if (ENABLE_Z3) - set(STORM_CPP_Z3_DEF "define") -else() - set(STORM_CPP_Z3_DEF "undef") -endif() +set(STORM_HAVE_Z3 ${FOUND_Z3}) # MathSAT Defines -if (ENABLE_MSAT) - set(STORM_CPP_MSAT_DEF "define") -else() - set(STORM_CPP_MSAT_DEF "undef") -endif() +set(STORM_HAVE_MSAT ${ENABLE_MSAT}) # Intel TBB Defines if (TBB_FOUND AND STORM_USE_INTELTBB) @@ -474,9 +452,6 @@ if (ENABLE_GUROBI) endif() #link_directories("${GUROBI_ROOT}/lib") endif() -if (ENABLE_Z3) - link_directories("${Z3_ROOT}/bin") -endif() if (ENABLE_MSAT) link_directories("${MSAT_ROOT}/lib") endif() @@ -548,8 +523,6 @@ if (ENABLE_GUROBI) message (STATUS "StoRM - Linking with Gurobi (include: ${GUROBI_INCLUDE_DIRS})") include_directories(${GUROBI_INCLUDE_DIRS}) target_link_libraries(storm ${GUROBI_LIBRARY}) - target_link_libraries(storm-functional-tests ${GUROBI_LIBRARY}) - target_link_libraries(storm-performance-tests ${GUROBI_LIBRARY}) endif(ENABLE_GUROBI) ############################################################# @@ -559,11 +532,8 @@ endif(ENABLE_GUROBI) ############################################################# if (ENABLE_CUDA) message (STATUS "StoRM - Linking with CUDA") - target_link_libraries(storm ${STORM_CUDA_LIB_NAME}) - target_link_libraries(storm-functional-tests ${STORM_CUDA_LIB_NAME}) - target_link_libraries(storm-performance-tests ${STORM_CUDA_LIB_NAME}) - - include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") + target_link_libraries(storm ${STORM_CUDA_LIB_NAME}) + include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") endif(ENABLE_CUDA) ############################################################# @@ -589,11 +559,12 @@ include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") ## Z3 (optional) ## ############################################################# -if (ENABLE_Z3) +if(STORM_HAVE_Z3) message (STATUS "StoRM - Linking with Z3") - include_directories("${Z3_ROOT}/include") - target_link_libraries(storm ${Z3_LIB_NAME}) -endif(ENABLE_Z3) + include_directories(${Z3_INCLUDE_DIRS}) + target_link_libraries(storm ${Z3_LIBRARIES}) +endif(STORM_HAVE_Z3) + ############################################################# ## @@ -605,8 +576,6 @@ if(STORM_HAVE_CARL) message(STATUS "StoRM - Linking with carl.") include_directories("${carl_INCLUDE_DIR}") target_link_libraries(storm lib_carl) - target_link_libraries(storm-functional-tests lib_carl) - target_link_libraries(storm-performance-tests lib_carl) endif() ############################################################# @@ -618,18 +587,12 @@ if (ENABLE_MSAT) message (STATUS "StoRM - Linking with MathSAT") include_directories("${MSAT_ROOT}/include") target_link_libraries(storm "mathsat") - target_link_libraries(storm-functional-tests "mathsat") - target_link_libraries(storm-performance-tests "mathsat") if(GMP_FOUND) include_directories("${GMP_INCLUDE_DIR}") target_link_libraries(storm "gmp") - target_link_libraries(storm-functional-tests "gmp") - target_link_libraries(storm-performance-tests "gmp") elseif(MPIR_FOUND) include_directories("${GMP_INCLUDE_DIR}") target_link_libraries(storm "mpir" "mpirxx") - target_link_libraries(storm-functional-tests "mpir" "mpirxx") - target_link_libraries(storm-performance-tests "mpir" "mpirxx") else(GMP_FOUND) message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") endif(GMP_FOUND) diff --git a/resources/cmake/FindZ3.cmake b/resources/cmake/FindZ3.cmake new file mode 100644 index 000000000..8b18ac133 --- /dev/null +++ b/resources/cmake/FindZ3.cmake @@ -0,0 +1,47 @@ +# - Try to find libz3 +# Once done this will define +# LIBZ3_FOUND - System has libz3 +# LIBZ3_INCLUDE_DIRS - The libz3 include directories +# LIBZ3_LIBRARIES - The libraries needed to use libz3 + +# dependencies +# -- TODO -- needed? + +# find include dir by searching for a concrete file, which definetely must be in it +find_path(Z3_INCLUDE_DIR + NAMES src/util/z3_exception.h #exemplary file, should only be available in z3 + PATHS ENV PATH INCLUDE + PATH_SUFFIXES z3 + ) + +# find library +find_library(Z3_LIBRARY + NAMES z3 + PATHS /usr/local/include/z3/build ENV PATH INCLUDE + ) + +find_program(Z3_EXEC + NAMES z3 + PATHS ENV PATH INCLUDE) + +# set up the final variables +set(Z3_LIBRARIES ${Z3_LIBRARY}) +set(Z3_INCLUDE_DIRS ${Z3_INCLUDE_DIR}/src/util) +set(Z3_SOLVER ${Z3_EXEC}) + +# set the LIBZ3_FOUND variable by utilizing the following macro +# (which also handles the REQUIRED and QUIET arguments) +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(z3 DEFAULT_MSG + Z3_LIBRARY Z3_INCLUDE_DIR) + +IF (NOT Z3_FIND_QUIETLY) + MESSAGE(STATUS "Found Z3: ${Z3_LIBRARY}") +ENDIF (NOT Z3_FIND_QUIETLY) + +# debug output to see if everything went well +#message(${Z3_INCLUDE_DIR}) +#message(${Z3_LIBRARY}) + +# make the set variables only visible in advanced mode +mark_as_advanced(Z3_LIBRARY Z3_INCLUDE_DIR Z3_SOLVER) \ No newline at end of file diff --git a/storm-config.h.in b/storm-config.h.in index 94de0014e..edab04fa6 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -15,22 +15,22 @@ #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" // Whether Gurobi is available and to be used (define/undef) -#@STORM_CPP_GUROBI_DEF@ STORM_HAVE_GUROBI +#cmakedefine STORM_HAVE_GUROBI // Whether CUDA is available (define/undef) #@STORM_CPP_CUDA_DEF@ STORM_HAVE_CUDA // Whether GLPK is available and to be used (define/undef) -#@STORM_CPP_GLPK_DEF@ STORM_HAVE_GLPK +#cmakedefine STORM_HAVE_GLPK // Whether CudaForStorm is available and to be used (define/undef) #@STORM_CPP_CUDAFORSTORM_DEF@ STORM_HAVE_CUDAFORSTORM // Whether Z3 is available and to be used (define/undef) -#@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3 +#cmakedefine STORM_HAVE_Z3 // Whether MathSAT is available and to be used (define/undef) -#@STORM_CPP_MSAT_DEF@ STORM_HAVE_MSAT +#cmakedefine STORM_HAVE_MSAT // Whether Intel Threading Building Blocks are available and to be used (define/undef) #@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB