From 6cfa6ac9c7cc57e0b0694eacf1b46030ac359576 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 16 Oct 2015 10:55:16 +0200
Subject: [PATCH] added timeout to smt solver interface

Former-commit-id: 0003c2c9cc18953d5e10ff98b98580b8294d010f
---
 src/solver/SmtSolver.cpp   |  8 ++++++++
 src/solver/SmtSolver.h     | 16 ++++++++++++++++
 src/solver/Z3SmtSolver.cpp | 15 +++++++++++++++
 src/solver/Z3SmtSolver.h   |  4 ++++
 4 files changed, 43 insertions(+)

diff --git a/src/solver/SmtSolver.cpp b/src/solver/SmtSolver.cpp
index d1f2536d6..cf1c4f577 100644
--- a/src/solver/SmtSolver.cpp
+++ b/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
\ No newline at end of file
diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h
index 475c3ee95..27943b79f 100644
--- a/src/solver/SmtSolver.h
+++ b/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;
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index fed950c2a..d2b050a1d 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/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;
+        }
+
 	}
 }
\ No newline at end of file
diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h
index 00dc8d434..a69914ac4 100644
--- a/src/solver/Z3SmtSolver.h
+++ b/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
             /*!