From ba81925c1d1aa4facd4019d19835638a63621309 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 9 Aug 2016 16:30:34 +0200 Subject: [PATCH] renamed smt2smtsolver to smtlibsmtsolver and cleaned make files Former-commit-id: 78c74dc9a54a3c62b0c0608febf9bf22998389ae --- CMakeLists.txt | 6 ++- .../cmake/{ => find_modules}/FindCLN.cmake | 0 .../cmake/{ => find_modules}/FindCUDD.cmake | 0 .../cmake/{ => find_modules}/FindCusp.cmake | 0 .../cmake/{ => find_modules}/FindGLPK.cmake | 0 .../cmake/{ => find_modules}/FindGMP.cmake | 0 .../cmake/{ => find_modules}/FindGiNaC.cmake | 0 .../cmake/{ => find_modules}/FindGurobi.cmake | 0 .../cmake/{ => find_modules}/FindHwloc.cmake | 0 .../cmake/{ => find_modules}/FindTBB.cmake | 0 .../cmake/{ => find_modules}/FindThrust.cmake | 0 .../cmake/{ => find_modules}/FindXerces.cmake | 0 .../cmake/{ => find_modules}/FindZ3.cmake | 0 .../GetGitRevisionDescription.cmake | 6 +-- .../GetGitRevisionDescription.cmake.in | 0 .../cmake/macros/RegisterSourceGroup.cmake | 21 ++++++++ resources/cmake/{ => macros}/cotire.cmake | 20 ++++---- src/CMakeLists.txt | 21 +------- .../region/SparseDtmcRegionModelChecker.cpp | 2 +- .../region/SparseDtmcRegionModelChecker.h | 4 +- src/settings/modules/Smt2SmtSolverSettings.h | 2 +- ...{Smt2SmtSolver.cpp => SmtlibSmtSolver.cpp} | 50 +++++++++---------- .../{Smt2SmtSolver.h => SmtlibSmtSolver.h} | 14 +++--- src/utility/ModelInstantiator.cpp | 4 +- src/utility/region.cpp | 8 +-- test/CMakeLists.txt | 2 +- 26 files changed, 81 insertions(+), 79 deletions(-) rename resources/cmake/{ => find_modules}/FindCLN.cmake (100%) rename resources/cmake/{ => find_modules}/FindCUDD.cmake (100%) rename resources/cmake/{ => find_modules}/FindCusp.cmake (100%) rename resources/cmake/{ => find_modules}/FindGLPK.cmake (100%) rename resources/cmake/{ => find_modules}/FindGMP.cmake (100%) rename resources/cmake/{ => find_modules}/FindGiNaC.cmake (100%) rename resources/cmake/{ => find_modules}/FindGurobi.cmake (100%) rename resources/cmake/{ => find_modules}/FindHwloc.cmake (100%) rename resources/cmake/{ => find_modules}/FindTBB.cmake (100%) rename resources/cmake/{ => find_modules}/FindThrust.cmake (100%) rename resources/cmake/{ => find_modules}/FindXerces.cmake (100%) rename resources/cmake/{ => find_modules}/FindZ3.cmake (100%) rename resources/cmake/{ => macros}/GetGitRevisionDescription.cmake (95%) rename resources/cmake/{ => macros}/GetGitRevisionDescription.cmake.in (100%) create mode 100644 resources/cmake/macros/RegisterSourceGroup.cmake rename resources/cmake/{ => macros}/cotire.cmake (99%) rename src/solver/{Smt2SmtSolver.cpp => SmtlibSmtSolver.cpp} (88%) rename src/solver/{Smt2SmtSolver.h => SmtlibSmtSolver.h} (93%) diff --git a/CMakeLists.txt b/CMakeLists.txt index c53d049b3..6e749e419 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -9,10 +9,12 @@ include_directories("${PROJECT_SOURCE_DIR}/src") # Add the resources/cmake folder to Module Search Path for FindTBB.cmake -set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/") - +set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/find_modules" "${PROJECT_SOURCE_DIR}/resources/cmake/macros") include(ExternalProject) + + +include(RegisterSourceGroup) ############################################################# ## ## CMake options of StoRM diff --git a/resources/cmake/FindCLN.cmake b/resources/cmake/find_modules/FindCLN.cmake similarity index 100% rename from resources/cmake/FindCLN.cmake rename to resources/cmake/find_modules/FindCLN.cmake diff --git a/resources/cmake/FindCUDD.cmake b/resources/cmake/find_modules/FindCUDD.cmake similarity index 100% rename from resources/cmake/FindCUDD.cmake rename to resources/cmake/find_modules/FindCUDD.cmake diff --git a/resources/cmake/FindCusp.cmake b/resources/cmake/find_modules/FindCusp.cmake similarity index 100% rename from resources/cmake/FindCusp.cmake rename to resources/cmake/find_modules/FindCusp.cmake diff --git a/resources/cmake/FindGLPK.cmake b/resources/cmake/find_modules/FindGLPK.cmake similarity index 100% rename from resources/cmake/FindGLPK.cmake rename to resources/cmake/find_modules/FindGLPK.cmake diff --git a/resources/cmake/FindGMP.cmake b/resources/cmake/find_modules/FindGMP.cmake similarity index 100% rename from resources/cmake/FindGMP.cmake rename to resources/cmake/find_modules/FindGMP.cmake diff --git a/resources/cmake/FindGiNaC.cmake b/resources/cmake/find_modules/FindGiNaC.cmake similarity index 100% rename from resources/cmake/FindGiNaC.cmake rename to resources/cmake/find_modules/FindGiNaC.cmake diff --git a/resources/cmake/FindGurobi.cmake b/resources/cmake/find_modules/FindGurobi.cmake similarity index 100% rename from resources/cmake/FindGurobi.cmake rename to resources/cmake/find_modules/FindGurobi.cmake diff --git a/resources/cmake/FindHwloc.cmake b/resources/cmake/find_modules/FindHwloc.cmake similarity index 100% rename from resources/cmake/FindHwloc.cmake rename to resources/cmake/find_modules/FindHwloc.cmake diff --git a/resources/cmake/FindTBB.cmake b/resources/cmake/find_modules/FindTBB.cmake similarity index 100% rename from resources/cmake/FindTBB.cmake rename to resources/cmake/find_modules/FindTBB.cmake diff --git a/resources/cmake/FindThrust.cmake b/resources/cmake/find_modules/FindThrust.cmake similarity index 100% rename from resources/cmake/FindThrust.cmake rename to resources/cmake/find_modules/FindThrust.cmake diff --git a/resources/cmake/FindXerces.cmake b/resources/cmake/find_modules/FindXerces.cmake similarity index 100% rename from resources/cmake/FindXerces.cmake rename to resources/cmake/find_modules/FindXerces.cmake diff --git a/resources/cmake/FindZ3.cmake b/resources/cmake/find_modules/FindZ3.cmake similarity index 100% rename from resources/cmake/FindZ3.cmake rename to resources/cmake/find_modules/FindZ3.cmake diff --git a/resources/cmake/GetGitRevisionDescription.cmake b/resources/cmake/macros/GetGitRevisionDescription.cmake similarity index 95% rename from resources/cmake/GetGitRevisionDescription.cmake rename to resources/cmake/macros/GetGitRevisionDescription.cmake index 718cee684..3653b95be 100644 --- a/resources/cmake/GetGitRevisionDescription.cmake +++ b/resources/cmake/macros/GetGitRevisionDescription.cmake @@ -37,10 +37,10 @@ set(__get_git_revision_description YES) # We must run the following at "include" time, not at function call time, # to find the path to this module rather than the path to a calling list file -get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH) +get_filename_component(_gitdescmoddir GetGitRevisionDescription.cmake PATH) function(get_git_head_revision _refspecvar _hashvar) - set(GIT_PARENT_DIR "${CMAKE_CURRENT_SOURCE_DIR}") + set(GIT_PARENT_DIR ${PROJECT_SOURCE_DIR}) set(GIT_DIR "${GIT_PARENT_DIR}/.git") while(NOT EXISTS "${GIT_DIR}") # .git dir not found, search parent directories set(GIT_PREVIOUS_PARENT "${GIT_PARENT_DIR}") @@ -71,7 +71,7 @@ function(get_git_head_revision _refspecvar _hashvar) set(HEAD_FILE "${GIT_DATA}/HEAD") configure_file("${GIT_DIR}/HEAD" "${HEAD_FILE}" COPYONLY) - configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in" + configure_file("${PROJECT_SOURCE_DIR}/resources/cmake/macros/GetGitRevisionDescription.cmake.in" "${GIT_DATA}/grabRef.cmake" @ONLY) include("${GIT_DATA}/grabRef.cmake") diff --git a/resources/cmake/GetGitRevisionDescription.cmake.in b/resources/cmake/macros/GetGitRevisionDescription.cmake.in similarity index 100% rename from resources/cmake/GetGitRevisionDescription.cmake.in rename to resources/cmake/macros/GetGitRevisionDescription.cmake.in diff --git a/resources/cmake/macros/RegisterSourceGroup.cmake b/resources/cmake/macros/RegisterSourceGroup.cmake new file mode 100644 index 000000000..d609e3589 --- /dev/null +++ b/resources/cmake/macros/RegisterSourceGroup.cmake @@ -0,0 +1,21 @@ +macro(register_source_groups_from_filestructure list_of_files) + foreach(FILE ${list_of_files}) + message(${FILE}) + get_filename_component(PARENT_DIR "${FILE}" PATH) + + # skip src or include and changes /'s to \\'s + string(REPLACE ${PROJECT_SOURCE_DIR} "" PARENT_DIR "${PARENT_DIR}") + string(REGEX REPLACE "(\\./)?(src|include)/?" "" GROUP "${PARENT_DIR}") + string(REPLACE "/" "\\" GROUP "${GROUP}") + message(${GROUP}) + + # group into "Source Files" and "Header Files" + # if ("${FILE}" MATCHES ".*\\.cpp") + # set(GROUP "Source Files\\${GROUP}") + # elseif("${FILE}" MATCHES ".*\\.h") + # set(GROUP "Header Files\\${GROUP}") + # endif() + + source_group("${GROUP}" FILES "${FILE}") + endforeach() +endmacro() \ No newline at end of file diff --git a/resources/cmake/cotire.cmake b/resources/cmake/macros/cotire.cmake similarity index 99% rename from resources/cmake/cotire.cmake rename to resources/cmake/macros/cotire.cmake index 3cc087a97..443e0d17d 100644 --- a/resources/cmake/cotire.cmake +++ b/resources/cmake/macros/cotire.cmake @@ -44,7 +44,7 @@ if (NOT CMAKE_SCRIPT_MODE_FILE) cmake_policy(POP) endif() -set (COTIRE_CMAKE_MODULE_FILE "${CMAKE_CURRENT_LIST_FILE}") +set (COTIRE_CMAKE_MODULE_FILE "cotire.cmake") set (COTIRE_CMAKE_MODULE_VERSION "1.3.4") include(CMakeParseArguments) @@ -89,7 +89,7 @@ endfunction() function (cotire_get_source_file_extension _sourceFile _extVar) # get_filename_component returns extension from first occurrence of . in file name # this function computes the extension from last occurrence of . in file name - string (FIND "${_sourceFile}" "." _index REVERSE) + string (FIND "${_sourceFile}" ".." _index REVERSE) if (_index GREATER -1) math (EXPR _index "${_index} + 1") string (SUBSTRING "${_sourceFile}" ${_index} -1 _sourceExt) @@ -476,7 +476,7 @@ function (cotire_get_target_compile_definitions _config _language _directory _ta string (TOUPPER "${_config}" _upperConfig) set (_configDefinitions "") # CMAKE_INTDIR for multi-configuration build systems - if (NOT "${CMAKE_CFG_INTDIR}" STREQUAL ".") + if (NOT "${CMAKE_CFG_INTDIR}" STREQUAL "..") list (APPEND _configDefinitions "CMAKE_INTDIR=\"${_config}\"") endif() # target export define symbol @@ -815,10 +815,10 @@ endmacro() function (cotire_parse_includes _language _scanOutput _ignoredIncudeDirs _honoredIncudeDirs _ignoredExtensions _selectedIncludesVar _unparsedLinesVar) if (WIN32) # prevent CMake macro invocation errors due to backslash characters in Windows paths - string (REPLACE "\\" "/" _scanOutput "${_scanOutput}") + string (REPLACE "\\" "." _scanOutput "${_scanOutput}") endif() # canonize slashes - string (REPLACE "//" "/" _scanOutput "${_scanOutput}") + string (REPLACE "//" "." _scanOutput "${_scanOutput}") # prevent semicolon from being interpreted as a line separator string (REPLACE ";" "\\;" _scanOutput "${_scanOutput}") # then separate lines @@ -954,7 +954,7 @@ function (cotire_scan_includes _includesVar) # cl.exe messes with the output streams unless the environment variable VS_UNICODE_OUTPUT is cleared unset (ENV{VS_UNICODE_OUTPUT}) endif() - execute_process(COMMAND ${_cmd} WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" + execute_process(COMMAND ${_cmd} WORKING_DIRECTORY ".." RESULT_VARIABLE _result OUTPUT_QUIET ERROR_VARIABLE _output) if (_result) message (STATUS "Result ${_result} scanning includes of ${_existingSourceFiles}.") @@ -1453,7 +1453,7 @@ function (cotire_precompile_prefix_header _prefixFile _pchFile _hostFile) # cl.exe messes with the output streams unless the environment variable VS_UNICODE_OUTPUT is cleared unset (ENV{VS_UNICODE_OUTPUT}) endif() - execute_process(COMMAND ${_cmd} WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" RESULT_VARIABLE _result) + execute_process(COMMAND ${_cmd} WORKING_DIRECTORY ".." RESULT_VARIABLE _result) if (_result) message (FATAL_ERROR "Error ${_result} precompiling ${_prefixFile}.") endif() @@ -2278,7 +2278,7 @@ function (cotire_setup_unity_build_target _languages _configurations _targetSour endif() # if cotire is applied to a target which has not been added in the current source dir, # non-existing files cannot be referenced from the unity build target (this is a CMake restriction) - if (NOT "${_targetSourceDir}" STREQUAL "${CMAKE_CURRENT_SOURCE_DIR}") + if (NOT "${_targetSourceDir}" STREQUAL "..") set (_nonExistingFiles "") foreach (_file ${_unityTargetSources}) if (NOT EXISTS "${_file}") @@ -2419,7 +2419,7 @@ function (cotire_target _target) set(_multiValueArgs LANGUAGES CONFIGURATIONS) cmake_parse_arguments(_option "${_options}" "${_oneValueArgs}" "${_multiValueArgs}" ${ARGN}) if (NOT _option_SOURCE_DIR) - set (_option_SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}") + set (_option_SOURCE_DIR "..") endif() if (NOT _option_BINARY_DIR) set (_option_BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}") @@ -2562,7 +2562,7 @@ function (cotire) cmake_parse_arguments(_option "${_options}" "${_oneValueArgs}" "${_multiValueArgs}" ${ARGN}) set (_targets ${_option_UNPARSED_ARGUMENTS}) if (NOT _option_SOURCE_DIR) - set (_option_SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}") + set (_option_SOURCE_DIR "..") endif() if (NOT _option_BINARY_DIR) set (_option_BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}") diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4e00d57f0..1a46888ae 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -25,26 +25,7 @@ set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.cpp) -foreach(FILE ${ALL_FILES}) - get_filename_component(PARENT_DIR "${FILE}" PATH) - - # skip src or include and changes /'s to \\'s - string(REPLACE ${PROJECT_SOURCE_DIR} "" PARENT_DIR "${PARENT_DIR}") - message(${PARENT_DIR}) - string(REGEX REPLACE "(\\./)?(src|include)/?" "" GROUP "${PARENT_DIR}") - string(REPLACE "/" "\\" GROUP "${GROUP}") - - - # group into "Source Files" and "Header Files" - # if ("${FILE}" MATCHES ".*\\.cpp") - # set(GROUP "Source Files\\${GROUP}") - # elseif("${FILE}" MATCHES ".*\\.h") - # set(GROUP "Header Files\\${GROUP}") - # endif() - - source_group("${GROUP}" FILES "${FILE}") -endforeach() - +register_source_groups_from_filestructure("${ALL_FILES}") # Add custom additional include or link directories if (ADDITIONAL_INCLUDE_DIRS) message(STATUS "StoRM - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index c02ce14cc..099eeb62f 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -595,7 +595,7 @@ namespace storm { STORM_LOG_DEBUG("Initializing the Smt Solver"); storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. - this->smtSolver = std::shared_ptr(new storm::solver::Smt2SmtSolver(manager, true)); + this->smtSolver = std::shared_ptr(new storm::solver::SmtlibSmtSolver(manager, true)); ParametricType bound= storm::utility::region::convertNumber(this->getSpecifiedFormulaBound()); diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 868ebe8b7..8a5e8e559 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -6,7 +6,7 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/Dtmc.h" #include "src/utility/region.h" -#include "src/solver/Smt2SmtSolver.h" +#include "src/solver/SmtlibSmtSolver.h" namespace storm { namespace modelchecker { @@ -119,7 +119,7 @@ namespace storm { std::shared_ptr reachabilityFunction; // the smt solver that is used to prove properties with the help of the reachabilityFunction - std::shared_ptr smtSolver; + std::shared_ptr smtSolver; }; } //namespace region diff --git a/src/settings/modules/Smt2SmtSolverSettings.h b/src/settings/modules/Smt2SmtSolverSettings.h index a6a3da920..58f3bb3ed 100644 --- a/src/settings/modules/Smt2SmtSolverSettings.h +++ b/src/settings/modules/Smt2SmtSolverSettings.h @@ -13,7 +13,7 @@ namespace storm { class Smt2SmtSolverSettings : public ModuleSettings { public: /*! - * Creates a new set of Smt2SmtSolver settings that is managed by the given manager. + * Creates a new set of SmtlibSmtSolver settings that is managed by the given manager. * * @param settingsManager The responsible manager. */ diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/SmtlibSmtSolver.cpp similarity index 88% rename from src/solver/Smt2SmtSolver.cpp rename to src/solver/SmtlibSmtSolver.cpp index 229fcb351..fbc852749 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/SmtlibSmtSolver.cpp @@ -7,7 +7,7 @@ #include #endif -#include "src/solver/Smt2SmtSolver.h" +#include "src/solver/SmtlibSmtSolver.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/Smt2SmtSolverSettings.h" @@ -23,23 +23,23 @@ namespace storm { namespace solver { - Smt2SmtSolver::Smt2ModelReference::Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager), expressionAdapter(expressionAdapter){ + SmtlibSmtSolver::SmtlibModelReference::SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager), expressionAdapter(expressionAdapter){ // Intentionally left empty. } - bool Smt2SmtSolver::Smt2ModelReference::getBooleanValue(storm::expressions::Variable const& variable) const { + bool SmtlibSmtSolver::SmtlibModelReference::getBooleanValue(storm::expressions::Variable const& variable) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - int_fast64_t Smt2SmtSolver::Smt2ModelReference::getIntegerValue(storm::expressions::Variable const& variable) const { + int_fast64_t SmtlibSmtSolver::SmtlibModelReference::getIntegerValue(storm::expressions::Variable const& variable) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - double Smt2SmtSolver::Smt2ModelReference::getRationalValue(storm::expressions::Variable const& variable) const { + double SmtlibSmtSolver::SmtlibModelReference::getRationalValue(storm::expressions::Variable const& variable) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) { + SmtlibSmtSolver::SmtlibSmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), useCarlExpressions(useCarlExpressions) { #ifndef STORM_HAVE_CARL STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL"); #endif @@ -50,7 +50,7 @@ namespace storm { init(); } - Smt2SmtSolver::~Smt2SmtSolver() { + SmtlibSmtSolver::~SmtlibSmtSolver() { writeCommand("( exit )", false); //do not wait for success because it does not matter at this point and may cause problems if the solver is not running properly #ifndef WINDOWS if(processIdOfSolver!=0){ @@ -63,32 +63,32 @@ namespace storm { #endif } - void Smt2SmtSolver::push() { + void SmtlibSmtSolver::push() { expressionAdapter->increaseScope(); writeCommand("( push 1 ) ", true); } - void Smt2SmtSolver::pop() { + void SmtlibSmtSolver::pop() { expressionAdapter->decreaseScope(); writeCommand("( pop 1 ) ", true); } - void Smt2SmtSolver::pop(uint_fast64_t n) { + void SmtlibSmtSolver::pop(uint_fast64_t n) { expressionAdapter->decreaseScope(n); writeCommand("( pop " + std::to_string(n) + " ) ", true); } - void Smt2SmtSolver::reset() { + void SmtlibSmtSolver::reset() { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - void Smt2SmtSolver::add(storm::expressions::Expression const& assertion) { + void SmtlibSmtSolver::add(storm::expressions::Expression const& assertion) { STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions"); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } #ifdef STORM_HAVE_CARL - void Smt2SmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) { + void SmtlibSmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) { STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions"); //if some of the occurring variables are not declared yet, we will have to. std::set variables; @@ -101,11 +101,11 @@ namespace storm { writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true); } - void Smt2SmtSolver::add(storm::ArithConstraint const& constraint) { + void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { add(constraint.lhs(), constraint.rel()); } - void Smt2SmtSolver::add(storm::ArithConstraint const& constraint) { + void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { //if some of the occurring variables are not declared yet, we will have to. std::set variables = constraint.lhs().gatherVariables(); std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); @@ -115,7 +115,7 @@ namespace storm { writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); } - void Smt2SmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint){ + void SmtlibSmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint){ STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool."); //if some of the occurring variables are not declared yet, we will have to (including the guard!). std::set variables = constraint.lhs().gatherVariables(); @@ -128,7 +128,7 @@ namespace storm { writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true); } - void Smt2SmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ + void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); std::set variableSet; variableSet.insert(variable); @@ -147,7 +147,7 @@ namespace storm { #endif - SmtSolver::CheckResult Smt2SmtSolver::check() { + SmtSolver::CheckResult SmtlibSmtSolver::check() { writeCommand("( check-sat )", false); #ifdef WINDOWS STORM_LOG_WARN("SMT-LIBv2 Solver can not be started on Windows as this is not yet implemented. Assume that the check-result is \"unknown\""); @@ -172,18 +172,18 @@ namespace storm { #endif } - SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set const& assumptions) { + SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::set const& assumptions) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } #ifndef WINDOWS - SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { + SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } #endif - void Smt2SmtSolver::init() { + void SmtlibSmtSolver::init() { if (storm::settings::getModule().isSolverCommandSet()){ #ifdef WINDOWS STORM_LOG_WARN("opening a thread for the smt solver is not implemented on Windows. Hence, no actual solving will be done") @@ -256,11 +256,11 @@ namespace storm { //writeCommand("( get-info :name )"); } - bool Smt2SmtSolver::isNeedsRestart() const { + bool SmtlibSmtSolver::isNeedsRestart() const { return this->needsRestart; } - void Smt2SmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) { + void SmtlibSmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) { if (isCommandFileOpen) { commandFile << smt2Command << std::endl; } @@ -280,7 +280,7 @@ namespace storm { #endif } - std::vector Smt2SmtSolver::readSolverOutput(bool waitForOutput){ + std::vector SmtlibSmtSolver::readSolverOutput(bool waitForOutput){ #ifndef WINDOWS if (processIdOfSolver==0){ STORM_LOG_DEBUG("failed to read solver output as the solver is not running"); @@ -332,7 +332,7 @@ namespace storm { #endif } - void Smt2SmtSolver::checkForErrorMessage(const std::string message){ + void SmtlibSmtSolver::checkForErrorMessage(const std::string message){ size_t errorOccurrance = message.find("error"); //do not throw an exception for timeout or memout errors if(message.find("timeout")!=std::string::npos){ diff --git a/src/solver/Smt2SmtSolver.h b/src/solver/SmtlibSmtSolver.h similarity index 93% rename from src/solver/Smt2SmtSolver.h rename to src/solver/SmtlibSmtSolver.h index 5f455cb3d..4974aa0c4 100644 --- a/src/solver/Smt2SmtSolver.h +++ b/src/solver/SmtlibSmtSolver.h @@ -17,12 +17,12 @@ namespace storm { * It is also possible to export the SMT2 script for later use. * @note The parsing of the solver responses is a little bit crude and might cause bugs (e.g., if a variable name has the infix "error") */ - class Smt2SmtSolver : public SmtSolver { + class SmtlibSmtSolver : public SmtSolver { public: - class Smt2ModelReference : public SmtSolver::ModelReference { + class SmtlibModelReference : public SmtSolver::ModelReference { public: - Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter); + SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter); virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override; virtual double getRationalValue(storm::expressions::Variable const& variable) const override; @@ -39,8 +39,8 @@ namespace storm { * In addition to storm expressions, this solver also allows carl expressions (but not both to not confuse variables). * Hence, there is a flag to chose between the two */ - Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false); - virtual ~Smt2SmtSolver(); + SmtlibSmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false); + virtual ~SmtlibSmtSolver(); virtual void push() override; @@ -141,10 +141,10 @@ namespace storm { std::unique_ptr expressionAdapter; // A flag storing whether the last call to a check method provided aussumptions. - bool lastCheckAssumptions; + //bool lastCheckAssumptions; // The last result that was returned by any of the check methods. - CheckResult lastResult; + //CheckResult lastResult; // A flag that states whether we want to use carl expressions. bool useCarlExpressions; diff --git a/src/utility/ModelInstantiator.cpp b/src/utility/ModelInstantiator.cpp index 630f3c8d9..85addd464 100644 --- a/src/utility/ModelInstantiator.cpp +++ b/src/utility/ModelInstantiator.cpp @@ -152,9 +152,7 @@ namespace storm { template void ModelInstantiator::checkValid() const { - for(auto& functions : this->functions) { - - } + // TODO write some checks } #ifdef STORM_HAVE_CARL diff --git a/src/utility/region.cpp b/src/utility/region.cpp index 466be4d45..c733f033d 100644 --- a/src/utility/region.cpp +++ b/src/utility/region.cpp @@ -4,7 +4,7 @@ #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/settings/SettingsManager.h" -#include "src/solver/Smt2SmtSolver.h" +#include "src/solver/SmtlibSmtSolver.h" #include "src/exceptions/IllegalArgumentException.h" #include "src/exceptions/NotImplementedException.h" @@ -129,7 +129,7 @@ namespace storm { } template<> - void addGuardedConstraintToSmtSolver(std::shared_ptr solver,storm::RationalFunctionVariable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){ + void addGuardedConstraintToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){ STORM_LOG_THROW(guard.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver whose guard is not of type bool"); storm::CompareRelation compRel; switch (relation){ @@ -154,7 +154,7 @@ namespace storm { } template<> - void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){ + void addParameterBoundsToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){ storm::CompareRelation compRel; switch (relation){ case storm::logic::ComparisonType::Greater: @@ -178,7 +178,7 @@ namespace storm { } template<> - void addBoolVariableToSmtSolver(std::shared_ptr solver,storm::RationalFunctionVariable const& variable, bool value){ + void addBoolVariableToSmtSolver(std::shared_ptr solver, storm::RationalFunctionVariable const& variable, bool value){ STORM_LOG_THROW(variable.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver that is a non boolean variable. Only boolean variables are allowed"); solver->add(variable, value); } diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 615b253e3..d9498b5ce 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -3,7 +3,7 @@ file(GLOB STORM_FUNCTIONAL_TEST_MAIN_FILE ${STORM_CPP_TESTS_BASE_PATH}/functional/storm-functional-tests.cpp) file(GLOB_RECURSE STORM_FUNCTIONAL_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/functional/*.h ${STORM_CPP_TESTS_BASE_PATH}/functional/*.cpp) -source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) +register_source_groups_from_filestructure("${STORM_FUNCTIONAL_TEST_FILES}") add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES}) target_link_libraries(storm-functional-tests storm)