83#ifdef STORM_USE_CLN_EA
84 STORM_PRINT(
"Using CLN numbers for exact arithmetic.\n");
86 STORM_PRINT(
"Using GMP numbers for exact arithmetic.\n");
88#ifdef STORM_USE_CLN_RF
89 STORM_PRINT(
"Using CLN numbers for rational functions.\n");
91 STORM_PRINT(
"Using GMP numbers for rational functions.\n");
95 STORM_PRINT(
"Linked with CArL v" << STORM_CARL_VERSION <<
".\n");
97 STORM_PRINT(
"Linked with GLPK v" << GLP_MAJOR_VERSION <<
"." << GLP_MINOR_VERSION <<
".\n");
106#ifdef STORM_HAVE_GUROBI
107 STORM_PRINT(
"Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR <<
"." << GRB_VERSION_MINOR <<
"." << GRB_VERSION_TECHNICAL <<
".\n");
111#ifdef STORM_HAVE_MATHSAT
112 char* msatVersion = msat_get_version();
113 STORM_PRINT(
"Linked with " << msatVersion <<
".\n");
114 msat_free(msatVersion);
118#ifdef STORM_HAVE_SOPLEX
119 STORM_PRINT(
"Linked with Soplex v" << SOPLEX_VERSION <<
".\n");
123#ifdef STORM_HAVE_SPOT
124 STORM_PRINT(
"Linked with Spot v" << spot::version() <<
".\n");
128#ifdef STORM_HAVE_XERCES
129 STORM_PRINT(
"Linked with Xerces-C v" << gXercesMajVersion <<
"." << gXercesMinVersion <<
"." << gXercesRevision <<
".\n");
134 unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
135 Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
136#ifdef STORM_HAVE_Z3_OPTIMIZE
137 STORM_PRINT(
"Linked with Z3 Theorem Prover v" << z3Major <<
"." << z3Minor <<
" Build " << z3BuildNumber <<
" Rev " << z3RevisionNumber
138 <<
" (with optimization features).\n");
140 STORM_PRINT(
"Linked with Z3 Theorem Prover v" << z3Major <<
"." << z3Minor <<
" Build " << z3BuildNumber <<
" Rev " << z3RevisionNumber <<
".\n");
143 STORM_PRINT(
"Not linked with Z3 Theorem Prover\n");
150 getrusage(RUSAGE_SELF, &ru);
152 std::cout <<
"\nPerformance statistics:\n";
155 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024;
159 uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024;
161 std::cout <<
" * peak memory usage: " << maximumResidentSizeInMegabytes <<
"MB\n";
162 char oldFillChar = std::cout.fill(
'0');
163 std::cout <<
" * CPU time: " << ru.ru_utime.tv_sec <<
"." << std::setw(3) << ru.ru_utime.tv_usec / 1000 <<
"s\n";
164 if (wallclockMilliseconds != 0) {
165 std::cout <<
" * wallclock time: " << (wallclockMilliseconds / 1000) <<
"." << std::setw(3) << (wallclockMilliseconds % 1000) <<
"s\n";
167 std::cout.fill(oldFillChar);