Z3 runs fine again.

Former-commit-id: a725a33f01

src/adapters/Z3ExpressionAdapter.h

@@ -65,6 +65,7 @@ namespace storm {
                 if (variableExpressionPair == variableToExpressionMapping.end()) {
                     return createVariable(variable);
                 }
+
                 return variableExpressionPair->second;
             }
             

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<Type, uint_fast64_t>::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<Type, uint_fast64_t>::iterator typeCountPair = auxiliaryVariableTypeToCountMapping.find(variableType);
-                uint_fast64_t& oldCount = auxiliaryVariableTypeToCountMapping[variableType];
+                std::unordered_map<Type, uint_fast64_t>::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;
@@ -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 {

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<std::string, uint_fast64_t> nameToIndexMapping;
             
@@ -411,10 +423,10 @@ namespace storm {
             mutable std::map<std::size_t, Type> 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;
         };
     }
 }

src/storage/expressions/SimpleValuation.cpp

@@ -30,7 +30,7 @@ namespace storm {
             if (other.integerValues != nullptr) {
                 integerValues = std::unique_ptr<std::vector<int_fast64_t>>(new std::vector<int_fast64_t>(*other.integerValues));
             }
-            if (other.booleanValues != nullptr) {
+            if (other.rationalValues != nullptr) {
                 rationalValues = std::unique_ptr<std::vector<double>>(new std::vector<double>(*other.rationalValues));
             }
         }

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 {

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);