mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 23:33:41 +00:00
Code Activity

display statistics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-20 10:29:27 -07:00
parent d78313e001
commit 2522c8b53d
1 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/test/polysat.cpp
View file

@ -861,12 +861,30 @@ void tst_polysat() {
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include <signal.h>
polysat::scoped_solver* g_solver = nullptr;
static void display_statistics() {
if (g_solver) {
statistics st;
g_solver->collect_statistics(st);
std::cout << st << "\n";
}
}
static void STD_CALL on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
display_statistics();
raise(SIGINT);
}
void tst_polysat_argv(char** argv, int argc, int& i) { void tst_polysat_argv(char** argv, int argc, int& i) {
// set up SMT2 parser to extract assertions // set up SMT2 parser to extract assertions
// assume they are simple bit-vector equations (and inequations) // assume they are simple bit-vector equations (and inequations)
// convert to solver state. // convert to solver state.
signal(SIGINT, on_ctrl_c);
if (argc < 3) { if (argc < 3) {
std::cerr << "Usage: " << argv[0] << " FILE\n"; std::cerr << "Usage: " << argv[0] << " FILE\n";
@ -884,6 +902,7 @@ void tst_polysat_argv(char** argv, int argc, int& i) {
VERIFY(parse_smt2_commands(ctx, is)); VERIFY(parse_smt2_commands(ctx, is));
auto fmls = ctx.assertions(); auto fmls = ctx.assertions();
polysat::scoped_solver s("polysat"); polysat::scoped_solver s("polysat");
g_solver = &s;
polysat::internalize(m, s, fmls); polysat::internalize(m, s, fmls);
std::cout << "checking\n"; std::cout << "checking\n";
s.check(); s.check();