From 52a8c324a5b575b8d8f8ae57eec69e5696145c03 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 9 Apr 2015 16:12:12 +0200 Subject: [PATCH] make storm compile when carl is not available added settings for smt-lib solver Former-commit-id: 7d1872267aadbce6cd759dcec3e0ad83d824a7ed --- .../SparseDtmcEliminationModelChecker.cpp | 9 ++- .../SparseDtmcEliminationModelChecker.h | 9 ++- src/settings/SettingsManager.cpp | 5 ++ src/settings/SettingsManager.h | 8 +++ .../modules/Smt2SmtSolverSettings.cpp | 48 ++++++++++++++ src/settings/modules/Smt2SmtSolverSettings.h | 65 +++++++++++++++++++ src/solver/Smt2SmtSolver.cpp | 32 +++++++-- 7 files changed, 163 insertions(+), 13 deletions(-) create mode 100644 src/settings/modules/Smt2SmtSolverSettings.cpp create mode 100644 src/settings/modules/Smt2SmtSolverSettings.h diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 42927db1c..1e0cdd9ba 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -988,6 +988,7 @@ namespace storm { } } +#ifdef STORM_HAVE_CARL template<> storm::storage::SparseMatrix SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::instantiateAsDouble(std::map substitutions){ @@ -1016,6 +1017,7 @@ namespace storm { storm::storage::SparseMatrix SparseDtmcEliminationModelChecker::FlexibleSparseMatrix::instantiateAsDouble(std::map substitutions){ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Instantiation of flexible matrix is not supported for this type"); } +#endif template @@ -1045,7 +1047,7 @@ namespace storm { return flexibleMatrix; } - +#ifdef STORM_HAVE_CARL template<> bool SparseDtmcEliminationModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ //Note: this is an 'experimental' implementation @@ -1318,13 +1320,14 @@ namespace storm { return false; } - + template bool SparseDtmcEliminationModelChecker::checkRegion(storm::logic::Formula const& formula, std::vector::ParameterRegion> parameterRegions){ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type"); } - + +#endif template class SparseDtmcEliminationModelChecker; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 0a8854bc2..15aff7f86 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -21,19 +21,21 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; - + +#ifdef STORM_HAVE_CARL struct ParameterRegion{ storm::Variable variable; storm::RationalFunction::CoeffType lowerBound; storm::RationalFunction::CoeffType upperBound; }; + /*! * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals) */ bool checkRegion(storm::logic::Formula const& formula, std::vector parameterRegions); - +#endif private: @@ -66,6 +68,7 @@ namespace storm { */ bool hasSelfLoop(storm::storage::sparse::state_type state); +#ifdef STORM_HAVE_CARL /*! * Instantiates the matrix, i.e., evaluate the occurring functions according to the given substitution of the variables * @@ -74,7 +77,7 @@ namespace storm { * @return A matrix with constant (double) entries */ storm::storage::SparseMatrix instantiateAsDouble(std::map substitutions); - +#endif private: std::vector data; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index dd5761dee..89db9eb0e 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -27,6 +27,7 @@ namespace storm { this->addModule(std::unique_ptr(new modules::BisimulationSettings(*this))); this->addModule(std::unique_ptr(new modules::GlpkSettings(*this))); this->addModule(std::unique_ptr(new modules::GurobiSettings(*this))); + this->addModule(std::unique_ptr(new modules::Smt2SmtSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::TopologicalValueIterationEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::ParametricSettings(*this))); this->addModule(std::unique_ptr(new modules::SparseDtmcEliminationModelCheckerSettings(*this))); @@ -511,6 +512,10 @@ namespace storm { return dynamic_cast(manager().getModule(storm::settings::modules::GurobiSettings::moduleName)); } + storm::settings::modules::Smt2SmtSolverSettings const& smt2SmtSolverSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::Smt2SmtSolverSettings::moduleName)); + } + storm::settings::modules::TopologicalValueIterationEquationSolverSettings const& topologicalValueIterationEquationSolverSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::TopologicalValueIterationEquationSolverSettings::moduleName)); } diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index 1a97bb07a..389d51f41 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -28,6 +28,7 @@ #include "src/settings/modules/BisimulationSettings.h" #include "src/settings/modules/GlpkSettings.h" #include "src/settings/modules/GurobiSettings.h" +#include "src/settings/modules/Smt2SmtSolverSettings.h" #include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h" #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" @@ -312,6 +313,13 @@ namespace storm { */ storm::settings::modules::GurobiSettings const& gurobiSettings(); + /*! + * Retrieves the settings of the SMT-LIBv2 SMT solver. + * + * @return the settings of SMT-LIBv2 SMT solver. + */ + storm::settings::modules::Smt2SmtSolverSettings const& smt2SmtSolverSettings(); + /*! * Retrieves the settings of the topological value iteration-based equation solver. * diff --git a/src/settings/modules/Smt2SmtSolverSettings.cpp b/src/settings/modules/Smt2SmtSolverSettings.cpp new file mode 100644 index 000000000..8d63f7bb2 --- /dev/null +++ b/src/settings/modules/Smt2SmtSolverSettings.cpp @@ -0,0 +1,48 @@ +#include "src/settings/modules/Smt2SmtSolverSettings.h" + +#include "src/settings/SettingsManager.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string Smt2SmtSolverSettings::moduleName = "smt2smtsolver"; + const std::string Smt2SmtSolverSettings::solverCommandOption = "solvercommand"; + const std::string Smt2SmtSolverSettings::exportSmtLibScriptOption = "exportSmtLibScript"; + + Smt2SmtSolverSettings::Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, solverCommandOption, true, "If set, this command is used to call the solver and to let the solver know that it should read SMT-LIBv2 commands from standard input. If not set, only a SMT-LIB script file might be exported.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("command", "path to the solver + command line arguments.").setDefaultValueString("").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, exportSmtLibScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build()); + } + + bool Smt2SmtSolverSettings::isSolverCommandSet() const{ + return this->getOption(solverCommandOption).getHasOptionBeenSet(); + } + + std::string Smt2SmtSolverSettings::getSolverCommand() const{ + return this->getOption(solverCommandOption).getArgumentByName("command").getValueAsString(); + } + + + bool Smt2SmtSolverSettings::isExportSmtLibScriptSet() const{ + return this->getOption(exportSmtLibScriptOption).getHasOptionBeenSet(); + } + + + std::string Smt2SmtSolverSettings::getExportSmtLibScriptPath() const{ + return this->getOption(solverCommandOption).getArgumentByName("path").getValueAsString(); + } + + + bool Smt2SmtSolverSettings::check() const { + if (isSolverCommandSet() || isExportSmtLibScriptSet()) { + //TODO check if paths are valid + + } + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/Smt2SmtSolverSettings.h b/src/settings/modules/Smt2SmtSolverSettings.h new file mode 100644 index 000000000..07702affd --- /dev/null +++ b/src/settings/modules/Smt2SmtSolverSettings.h @@ -0,0 +1,65 @@ +#ifndef STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_ +#define STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for interaction with SMT-LIBv2 solvers. + */ + class Smt2SmtSolverSettings : public ModuleSettings { + public: + /*! + * Creates a new set of Smt2SmtSolver settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves whether the solver command has been set. + * + * @return True iff the solver command has been set. + */ + bool isSolverCommandSet() const; + + /*! + * Retrieves the solver command i.e. the path and the command line arguments for the solver. + * + * @return The solver command to be used + */ + std::string getSolverCommand() const; + + /*! + * Retrieves whether the SMT-LIBv2 script should be exportet to a file. + * + * @return True iff the SMT-LIBv2 script should be exportet to a file. + */ + bool isExportSmtLibScriptSet() const; + + /*! + * Retrieves the path where the SMT-LIBv2 script file should be exportet to. + * + * @return the path where the SMT-LIBv2 script file should be exportet to. + */ + std::string getExportSmtLibScriptPath() const; + + bool check() const override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string solverCommandOption; + static const std::string exportSmtLibScriptOption; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_SMT2SMTSOLVERSETTINGS_H_ */ diff --git a/src/solver/Smt2SmtSolver.cpp b/src/solver/Smt2SmtSolver.cpp index d9201c09f..2ca8ec5e8 100644 --- a/src/solver/Smt2SmtSolver.cpp +++ b/src/solver/Smt2SmtSolver.cpp @@ -1,12 +1,13 @@ #include "src/solver/Smt2SmtSolver.h" +#include "src/settings/SettingsManager.h" #include "src/exceptions/NotSupportedException.h" -#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/NotImplementedException.h" +#include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/IllegalFunctionCallException.h" #include "utility/macros.h" #include "adapters/CarlAdapter.h" -#include "exceptions/IllegalArgumentException.h" -#include "exceptions/IllegalFunctionCallException.h" namespace storm { namespace solver { @@ -99,7 +100,14 @@ namespace storm { SmtSolver::CheckResult Smt2SmtSolver::check() { writeCommand("( check-sat )"); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){ + // todo get the result + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); + } + else{ + STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\""); + return SmtSolver::CheckResult::Unknown; + } } SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set const& assumptions) { @@ -114,9 +122,19 @@ namespace storm { #endif void Smt2SmtSolver::init() { - //hard coded output file.. for now - commandFile.open("/home/tim/Desktop/smtlibcommand.txt", std::ios::trunc); - STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){ + //todo call the solver! + std::string cmd = storm::settings::smt2SmtSolverSettings().getSolverCommand(); + } + else{ + STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done"); + } + + if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){ + STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file"); + commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc); + STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + } //some initial commands writeCommand("( set-logic QF_NRA )");