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

Some fixes to make new SMT framework compile with clang under Mac OS (includes fixes to some initializiation ordering warnings). Bugfix for PRISM parser to correctly handle formulas. 

Former-commit-id: d513476066
tempestpy_adaptions
dehnert 11 years ago
parent
3887cb57aa
commit
40c698af90
6 changed files with 17 additions and 15 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. 6
      src/adapters/Z3ExpressionAdapter.h
  2. 4
      src/parser/PrismParser.cpp
  3. 2
      src/parser/PrismParser.h
  4. 4
      src/solver/Z3SmtSolver.cpp
  5. 4
      src/storage/SparseMatrix.cpp
  6. 12
      test/functional/adapter/Z3ExpressionAdapterTest.cpp

6
src/adapters/Z3ExpressionAdapter.h
View File

@ -39,9 +39,9 @@ namespace storm {
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap)
: context(context)
, stack()
, variableToExpressionMap(variableToExpressionMap)
, additionalVariableCounter(0)
, additionalAssertions() {
, additionalAssertions()
, additionalVariableCounter(0)
, variableToExpressionMap(variableToExpressionMap) {
// Intentionally left empty.
}

4
src/parser/PrismParser.cpp
View File

@ -265,10 +265,12 @@ namespace storm {
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
}
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
this->identifiers_.add(formulaName, expression);
} else {
this->identifiers_.at(formulaName) = expression;
}
return storm::prism::Formula(formulaName, expression, this->getFilename());
}

2
src/parser/PrismParser.h
View File

@ -225,7 +225,7 @@ namespace storm {
storm::prism::Constant createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Constant createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression) const;
storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression);
storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const;
storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;

4
src/solver/Z3SmtSolver.cpp
View File

@ -7,9 +7,9 @@ namespace storm {
#ifdef STORM_HAVE_Z3
: m_context()
, m_solver(m_context)
, m_adapter(m_context, {})
, lastResult(CheckResult::UNKNOWN)
, m_adapter(m_context, std::map<std::string, z3::expr>())
, lastCheckAssumptions(false)
, lastResult(CheckResult::UNKNOWN)
#endif
{
//intentionally left empty

4
src/storage/SparseMatrix.cpp
View File

@ -778,8 +778,8 @@ namespace storm {
const_iterator ite;
std::vector<uint_fast64_t>::const_iterator rowIterator = this->rowIndications.begin() + startRow;
std::vector<uint_fast64_t>::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow;
std::vector<T>::iterator resultIterator = result.begin() + startRow;
std::vector<T>::iterator resultIteratorEnd = result.begin() + endRow;
typename std::vector<T>::iterator resultIterator = result.begin() + startRow;
typename std::vector<T>::iterator resultIteratorEnd = result.begin() + endRow;
for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) {
*resultIterator = storm::utility::constantZero<T>();

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

@ -11,7 +11,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) {
z3::solver s(ctx);
z3::expr conjecture = ctx.bool_val(false);
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue();
z3::expr z3True = ctx.bool_val(true);
@ -54,7 +54,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Integer) {
z3::solver s(ctx);
z3::expr conjecture = ctx.bool_val(false);
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y"));
z3::expr z3Add = (ctx.int_const("x") + ctx.int_const("y") < -ctx.int_const("y"));
@ -81,7 +81,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Real) {
z3::solver s(ctx);
z3::expr conjecture = ctx.bool_val(false);
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y"));
z3::expr z3Add = (ctx.real_const("x") + ctx.real_const("y") < -ctx.real_const("y"));
@ -108,7 +108,7 @@ TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) {
z3::solver s(ctx);
z3::expr conjecture = ctx.bool_val(false);
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
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);
@ -124,7 +124,7 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) {
z3::solver s(ctx);
z3::expr conjecture = ctx.bool_val(false);
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991));
z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i");
@ -167,7 +167,7 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
unsigned args = 2;
storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
z3::expr z3True = ctx.bool_val(true);
storm::expressions::Expression exprTrue;

Write Preview
Loading…
Cancel
Save