mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
add back max_occs parameter dependency to solve-eqs
This commit is contained in:
parent
acd2eaa390
commit
94b79eefea
2 changed files with 48 additions and 1 deletions
|
@ -262,6 +262,48 @@ namespace euf {
|
|||
}
|
||||
}
|
||||
|
||||
void solve_eqs::collect_num_occs(expr * t, expr_fast_mark1 & visited) {
|
||||
ptr_buffer<app, 128> stack;
|
||||
|
||||
auto visit = [&](expr* arg) {
|
||||
if (is_uninterp_const(arg)) {
|
||||
m_num_occs.insert_if_not_there(arg, 0)++;
|
||||
}
|
||||
if (!visited.is_marked(arg) && is_app(arg)) {
|
||||
visited.mark(arg, true);
|
||||
stack.push_back(to_app(arg));
|
||||
}
|
||||
};
|
||||
|
||||
visit(t);
|
||||
|
||||
while (!stack.empty()) {
|
||||
app * t = stack.back();
|
||||
stack.pop_back();
|
||||
for (expr* arg : *t)
|
||||
visit(arg);
|
||||
}
|
||||
}
|
||||
|
||||
void solve_eqs::collect_num_occs() {
|
||||
if (m_config.m_max_occs == UINT_MAX)
|
||||
return; // no need to compute num occs
|
||||
m_num_occs.reset();
|
||||
expr_fast_mark1 visited;
|
||||
for (unsigned i : indices())
|
||||
collect_num_occs(m_fmls[i].fml(), visited);
|
||||
}
|
||||
|
||||
// Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs
|
||||
bool solve_eqs::check_occs(expr * t) const {
|
||||
if (m_config.m_max_occs == UINT_MAX)
|
||||
return true;
|
||||
unsigned num = 0;
|
||||
m_num_occs.find(t, num);
|
||||
TRACE("solve_eqs_check_occs", tout << mk_ismt2_pp(t, m_manager) << " num_occs: " << num << " max: " << m_max_occs << "\n";);
|
||||
return num <= m_config.m_max_occs;
|
||||
}
|
||||
|
||||
void solve_eqs::save_subst(vector<dependent_expr> const& old_fmls) {
|
||||
if (!m_subst->empty())
|
||||
m_fmls.model_trail().push(m_subst.detach(), old_fmls);
|
||||
|
|
|
@ -56,10 +56,12 @@ namespace euf {
|
|||
expr_mark m_unsafe_vars; // expressions that cannot be replaced
|
||||
ptr_vector<expr> m_todo;
|
||||
expr_mark m_visited;
|
||||
obj_map<expr, unsigned> m_num_occs;
|
||||
|
||||
|
||||
bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; }
|
||||
unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; }
|
||||
bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); }
|
||||
bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e) && check_occs(e); }
|
||||
void get_eqs(dep_eq_vector& eqs);
|
||||
void filter_unsafe_vars();
|
||||
void extract_subst();
|
||||
|
@ -67,6 +69,9 @@ namespace euf {
|
|||
void normalize();
|
||||
void apply_subst(vector<dependent_expr>& old_fmls);
|
||||
void save_subst(vector<dependent_expr> const& old_fmls);
|
||||
void collect_num_occs(expr * t, expr_fast_mark1 & visited);
|
||||
void collect_num_occs();
|
||||
bool check_occs(expr* t) const;
|
||||
|
||||
public:
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue