iMC changes outside of storm-pars

src/storm/adapters/Z3ExpressionAdapter.cpp

@@ -166,6 +166,11 @@ storm::expressions::Expression Z3ExpressionAdapter::translateExpression(z3::expr
                         return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
                     }
                 }
+            case Z3_OP_AGNUM:
+                STORM_LOG_WARN("Interpreting algebraic numbers as rational numbers. This is not an exact computation.");
+                // Get the value of an algebraic number, converted to a rational, with precision 1/10^16.
+                return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(
+                    std::string(Z3_get_numeral_string(expr.ctx(), Z3_get_algebraic_number_lower(expr.ctx(), expr, 16)))));
             case Z3_OP_UNINTERPRETED:
                 // Currently, we only support uninterpreted constant functions.
                 STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException,

src/storm/api/bisimulation.h

@@ -19,11 +19,18 @@ namespace api {
 template<typename ModelType>
 std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
                                                                               std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
-                                                                              storm::storage::BisimulationType type) {
+                                                                              storm::storage::BisimulationType type, bool graphPreserving = true) {
     typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options options;
-    if (!formulas.empty()) {
+    if (!formulas.empty() && graphPreserving) {
         options = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
     }
+    // If we cannot use formula-based decomposition because of
+    // non-graph-preserving regions but there are reward models, we need to
+    // preserve those
+    if (!graphPreserving &&
+        std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
+        options.setKeepRewards(true);
+    }
     options.setType(type);
 
     storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
@@ -34,11 +41,18 @@ std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(st
 template<typename ModelType>
 std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
                                                                                  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
-                                                                                 storm::storage::BisimulationType type) {
+                                                                                 storm::storage::BisimulationType type, bool graphPreserving = true) {
     typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options options;
-    if (!formulas.empty()) {
+    if (!formulas.empty() && graphPreserving) {
         options = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options(*model, formulas);
     }
+    // If we cannot use formula-based decomposition because of
+    // non-graph-preserving regions but there are reward models, we need to
+    // preserve those
+    if (!graphPreserving &&
+        std::any_of(formulas.begin(), formulas.end(), [](auto const& formula) { return formula->getReferencedRewardModels().size() > 0; })) {
+        options.setKeepRewards(true);
+    }
     options.setType(type);
 
     storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
@@ -49,7 +63,7 @@ std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization
 template<typename ValueType>
 std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMinimization(
     std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
-    storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong) {
+    storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true) {
     STORM_LOG_THROW(
         model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp),
         storm::exceptions::NotSupportedException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
@@ -59,13 +73,13 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMini
 
     if (model->isOfType(storm::models::ModelType::Dtmc)) {
         return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(
-            model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type);
+            model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type, graphPreserving);
     } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
         return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
-            model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type);
+            model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type, graphPreserving);
     } else {
         return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(
-            model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type);
+            model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type, graphPreserving);
     }
 }
 

src/storm/logic/Bound.cpp

@@ -29,9 +29,15 @@ ValueType Bound::evaluateThresholdAs() const {
 }
 
 template bool Bound::isSatisfied(double const& compareValue) const;
-template bool Bound::isSatisfied(storm::RationalNumber const& compareValue) const;
+#if defined(STORM_HAVE_CLN)
+template bool Bound::isSatisfied(storm::ClnRationalNumber const& compareValue) const;
+template storm::ClnRationalNumber Bound::evaluateThresholdAs() const;
+#endif
+#if defined(STORM_HAVE_GMP)
+template bool Bound::isSatisfied(storm::GmpRationalNumber const& compareValue) const;
+template storm::GmpRationalNumber Bound::evaluateThresholdAs() const;
+#endif
 template double Bound::evaluateThresholdAs() const;
-template storm::RationalNumber Bound::evaluateThresholdAs() const;
 template storm::RationalFunction Bound::evaluateThresholdAs() const;
 
 }  // namespace storm::logic