Started refactoring SMT solvers. Now displaying MathSAT version in CLI.

Former-commit-id: 1736a0bb6b

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)
 
 #############################################################
 ##

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_ */

src/solver/MathSatSmtSolver.h → 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

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<storm::expressions::Expression> const& assertions) {
+            for (storm::expressions::Expression assertion : assertions) {
+                this->add(assertion);
+            }
+        }
+        
+        void SmtSolver::add(std::initializer_list<storm::expressions::Expression> 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<storm::expressions::SimpleValuation> SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
+        }
+        
+        uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
+        }
+        
+        uint_fast64_t SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
+        }
+        
+        std::vector<storm::expressions::Expression> SmtSolver::getUnsatCore() {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of unsatisfiable cores.");
+        }
+        
+        std::vector<storm::expressions::Expression> 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<uint_fast64_t> groupsA) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support generation of interpolants.");
+        }
+
+    } // namespace solver
+} // namespace storm

src/solver/SmtSolver.h

@@ -3,11 +3,6 @@
 
 #include <cstdint>
 
-#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"
 
@@ -25,218 +20,204 @@ namespace storm {
          */
 		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 double getDoubleValue(std::string const& name) const = 0;
 			};
+            
 		public:
 			/*!
-			* Constructs a new smt solver with the given options.
+             * 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
+             * @throws storm::exceptions::IllegalArgumentValueException if an option is unsupported for the solver.
+             */
+			SmtSolver();
+            
+            /*!
+             * Destructs the solver instance
              */
-			SmtSolver(Options options = Options::ModelGeneration) {};
-			virtual ~SmtSolver() {};
+			virtual ~SmtSolver();
             
-			SmtSolver(const SmtSolver&) = delete;
-			SmtSolver(const SmtSolver&&) {};
+			SmtSolver(SmtSolver const& other) = default;
+			SmtSolver(SmtSolver&& other) = default;
+			SmtSolver& operator=(SmtSolver const& other) = default;
+			SmtSolver& operator=(SmtSolver&& other) = default;
             
-			//! pushes a backtrackingpoint in the solver
+			/*!
+             * 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;
             
+            /*!
+             * Adds an assertion to the solver's stack.
+             *
+             * @param assertion The assertion to add.
+             */
+			virtual void add(storm::expressions::Expression const& assertion) = 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<storm::expressions::Expression> 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<storm::expressions::Expression> &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<storm::expressions::Expression> const& es) {
-				for (storm::expressions::Expression e : es) {
-					this->assertExpression(e);
-				}
-			}
+            /*!
+             * Adds the given set of assertions to the solver's stack.
+             *
+             * @param assertions The assertions to add.
+             */
+			void add(std::set<storm::expressions::Expression> const& assertions);
             
             /*!
-			* check satisfiability of the conjunction of the currently asserted expressions
+             * Adds the given list of assertions to the solver's stack.
              *
-			* @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
+             * @param assertions The assertions to add.
+             */
+			void add(std::initializer_list<storm::expressions::Expression> const& assertions);
+            
+			/*!
+             * 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<storm::expressions::Expression> 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<storm::expressions::Expression> &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<storm::expressions::Expression> 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
+             * 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() {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
-			}
+			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.
+             * 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 valuations exist, such that the currently asserted formulas are satisfiable, this function will never return!
+             * @warning If infinitely many models exist, this function will never return.
              *
-			* @param important A set of expressions over which to perform all sat.
+             * @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
-			*
-			* @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<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
-			}
+			virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> 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.
+             * 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.
              *
-			* @returns the number of valuations of the important atoms, such that the currently asserted formulas are satisfiable that where found
+             * @param important The set of important atoms over which to perform all sat.
+             * @param callback A function to call for each found model.
              *
-			* @throws IllegalFunctionCallException if model generation is not configured for this solver
-			* @throws NotImplementedException if model generation is not implemented with this solver class
+             * @return The number of models of the important atoms that where found.
              */
-			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
-			}
+			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> 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.
+             * 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.
              *
-			* @returns the number of valuations of the important atoms, such that the currently asserted formulas are satisfiable that where found
+             * @param important The set of important atoms over which to perform all sat.
+             * @param callback A function to call for each found model.
              *
-			* @throws IllegalFunctionCallException if model generation is not configured for this solver
-			* @throws NotImplementedException if model generation is not implemented with this solver class
+             * @return The number of models of the important atoms that where found.
              */
-			virtual uint_fast64_t allSat(std::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> 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
+			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback);
             
 			/*!
-			* Retrieves the unsat core of the last call to check()
-			*
-			* @returns a subset of the asserted formulas s.t. this subset is unsat
+             * 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.
              *
-			* @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
+             * @return A subset of the asserted formulas whose conjunction is unsatisfiable.
              */
-			virtual std::vector<storm::expressions::Expression> getUnsatCore() {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation.");
-			}
+			virtual std::vector<storm::expressions::Expression> getUnsatCore();
             
 			/*!
-			* 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
+             * 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.
              *
-			* @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
+             * @return A subset of the assumptions of the last call to checkWithAssumptions whose conjunction with the
+             * solver's stack is unsatisfiable.
              */
-			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support unsat core generation.");
-			}
+			virtual std::vector<storm::expressions::Expression> 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
+             * 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.
              *
-			* @throws IllegalFunctionCallException if interpolation is not configured for this solver
-			* @throws NotImplementedException if interpolation is not implemented with this solver class
+             * @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) {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation.");
-			}
+			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
+             * 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.
              *
-			* @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.
+             * @param groupsA The indices of all interpolation groups whose conjunctions form the formula A.
              *
-			* @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
+             * @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<uint_fast64_t> groupsA) {
-				throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support interpolation.");
-			}
+			virtual storm::expressions::Expression getInterpolant(std::vector<uint_fast64_t> groupsA);
 		};
 	}
 }

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
-			: m_context()
-			, m_solver(m_context)
-			, m_adapter(m_context, std::map<std::string, z3::expr>())
+			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
+			: context()
+			, solver(context)
+			, expressionAdapter(context, std::map<std::string, z3::expr>())
 			, lastCheckAssumptions(false)
-            , lastResult(CheckResult::UNKNOWN)
+            , lastResult(CheckResult::Unknown)
 #endif
 		{
-			//intentionally left empty
+			// Intentionally left empty.
+		}
+        
+		Z3SmtSolver::~Z3SmtSolver() {
+            // Intentionally left empty.
         }
-		Z3SmtSolver::~Z3SmtSolver() {};
 
 		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<unsigned int>(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<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
 		{
 #ifdef STORM_HAVE_Z3
-			
 			std::vector<storm::expressions::SimpleValuation> valuations;
-
 			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<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> 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<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important)
+		uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> 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<storm::expressions::Expression> 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<storm::expressions::Expression> 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
 		}
 	}

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<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
 
-			virtual uint_fast64_t allSat(std::function<bool(ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) override;
+			virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(ModelReference&)> callback) override;
 
 			virtual std::vector<storm::expressions::Expression> 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
 		};

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;

storm-config.h.in

@@ -8,9 +8,9 @@
 #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

storm-version.cpp.in

@@ -1,27 +1,34 @@
 #include "src/utility/storm-version.h"
 
-namespace storm
-{
-namespace utility
-{
+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@";
     }