add smt stats printing
MODIFY
smt/solver.cpp
smt/solver.cpp
#include "smt/ctx.h"
#include "util/compiler.h"
#include "util/config.h"
+#include <iomanip>
#include <z3.h>
using namespace smt;
@@ -164,6 +165,25 @@ void Solver::check(initializer_list<E> queries) {
}
}
+void solver_print_stats(ostream &os) {
+ float total = num_queries / 100.0;
+ float trivial_pc = num_queries == 0 ? 0 :
+ (num_trivial * 100.0) / (num_trivial + num_queries);
+ float unknown_pc = num_queries == 0 ? 0 : num_unknown / total;
+ float sat_pc = num_queries == 0 ? 0 : num_sats / total;
+ float unsat_pc = num_queries == 0 ? 0 : num_unsats / total;
+
+ os << fixed << setprecision(1);
+ os << "\n------------------- SMT STATS -------------------\n"
+ "Num queries: " << num_queries << "\n"
+ "Num invalid: " << num_invalid << "\n"
+ "Num skips: " << num_skips << "\n"
+ "Num trivial " << num_trivial << " (" << trivial_pc << "%)\n"
+ "Num unknown " << num_unknown << " (" << unknown_pc << "%)\n"
+ "Num SAT: " << num_sats << " (" << sat_pc << "%)\n"
+ "Num UNSAT: " << num_unsats << " (" << unsat_pc << "%)\n";
+}
+
EnableSMTQueriesTMP::EnableSMTQueriesTMP() : old(config::skip_smt) {
config::skip_smt = false;

MODIFY
smt/solver.h
smt/solver.h
#include <cassert>
#include <cstdint>
#include <functional>
+#include <ostream>
#include <utility>
typedef struct _Z3_model* Z3_model;
@@ -109,6 +110,9 @@ public:
};
+void solver_print_stats(std::ostream &os);
+
+
struct EnableSMTQueriesTMP {
bool old;
EnableSMTQueriesTMP();

MODIFY
tools/alive.cpp
tools/alive.cpp
#include "ir/function.h"
#include "smt/smt.h"
+#include "smt/solver.h"
#include "tools/alive_parser.h"
#include "util/config.h"
#include "util/file.h"
@@ -112,9 +113,8 @@ int main(int argc, char **argv) {
}
}
- if (show_smt_stats) {
- // TODO
- }
+ if (show_smt_stats)
+ smt::solver_print_stats(cout);
return num_errors;
}

add smt stats printing