mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

fix #7404, relates to #7400.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-27 11:36:10 +01:00
parent d047b86439
commit 01cf0427b4
6 changed files with 55 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/core/simplify_tactic.cpp
View file

@ -98,6 +98,7 @@ void simplify_tactic::operator()(goal_ref const & in,
(*m_imp)(*(in.get()));
in->inc_depth();
result.push_back(in.get());
m_clean = false;
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.msg());
@ -106,10 +107,13 @@ void simplify_tactic::operator()(goal_ref const & in,
void simplify_tactic::cleanup() {
if (m_clean)
return;
ast_manager & m = m_imp->m();
params_ref p = std::move(m_params);
m_imp->~imp();
new (m_imp) imp(m, p);
m_clean = true;
}
void simplify_tactic::collect_statistics(statistics& st) const {

1
src/tactic/core/simplify_tactic.h
View file

@ -69,6 +69,7 @@ There are several options to control its behavior.
#include "tactic/tactical.h"
class simplify_tactic : public tactic {
bool m_clean = true;
struct imp;
imp * m_imp;
params_ref m_params;

19
src/tactic/smtlogics/qfnra_tactic.cpp
View file

@ -89,7 +89,7 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) {
p_i.set_bool("shuffle_vars", true);
// if ((i & 1) == 0)
// p_i.set_bool("randomize", false);
ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000));
ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000); }));
}
{
ts.push_back(mk_qfnra_nlsat_tactic(m, p));
@ -147,7 +147,7 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) {
p_i.set_bool("shuffle_vars", true);
// if ((i & 1) == 0)
// p_i.set_bool("randomize", false);
ts.push_back(try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000));
ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000); }));
}
{
ts.push_back(mk_qfnra_nlsat_tactic(m, p));
@ -308,15 +308,20 @@ const double SMALL_THRESHOLD = 80.0;
const double MIDDLE_THRESHOLD = 300.0;
const double LARGE_THRESHOLD = 600.0;
tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) {
auto very_small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_small_solver(m, p); });
auto small_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_small_solver(m, p); });
auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); });
auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); });
auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); });
return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)),
mk_qfnra_very_small_solver(m, p),
very_small_t,
cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)),
mk_qfnra_small_solver(m, p),
small_t,
cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)),
mk_qfnra_middle_solver(m, p),
middle_t,
cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)),
mk_qfnra_large_solver(m, p),
mk_qfnra_very_large_solver(m, p)
large_t,
very_large_t
)
)
)

26
src/tactic/tactic.cpp
View file

@ -95,6 +95,32 @@ tactic * mk_skip_tactic() {
return alloc(skip_tactic);
}
class lazy_tactic : public tactic {
ast_manager& m;
params_ref p;
std::function<tactic* (ast_manager& m, params_ref const& p)> m_mk_tactic;
tactic* m_tactic = nullptr;
void ensure_tactic() { if (!m_tactic) m_tactic = m_mk_tactic(m, p); }
public:
lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic* (ast_manager&, params_ref const&)> mk_tactic) : m(m), p(p), m_mk_tactic(mk_tactic) {}
~lazy_tactic() override { dealloc(m_tactic); }
void operator()(goal_ref const& in, goal_ref_buffer& result) override {
ensure_tactic();
(*m_tactic)(in, result);
}
void cleanup() override { if (m_tactic) m_tactic->cleanup(); }
char const* name() const override { return "lazy tactic"; }
void collect_statistics(statistics& st) const override { if (m_tactic) m_tactic->collect_statistics(st); }
void user_propagate_initialize_value(expr* var, expr* value) override { if (m_tactic) m_tactic->user_propagate_initialize_value(var, value); }
tactic* translate(ast_manager& m) override { ensure_tactic(); return m_tactic->translate(m); }
void reset() override { if (m_tactic) m_tactic->reset(); }
};
tactic* mk_lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic*(ast_manager& m, params_ref const& p)> mkt) {
return alloc(lazy_tactic, m, p, mkt);
}
class fail_tactic : public tactic {
public:
void operator()(goal_ref const & in, goal_ref_buffer & result) override {

1
src/tactic/tactic.h
View file

@ -135,6 +135,7 @@ public:
tactic * mk_skip_tactic();
tactic * mk_fail_tactic();
tactic * mk_fail_if_undecided_tactic();
tactic* mk_lazy_tactic(ast_manager& m, params_ref const& p, std::function<tactic*(ast_manager& m, params_ref const& p)>);
/*
ADD_TACTIC("skip", "do nothing tactic.", "mk_skip_tactic()")

14
src/tactic/tactical.cpp
View file

@ -30,6 +30,7 @@ class binary_tactical : public tactic {
protected:
tactic_ref m_t1;
tactic_ref m_t2;
bool m_clean = true;
public:
@ -61,8 +62,11 @@ public:
}
void cleanup() override {
if (m_clean)
return;
m_t1->cleanup();
m_t2->cleanup();
m_clean = true;
}
void reset() override {
@ -103,7 +107,8 @@ public:
char const* name() const override { return "and_then"; }
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
m_clean = false;
bool proofs_enabled = in->proofs_enabled();
bool cores_enabled = in->unsat_core_enabled();
@ -872,6 +877,7 @@ tactic * par_and_then(unsigned num, tactic * const * ts) {
class unary_tactical : public tactic {
protected:
tactic_ref m_t;
bool m_clean = true;
public:
@ -880,11 +886,12 @@ public:
SASSERT(t);
}
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
m_clean = false;
m_t->operator()(in, result);
}
void cleanup(void) override { m_t->cleanup(); }
void cleanup(void) override { if (!m_clean) m_t->cleanup(); m_clean = true; }
void collect_statistics(statistics & st) const override { m_t->collect_statistics(st); }
void reset_statistics() override { m_t->reset_statistics(); }
void updt_params(params_ref const & p) override { m_t->updt_params(p); }
@ -1158,6 +1165,7 @@ public:
char const* name() const override { return "cond"; }
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
m_clean = false;
if (m_p->operator()(*(in.get())).is_true())
m_t1->operator()(in, result);
else