DetScheds Objective helper: Detect when exact arithmetic is used.

src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp

@@ -170,6 +170,11 @@ namespace storm {
                 // Change the optimization direction in the formula.
                 auto newFormula = storm::logic::CloneVisitor().clone(formula);
                 newFormula->asOperatorFormula().setOptimalityType(lowerValueBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize);
+                
+                if (std::is_same<typename ModelType::ValueType, storm::RationalNumber>::value) {
+                    // don't have to worry about precision in exact mode.
+                    return evaluateOperatorFormula(env, model, *newFormula);
+                } else {
                     // Create an environment where sound results are enforced
                     storm::Environment soundEnv(env);
                     soundEnv.solver().setForceSoundness(true);
@@ -185,13 +190,14 @@ namespace storm {
                     }
                     return result;
                 }
+            }
             
             template <typename ModelType>
             typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getUpperValueBoundAtState(Environment const& env, uint64_t state) const{
                 //return objective.upperResultBound.get();
-                // TODO: try this.
                 if (!upperResultBounds) {
                     upperResultBounds = computeValueBounds(env, false, model, *objective.formula);
+                    storm::utility::vector::clip(upperResultBounds.get(), objective.lowerResultBound, objective.upperResultBound);
                     STORM_LOG_THROW(!storm::utility::vector::hasInfinityEntry(upperResultBounds.get()), storm::exceptions::NotSupportedException, "The upper bound for objective " << *objective.originalFormula << " is infinity at some state. This is not supported.");
                 }
                 return upperResultBounds.get()[state];
@@ -201,9 +207,9 @@ namespace storm {
             template <typename ModelType>
             typename ModelType::ValueType const& DeterministicSchedsObjectiveHelper<ModelType>::getLowerValueBoundAtState(Environment const& env, uint64_t state) const{
                 // return objective.lowerResultBound.get();
-                //TODO: try this.
                 if (!lowerResultBounds) {
                     lowerResultBounds = computeValueBounds(env, true, model, *objective.formula);
+                    storm::utility::vector::clip(lowerResultBounds.get(), objective.lowerResultBound, objective.upperResultBound);
                     STORM_LOG_THROW(!storm::utility::vector::hasInfinityEntry(lowerResultBounds.get()), storm::exceptions::NotSupportedException, "The lower bound for objective " << *objective.originalFormula << " is infinity at some state. This is not supported.");
                 }
                 return lowerResultBounds.get()[state];