added timeout to smt solver interface

Former-commit-id: 0003c2c9cc

src/solver/SmtSolver.cpp

@@ -83,6 +83,14 @@ namespace storm {
         storm::expressions::ExpressionManager& SmtSolver::getManager() {
             return manager;
         }
+        
+        bool SmtSolver::setTimeout(uint_fast64_t milliseconds) {
+            return false;
+        }
+        
+        bool SmtSolver::unsetTimeout() {
+            return false;
+        }
 
     } // namespace solver
 } // namespace storm

src/solver/SmtSolver.h

@@ -276,6 +276,22 @@ namespace storm {
              */
             storm::expressions::ExpressionManager& getManager();
             
+            /*!
+             * If supported by the solver, this will limit all subsequent satisfiability queries to the given number of
+             * milliseconds.
+             *
+             * @param milliseconds The amount of milliseconds before timing out.
+             * @return True iff the solver supports setting a timeout.
+             */
+            virtual bool setTimeout(uint_fast64_t milliseconds);
+            
+            /*!
+             * If supported by the solver, this unsets a previous timeout.
+             *
+             * @return True iff the solver supports timeouts.
+             */
+            virtual bool unsetTimeout();
+            
         private:
             // The manager responsible for the expressions that interact with this solver.
             storm::expressions::ExpressionManager& manager;

src/solver/Z3SmtSolver.cpp

@@ -338,5 +338,20 @@ namespace storm {
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
 #endif
 		}
+        
+        bool Z3SmtSolver::setTimeout(uint_fast64_t milliseconds) {
+            z3::params paramObject(*context);
+            paramObject.set(":timeout", static_cast<unsigned>(milliseconds));
+            solver->set(paramObject);
+            return true;
+        }
+        
+        bool Z3SmtSolver::unsetTimeout() {
+            z3::params paramObject(*context);
+            paramObject.set(":timeout", 0u);
+            solver->set(paramObject);
+            return true;
+        }
+
 	}
 }

src/solver/Z3SmtSolver.h

@@ -67,6 +67,10 @@ namespace storm {
 
 			virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
 
+            virtual bool setTimeout(uint_fast64_t milliseconds) override;
+            
+            virtual bool unsetTimeout() override;
+            
 		private:
 #ifdef STORM_HAVE_Z3
             /*!