From 7ff3dcecfb7cfab8fb424459a0a5766f5d0b0c97 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 18 Dec 2014 11:19:31 +0100
Subject: [PATCH] Added test for interpolation to MathSat tests.

Former-commit-id: ac94857726b0956c8c2b747f5ef54d96804c2f91
---
 src/solver/MathSatSmtSolver.cpp               |  8 +++--
 src/solver/MathSatSmtSolver.h                 |  1 -
 .../solver/MathSatSmtSolverTest.cpp           | 36 +++++++++++++++++++
 test/functional/solver/Z3SmtSolverTest.cpp    |  1 +
 4 files changed, 43 insertions(+), 3 deletions(-)

diff --git a/src/solver/MathSatSmtSolver.cpp b/src/solver/MathSatSmtSolver.cpp
index 2e14ba701..278ed2b3b 100644
--- a/src/solver/MathSatSmtSolver.cpp
+++ b/src/solver/MathSatSmtSolver.cpp
@@ -14,7 +14,7 @@ namespace storm {
 #endif
 		{
 #ifdef STORM_HAVE_MSAT
-			m_cfg = msat_create_config();
+			msat_config m_cfg = msat_create_config();
 			
 			if (static_cast<int>(options)& static_cast<int>(Options::InterpolantComputation)) {
 				msat_set_option(m_cfg, "interpolation", "true");
@@ -23,13 +23,15 @@ namespace storm {
             msat_set_option(m_cfg, "model_generation", "true");
             
 			m_env = msat_create_env(m_cfg);
+            STORM_LOG_THROW(!MSAT_ERROR_ENV(m_env), storm::exceptions::UnexpectedException, "Unable to create Mathsat environment.");
 
+            msat_destroy_config(m_cfg);
+            
 			m_adapter = new storm::adapters::MathSatExpressionAdapter(m_env, variableToDeclMap);
 #endif
 		}
 		MathSatSmtSolver::~MathSatSmtSolver() {
 			msat_destroy_env(m_env);
-			msat_destroy_config(m_cfg);
 		};
 
 		void MathSatSmtSolver::push()
@@ -356,6 +358,8 @@ namespace storm {
 			}
 			msat_term interpolant = msat_get_interpolant(m_env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size());
 
+            STORM_LOG_THROW(!MSAT_ERROR_TERM(interpolant), storm::exceptions::UnexpectedException, "Unable to retrieve an interpolant.");
+            
 			return this->m_adapter->translateTerm(interpolant);
 #else
 			STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
diff --git a/src/solver/MathSatSmtSolver.h b/src/solver/MathSatSmtSolver.h
index f2f73c460..009556196 100644
--- a/src/solver/MathSatSmtSolver.h
+++ b/src/solver/MathSatSmtSolver.h
@@ -72,7 +72,6 @@ namespace storm {
 		private:
 
 #ifdef STORM_HAVE_MSAT
-			msat_config m_cfg;
 			msat_env m_env;
 			storm::adapters::MathSatExpressionAdapter *m_adapter;
 
diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp
index 3bcbc11c8..e495c4be8 100644
--- a/test/functional/solver/MathSatSmtSolverTest.cpp
+++ b/test/functional/solver/MathSatSmtSolverTest.cpp
@@ -220,4 +220,40 @@ TEST(MathSatSmtSolver, UnsatAssumptions) {
     ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
 }
 
+TEST(MathSatSmtSolver, InterpolationTest) {
+    storm::solver::MathSatSmtSolver s(storm::solver::SmtSolver::Options::InterpolantComputation);
+    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");
+    storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
+    storm::expressions::Expression exprFormula = a > b;
+    storm::expressions::Expression exprFormula2 = b > c;
+    storm::expressions::Expression exprFormula3 = c > a;
+    
+    s.setInterpolationGroup(0);
+    s.assertExpression(exprFormula);
+    s.setInterpolationGroup(1);
+    s.assertExpression(exprFormula2);
+    s.setInterpolationGroup(2);
+    s.assertExpression(exprFormula3);
+
+    ASSERT_NO_THROW(result = s.check());
+    ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+    
+    storm::expressions::Expression interpol;
+    ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1}));
+    
+    storm::solver::MathSatSmtSolver s2;
+
+    ASSERT_NO_THROW(s2.assertExpression(!(exprFormula && exprFormula2).implies(interpol)));
+    ASSERT_NO_THROW(result = s2.check());
+    ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+
+    ASSERT_NO_THROW(s2.reset());
+    ASSERT_NO_THROW(s2.assertExpression(interpol && exprFormula3));
+    ASSERT_NO_THROW(result = s2.check());
+    ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+}
+
 #endif
\ No newline at end of file
diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp
index e605460e1..30d023f0d 100644
--- a/test/functional/solver/Z3SmtSolverTest.cpp
+++ b/test/functional/solver/Z3SmtSolverTest.cpp
@@ -223,4 +223,5 @@ TEST(Z3SmtSolver, UnsatAssumptions) {
 	ASSERT_TRUE(unsatCore[0].isVariable());
 	ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
 }
+
 #endif
\ No newline at end of file