Started on making MathSatSmtSolver work properly.

Former-commit-id: c370658b26

src/adapters/MathSatExpressionAdapter.h

@@ -47,6 +47,37 @@ namespace storm {
 			* @return An equivalent term for MathSAT.
 			*/
 			msat_term translateExpression(storm::expressions::Expression const& expression, bool createMathSatVariables = false) {
+                if (createMathSatVariables) {
+					std::map<std::string, storm::expressions::ExpressionReturnType> variables;
+                    
+					try	{
+						variables = expression.getVariablesAndTypes();
+					}
+					catch (storm::exceptions::InvalidTypeException* e) {
+						STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with ambigious type while trying to autocreate solver variables: " << e);
+					}
+                    
+					for (auto variableAndType : variables) {
+						if (this->variableToDeclMap.find(variableAndType.first) == this->variableToDeclMap.end()) {
+							switch (variableAndType.second)
+							{
+								case storm::expressions::ExpressionReturnType::Bool:
+									this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_bool_type(env))));
+									break;
+								case storm::expressions::ExpressionReturnType::Int:
+									this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_integer_type(env))));
+									break;
+								case storm::expressions::ExpressionReturnType::Double:
+									this->variableToDeclMap.insert(std::make_pair(variableAndType.first, msat_declare_function(env, variableAndType.first.c_str(), msat_get_rational_type(env))));
+									break;
+								default:
+									STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Encountered variable with unknown type while trying to autocreate solver variables: " << variableAndType.first);
+									break;
+							}
+						}
+					}
+				}
+                
 				//LOG4CPLUS_TRACE(logger, "Translating expression:\n" << expression->toString());
 				expression.getBaseExpression().accept(this);
 				msat_term result = stack.top();

src/exceptions/UnexpectedException.h

@@ -0,0 +1,15 @@
+#ifndef STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_
+#define STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+        
+        STORM_NEW_EXCEPTION(UnexpectedException)
+        
+    } // namespace exceptions
+} // namespace storm
+
+#endif /* STORM_EXCEPTIONS_UNEXPECTEDEXCEPTION_H_ */

src/solver/MathSatSmtSolver.cpp

@@ -2,6 +2,8 @@
 
 #include <vector>
 
+#include "src/exceptions/UnexpectedException.h"
+
 namespace storm {
 	namespace solver {
 
@@ -17,6 +19,9 @@ namespace storm {
 			if (static_cast<int>(options)& static_cast<int>(Options::InterpolantComputation)) {
 				msat_set_option(m_cfg, "interpolation", "true");
 			}
+            
+            msat_set_option(m_cfg, "model_generation", "true");
+            
 			m_env = msat_create_env(m_cfg);
 
 			m_adapter = new storm::adapters::MathSatExpressionAdapter(m_env, variableToDeclMap);
@@ -169,6 +174,8 @@ namespace storm {
 
 			msat_model_iterator model = msat_create_model_iterator(m_env);
 
+            STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(model), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator.");
+            
 			while (msat_model_iterator_has_next(model)) {
 				msat_term t, v;
 				msat_model_iterator_next(model, &t, &v);

test/functional/solver/MathSatSmtSolverTest.cpp

@@ -0,0 +1,58 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_MSAT
+#include "src/solver/MathSatSmtSolver.h"
+
+TEST(MathSatSmtSolver, CheckSat) {
+	storm::solver::MathSatSmtSolver s;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+    
+	storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
+    
+	ASSERT_NO_THROW(s.assertExpression(exprDeMorgan));
+	ASSERT_NO_THROW(result = s.check());
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+	ASSERT_NO_THROW(s.reset());
+    
+	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
+	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
+	storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
+	storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
+    && a < storm::expressions::Expression::createIntegerLiteral(5)
+    && b > storm::expressions::Expression::createIntegerLiteral(7)
+    && c == (a * b)
+    && b + a > c;
+    
+	ASSERT_NO_THROW(s.assertExpression(exprFormula));
+	ASSERT_NO_THROW(result = s.check());
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+	ASSERT_NO_THROW(s.reset());
+}
+
+TEST(MathSatSmtSolver, CheckUnsat) {
+	storm::solver::MathSatSmtSolver s;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+    
+	storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
+    
+	ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan));
+	ASSERT_NO_THROW(result = s.check());
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+	ASSERT_NO_THROW(s.reset());
+    
+	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
+	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
+	storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
+	storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2)
+    && a < storm::expressions::Expression::createIntegerLiteral(5)
+    && b > storm::expressions::Expression::createIntegerLiteral(7)
+    && c == (a + b + storm::expressions::Expression::createIntegerLiteral(1))
+    && b + a > c;
+    
+	ASSERT_NO_THROW(s.assertExpression(exprFormula));
+	ASSERT_NO_THROW(result = s.check());
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+}
+
+#endif

test/functional/solver/Z3SmtSolverTest.cpp

@@ -7,7 +7,7 @@
 
 TEST(Z3SmtSolver, CheckSat) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
 
 	storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
 
@@ -33,7 +33,7 @@ TEST(Z3SmtSolver, CheckSat) {
 
 TEST(Z3SmtSolver, CheckUnsat) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
 
 	storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
 
@@ -60,7 +60,7 @@ TEST(Z3SmtSolver, CheckUnsat) {
 
 TEST(Z3SmtSolver, Backtracking) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
 
 	storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue();
 	storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse();
@@ -114,7 +114,7 @@ TEST(Z3SmtSolver, Backtracking) {
 
 TEST(Z3SmtSolver, Assumptions) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result = storm::solver::Z3SmtSolver::CheckResult::UNKNOWN;
+	storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
 
 	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
 	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -143,7 +143,7 @@ TEST(Z3SmtSolver, Assumptions) {
 
 TEST(Z3SmtSolver, GenerateModel) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result;
+	storm::solver::SmtSolver::CheckResult result;
 
 	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
 	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -167,7 +167,7 @@ TEST(Z3SmtSolver, GenerateModel) {
 
 TEST(Z3SmtSolver, AllSat) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result;
+	storm::solver::SmtSolver::CheckResult result;
 
 	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
 	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -201,7 +201,7 @@ TEST(Z3SmtSolver, AllSat) {
 
 TEST(Z3SmtSolver, UnsatAssumptions) {
 	storm::solver::Z3SmtSolver s;
-	storm::solver::Z3SmtSolver::CheckResult result;
+	storm::solver::SmtSolver::CheckResult result;
 
 	storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
 	storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");