From a409a4a6775aa5ec97654ec038b01f918063cbf6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Oct 2022 20:10:55 -0700 Subject: [PATCH] enforce flat within QF_BV tactic, cap in-processing var-elim loops --- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/rewriter/th_rewriter.cpp | 2 +- src/sat/sat_simplifier.cpp | 4 +++- src/tactic/core/solve_eqs_tactic.cpp | 19 +++++++++---------- src/tactic/smtlogics/qfbv_tactic.cpp | 1 + 5 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index cb00938d7..26dc00675 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -354,7 +354,7 @@ class seq_rewriter { public: 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) { } ast_manager & m() const { return m_util.get_manager(); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f7ac45ff5..96b69dbc3 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -850,7 +850,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_f_rw(m, p), m_dl_rw(m), m_pb_rw(m), - m_seq_rw(m), + m_seq_rw(m, p), m_char_rw(m), m_rec_rw(m), m_a_util(m), diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b0faaf6c9..b67ef6a2a 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -229,6 +229,7 @@ namespace sat { } } + unsigned count = 0; do { if (m_subsumption) subsume(); @@ -240,8 +241,9 @@ namespace sat { return; if (!m_subsumption || m_sub_counter < 0) 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; if (m_need_cleanup || vars_eliminated) { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 30e4a8c4b..a7b206d5b 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -36,6 +36,7 @@ class solve_eqs_tactic : public tactic { ast_manager & m_manager; expr_replacer * m_r; + params_ref m_params; bool m_r_owner; arith_util m_a_util; obj_map m_num_occs; @@ -80,7 +81,8 @@ class solve_eqs_tactic : public tactic { ast_manager & m() const { return m_manager; } 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_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()); @@ -702,8 +704,8 @@ class solve_eqs_tactic : public tactic { if (m_produce_proofs) return; unsigned size = g.size(); - hoist_rewriter_star rw(m()); - th_rewriter thrw(m()); + hoist_rewriter_star rw(m(), m_params); + th_rewriter thrw(m(), m_params); expr_ref tmp(m()), tmp2(m()); TRACE("solve_eqs", g.display(tout);); @@ -1082,15 +1084,13 @@ class solve_eqs_tactic : public tactic { }; imp * m_imp; - params_ref m_params; public: - solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner): - m_params(p) { + solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner) { m_imp = alloc(imp, m, p, r, owner); } 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 { @@ -1100,8 +1100,7 @@ public: char const* name() const override { return "solve_eqs"; } void updt_params(params_ref const & p) override { - m_params.append(p); - m_imp->updt_params(m_params); + m_imp->updt_params(p); } void collect_param_descrs(param_descrs & r) override { @@ -1126,7 +1125,7 @@ public: bool owner = m_imp->m_r_owner; 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; std::swap(d, m_imp); dealloc(d); diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index b242d86cf..1366b701e 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -86,6 +86,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); + local_ctx_p.set_bool("flat", false); params_ref solver_p; solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.