From aecd0e3cb805b3a2d7ff42e7a2964c9930af2df3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Jul 2014 13:14:49 +0200 Subject: [PATCH] Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available. Former-commit-id: 307036e25cb1d56cf6d354fbf830736e486f9247 --- src/adapters/Z3ExpressionAdapter.h | 3 ++ src/solver/Z3SmtSolver.cpp | 6 +-- src/solver/Z3SmtSolver.h | 4 ++ .../adapter/Z3ExpressionAdapterTest.cpp | 33 ++-------------- test/functional/solver/GlpkLpSolverTest.cpp | 34 +--------------- test/functional/solver/GurobiLpSolverTest.cpp | 34 +--------------- test/functional/solver/Z3SmtSolverTest.cpp | 39 ++----------------- 7 files changed, 19 insertions(+), 134 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 81e8a222e..7f850f9d3 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -10,8 +10,11 @@ #include +// Include the headers of Z3 only if it is available. +#ifdef STORM_HAVE_Z3 #include "z3++.h" #include "z3.h" +#endif #include "storm-config.h" #include "src/storage/expressions/Expressions.h" diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 42ad53c2e..45720c293 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -148,8 +148,8 @@ namespace storm { #endif } - storm::expressions::SimpleValuation Z3SmtSolver::z3ModelToStorm(z3::model m) { #ifdef STORM_HAVE_Z3 + storm::expressions::SimpleValuation Z3SmtSolver::z3ModelToStorm(z3::model m) { storm::expressions::SimpleValuation stormModel; for (unsigned i = 0; i < m.num_consts(); ++i) { @@ -174,10 +174,8 @@ namespace storm { } return stormModel; -#else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support."); -#endif } +#endif std::vector Z3SmtSolver::allSat(std::vector const& important) { diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index b3b20a46a..0f2059443 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -5,8 +5,10 @@ #include "src/solver/SmtSolver.h" #include "src/adapters/Z3ExpressionAdapter.h" +#ifdef STORM_HAVE_Z3 #include "z3++.h" #include "z3.h" +#endif namespace storm { namespace solver { @@ -40,7 +42,9 @@ namespace storm { virtual std::vector getUnsatAssumptions() override; protected: +#ifdef STORM_HAVE_Z3 virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m); +#endif private: #ifdef STORM_HAVE_Z3 diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index b92a0ec03..b92794f87 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -1,12 +1,12 @@ #include "gtest/gtest.h" #include "storm-config.h" +#ifdef STORM_HAVE_Z3 #include "z3++.h" #include "src/adapters/Z3ExpressionAdapter.h" #include "src/settings/Settings.h" TEST(Z3ExpressionAdapter, StormToZ3Basic) { -#ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); @@ -42,14 +42,9 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) { s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3ExpressionAdapter, StormToZ3Integer) { -#ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); @@ -69,14 +64,9 @@ TEST(Z3ExpressionAdapter, StormToZ3Integer) { s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3ExpressionAdapter, StormToZ3Real) { -#ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); @@ -96,14 +86,9 @@ TEST(Z3ExpressionAdapter, StormToZ3Real) { s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); s.reset(); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) { -#ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); @@ -112,14 +97,9 @@ TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) { storm::expressions::Expression exprFail1 = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createDoubleVariable("y")); ASSERT_THROW(conjecture = adapter.translateExpression(exprFail1, true), storm::exceptions::InvalidTypeException); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { -#ifdef STORM_HAVE_Z3 z3::context ctx; z3::solver s(ctx); z3::expr conjecture = ctx.bool_val(false); @@ -156,13 +136,9 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { s.add(conjecture); ASSERT_TRUE(s.check() == z3::unsat); //it is NOT logical equivalent s.reset(); -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3ExpressionAdapter, Z3ToStormBasic) { -#ifdef STORM_HAVE_Z3 z3::context ctx; unsigned args = 2; @@ -197,8 +173,5 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) { ASSERT_EQ("x", exprNor.getOperand(0).getOperand(0).getIdentifier()); ASSERT_TRUE(exprNor.getOperand(0).getOperand(1).isVariable()); ASSERT_EQ("y", exprNor.getOperand(0).getOperand(1).getIdentifier()); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif -} \ No newline at end of file +} +#endif \ No newline at end of file diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index a6410611d..32048bab9 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/test/functional/solver/GlpkLpSolverTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" +#ifdef STORM_HAVE_GLPK #include "src/solver/GlpkLpSolver.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidAccessException.h" #include "src/settings/Settings.h" TEST(GlpkLpSolver, LPOptimizeMax) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -35,13 +35,9 @@ TEST(GlpkLpSolver, LPOptimizeMax) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, LPOptimizeMin) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -69,13 +65,9 @@ TEST(GlpkLpSolver, LPOptimizeMin) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, MILPOptimizeMax) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); @@ -103,13 +95,9 @@ TEST(GlpkLpSolver, MILPOptimizeMax) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, MILPOptimizeMin) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); @@ -137,13 +125,9 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, LPInfeasible) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -168,13 +152,9 @@ TEST(GlpkLpSolver, LPInfeasible) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, MILPInfeasible) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -199,13 +179,9 @@ TEST(GlpkLpSolver, MILPInfeasible) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, LPUnbounded) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -228,13 +204,9 @@ TEST(GlpkLpSolver, LPUnbounded) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } TEST(GlpkLpSolver, MILPUnbounded) { -#ifdef STORM_HAVE_GLPK storm::solver::GlpkLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -257,7 +229,5 @@ TEST(GlpkLpSolver, MILPUnbounded) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without glpk support."; -#endif } +#endif \ No newline at end of file diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index ee0ebfa03..a862fac42 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" +#ifdef STORM_HAVE_GUROBI #include "src/solver/GurobiLpSolver.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidAccessException.h" #include "src/settings/Settings.h" TEST(GurobiLpSolver, LPOptimizeMax) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -35,13 +35,9 @@ TEST(GurobiLpSolver, LPOptimizeMax) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, LPOptimizeMin) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); @@ -69,13 +65,9 @@ TEST(GurobiLpSolver, LPOptimizeMin) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, MILPOptimizeMax) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); @@ -103,13 +95,9 @@ TEST(GurobiLpSolver, MILPOptimizeMax) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, MILPOptimizeMin) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Minimize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedIntegerVariable("y", 0, 2)); @@ -137,13 +125,9 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { double objectiveValue = 0; ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue()); ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, LPInfeasible) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -168,13 +152,9 @@ TEST(GurobiLpSolver, LPInfeasible) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, MILPInfeasible) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -199,13 +179,9 @@ TEST(GurobiLpSolver, MILPInfeasible) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, LPUnbounded) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBoundedContinuousVariable("x", 0, 1, -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -228,13 +204,9 @@ TEST(GurobiLpSolver, LPUnbounded) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } TEST(GurobiLpSolver, MILPUnbounded) { -#ifdef STORM_HAVE_GUROBI storm::solver::GurobiLpSolver solver(storm::solver::LpSolver::ModelSense::Maximize); ASSERT_NO_THROW(solver.addBinaryVariable("x", -1)); ASSERT_NO_THROW(solver.addLowerBoundedContinuousVariable("y", 0, 2)); @@ -256,7 +228,5 @@ TEST(GurobiLpSolver, MILPUnbounded) { ASSERT_THROW(zValue = solver.getContinuousValue("z"), storm::exceptions::InvalidAccessException); double objectiveValue = 0; ASSERT_THROW(objectiveValue = solver.getObjectiveValue(), storm::exceptions::InvalidAccessException); -#else - ASSERT_TRUE(false) << "StoRM built without Gurobi support."; -#endif } +#endif \ No newline at end of file diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp index 79d0cd0d0..c3222404c 100644 --- a/test/functional/solver/Z3SmtSolverTest.cpp +++ b/test/functional/solver/Z3SmtSolverTest.cpp @@ -1,11 +1,11 @@ #include "gtest/gtest.h" #include "storm-config.h" +#ifdef STORM_HAVE_Z3 #include "src/solver/Z3SmtSolver.h" #include "src/settings/Settings.h" TEST(Z3SmtSolver, CheckSat) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -29,14 +29,9 @@ TEST(Z3SmtSolver, CheckSat) { ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); ASSERT_NO_THROW(s.reset()); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, CheckUnsat) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -60,15 +55,10 @@ TEST(Z3SmtSolver, CheckUnsat) { ASSERT_NO_THROW(s.assertExpression(exprFormula)); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, Backtracking) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -120,14 +110,9 @@ TEST(Z3SmtSolver, Backtracking) { ASSERT_NO_THROW(s.pop()); ASSERT_NO_THROW(result = s.check()); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, Assumptions) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -154,14 +139,9 @@ TEST(Z3SmtSolver, Assumptions) { ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 })); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, GenerateModel) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -182,15 +162,10 @@ TEST(Z3SmtSolver, GenerateModel) { int_fast64_t a_eval; (a_eval = model.getIntegerValue("a")); ASSERT_EQ(1, a_eval); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, AllSat) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -222,14 +197,9 @@ TEST(Z3SmtSolver, AllSat) { ASSERT_TRUE((valuations[i].getBooleanValue("x") != valuations[j].getBooleanValue("x")) || (valuations[i].getBooleanValue("y") != valuations[j].getBooleanValue("y"))); } } - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif } TEST(Z3SmtSolver, UnsatAssumptions) { -#ifdef STORM_HAVE_Z3 storm::solver::Z3SmtSolver s; storm::solver::Z3SmtSolver::CheckResult result; @@ -252,8 +222,5 @@ TEST(Z3SmtSolver, UnsatAssumptions) { ASSERT_EQ(unsatCore.size(), 1); ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); - -#else - ASSERT_TRUE(false) << "StoRM built without Z3 support."; -#endif -} \ No newline at end of file +} +#endif \ No newline at end of file