From 2eeaa06d76c6a340003247a8f14df0c90baee084 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 7 Jan 2015 12:46:38 +0100 Subject: [PATCH] Z3 runs fine again. Former-commit-id: a725a33f01b9f5f55fc3bcc6790f719426e8846f --- src/adapters/Z3ExpressionAdapter.h | 1 + src/storage/expressions/ExpressionManager.cpp | 49 +++++++++---------- src/storage/expressions/ExpressionManager.h | 16 +++++- src/storage/expressions/SimpleValuation.cpp | 2 +- src/storage/expressions/Type.h | 8 +-- .../adapter/Z3ExpressionAdapterTest.cpp | 1 + 6 files changed, 45 insertions(+), 32 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 0279df1ec..556548e88 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -65,6 +65,7 @@ namespace storm { if (variableExpressionPair == variableToExpressionMapping.end()) { return createVariable(variable); } + return variableExpressionPair->second; } diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index 00d28875b..fbe608a5c 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -118,7 +118,8 @@ namespace storm { } Variable ExpressionManager::declareBooleanVariable(std::string const& name) { - return this->declareVariable(name, this->getBooleanType()); + Variable var = this->declareVariable(name, this->getBooleanType()); + return var; } Variable ExpressionManager::declareIntegerVariable(std::string const& name) { @@ -135,36 +136,34 @@ namespace storm { } Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType) { - STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); - auto nameIndexPair = nameToIndexMapping.find(name); - if (nameIndexPair != nameToIndexMapping.end()) { - return Variable(this->getSharedPointer(), nameIndexPair->second); - } else { - std::unordered_map::iterator typeCountPair = variableTypeToCountMapping.find(variableType); - uint_fast64_t& oldCount = variableTypeToCountMapping[variableType]; - - // Compute the index of the new variable. - uint_fast64_t newIndex = oldCount++ | variableType.getMask(); - - // Properly insert the variable into the data structure. - nameToIndexMapping[name] = newIndex; - indexToNameMapping[newIndex] = name; - indexToTypeMapping[newIndex] = variableType; - return Variable(this->getSharedPointer(), newIndex); - } + return declareOrGetVariable(name, variableType, false, true); } Variable ExpressionManager::declareOrGetAuxiliaryVariable(std::string const& name, storm::expressions::Type const& variableType) { - STORM_LOG_THROW(isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); + return declareOrGetVariable(name, variableType, true, true); + } + + Variable ExpressionManager::declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary, bool checkName) { + STORM_LOG_THROW(!checkName || isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); auto nameIndexPair = nameToIndexMapping.find(name); if (nameIndexPair != nameToIndexMapping.end()) { return Variable(this->getSharedPointer(), nameIndexPair->second); } else { - std::unordered_map::iterator typeCountPair = auxiliaryVariableTypeToCountMapping.find(variableType); - uint_fast64_t& oldCount = auxiliaryVariableTypeToCountMapping[variableType]; + std::unordered_map::iterator typeCountPair; + if (auxiliary) { + typeCountPair = auxiliaryVariableTypeToCountMapping.find(variableType); + if (typeCountPair == auxiliaryVariableTypeToCountMapping.end()) { + typeCountPair = auxiliaryVariableTypeToCountMapping.insert(typeCountPair, std::make_pair(variableType, 0)); + } + } else { + typeCountPair = variableTypeToCountMapping.find(variableType); + if (typeCountPair == variableTypeToCountMapping.end()) { + typeCountPair = variableTypeToCountMapping.insert(typeCountPair, std::make_pair(variableType, 0)); + } + } // Compute the index of the new variable. - uint_fast64_t newIndex = oldCount++ | variableType.getMask() | auxiliaryMask; + uint_fast64_t newIndex = typeCountPair->second++ | variableType.getMask() | (auxiliary ? auxiliaryMask : 0); // Properly insert the variable into the data structure. nameToIndexMapping[name] = newIndex; @@ -173,7 +172,7 @@ namespace storm { return Variable(this->getSharedPointer(), newIndex); } } - + Variable ExpressionManager::getVariable(std::string const& name) const { auto nameIndexPair = nameToIndexMapping.find(name); STORM_LOG_THROW(nameIndexPair != nameToIndexMapping.end(), storm::exceptions::InvalidArgumentException, "Unknown variable '" << name << "'."); @@ -190,12 +189,12 @@ namespace storm { Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType) { std::string newName = "__x" + std::to_string(freshVariableCounter++); - return declareVariable(newName, variableType); + return declareOrGetVariable(newName, variableType, false, false); } Variable ExpressionManager::declareFreshAuxiliaryVariable(storm::expressions::Type const& variableType) { std::string newName = "__x" + std::to_string(freshVariableCounter++); - return declareAuxiliaryVariable(newName, variableType); + return declareOrGetVariable(newName, variableType, true, false); } uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const { diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 3000b44cd..5106beb5a 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -380,6 +380,18 @@ namespace storm { */ bool variableExists(std::string const& name) const; + /*! + * Declares a variable with the given name if it does not yet exist. + * + * @param name The name of the variable to declare. + * @param variableType The type of the variable to declare. + * @param auxiliary A flag indicating whether the variable is an auxiliary one. + * @param checkName If set to true, the variable's name is checked that prevents internal variables from + * being declared from the outside. + * @return The variable. + */ + Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary, bool checkName); + // A mapping from all variable names (auxiliary + normal) to their indices. std::unordered_map nameToIndexMapping; @@ -411,10 +423,10 @@ namespace storm { mutable std::map boundedIntegerTypes; // A mask that can be used to query whether a variable is an auxiliary variable. - static const uint64_t auxiliaryMask = (1 << 60); + static const uint64_t auxiliaryMask = (1ull << 60); // A mask that can be used to project a variable index to its offset (with the group of equally typed variables). - static const uint64_t offsetMask = (1 << 60) - 1; + static const uint64_t offsetMask = (1ull << 60) - 1; }; } } diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 34ff6aae6..b49a717c9 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -30,7 +30,7 @@ namespace storm { if (other.integerValues != nullptr) { integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); } - if (other.booleanValues != nullptr) { + if (other.rationalValues != nullptr) { rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); } } diff --git a/src/storage/expressions/Type.h b/src/storage/expressions/Type.h index 3e3fa87f9..849f915f6 100644 --- a/src/storage/expressions/Type.h +++ b/src/storage/expressions/Type.h @@ -51,7 +51,7 @@ namespace storm { virtual bool isBooleanType() const override; private: - static const uint64_t mask = (1 << 61); + static const uint64_t mask = (1ull << 61); }; class IntegerType : public BaseType { @@ -61,7 +61,7 @@ namespace storm { virtual bool isIntegerType() const override; private: - static const uint64_t mask = (1 << 62); + static const uint64_t mask = (1ull << 62); }; class BoundedIntegerType : public BaseType { @@ -89,7 +89,7 @@ namespace storm { virtual bool isBoundedIntegerType() const override; private: - static const uint64_t mask = (1 << 61) | (1 << 62); + static const uint64_t mask = (1ull << 61) | (1ull << 62); // The bit width of the type. std::size_t width; @@ -102,7 +102,7 @@ namespace storm { virtual bool isRationalType() const override; private: - static const uint64_t mask = (1 << 63); + static const uint64_t mask = (1ull << 63); }; class ErrorType : public BaseType { diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp index e2beb816b..763ffa3ef 100644 --- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp +++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp @@ -116,6 +116,7 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) { storm::expressions::Expression exprFloor = storm::expressions::floor(d) == i && d > manager->rational(4.1) && d < manager->rational(4.991); z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i"); + conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor)); ASSERT_NO_THROW(conjecture = !z3::expr(ctx, Z3_mk_iff(ctx, adapter.translateExpression(exprFloor), z3Floor))); s.add(conjecture);