sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

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: 307036e25c
main
dehnert 11 years ago
parent
5bb76eb12e
commit
aecd0e3cb8
7 changed files with 19 additions and 134 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/adapters/Z3ExpressionAdapter.h
  2. 6
      src/solver/Z3SmtSolver.cpp
  3. 4
      src/solver/Z3SmtSolver.h
  4. 33
      test/functional/adapter/Z3ExpressionAdapterTest.cpp
  5. 34
      test/functional/solver/GlpkLpSolverTest.cpp
  6. 34
      test/functional/solver/GurobiLpSolverTest.cpp
  7. 39
      test/functional/solver/Z3SmtSolverTest.cpp

3
src/adapters/Z3ExpressionAdapter.h
View File

@ -10,8 +10,11 @@
#include <stack>
// 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"

6
src/solver/Z3SmtSolver.cpp
View File

@ -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<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
{

4
src/solver/Z3SmtSolver.h
View File

@ -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<storm::expressions::Expression> getUnsatAssumptions() override;
protected:
#ifdef STORM_HAVE_Z3
virtual storm::expressions::SimpleValuation z3ModelToStorm(z3::model m);
#endif
private:
#ifdef STORM_HAVE_Z3

33
test/functional/adapter/Z3ExpressionAdapterTest.cpp
View File

@ -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
}
}
#endif

34
test/functional/solver/GlpkLpSolverTest.cpp
View File

@ -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

34
test/functional/solver/GurobiLpSolverTest.cpp
View File

@ -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

39
test/functional/solver/Z3SmtSolverTest.cpp
View File

@ -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
}
}
#endif
Write Preview
Loading…
Cancel
Save