Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3

Added first simple tests for Z3SmtSolver and Z3ExpressionAdapter


Former-commit-id: 77ade5ffa6

src/adapters/Z3ExpressionAdapter.h

@@ -13,6 +13,7 @@
 #include "z3++.h"
 #include "z3.h"
 
+#include "storm-config.h"
 #include "src/storage/expressions/Expressions.h"
 #include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/ExpressionEvaluationException.h"
@@ -21,7 +22,8 @@
 
 namespace storm {
     namespace adapters {
-        
+
+#ifdef STORM_HAVE_Z3
         class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor {
         public:
             /*!
@@ -392,7 +394,7 @@ namespace storm {
 
             std::map<std::string, z3::expr> variableToExpressionMap;
         };
-        
+#endif
     } // namespace adapters
 } // namespace storm
 

src/solver/Z3SmtSolver.cpp

@@ -4,40 +4,64 @@
 namespace storm {
 	namespace solver {
 		Z3SmtSolver::Z3SmtSolver(Options options)
+#ifdef STORM_HAVE_Z3
 			: m_context()
 			, m_solver(m_context)
-			, m_adapter(m_context, {}) {
+			, m_adapter(m_context, {})
+#endif
+		{
 			//intentionally left empty
 		}
 		Z3SmtSolver::~Z3SmtSolver() {};
 
 		void Z3SmtSolver::push()
 		{
+#ifdef STORM_HAVE_Z3
 			this->m_solver.push();
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		void Z3SmtSolver::pop()
 		{
+#ifdef STORM_HAVE_Z3
 			this->m_solver.pop();
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "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);
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		void Z3SmtSolver::reset()
 		{
+#ifdef STORM_HAVE_Z3
 			this->m_solver.reset();
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		void Z3SmtSolver::assertExpression(storm::expressions::Expression &e)
 		{
+#ifdef STORM_HAVE_Z3
 			this->m_solver.add(m_adapter.translateExpression(e, true));
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		SmtSolver::CheckResult Z3SmtSolver::check()
 		{
+#ifdef STORM_HAVE_Z3
 			switch (this->m_solver.check())
 			{
 				case z3::sat:
@@ -47,10 +71,15 @@ namespace storm {
 				default:
 					break;
 			}
+			return SmtSolver::CheckResult::UNKNOWN;
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions)
 		{
+#ifdef STORM_HAVE_Z3
 			z3::expr_vector z3Assumptions(this->m_context);
 
 			for (storm::expressions::Expression assumption : assumptions) {
@@ -66,10 +95,15 @@ namespace storm {
 			default:
 				break;
 			}
+			return SmtSolver::CheckResult::UNKNOWN;
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> &assumptions)
 		{
+#ifdef STORM_HAVE_Z3
 			z3::expr_vector z3Assumptions(this->m_context);
 
 			for (storm::expressions::Expression assumption : assumptions) {
@@ -85,21 +119,37 @@ namespace storm {
 			default:
 				break;
 			}
+			return SmtSolver::CheckResult::UNKNOWN;
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		storm::expressions::SimpleValuation Z3SmtSolver::getModel()
 		{
-			throw std::logic_error("The method or operation is not implemented.");
+#ifdef STORM_HAVE_Z3
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		std::set<storm::expressions::SimpleValuation> Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers)
 		{
-			throw std::logic_error("The method or operation is not implemented.");
+#ifdef STORM_HAVE_Z3
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 		uint_fast64_t Z3SmtSolver::solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback)
 		{
-			throw std::logic_error("The method or operation is not implemented.");
+#ifdef STORM_HAVE_Z3
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
+#else
+			LOG_THROW(true, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
+#endif
 		}
 
 	}

src/solver/Z3SmtSolver.h

@@ -1,6 +1,7 @@
 #ifndef STORM_SOLVER_Z3SMTSOLVER
 #define STORM_SOLVER_Z3SMTSOLVER
 
+#include "storm-config.h"
 #include "src/solver/SmtSolver.h"
 #include "src/adapters/Z3ExpressionAdapter.h"
 
@@ -37,9 +38,12 @@ namespace storm {
 			virtual uint_fast64_t solveAndDiversify(std::set<storm::expressions::SimpleValuation> diversifyers, std::function<bool(storm::expressions::Valuation&) > callback);
 
 		private:
+
+#ifdef STORM_HAVE_Z3
 			z3::context m_context;
 			z3::solver m_solver;
 			storm::adapters::Z3ExpressionAdapter m_adapter;
+#endif
 		};
 	}
 }

test/functional/adapter/Z3ExpressionAdapterTest.cpp

@@ -0,0 +1,49 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "z3++.h"
+#include "src/adapters/Z3ExpressionAdapter.h"
+#include "src/settings/Settings.h"
+
+TEST(Z3ExpressionAdapter, StormToZ3) {
+#ifdef STORM_HAVE_Z3
+	z3::context ctx;
+	z3::solver s(ctx);
+	z3::expr conjecture = ctx.bool_val(false);
+
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+
+	storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue();
+	z3::expr z3True = ctx.bool_val(true);
+	ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprTrue), z3True)));
+	s.add(conjecture);
+	ASSERT_TRUE(s.check() == z3::unsat);
+	s.reset();
+
+	storm::expressions::Expression exprFalse = storm::expressions::Expression::createFalse();
+	z3::expr z3False = ctx.bool_val(false);
+	ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFalse), z3False)));
+	s.add(conjecture);
+	ASSERT_TRUE(s.check() == z3::unsat);
+	s.reset();
+
+	storm::expressions::Expression exprConjunction = (storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y"));
+	z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y"));
+	ASSERT_THROW( adapter.translateExpression(exprConjunction, false), std::out_of_range ); //variables not yet created in adapter
+	ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprConjunction, true), z3Conjunction)));
+	s.add(conjecture);
+	ASSERT_TRUE(s.check() == z3::unsat);
+	s.reset();
+
+	storm::expressions::Expression exprNor = !(storm::expressions::Expression::createBooleanVariable("x") || storm::expressions::Expression::createBooleanVariable("y"));
+	z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y"));
+	ASSERT_NO_THROW(adapter.translateExpression(exprNor, false)); //variables already created in adapter
+	ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprNor, true), z3Nor)));
+	s.add(conjecture);
+	ASSERT_TRUE(s.check() == z3::unsat);
+	s.reset();
+#else
+    ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}
+

test/functional/solver/Z3SmtSolverTest.cpp

@@ -0,0 +1,21 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/solver/Z3SmtSolver.h"
+#include "src/settings/Settings.h"
+
+TEST(Z3SmtSolver, CheckSatisfiability) {
+#ifdef STORM_HAVE_Z3
+	storm::solver::Z3SmtSolver s;
+
+	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));
+	storm::solver::Z3SmtSolver::CheckResult result;
+	ASSERT_NO_THROW(result = s.check());
+	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+
+#else
+    ASSERT_TRUE(false) << "StoRM built without Z3 support.";
+#endif
+}