mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

Dump benchmarks in pool_solver

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 10:40:42 -07:00
parent b50da20531
commit bebfac047e
1 changed files with 59 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

100
src/solver/solver_pool.cpp
View file

@ -32,8 +32,11 @@ class pool_solver : public solver_na2as {
expr_ref_vector m_flat; expr_ref_vector m_flat;
bool m_pushed; bool m_pushed;
bool m_in_delayed_scope; bool m_in_delayed_scope;
bool m_dump_benchmarks;
double m_dump_threshold;
unsigned m_dump_counter; unsigned m_dump_counter;
bool is_virtual() const { return !m.is_true(m_pred); } bool is_virtual() const { return !m.is_true(m_pred); }
public: public:
pool_solver(solver* b, solver_pool& pool, app_ref& pred): pool_solver(solver* b, solver_pool& pool, app_ref& pred):
@ -47,10 +50,13 @@ public:
m_flat(m), m_flat(m),
m_pushed(false), m_pushed(false),
m_in_delayed_scope(false), m_in_delayed_scope(false),
m_dump_benchmarks(false),
m_dump_threshold(5.0),
m_dump_counter(0) { m_dump_counter(0) {
if (is_virtual()) { if (is_virtual()) {
solver_na2as::assert_expr_core2(m.mk_true(), pred); solver_na2as::assert_expr_core2(m.mk_true(), pred);
} }
updt_params(m_base->get_params());
} }
~pool_solver() override { ~pool_solver() override {
@ -64,7 +70,11 @@ public:
solver* base_solver() { return m_base.get(); } solver* base_solver() { return m_base.get(); }
solver* translate(ast_manager& m, params_ref const& p) override { UNREACHABLE(); return nullptr; } solver* translate(ast_manager& m, params_ref const& p) override { UNREACHABLE(); return nullptr; }
void updt_params(params_ref const& p) override { solver::updt_params(p); m_base->updt_params(p); } void updt_params(params_ref const& p) override {
solver::updt_params(p); m_base->updt_params(p);
m_dump_benchmarks = solver::get_params().get_bool("dump_benchmarks", false);
m_dump_threshold = solver::get_params().get_double("dump_threshold", 5.0);
}
void push_params() override {m_base->push_params();} void push_params() override {m_base->push_params();}
void pop_params() override {m_base->pop_params();} void pop_params() override {m_base->pop_params();}
@ -76,8 +86,8 @@ public:
void get_unsat_core(ptr_vector<expr> & r) override { void get_unsat_core(ptr_vector<expr> & r) override {
m_base->get_unsat_core(r); m_base->get_unsat_core(r);
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < r.size(); ++i) for (unsigned i = 0; i < r.size(); ++i)
if (m_pred != r[i]) if (m_pred != r[i])
r[j++] = r[i]; r[j++] = r[i];
r.shrink(j); r.shrink(j);
} }
@ -132,8 +142,10 @@ public:
} }
set_status(res); set_status(res);
if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) { if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
dump_benchmark(num_assumptions, assumptions, res, sw); expr_ref_vector cube(m, num_assumptions, assumptions);
expr_ref_vector clause(m);
dump_benchmark(cube, clause, res, sw.get_seconds());
} }
return res; return res;
} }
@ -164,9 +176,9 @@ public:
} }
set_status(res); set_status(res);
// if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) { if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
// dump_benchmark(num_assumptions, assumptions, res, sw); dump_benchmark(cube, clause, res, sw.get_seconds());
// } }
return res; return res;
} }
@ -179,9 +191,9 @@ public:
m_pushed = true; m_pushed = true;
m_in_delayed_scope = false; m_in_delayed_scope = false;
} }
if (!m_pushed) { if (!m_pushed) {
m_in_delayed_scope = true; m_in_delayed_scope = true;
} }
else { else {
SASSERT(!m_in_delayed_scope); SASSERT(!m_in_delayed_scope);
@ -196,24 +208,24 @@ public:
SASSERT(!m_in_delayed_scope); SASSERT(!m_in_delayed_scope);
m_base->pop(n); m_base->pop(n);
m_pushed = lvl - n > 0; m_pushed = lvl - n > 0;
} }
else { else {
m_in_delayed_scope = lvl - n > 0; m_in_delayed_scope = lvl - n > 0;
} }
} }
void assert_expr_core(expr * e) override { void assert_expr_core(expr * e) override {
SASSERT(!m_pushed || get_scope_level() > 0); SASSERT(!m_pushed || get_scope_level() > 0);
if (m.is_true(e)) return; if (m.is_true(e)) return;
if (m_in_delayed_scope) { if (m_in_delayed_scope) {
internalize_assertions(); internalize_assertions();
m_base->push(); m_base->push();
m_pushed = true; m_pushed = true;
m_in_delayed_scope = false; m_in_delayed_scope = false;
} }
if (m_pushed) { if (m_pushed) {
m_base->assert_expr(e); m_base->assert_expr(e);
} }
else { else {
m_flat.push_back(e); m_flat.push_back(e);
@ -221,7 +233,7 @@ public:
m_assertions.append(m_flat); m_assertions.append(m_flat);
m_flat.reset(); m_flat.reset();
} }
} }
void get_model_core(model_ref & _m) override { m_base->get_model_core(_m); } void get_model_core(model_ref & _m) override { m_base->get_model_core(_m); }
@ -235,7 +247,7 @@ public:
void set_progress_callback(progress_callback * callback) override { m_base->set_progress_callback(callback); } void set_progress_callback(progress_callback * callback) override { m_base->set_progress_callback(callback); }
expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { return expr_ref_vector(m); } expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { return expr_ref_vector(m); }
ast_manager& get_manager() const override { return m_base->get_manager(); } ast_manager& get_manager() const override { return m_base->get_manager(); }
void refresh(solver* new_base) { void refresh(solver* new_base) {
@ -253,42 +265,49 @@ public:
private: private:
void dump_benchmark(unsigned num_assumptions, expr * const * assumptions, lbool res, stopwatch& sw) { void dump_benchmark(const expr_ref_vector &cube, const expr_ref_vector &clause,
std::string file_name = mk_file_name(); lbool last_status, double last_time) {
std::string file_name = mk_file_name();
std::ofstream out(file_name); std::ofstream out(file_name);
if (!out) { if (!out) {
IF_VERBOSE(0, verbose_stream() << "could not open file " << file_name << " for output\n"); IF_VERBOSE(0, verbose_stream() << "could not open file " << file_name << " for output\n");
return; return;
} }
out << "(set-info :status " << lbool2status(res) << ")\n"; out << "(set-info :status " << lbool2status(last_status) << ")\n";
m_base->display(out, num_assumptions, assumptions); m_base->display(out, cube.size(), cube.c_ptr());
out << "(check-sat"; if (!clause.empty()) {
for (unsigned i = 0; i < num_assumptions; ++i) { out << ";; extra clause\n";
out << " " << mk_pp(assumptions[i], m); out << "(assert (or ";
for (auto *lit : clause) out << mk_pp(lit, m) << " ";
out << "))\n";
} }
out << ")";
out << "(check-sat";
for (auto * lit : cube) out << " " << mk_pp(lit, m);
out << ")\n";
out << "(exit)\n"; out << "(exit)\n";
::statistics st; ::statistics st;
m_base->collect_statistics(st); m_base->collect_statistics(st);
st.update("time", sw.get_seconds()); st.update("time", last_time);
st.display_smt2(out); st.display_smt2(out);
out.close(); out.close();
} }
char const* lbool2status(lbool r) const { char const* lbool2status(lbool r) const {
switch (r) { switch (r) {
case l_true: return "sat"; case l_true: return "sat";
case l_false: return "unsat"; case l_false: return "unsat";
case l_undef: return "unknown"; case l_undef: return "unknown";
} }
return "?"; return "?";
} }
std::string mk_file_name() { std::string mk_file_name() {
std::stringstream file_name; std::stringstream file_name;
file_name << "virt_solver"; file_name << "pool_solver";
if (is_virtual()) file_name << "_" << m_pred->get_decl()->get_name(); if (is_virtual()) file_name << "_" << m_pred->get_decl()->get_name();
file_name << "_" << (m_dump_counter++) << ".smt2"; file_name << "_" << (m_dump_counter++) << ".smt2";
return file_name.str(); return file_name.str();
} }
@ -317,12 +336,11 @@ ptr_vector<solver> solver_pool::get_base_solvers() const {
void solver_pool::updt_params(const params_ref &p) { void solver_pool::updt_params(const params_ref &p) {
m_base_solver->updt_params(p); m_base_solver->updt_params(p);
ptr_vector<solver> solvers = get_base_solvers(); for (solver *s : m_solvers) s->updt_params(p);
for (solver *s : solvers) s->updt_params(p);
} }
void solver_pool::collect_statistics(statistics &st) const { void solver_pool::collect_statistics(statistics &st) const {
ptr_vector<solver> solvers = get_base_solvers(); ptr_vector<solver> solvers = get_base_solvers();
for (solver* s : solvers) s->collect_statistics(st); for (solver* s : solvers) s->collect_statistics(st);
st.update("time.pool_solver.smt.total", m_check_watch.get_seconds()); st.update("time.pool_solver.smt.total", m_check_watch.get_seconds());
st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds()); st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds());
st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds()); st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds());
@ -336,7 +354,7 @@ void solver_pool::reset_statistics() {
#if 0 #if 0
ptr_vector<solver> solvers = get_base_solvers(); ptr_vector<solver> solvers = get_base_solvers();
for (solver* s : solvers) { for (solver* s : solvers) {
s->reset_statistics(); s->reset_statistics();
} }
#endif #endif
m_stats.reset(); m_stats.reset();
@ -348,7 +366,7 @@ void solver_pool::reset_statistics() {
/** /**
\brief Create a fresh solver instance. \brief Create a fresh solver instance.
The first num_pools solvers are independent and The first num_pools solvers are independent and
use a fresh instance of the base solver. use a fresh instance of the base solver.
Subsequent solvers reuse the first num_polls base solvers, rotating Subsequent solvers reuse the first num_polls base solvers, rotating
among the first num_pools. among the first num_pools.
@ -374,7 +392,7 @@ solver* solver_pool::mk_solver() {
void solver_pool::reset_solver(solver* s) { void solver_pool::reset_solver(solver* s) {
pool_solver* ps = dynamic_cast<pool_solver*>(s); pool_solver* ps = dynamic_cast<pool_solver*>(s);
SASSERT(ps); SASSERT(ps);
if (ps) ps->reset(); if (ps) ps->reset();
} }
void solver_pool::refresh(solver* base_solver) { void solver_pool::refresh(solver* base_solver) {