84#ifdef STORM_USE_CLN_EA
85 STORM_PRINT(
"Using CLN numbers for exact arithmetic.\n");
87 STORM_PRINT(
"Using GMP numbers for exact arithmetic.\n");
89#ifdef STORM_USE_CLN_RF
90 STORM_PRINT(
"Using CLN numbers for rational functions.\n");
92 STORM_PRINT(
"Using GMP numbers for rational functions.\n");
96 STORM_PRINT(
"Linked with CArL v" << STORM_CARL_VERSION <<
".\n");
98 STORM_PRINT(
"Linked with GLPK v" << GLP_MAJOR_VERSION <<
"." << GLP_MINOR_VERSION <<
".\n");
107#ifdef STORM_HAVE_GUROBI
108 STORM_PRINT(
"Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR <<
"." << GRB_VERSION_MINOR <<
"." << GRB_VERSION_TECHNICAL <<
".\n");
112#ifdef STORM_HAVE_MATHSAT
113 char* msatVersion = msat_get_version();
114 STORM_PRINT(
"Linked with " << msatVersion <<
".\n");
115 msat_free(msatVersion);
119#ifdef STORM_HAVE_SOPLEX
120 STORM_PRINT(
"Linked with Soplex v" << SOPLEX_VERSION <<
".\n");
124#ifdef STORM_HAVE_SPOT
125 STORM_PRINT(
"Linked with Spot v" << spot::version() <<
".\n");
129#ifdef STORM_HAVE_XERCES
130 STORM_PRINT(
"Linked with Xerces-C v" << gXercesMajVersion <<
"." << gXercesMinVersion <<
"." << gXercesRevision <<
".\n");
135 unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
136 Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
137#ifdef STORM_HAVE_Z3_OPTIMIZE
138 STORM_PRINT(
"Linked with Z3 Theorem Prover v" << z3Major <<
"." << z3Minor <<
" Build " << z3BuildNumber <<
" Rev " << z3RevisionNumber
139 <<
" (with optimization features).\n");
141 STORM_PRINT(
"Linked with Z3 Theorem Prover v" << z3Major <<
"." << z3Minor <<
" Build " << z3BuildNumber <<
" Rev " << z3RevisionNumber <<
".\n");
144 STORM_PRINT(
"Not linked with Z3 Theorem Prover\n");
151 getrusage(RUSAGE_SELF, &ru);
153 std::cout <<
"\nPerformance statistics:\n";
156 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024;
160 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024;
162 std::cout <<
" * peak memory usage: " << maximumResidentSizeInMegabytes <<
"MB\n";
163 char oldFillChar = std::cout.fill(
'0');
164 std::cout <<
" * CPU time: " << ru.ru_utime.tv_sec <<
"." << std::setw(3) << ru.ru_utime.tv_usec / 1000 <<
"s\n";
165 if (wallclockMilliseconds != 0) {
166 std::cout <<
" * wallclock time: " << (wallclockMilliseconds / 1000) <<
"." << std::setw(3) << (wallclockMilliseconds % 1000) <<
"s\n";
168 std::cout.fill(oldFillChar);