From 29687ca5d536048dfda0b2b3d64069abc253ad64 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 8 May 2017 16:52:39 +0200
Subject: [PATCH] added some statistics output

---
 .../SparseCbAchievabilityQuery.cpp             | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp
index 5c25aa096..24b67bc03 100644
--- a/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/constraintBased/SparseCbAchievabilityQuery.cpp
@@ -8,8 +8,10 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/utility/solver.h"
+#include "storm/utility/Stopwatch.h"
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/MultiObjectiveSettings.h"
 #include "storm/storage/expressions/Expressions.h"
 
@@ -39,15 +41,23 @@ namespace storm {
             
             template <class SparseModelType>
             bool SparseCbAchievabilityQuery<SparseModelType>::checkAchievability() {
-                
+                STORM_LOG_INFO("Building constraint system to check achievability.");
                 //this->preprocessedModel.writeDotToStream(std::cout);
-                
+                storm::utility::Stopwatch swInitialization(true);
                 initializeConstraintSystem();
-                solver->push();
+                STORM_LOG_INFO("Constraint system consists of " << expectedChoiceVariables.size() << " + " << bottomStateVariables.size() << " variables");
                 addObjectiveConstraints();
-                solver->push();
+                swInitialization.stop();
                 
+                storm::utility::Stopwatch swCheck(true);
+                STORM_LOG_INFO("Invoking SMT Solver.");
                 storm::solver::SmtSolver::CheckResult result = solver->check();
+                swCheck.stop();
+                
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    STORM_PRINT_AND_LOG("Building the constraintsystem took " << swInitialization << " seconds and checking the SMT formula took " << swCheck << " seconds." << std::endl);
+                }
+                
                 switch(result) {
                     case storm::solver::SmtSolver::CheckResult::Sat:
                         // std::cout << std::endl << "Satisfying assignment: " << std::endl << solver->getModelAsValuation().toString(true) << std::endl;