mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

enforce flat within QF_BV tactic, cap in-processing var-elim loops

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-27 20:10:55 -07:00
parent 1fae3aa152
commit a409a4a677
5 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_rewriter.h
View file

@ -354,7 +354,7 @@ class seq_rewriter {
public: public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_br(m), m_re2aut(m), m_op_cache(m), m_es(m), m_util(m), m_autil(m), m_br(m, p), m_re2aut(m), m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) { m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
} }
ast_manager & m() const { return m_util.get_manager(); } ast_manager & m() const { return m_util.get_manager(); }

2
src/ast/rewriter/th_rewriter.cpp
View file

@ -850,7 +850,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_f_rw(m, p), m_f_rw(m, p),
m_dl_rw(m), m_dl_rw(m),
m_pb_rw(m), m_pb_rw(m),
m_seq_rw(m), m_seq_rw(m, p),
m_char_rw(m), m_char_rw(m),
m_rec_rw(m), m_rec_rw(m),
m_a_util(m), m_a_util(m),

4
src/sat/sat_simplifier.cpp
View file

@ -229,6 +229,7 @@ namespace sat {
} }
} }
unsigned count = 0;
do { do {
if (m_subsumption) if (m_subsumption)
subsume(); subsume();
@ -240,8 +241,9 @@ namespace sat {
return; return;
if (!m_subsumption || m_sub_counter < 0) if (!m_subsumption || m_sub_counter < 0)
break; break;
++count;
} }
while (!m_sub_todo.empty()); while (!m_sub_todo.empty() && count < 20);
bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars; bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
if (m_need_cleanup || vars_eliminated) { if (m_need_cleanup || vars_eliminated) {

19
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -36,6 +36,7 @@ class solve_eqs_tactic : public tactic {
ast_manager & m_manager; ast_manager & m_manager;
expr_replacer * m_r; expr_replacer * m_r;
params_ref m_params;
bool m_r_owner; bool m_r_owner;
arith_util m_a_util; arith_util m_a_util;
obj_map<expr, unsigned> m_num_occs; obj_map<expr, unsigned> m_num_occs;
@ -80,7 +81,8 @@ class solve_eqs_tactic : public tactic {
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
tactic_params tp(p); m_params.append(p);
tactic_params tp(m_params);
m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver()); m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
m_theory_solver = p.get_bool("theory_solver", tp.solve_eqs_theory_solver()); m_theory_solver = p.get_bool("theory_solver", tp.solve_eqs_theory_solver());
m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs()); m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
@ -702,8 +704,8 @@ class solve_eqs_tactic : public tactic {
if (m_produce_proofs) if (m_produce_proofs)
return; return;
unsigned size = g.size(); unsigned size = g.size();
hoist_rewriter_star rw(m()); hoist_rewriter_star rw(m(), m_params);
th_rewriter thrw(m()); th_rewriter thrw(m(), m_params);
expr_ref tmp(m()), tmp2(m()); expr_ref tmp(m()), tmp2(m());
TRACE("solve_eqs", g.display(tout);); TRACE("solve_eqs", g.display(tout););
@ -1082,15 +1084,13 @@ class solve_eqs_tactic : public tactic {
}; };
imp * m_imp; imp * m_imp;
params_ref m_params;
public: public:
solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner): solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner) {
m_params(p) {
m_imp = alloc(imp, m, p, r, owner); m_imp = alloc(imp, m, p, r, owner);
} }
tactic * translate(ast_manager & m) override { tactic * translate(ast_manager & m) override {
return alloc(solve_eqs_tactic, m, m_params, mk_expr_simp_replacer(m, m_params), true); return alloc(solve_eqs_tactic, m, m_imp->m_params, mk_expr_simp_replacer(m, m_imp->m_params), true);
} }
~solve_eqs_tactic() override { ~solve_eqs_tactic() override {
@ -1100,8 +1100,7 @@ public:
char const* name() const override { return "solve_eqs"; } char const* name() const override { return "solve_eqs"; }
void updt_params(params_ref const & p) override { void updt_params(params_ref const & p) override {
m_params.append(p); m_imp->updt_params(p);
m_imp->updt_params(m_params);
} }
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
@ -1126,7 +1125,7 @@ public:
bool owner = m_imp->m_r_owner; bool owner = m_imp->m_r_owner;
m_imp->m_r_owner = false; // stole replacer m_imp->m_r_owner = false; // stole replacer
imp * d = alloc(imp, m, m_params, r, owner); imp * d = alloc(imp, m, m_imp->m_params, r, owner);
d->m_num_eliminated_vars = num_elim_vars; d->m_num_eliminated_vars = num_elim_vars;
std::swap(d, m_imp); std::swap(d, m_imp);
dealloc(d); dealloc(d);

1
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -86,6 +86,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
params_ref local_ctx_p = p; params_ref local_ctx_p = p;
local_ctx_p.set_bool("local_ctx", true); local_ctx_p.set_bool("local_ctx", true);
local_ctx_p.set_bool("flat", false);
params_ref solver_p; params_ref solver_p;
solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.