From c474920fa411f8ff8dd8bbbb858b449a2c3ce2c8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 18 Dec 2014 16:47:13 +0100 Subject: [PATCH] Started refactoring SMT solvers. Now displaying MathSAT version in CLI. Former-commit-id: 1736a0bb6b340595428a02fba1f36e5fab431338 --- CMakeLists.txt | 24 +- src/exceptions/NotSupportedException.h | 15 + ...hSatSmtSolver.cpp => MathsatSmtSolver.cpp} | 0 ...{MathSatSmtSolver.h => MathsatSmtSolver.h} | 9 + src/solver/SmtSolver.cpp | 62 +++ src/solver/SmtSolver.h | 379 +++++++++--------- src/solver/Z3SmtSolver.cpp | 239 +++++------ src/solver/Z3SmtSolver.h | 46 ++- src/utility/cli.h | 8 + storm-config.h.in | 4 +- storm-version.cpp.in | 57 +-- 11 files changed, 474 insertions(+), 369 deletions(-) create mode 100644 src/exceptions/NotSupportedException.h rename src/solver/{MathSatSmtSolver.cpp => MathsatSmtSolver.cpp} (100%) rename src/solver/{MathSatSmtSolver.h => MathsatSmtSolver.h} (89%) create mode 100644 src/solver/SmtSolver.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index b9ea42169..4229059b3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -29,7 +29,7 @@ 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(MathSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).") +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.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") @@ -82,10 +82,10 @@ else() set(Z3_LIB_NAME "z3") endif() -if ("${MathSAT_ROOT}" STREQUAL "") - set(ENABLE_MathSAT OFF) +if ("${MSAT_ROOT}" STREQUAL "") + set(ENABLE_MSAT OFF) else() - set(ENABLE_MathSAT ON) + set(ENABLE_MSAT ON) endif() message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") @@ -214,10 +214,10 @@ else() endif() # MathSAT Defines -if (ENABLE_MathSAT) - set(STORM_CPP_MathSAT_DEF "define") +if (ENABLE_MSAT) + set(STORM_CPP_MSAT_DEF "define") else() - set(STORM_CPP_MathSAT_DEF "undef") + set(STORM_CPP_MSAT_DEF "undef") endif() # Intel TBB Defines @@ -331,8 +331,8 @@ endif() if (ENABLE_Z3) link_directories("${Z3_ROOT}/bin") endif() -if (ENABLE_MathSAT) - link_directories("${MathSAT_ROOT}/lib") +if (ENABLE_MSAT) + link_directories("${MSAT_ROOT}/lib") endif() if(GMP_FOUND) link_directories(${GMP_LIBRARY_DIR}) @@ -439,9 +439,9 @@ endif(ENABLE_Z3) ## MathSAT (optional) ## ############################################################# -if (ENABLE_MathSAT) +if (ENABLE_MSAT) message (STATUS "StoRM - Linking with MathSAT") - include_directories("${MathSAT_ROOT}/include") + include_directories("${MSAT_ROOT}/include") target_link_libraries(storm "mathsat") target_link_libraries(storm-functional-tests "mathsat") target_link_libraries(storm-performance-tests "mathsat") @@ -458,7 +458,7 @@ if (ENABLE_MathSAT) else(GMP_FOUND) message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") endif(GMP_FOUND) -endif(ENABLE_MathSAT) +endif(ENABLE_MSAT) ############################################################# ## diff --git a/src/exceptions/NotSupportedException.h b/src/exceptions/NotSupportedException.h new file mode 100644 index 000000000..51a70d8c1 --- /dev/null +++ b/src/exceptions/NotSupportedException.h @@ -0,0 +1,15 @@ +#ifndef STORM_EXCEPTIONS_NOTSUPPORTEDEXCEPTION_H_ +#define STORM_EXCEPTIONS_NOTSUPPORTEDEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(NotSupportedException) + + } // namespace exceptions +} // namespace storm + +#endif /* STORM_EXCEPTIONS_NOTSUPPORTEDEXCEPTION_H_ */ diff --git a/src/solver/MathSatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp similarity index 100% rename from src/solver/MathSatSmtSolver.cpp rename to src/solver/MathsatSmtSolver.cpp diff --git a/src/solver/MathSatSmtSolver.h b/src/solver/MathsatSmtSolver.h similarity index 89% rename from src/solver/MathSatSmtSolver.h rename to src/solver/MathsatSmtSolver.h index 009556196..4cea5f5ee 100644 --- a/src/solver/MathSatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -18,6 +18,15 @@ namespace storm { namespace solver { class MathSatSmtSolver : public SmtSolver { public: + /*! + * A class that captures options that may be passed to Mathsat solver. + */ + class Options { + bool enableModelGeneration = false; + bool enableUnsatCoreGeneration = false; + bool enableInterpolantGeneration = false; + }; + class MathSatModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_MSAT diff --git a/src/solver/SmtSolver.cpp b/src/solver/SmtSolver.cpp new file mode 100644 index 000000000..caaeae5d6 --- /dev/null +++ b/src/solver/SmtSolver.cpp @@ -0,0 +1,62 @@ +#include "src/solver/SmtSolver.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotSupportedException.h" + +namespace storm { + namespace solver { + + SmtSolver::SmtSolver() { + // Intentionally left empty. + } + + SmtSolver::~SmtSolver() { + // Intentionally left empty. + } + + void SmtSolver::add(std::set const& assertions) { + for (storm::expressions::Expression assertion : assertions) { + this->add(assertion); + } + } + + void SmtSolver::add(std::initializer_list const& assertions) { + for (storm::expressions::Expression assertion : assertions) { + this->add(assertion); + } + } + + storm::expressions::SimpleValuation SmtSolver::getModel() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); + } + + std::vector SmtSolver::allSat(std::vector const& important) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); + } + + uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function callback) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); + } + + uint_fast64_t SmtSolver::allSat(std::vector const& important, std::function callback) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation."); + } + + std::vector SmtSolver::getUnsatCore() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of unsatisfiable cores."); + } + + std::vector SmtSolver::getUnsatAssumptions() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of unsatisfiable cores."); + } + + void SmtSolver::setInterpolationGroup(uint_fast64_t group) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); + } + + storm::expressions::Expression SmtSolver::getInterpolant(std::vector groupsA) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants."); + } + + } // namespace solver +} // namespace storm \ No newline at end of file diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 780f83a62..ae556f278 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -3,11 +3,6 @@ #include -#include "exceptions/IllegalArgumentValueException.h" -#include "exceptions/NotImplementedException.h" -#include "exceptions/IllegalArgumentTypeException.h" -#include "exceptions/IllegalFunctionCallException.h" -#include "exceptions/InvalidStateException.h" #include "storage/expressions/Expressions.h" #include "storage/expressions/SimpleValuation.h" @@ -19,224 +14,210 @@ namespace storm { namespace solver { - + /*! - * An interface that captures the functionality of an SMT solver. - */ + * An interface that captures the functionality of an SMT solver. + */ class SmtSolver { public: - //! Option flags for smt solvers. - enum class Options { - ModelGeneration = 0x01, - UnsatCoreComputation = 0x02, - InterpolantComputation = 0x04 - }; //! possible check results - enum class CheckResult { SAT, UNSAT, UNKNOWN }; - + enum class CheckResult { Sat, Unsat, Unknown }; + + /*! + * The base class for all model references. They are used to provide a lightweight method of accessing the + * models the solver generates (that is, without constructing other objects). + */ class ModelReference { public: - virtual bool getBooleanValue(std::string const& name) const =0; - virtual int_fast64_t getIntegerValue(std::string const& name) const =0; + virtual bool getBooleanValue(std::string const& name) const = 0; + virtual int_fast64_t getIntegerValue(std::string const& name) const = 0; + virtual double getDoubleValue(std::string const& name) const = 0; }; + public: /*! - * Constructs a new smt solver with the given options. - * - * @param options the options for the solver - * @throws storm::exceptions::IllegalArgumentValueException if an option is unsupported for the solver - */ - SmtSolver(Options options = Options::ModelGeneration) {}; - virtual ~SmtSolver() {}; - - SmtSolver(const SmtSolver&) = delete; - SmtSolver(const SmtSolver&&) {}; - - //! pushes a backtrackingpoint in the solver + * Constructs a new Smt solver with the given options. + * + * @throws storm::exceptions::IllegalArgumentValueException if an option is unsupported for the solver. + */ + SmtSolver(); + + /*! + * Destructs the solver instance + */ + virtual ~SmtSolver(); + + SmtSolver(SmtSolver const& other) = default; + SmtSolver(SmtSolver&& other) = default; + SmtSolver& operator=(SmtSolver const& other) = default; + SmtSolver& operator=(SmtSolver&& other) = default; + + /*! + * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those + * assertions from the solver's stack that were added after this call. + */ virtual void push() = 0; - //! pops a backtrackingpoint in the solver + + /*! + * Pops a backtracking point from the solver's stack. This deletes all assertions from the solver's stack + * that were added after the last call to push(). + */ virtual void pop() = 0; - //! pops multiple backtrack points - //! @param n number of backtrackingpoint to pop + + /*! + * Pops multiple backtracking points from the solver's stack in the same way as pop() does. + * + * @param n The number of backtracking points to pop. + */ virtual void pop(uint_fast64_t n) = 0; - //! removes all assertions + + /*! + * Removes all assertions from the solver's stack. + */ virtual void reset() = 0; - - - //! assert an expression in the solver - //! @param e the asserted expression, the return type has to be bool - //! @throws IllegalArgumentTypeException if the return type of the expression is not bool - virtual void assertExpression(storm::expressions::Expression const& e) = 0; - //! assert a set of expressions in the solver - //! @param es the asserted expressions - //! @see assert(storm::expressions::Expression &e) - virtual void assertExpression(std::set const& es) { - for (storm::expressions::Expression e : es) { - this->assertExpression(e); - } - } - //! assert a set of expressions in the solver - //! @param es the asserted expressions - //! @see assert(storm::expressions::Expression &e) - /* std::hash unavailable for expressions - virtual void assertExpression(std::unordered_set &es) { - for (storm::expressions::Expression e : es) { - this->assertExpression(e); - } - }*/ - //! assert a set of expressions in the solver - //! @param es the asserted expressions - //! @see assert(storm::expressions::Expression &e) - virtual void assertExpression(std::initializer_list const& es) { - for (storm::expressions::Expression e : es) { - this->assertExpression(e); - } - } - + + /*! + * Adds an assertion to the solver's stack. + * + * @param assertion The assertion to add. + */ + virtual void add(storm::expressions::Expression const& assertion) = 0; + + /*! + * Adds the given set of assertions to the solver's stack. + * + * @param assertions The assertions to add. + */ + void add(std::set const& assertions); + + /*! + * Adds the given list of assertions to the solver's stack. + * + * @param assertions The assertions to add. + */ + void add(std::initializer_list const& assertions); + /*! - * check satisfiability of the conjunction of the currently asserted expressions - * - * @returns CheckResult::SAT if the conjunction of the asserted expressions is satisfiable, - * CheckResult::UNSAT if it is unsatisfiable and CheckResult::UNKNOWN if the solver - * could not determine satisfiability - */ + * Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable. + * + * @return Sat if the conjunction of the asserted expressions is satisfiable, Unsat if it is unsatisfiable + * and Unknown if the solver could not determine satisfiability. + */ virtual CheckResult check() = 0; - //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions - //! @param es the asserted expressions - //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool - //! @see check() + + /*! + * Checks whether the conjunction of assertions that are currently on the solver's stack together with the + * provided assumptions is satisfiable. The assumptions are, however, not added to the solver's stack, but + * are merely considered for this one call. + * + * @param assumptions The assumptions to add to the call. + * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is + * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. + */ virtual CheckResult checkWithAssumptions(std::set const& assumptions) = 0; - //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions - //! @param es the asserted expressions - //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool - //! @see check() - /* std::hash unavailable for expressions - virtual CheckResult checkWithAssumptions(std::unordered_set &assumptions) = 0; - */ - //! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions - //! @param es the asserted expressions - //! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool - //! @see check() + + /*! + * Checks whether the conjunction of assertions that are currently on the solver's stack together with the + * provided assumptions is satisfiable. The assumptions are, however, not added to the solver's stack, but + * are merely considered for this one call. + * + * @param assumptions The assumptions to add to the call. + * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is + * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. + */ virtual CheckResult checkWithAssumptions(std::initializer_list assumptions) = 0; - + /*! - * Gets a model for the assertion stack (and possibly assumtions) for the last call to ::check or ::checkWithAssumptions if that call - * returned CheckResult::SAT. Otherwise an exception is thrown. - * @remark Note that this function may throw an exception if it is not called immediately after a call to::check or ::checkWithAssumptions - * that returned CheckResult::SAT depending on the implementation. - * @throws InvalidStateException if no model is available - * @throws IllegalFunctionCallException if model generation is not configured for this solver - * @throws NotImplementedException if model generation is not implemented with this solver class - */ - virtual storm::expressions::SimpleValuation getModel() { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); - } - + * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that + * satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the + * solver was instantiated with support for model generation. Note that this function may throw an exception + * if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat + * depending on the implementation. + */ + virtual storm::expressions::SimpleValuation getModel(); + /*! - * Performs all AllSat over the important atoms. All valuations of the important atoms such that the currently asserted formulas are satisfiable - * are returned from the function. - * - * @warning If infinitely many valuations exist, such that the currently asserted formulas are satisfiable, this function will never return! - * - * @param important A set of expressions over which to perform all sat. - * - * @returns the set of all valuations of the important atoms, such that the currently asserted formulas are satisfiable - * - * @throws IllegalFunctionCallException if model generation is not configured for this solver - * @throws NotImplementedException if model generation is not implemented with this solver class - */ - virtual std::vector allSat(std::vector const& important) { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); - } - + * Performs AllSat over the (provided) important atoms. That is, this function returns all models of the + * assertions on the solver's stack. + * + * @warning If infinitely many models exist, this function will never return. + * + * @param important The set of important atoms over which to perform all sat. + * + * @returns the set of all valuations of the important atoms, such that the currently asserted formulas are satisfiable + */ + virtual std::vector allSat(std::vector const& important); + /*! - * Performs all AllSat over the important atoms. Once a valuation of the important atoms such that the currently asserted formulas are satisfiable - * is found the callback is called with that valuation. - * - * @param important A set of expressions over which to perform all sat. - * @param callback A function to call for each found valuation. - * - * @returns the number of valuations of the important atoms, such that the currently asserted formulas are satisfiable that where found - * - * @throws IllegalFunctionCallException if model generation is not configured for this solver - * @throws NotImplementedException if model generation is not implemented with this solver class - */ - virtual uint_fast64_t allSat(std::vector const& important, std::function callback) { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); - } - + * Performs AllSat over the (provided) important atoms. That is, this function determines all models of the + * assertions on the solver's stack. While doing so, every time a model is found, the provided callback is + * called and informed about the content of the current model. The callback function can signal to abort the + * enumeration process by returning false. + * + * @param important The set of important atoms over which to perform all sat. + * @param callback A function to call for each found model. + * + * @return The number of models of the important atoms that where found. + */ + virtual uint_fast64_t allSat(std::vector const& important, std::function callback); + + /*! + * Performs AllSat over the (provided) important atoms. That is, this function determines all models of the + * assertions on the solver's stack. While doing so, every time a model is found, the provided callback is + * called and informed about the content of the current model. The callback function can signal to abort the + * enumeration process by returning false. + * + * @param important The set of important atoms over which to perform all sat. + * @param callback A function to call for each found model. + * + * @return The number of models of the important atoms that where found. + */ + virtual uint_fast64_t allSat(std::vector const& important, std::function callback); + /*! - * Performs all AllSat over the important atoms. Once a valuation of the important atoms such that the currently asserted formulas are satisfiable - * is found the callback is called with a reference to the model. The lifetime of that model is controlled by the solver implementation. It will most - * certainly be invalid after the callback returned. - * - * @param important A set of expressions over which to perform all sat. - * @param callback A function to call for each found valuation. - * - * @returns the number of valuations of the important atoms, such that the currently asserted formulas are satisfiable that where found - * - * @throws IllegalFunctionCallException if model generation is not configured for this solver - * @throws NotImplementedException if model generation is not implemented with this solver class - */ - virtual uint_fast64_t allSat(std::function callback, std::vector const& important) { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation."); - } //hack: switching the parameters is the only way to have overloading work with lambdas - + * If the last call to check() returned Unsat, this function can be used to retrieve the unsatisfiable core + * of the assertions on the solver's stack, provided that the solver has been instantiated with support for + * the generation of unsatisfiable cores. + * + * @return A subset of the asserted formulas whose conjunction is unsatisfiable. + */ + virtual std::vector getUnsatCore(); + /*! - * Retrieves the unsat core of the last call to check() - * - * @returns a subset of the asserted formulas s.t. this subset is unsat - * - * @throws InvalidStateException if no unsat core is available, i.e. the asserted formulas are consistent - * @throws IllegalFunctionCallException if unsat core generation is not configured for this solver - * @throws NotImplementedException if unsat core generation is not implemented with this solver class - */ - virtual std::vector getUnsatCore() { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation."); - } - - /*! - * Retrieves a subset of the assumptions from the last call to checkWithAssumptions(), s.t. the result is still unsatisfiable - * - * @returns a subset of the assumptions s.t. this subset of the assumptions results in unsat - * - * @throws InvalidStateException if no unsat assumptions is available, i.e. the asserted formulas are consistent - * @throws IllegalFunctionCallException if unsat assumptions generation is not configured for this solver - * @throws NotImplementedException if unsat assumptions generation is not implemented with this solver class - */ - virtual std::vector getUnsatAssumptions() { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation."); - } - + * If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a subset + * of the assumptions such that the assertion stack and these assumptions are unsatisfiable. This may only + * be called provided that the solver has been instantiated with support for the generation of unsatisfiable + * cores. + * + * @return A subset of the assumptions of the last call to checkWithAssumptions whose conjunction with the + * solver's stack is unsatisfiable. + */ + virtual std::vector getUnsatAssumptions(); + /*! - * Sets the current interpolation group. All terms added to the assertion stack after this call will belong to - * the set group until the next call to this function. - * - * @param group the interpolation group all expressions asserted after this call are assigned - * - * @throws IllegalFunctionCallException if interpolation is not configured for this solver - * @throws NotImplementedException if interpolation is not implemented with this solver class - */ - virtual void setInterpolationGroup(uint_fast64_t group) { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation."); - } - + * Sets the current interpolation group. All terms added to the assertion stack after this call will belong + * to the set group until the next call to this function. Note that, depending on the solver, it might not + * be possible to "re-open" groups, so this should be used with care. Also, this functionality is only + * available if the solver has been instantiated with support for interpolant generation. + * + * @param group The index of the interpolation group with which all assertions added after this call will be + * associated. + */ + virtual void setInterpolationGroup(uint_fast64_t group); + /*! - * Retrieves an interpolant for a pair (A, B) of formulas. The formula A is the conjunction of all - * formulas in the groups listet in the parameter groupsA, the formula B ist the conjunction of all - * other asserted formulas. The solver has to be in an UNSAT state. - * - * @param groupsA the interpolation groups whose conjunctions make up the formula A - * - * @returns the interpolant for (A, B), i.e. an expression I that is implied by A but the conjunction of I and B is inconsistent. - * - * @throws InvalidStateException if no unsat assumptions is available, i.e. the asserted formulas are consistent - * @throws IllegalFunctionCallException if unsat assumptions generation is not configured for this solver - * @throws NotImplementedException if unsat assumptions generation is not implemented with this solver class - */ - virtual storm::expressions::Expression getInterpolant(std::vector groupsA) { - throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation."); - } + * If the last call to check() returned Unsat, the solver has been instantiated with support for interpolant + * generation and at least two non-empty interpolation groups have been added, the function can be used to + * retrieve an interpolant for the pair (A, B) of formulas where A is the conjunction of all the assertions + * in the groups provided as a parameter and B is the set of all other assertions. To obtain meaningful + * results, the conjunction of the formulas within one group should be satisfiable. + * + * @param groupsA The indices of all interpolation groups whose conjunctions form the formula A. + * + * @return The interpolant for the formulas (A, B), i.e. an expression I that is implied by A but the + * conjunction of I and B is inconsistent. + */ + virtual storm::expressions::Expression getInterpolant(std::vector groupsA); }; } } diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index afe6e1508..28ad16c86 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -1,89 +1,104 @@ #include "src/solver/Z3SmtSolver.h" +#include "src/exceptions/NotSupportedException.h" +#include "src/exceptions/InvalidStateException.h" namespace storm { namespace solver { #ifdef STORM_HAVE_Z3 - Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model &m, storm::adapters::Z3ExpressionAdapter &adapter) : m_model(m), m_adapter(adapter) { - + Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model const& model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : model(model), expressionAdapter(expressionAdapter) { + // Intentionally left empty. } #endif bool Z3SmtSolver::Z3ModelReference::getBooleanValue(std::string const& name) const { #ifdef STORM_HAVE_Z3 - z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name)); - z3::expr z3ExprValuation = m_model.eval(z3Expr, true); - return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsBool(); + z3::expr z3Expr = this->expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name)); + z3::expr z3ExprValuation = model.eval(z3Expr, true); + return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsBool(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } int_fast64_t Z3SmtSolver::Z3ModelReference::getIntegerValue(std::string const& name) const { #ifdef STORM_HAVE_Z3 - z3::expr z3Expr = this->m_adapter.translateExpression(storm::expressions::Expression::createIntegerVariable(name)); - z3::expr z3ExprValuation = m_model.eval(z3Expr, true); - return this->m_adapter.translateExpression(z3ExprValuation).evaluateAsInt(); + z3::expr z3Expr = this->expressionAdapter.translateExpression(storm::expressions::Expression::createIntegerVariable(name)); + z3::expr z3ExprValuation = model.eval(z3Expr, true); + return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - Z3SmtSolver::Z3SmtSolver(Options options) + double Z3SmtSolver::Z3ModelReference::getDoubleValue(std::string const& name) const { +#ifdef STORM_HAVE_Z3 + z3::expr z3Expr = this->expressionAdapter.translateExpression(storm::expressions::Expression::createDoubleVariable(name)); + z3::expr z3ExprValuation = model.eval(z3Expr, true); + return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble(); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); +#endif + } + + Z3SmtSolver::Z3SmtSolver() #ifdef STORM_HAVE_Z3 - : m_context() - , m_solver(m_context) - , m_adapter(m_context, std::map()) + : context() + , solver(context) + , expressionAdapter(context, std::map()) , lastCheckAssumptions(false) - , lastResult(CheckResult::UNKNOWN) + , lastResult(CheckResult::Unknown) #endif { - //intentionally left empty + // Intentionally left empty. } - Z3SmtSolver::~Z3SmtSolver() {}; + + Z3SmtSolver::~Z3SmtSolver() { + // Intentionally left empty. + } void Z3SmtSolver::push() { #ifdef STORM_HAVE_Z3 - this->m_solver.push(); + this->solver.push(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } void Z3SmtSolver::pop() { #ifdef STORM_HAVE_Z3 - this->m_solver.pop(); + this->solver.pop(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } void Z3SmtSolver::pop(uint_fast64_t n) { #ifdef STORM_HAVE_Z3 - this->m_solver.pop((unsigned int)n); + this->solver.pop(static_cast(n)); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } void Z3SmtSolver::reset() { #ifdef STORM_HAVE_Z3 - this->m_solver.reset(); + this->solver.reset(); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - void Z3SmtSolver::assertExpression(storm::expressions::Expression const& e) + void Z3SmtSolver::add(storm::expressions::Expression const& assertion) { #ifdef STORM_HAVE_Z3 - this->m_solver.add(m_adapter.translateExpression(e, true)); + this->solver.add(expressionAdapter.translateExpression(assertion, true)); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } @@ -91,20 +106,20 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = false; - switch (this->m_solver.check()) { + switch (this->solver.check()) { case z3::sat: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case z3::unsat: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } @@ -112,26 +127,26 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = true; - z3::expr_vector z3Assumptions(this->m_context); + z3::expr_vector z3Assumptions(this->context); for (storm::expressions::Expression assumption : assumptions) { - z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); + z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption)); } - switch (this->m_solver.check(z3Assumptions)) { + switch (this->solver.check(z3Assumptions)) { case z3::sat: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case z3::unsat: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } @@ -139,58 +154,56 @@ namespace storm { { #ifdef STORM_HAVE_Z3 lastCheckAssumptions = true; - z3::expr_vector z3Assumptions(this->m_context); + z3::expr_vector z3Assumptions(this->context); for (storm::expressions::Expression assumption : assumptions) { - z3Assumptions.push_back(this->m_adapter.translateExpression(assumption)); + z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption)); } - switch (this->m_solver.check(z3Assumptions)) { + switch (this->solver.check(z3Assumptions)) { case z3::sat: - this->lastResult = SmtSolver::CheckResult::SAT; + this->lastResult = SmtSolver::CheckResult::Sat; break; case z3::unsat: - this->lastResult = SmtSolver::CheckResult::UNSAT; + this->lastResult = SmtSolver::CheckResult::Unsat; break; default: - this->lastResult = SmtSolver::CheckResult::UNKNOWN; + this->lastResult = SmtSolver::CheckResult::Unknown; break; } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } storm::expressions::SimpleValuation Z3SmtSolver::getModel() { #ifdef STORM_HAVE_Z3 - - STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); - - return this->z3ModelToStorm(this->m_solver.get_model()); + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); + return this->convertZ3ModelToValuation(this->solver.get_model()); #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } #ifdef STORM_HAVE_Z3 - storm::expressions::SimpleValuation Z3SmtSolver::z3ModelToStorm(z3::model m) { + storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) { storm::expressions::SimpleValuation stormModel; - for (unsigned i = 0; i < m.num_consts(); ++i) { - z3::func_decl var_i = m.get_const_decl(i); - storm::expressions::Expression var_i_interp = this->m_adapter.translateExpression(m.get_const_interp(var_i)); + for (unsigned i = 0; i < model.num_consts(); ++i) { + z3::func_decl variableI = model.get_const_decl(i); + storm::expressions::Expression variableIInterpretation = this->expressionAdapter.translateExpression(model.get_const_interp(variableI)); - switch (var_i_interp.getReturnType()) { + switch (variableIInterpretation.getReturnType()) { case storm::expressions::ExpressionReturnType::Bool: - stormModel.addBooleanIdentifier(var_i.name().str(), var_i_interp.evaluateAsBool()); + stormModel.addBooleanIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsBool()); break; case storm::expressions::ExpressionReturnType::Int: - stormModel.addIntegerIdentifier(var_i.name().str(), var_i_interp.evaluateAsInt()); + stormModel.addIntegerIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsInt()); break; case storm::expressions::ExpressionReturnType::Double: - stormModel.addDoubleIdentifier(var_i.name().str(), var_i_interp.evaluateAsDouble()); + stormModel.addDoubleIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsDouble()); break; default: STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") @@ -206,128 +219,122 @@ namespace storm { std::vector Z3SmtSolver::allSat(std::vector const& important) { #ifdef STORM_HAVE_Z3 - std::vector valuations; - - this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool {valuations.push_back(valuation); return true; }); - + this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; - #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function callback) { #ifdef STORM_HAVE_Z3 - for (storm::expressions::Expression e : important) { - if (!e.isVariable()) { - throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; - } + for (storm::expressions::Expression const& atom : important) { + STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables."); } - uint_fast64_t numModels = 0; + uint_fast64_t numberOfModels = 0; bool proceed = true; + // Save the current assertion stack, to be able to backtrack after the procedure. this->push(); - while (proceed && this->check() == CheckResult::SAT) { - ++numModels; - z3::model m = this->m_solver.get_model(); + // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration. + while (proceed && this->check() == CheckResult::Sat) { + ++numberOfModels; + z3::model model = this->solver.get_model(); - z3::expr modelExpr = this->m_context.bool_val(true); + z3::expr modelExpr = this->context.bool_val(true); storm::expressions::SimpleValuation valuation; - for (storm::expressions::Expression importantAtom : important) { - z3::expr z3ImportantAtom = this->m_adapter.translateExpression(importantAtom); - z3::expr z3ImportantAtomValuation = m.eval(z3ImportantAtom, true); + for (storm::expressions::Expression const& importantAtom : important) { + z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom); + z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true); modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation); if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Bool) { - valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsBool()); + valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsBool()); } else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Int) { - valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsInt()); + valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsInt()); } else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Double) { - valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->m_adapter.translateExpression(z3ImportantAtomValuation).evaluateAsDouble()); + valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsDouble()); } else { - throw storm::exceptions::InvalidTypeException() << "Important atom has invalid type"; + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Important atom has invalid type."); } } + // Check if we are required to proceed, and if so rule out the current model. proceed = callback(valuation); - - this->m_solver.add(!modelExpr); + if (proceed) { + this->solver.add(!modelExpr); + } } + // Restore the old assertion stack and return. this->pop(); - - return numModels; + return numberOfModels; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - uint_fast64_t Z3SmtSolver::allSat(std::function callback, std::vector const& important) + uint_fast64_t Z3SmtSolver::allSat(std::vector const& important, std::function callback) { #ifdef STORM_HAVE_Z3 - for (storm::expressions::Expression e : important) { - if (!e.isVariable()) { - throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions."; - } + for (storm::expressions::Expression const& atom : important) { + STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables."); } - uint_fast64_t numModels = 0; + uint_fast64_t numberOfModels = 0; bool proceed = true; + // Save the current assertion stack, to be able to backtrack after the procedure. this->push(); - while (proceed && this->check() == CheckResult::SAT) { - ++numModels; - z3::model m = this->m_solver.get_model(); + // Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration. + while (proceed && this->check() == CheckResult::Sat) { + ++numberOfModels; + z3::model model = this->solver.get_model(); - z3::expr modelExpr = this->m_context.bool_val(true); + z3::expr modelExpr = this->context.bool_val(true); storm::expressions::SimpleValuation valuation; - for (storm::expressions::Expression importantAtom : important) { - z3::expr z3ImportantAtom = this->m_adapter.translateExpression(importantAtom); - z3::expr z3ImportantAtomValuation = m.eval(z3ImportantAtom, true); + for (storm::expressions::Expression const& importantAtom : important) { + z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom); + z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true); modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation); } + Z3ModelReference modelRef(model, expressionAdapter); - Z3ModelReference modelRef(m, m_adapter); + // Check if we are required to proceed, and if so rule out the current model. proceed = callback(modelRef); - - this->m_solver.add(!modelExpr); + if (proceed) { + this->solver.add(!modelExpr); + } } this->pop(); - - return numModels; + return numberOfModels; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } std::vector Z3SmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_Z3 - if (lastResult != SmtSolver::CheckResult::UNSAT) { - throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat."; - } - if (!lastCheckAssumptions) { - throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last check had no assumptions."; - } - - z3::expr_vector z3UnsatAssumptions = this->m_solver.unsat_core(); + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") + STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); + z3::expr_vector z3UnsatAssumptions = this->solver.unsat_core(); std::vector unsatAssumptions; for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) { - unsatAssumptions.push_back(this->m_adapter.translateExpression(z3UnsatAssumptions[i])); + unsatAssumptions.push_back(this->expressionAdapter.translateExpression(z3UnsatAssumptions[i])); } return unsatAssumptions; #else - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } } diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 1b5009957..b389f7dfc 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -17,18 +17,23 @@ namespace storm { class Z3ModelReference : public SmtSolver::ModelReference { public: #ifdef STORM_HAVE_Z3 - Z3ModelReference(z3::model& m, storm::adapters::Z3ExpressionAdapter &adapter); + Z3ModelReference(z3::model const& m, storm::adapters::Z3ExpressionAdapter& expressionAdapter); #endif virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; + virtual double getDoubleValue(std::string const& name) const override; private: #ifdef STORM_HAVE_Z3 - z3::model &m_model; - storm::adapters::Z3ExpressionAdapter &m_adapter; + // The Z3 model out of which the information can be extracted. + z3::model const& model; + + // The expression adapter that is used to translate the variable names. + storm::adapters::Z3ExpressionAdapter& expressionAdapter; #endif }; + public: - Z3SmtSolver(Options options = Options::ModelGeneration); + Z3SmtSolver(); virtual ~Z3SmtSolver(); virtual void push() override; @@ -39,7 +44,7 @@ namespace storm { virtual void reset() override; - virtual void assertExpression(storm::expressions::Expression const& e) override; + virtual void add(storm::expressions::Expression const& assertion) override; virtual CheckResult check() override; @@ -53,22 +58,33 @@ namespace storm { virtual uint_fast64_t allSat(std::vector const& important, std::function callback) override; - virtual uint_fast64_t allSat(std::function callback, std::vector const& important) override; + virtual uint_fast64_t allSat(std::vector const& important, std::function callback) override; virtual std::vector getUnsatAssumptions() override; - protected: -#ifdef STORM_HAVE_Z3 - virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m); -#endif private: - #ifdef STORM_HAVE_Z3 - z3::context m_context; - z3::solver m_solver; - storm::adapters::Z3ExpressionAdapter m_adapter; - + /*! + * Converts the given Z3 model to an evaluation. + * + * @param model The Z3 model to convert. + * @return The valuation of variables corresponding to the given model. + */ + storm::expressions::SimpleValuation convertZ3ModelToValuation(z3::model const& model); + + // The context used by the solver. + z3::context context; + + // The actual solver object. + z3::solver solver; + + // An expression adapter that is used for translating the expression into Z3's format. + storm::adapters::Z3ExpressionAdapter expressionAdapter; + + // A flag storing whether the last call to a check method provided aussumptions. bool lastCheckAssumptions; + + // The last result that was returned by any of the check methods. CheckResult lastResult; #endif }; diff --git a/src/utility/cli.h b/src/utility/cli.h index 321e60779..323c4473d 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -22,6 +22,9 @@ #ifdef STORM_HAVE_Z3 # include "z3.h" #endif +#ifdef STORM_HAVE_MSAT +# include "mathsat.h" +#endif #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -136,6 +139,11 @@ namespace storm { Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; #endif +#ifdef STORM_HAVE_MSAT + char* msatVersion = msat_get_version(); + std::cout << "Linked with MathSAT v" << msatVersion << "." << std::endl; + msat_free(msatVersion); +#endif // "Compute" the command line argument string with which STORM was invoked. std::stringstream commandStream; diff --git a/storm-config.h.in b/storm-config.h.in index dd19cc6df..8e4827957 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -7,10 +7,10 @@ #ifndef STORM_GENERATED_STORMCONFIG_H_ #define STORM_GENERATED_STORMCONFIG_H_ - // The path of the sources from which StoRM will be/was build #define STORM_CPP_BASE_PATH "@PROJECT_SOURCE_DIR@" + // The path used in the functional and performance tests to load the supplied example files #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" @@ -24,7 +24,7 @@ #@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3 // Whether MathSAT is available and to be used (define/undef) -#@STORM_CPP_MathSAT_DEF@ STORM_HAVE_MSAT +#@STORM_CPP_MSAT_DEF@ STORM_HAVE_MSAT // Whether Intel Threading Building Blocks are available and to be used (define/undef) #@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB diff --git a/storm-version.cpp.in b/storm-version.cpp.in index c35b0c2af..9de4c4481 100644 --- a/storm-version.cpp.in +++ b/storm-version.cpp.in @@ -1,28 +1,35 @@ #include "src/utility/storm-version.h" -namespace storm -{ -namespace utility -{ -// The major version of StoRM -const unsigned StormVersion::versionMajor = @STORM_CPP_VERSION_MAJOR@; -// The minor version of StoRM -const unsigned StormVersion::versionMinor = @STORM_CPP_VERSION_MINOR@; -// The patch version of StoRM -const unsigned StormVersion::versionPatch = @STORM_CPP_VERSION_PATCH@; -// The short hash of the git commit this build is bases on -const std::string StormVersion::gitRevisionHash = "@STORM_CPP_VERSION_HASH@"; -// How many commits passed since the tag was last set -const unsigned StormVersion::commitsAhead = @STORM_CPP_VERSION_COMMITS_AHEAD@; -// 0 iff there no files were modified in the checkout, 1 else -const unsigned StormVersion::dirty = @STORM_CPP_VERSION_DIRTY@; -// The system which has compiled storm -const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@"; -// The system version which has compiled storm -const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@"; -// The build type that was used to build storm -const std::string StormVersion::buildType = "@CMAKE_BUILD_TYPE@"; -// The compiler version that was used to build storm -const std::string StormVersion::cxxCompiler = "@STORM_COMPILED_BY@ @CMAKE_CXX_COMPILER_VERSION@"; +namespace storm { + namespace utility { + // The major version of StoRM + const unsigned StormVersion::versionMajor = @STORM_CPP_VERSION_MAJOR@; + + // The minor version of StoRM + const unsigned StormVersion::versionMinor = @STORM_CPP_VERSION_MINOR@; + + // The patch version of StoRM + const unsigned StormVersion::versionPatch = @STORM_CPP_VERSION_PATCH@; + + // The short hash of the git commit this build is bases on + const std::string StormVersion::gitRevisionHash = "@STORM_CPP_VERSION_HASH@"; + + // How many commits passed since the tag was last set + const unsigned StormVersion::commitsAhead = @STORM_CPP_VERSION_COMMITS_AHEAD@; + + // 0 iff there no files were modified in the checkout, 1 else + const unsigned StormVersion::dirty = @STORM_CPP_VERSION_DIRTY@; + + // The system which has compiled storm + const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@"; + + // The system version which has compiled storm + const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@"; + + // The build type that was used to build storm + const std::string StormVersion::buildType = "@CMAKE_BUILD_TYPE@"; + + // The compiler version that was used to build storm + const std::string StormVersion::cxxCompiler = "@STORM_COMPILED_BY@ @CMAKE_CXX_COMPILER_VERSION@"; + } } -} \ No newline at end of file