mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 08:45:47 +00:00
Code Activity

remove legacy solve_eqs_tactic entirely

Browse source 
also, bug fixes to elim_unconstrained (elim_uncnstr2) which is to replace legacy tactic for eliminating unconstrained constants.
This commit is contained in:
Nikolaj Bjorner 2022-11-14 18:57:16 -08:00
parent 3f2bbe5589
commit 6297c001ee
23 changed files with 56 additions and 1203 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/simplifiers/dependent_expr_state.h
View file

@ -61,9 +61,9 @@ public:
*/
class dependent_expr_simplifier {
protected:
ast_manager& m;
ast_manager& m;
dependent_expr_state& m_fmls;
trail_stack& m_trail;
trail_stack& m_trail;
unsigned m_qhead = 0; // pointer into last processed formula in m_fmls
unsigned num_scopes() const { return m_trail.get_num_scopes(); }
@ -78,6 +78,7 @@ public:
virtual void collect_statistics(statistics& st) const {}
virtual void reset_statistics() {}
virtual void updt_params(params_ref const& p) {}
virtual void collect_param_descrs(param_descrs& r) {}
};
/**

19
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -47,11 +47,9 @@ Author:
elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) {
std::function<bool(expr*)> is_var = [&](expr* e) {
return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount == 1;
return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount <= 1;
};
m_inverter.set_is_var(is_var);
}
@ -61,7 +59,6 @@ bool elim_unconstrained::is_var_lt(int v1, int v2) const {
return n1.m_refcount < n2.m_refcount;
}
void elim_unconstrained::eliminate() {
while (!m_heap.empty()) {
@ -79,8 +76,7 @@ void elim_unconstrained::eliminate() {
continue;
}
expr* e = get_parent(v);
for (expr* p : n.m_parents)
IF_VERBOSE(11, verbose_stream() << "parent " << mk_bounded_pp(p, m) << "\n");
IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";);
if (!e || !is_app(e) || !is_ground(e)) {
n.m_refcount = 0;
continue;
@ -90,6 +86,7 @@ void elim_unconstrained::eliminate() {
for (expr* arg : *to_app(t))
m_args.push_back(get_node(arg).m_term);
if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) {
IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n");
n.m_refcount = 0;
continue;
}
@ -103,12 +100,12 @@ void elim_unconstrained::eliminate() {
m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
get_node(e).m_term = r;
get_node(e).m_refcount++;
IF_VERBOSE(11, verbose_stream() << mk_pp(e, m) << "\n");
SASSERT(!m_heap.contains(e->get_id()));
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
SASSERT(!m_heap.contains(root(e)));
if (is_uninterp_const(r))
m_heap.insert(e->get_id());
m_heap.insert(root(e));
IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " " << mk_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n");
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";);
SASSERT(!side_cond && "not implemented to add side conditions\n");
}
@ -178,7 +175,7 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
n.m_term = e;
n.m_refcount = 0;
if (is_uninterp_const(e))
m_heap.insert(e->get_id());
m_heap.insert(root(e));
if (is_quantifier(e)) {
expr* body = to_quantifier(e)->get_expr();
get_node(body).m_parents.push_back(e);

15
src/ast/simplifiers/elim_unconstrained.h
View file

@ -23,9 +23,9 @@ Author:
class elim_unconstrained : public dependent_expr_simplifier {
struct node {
unsigned m_refcount;
expr* m_term;
expr* m_orig;
unsigned m_refcount = 0;
expr* m_term = nullptr;
expr* m_orig = nullptr;
ptr_vector<expr> m_parents;
};
struct var_lt {
@ -52,11 +52,12 @@ class elim_unconstrained : public dependent_expr_simplifier {
bool is_var_lt(int v1, int v2) const;
node& get_node(unsigned n) { return m_nodes[n]; }
node const& get_node(unsigned n) const { return m_nodes[n]; }
node& get_node(expr* t) { return m_nodes[m_root[t->get_id()]]; }
node const& get_node(expr* t) const { return m_nodes[m_root[t->get_id()]]; }
node& get_node(expr* t) { return m_nodes[root(t)]; }
unsigned root(expr* t) const { return m_root[t->get_id()]; }
node const& get_node(expr* t) const { return m_nodes[root(t)]; }
unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; }
void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(root(t)); }
void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(root(t)); }
void gc(expr* t);
expr* get_parent(unsigned n) const;
void init_terms(expr_ref_vector const& terms);

7
src/ast/simplifiers/solve_eqs.cpp
View file

@ -240,6 +240,13 @@ namespace euf {
ex->updt_params(p);
}
void solve_eqs::collect_param_descrs(param_descrs& r) {
r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
}
void solve_eqs::collect_statistics(statistics& st) const {
st.update("solve-eqs-steps", m_stats.m_num_steps);
st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars);

2
src/ast/simplifiers/solve_eqs.h
View file

@ -72,6 +72,8 @@ namespace euf {
void updt_params(params_ref const& p) override;
void collect_param_descrs(param_descrs& r) override;
void collect_statistics(statistics& st) const override;
};