From 606940e60c4edda87e504e7fab30411481143c70 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Aug 2023 10:29:48 -0700 Subject: [PATCH] nits Signed-off-by: Nikolaj Bjorner --- src/qe/lite/qel.cpp | 6 +- src/qe/lite/qel.h | 7 +- src/qe/mbp/mbp_term_graph.cpp | 117 ++++++++++++++++++++-------------- src/qe/mbp/mbp_term_graph.h | 32 +++++----- 4 files changed, 90 insertions(+), 72 deletions(-) diff --git a/src/qe/lite/qel.cpp b/src/qe/lite/qel.cpp index 583f51cc9..addd33c3c 100644 --- a/src/qe/lite/qel.cpp +++ b/src/qe/lite/qel.cpp @@ -18,18 +18,16 @@ Author: Hari Govind V K (hgvk94) Isabel Garcia (igcontreras) -Revision History: - --*/ #include "qe/lite/qel.h" #include "qe/mbp/mbp_term_graph.h" class qel::impl { - private: +private: ast_manager &m; - public: +public: impl(ast_manager &m, params_ref const &p) : m(m) {} void operator()(app_ref_vector &vars, expr_ref &fml) { diff --git a/src/qe/lite/qel.h b/src/qe/lite/qel.h index 9db6a32b4..ab960bc47 100644 --- a/src/qe/lite/qel.h +++ b/src/qe/lite/qel.h @@ -19,9 +19,6 @@ Author: Hari Govind V K (hgvk94) Isabel Garcia (igcontreras) -Revision History: - - --*/ #pragma once @@ -34,8 +31,8 @@ Revision History: class qel { class impl; impl *m_impl; - - public: + +public: qel(ast_manager &m, params_ref const &p); ~qel(); diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index ee371bdfa..3dc8a20f7 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -364,19 +364,25 @@ static std::ostream &operator<<(std::ostream &out, term const &t) { return t.display(out); } + // t1 != t2 void term_graph::add_deq_proc::operator()(term *t1, term *t2) { - ptr_vector ts(2); - ts[0] = t1; - ts[1] = t2; - (*this)(ts); + term::set_deq(t1->get_root().get_deqs(), m_deq_cnt); + term::set_deq(t2->get_root().get_deqs(), m_deq_cnt); + inc_count(); } // distinct(ts) void term_graph::add_deq_proc::operator()(ptr_vector &ts) { - for (auto t : ts) { term::set_deq(t->get_root().get_deqs(), m_deq_cnt); } - SASSERT(m_deq_cnt < UINT64_MAX); + for (auto t : ts) + term::set_deq(t->get_root().get_deqs(), m_deq_cnt); + inc_count(); +} + +void term_graph::add_deq_proc::inc_count() { m_deq_cnt++; + if (m_deq_cnt == 0) + throw default_exception("unexpected wrap-around on m_deq_cnt"); } bool term_graph::is_variable_proc::operator()(const expr *e) const { @@ -429,8 +435,7 @@ bool term_graph::term_eq::operator()(term const *a, term const *b) const { } term_graph::term_graph(ast_manager &man) - : m(man), m_lits(m), m_pinned(m), m_projector(nullptr), - m_explicit_eq(false), m_repick_repr(false) { + : m(man), m_lits(m), m_pinned(m) { m_is_var.reset(); m_plugins.register_plugin(mbp::mk_basic_solve_plugin(m, m_is_var)); m_plugins.register_plugin(mbp::mk_arith_solve_plugin(m, m_is_var)); @@ -447,15 +452,18 @@ bool term_graph::is_pure_def(expr *atom, expr *&v) { } static family_id get_family_id(ast_manager &m, expr *lit) { - if (m.is_not(lit, lit)) return get_family_id(m, lit); + if (m.is_not(lit, lit)) + return get_family_id(m, lit); expr *a = nullptr, *b = nullptr; - // deal with equality using sort of range - if (m.is_eq(lit, a, b)) { return a->get_sort()->get_family_id(); } - // extract family_id of top level app - else if (is_app(lit)) { return to_app(lit)->get_decl()->get_family_id(); } - else { return null_family_id; } + if (m.is_eq(lit, a, b)) // deal with equality using sort of range + return a->get_sort()->get_family_id(); + else if (is_app(lit)) // extract family_id of top level app + return to_app(lit)->get_decl()->get_family_id(); + else + return null_family_id; } + void term_graph::add_lit(expr *l) { expr_ref lit(m); expr_ref_vector lits(m); @@ -492,7 +500,8 @@ void term_graph::get_terms(expr_ref_vector &res, bool exclude_cground) { auto terms = m_terms.filter_pure(fil); res.resize(terms.size()); unsigned i = 0; - for (term *t : terms) res[i++] = t->get_expr(); + for (term *t : terms) + res[i++] = t->get_expr(); } bool term_graph::is_cgr(expr *e) { @@ -543,12 +552,13 @@ term *term_graph::internalize_term(expr *t) { continue; } unsigned sz = todo.size(); - if (is_app(t)) { - for (expr *arg : *::to_app(t)) { - if (!get_term(arg)) todo.push_back(arg); - } - } - if (sz < todo.size()) continue; + if (is_app(t)) + for (expr *arg : *::to_app(t)) + if (!get_term(arg)) + todo.push_back(arg); + + if (sz < todo.size()) + continue; todo.pop_back(); res = mk_term(t); @@ -556,11 +566,11 @@ term *term_graph::internalize_term(expr *t) { // could be congruent with some other term, if that is the case, we // need to merge them. term *res_old = m_cg_table.insert_if_not_there(res); - if (res->is_cgr()) res_old->set_cgr(true); + if (res->is_cgr()) + res_old->set_cgr(true); SASSERT(res_old->is_cgr() == res->is_cgr()); - if (res_old->get_root().get_id() != res->get_root().get_id()) { - m_merge.push_back(std::make_pair(res, res_old)); - } + if (res_old->get_root().get_id() != res->get_root().get_id()) + m_merge.push_back({res, res_old}); } merge_flush(); SASSERT(res); @@ -572,10 +582,12 @@ void term_graph::internalize_eq(expr *a1, expr *a2) { merge(*internalize_term(a1), *internalize_term(a2)); merge_flush(); SASSERT(m_merge.empty()); - if (!m_explicit_eq) return; + if (!m_explicit_eq) + return; expr_ref eq(m.mk_eq(a1, a2), m); term *res = get_term(eq); - if (!res) mk_term(eq); + if (!res) + mk_term(eq); } void term_graph::internalize_distinct(expr *d) { @@ -599,26 +611,29 @@ void term_graph::internalize_deq(expr *a1, expr *a2) { term *t2 = internalize_term(a2); m_add_deq(t1, t2); m_deq_pairs.push_back({t1, t2}); - if (!m_explicit_eq) return; + if (!m_explicit_eq) + return; expr_ref eq(m.mk_eq(a1, a2), m); term *eq_term = mk_term(eq); eq_term->set_neq_child(); expr_ref deq(m.mk_not(eq), m); term *res = get_term(deq); - if (!res) mk_term(deq); + if (!res) + mk_term(deq); } void term_graph::internalize_lit(expr *lit) { expr *e1 = nullptr, *e2 = nullptr, *ne = nullptr, *v = nullptr; - if (m.is_eq(lit, e1, e2)) { // internalize equality + if (m.is_eq(lit, e1, e2)) // internalize equality internalize_eq(e1, e2); - } - else if (m.is_distinct(lit)) { internalize_distinct(lit); } - else if (m.is_not(lit, ne) && m.is_eq(ne, e1, e2)) { + else if (m.is_distinct(lit)) + internalize_distinct(lit); + else if (m.is_not(lit, ne) && m.is_eq(ne, e1, e2)) internalize_deq(e1, e2); - } - else { internalize_term(lit); } - if (is_pure_def(lit, v)) { m_is_var.mark_solved(v); } + else + internalize_term(lit); + if (is_pure_def(lit, v)) + m_is_var.mark_solved(v); } void term_graph::merge_flush() { @@ -674,7 +689,8 @@ void term_graph::merge(term &t1, term &t2) { } } } - if (prop_cgroundness) cground_percolate_up(a); + if (prop_cgroundness) + cground_percolate_up(a); SASSERT(marks_are_clear()); } @@ -694,10 +710,12 @@ expr *term_graph::mk_app_core(expr *e) { expr_ref term_graph::mk_app(term &r) { SASSERT(r.is_repr()); - if (r.get_num_args() == 0) { return expr_ref(r.get_expr(), m); } + if (r.get_num_args() == 0) + return expr_ref(r.get_expr(), m); expr *res = nullptr; - if (m_term2app.find(r.get_id(), res)) { return expr_ref(res, m); } + if (m_term2app.find(r.get_id(), res)) + return expr_ref(res, m); res = mk_app_core(r.get_expr()); m_term2app.insert(r.get_id(), res); @@ -716,7 +734,8 @@ expr_ref term_graph::mk_app(expr *a) { void term_graph::mk_equalities(term &t, expr_ref_vector &out) { SASSERT(t.is_repr()); - if (t.get_class_size() == 1) return; + if (t.get_class_size() == 1) + return; expr_ref rep(mk_app(t), m); for (term *it = &t.get_next(); it != &t; it = &it->get_next()) { expr *mem = mk_app_core(it->get_expr()); @@ -725,7 +744,8 @@ void term_graph::mk_equalities(term &t, expr_ref_vector &out) { } void term_graph::mk_all_equalities(term &t, expr_ref_vector &out) { - if (t.get_class_size() == 1) return; + if (t.get_class_size() == 1) + return; mk_equalities(t, out); @@ -762,22 +782,25 @@ void term_graph::mk_qe_lite_equalities(term &t, expr_ref_vector &out, // don't add equalities for vars to eliminate if (m_is_var.contains(a->get_decl())) continue; expr *mem = mk_app_core(e); - if (rep != mem && !contains_nc(mem)) out.push_back(m.mk_eq(rep, mem)); + if (rep != mem && !contains_nc(mem)) + out.push_back(m.mk_eq(rep, mem)); } } void term_graph::reset_marks() { - for (term *t : m_terms) { t->set_mark(false); } + for (term *t : m_terms) t->set_mark(false); } void term_graph::reset_marks2() { - for (term *t : m_terms) { t->set_mark2(false); } + for (term *t : m_terms) t->set_mark2(false); } bool term_graph::marks_are_clear() { - for (term *t : m_terms) { - if (t->is_marked()) return false; - } + return all_of(m_terms, [](term* t) { return !t->is_marked(); }); + + for (term *t : m_terms) + if (t->is_marked()) + return false; return true; } diff --git a/src/qe/mbp/mbp_term_graph.h b/src/qe/mbp/mbp_term_graph.h index 1300034a6..58afcaf02 100644 --- a/src/qe/mbp/mbp_term_graph.h +++ b/src/qe/mbp/mbp_term_graph.h @@ -47,7 +47,7 @@ class term_graph { bool m_exclude; obj_hashtable m_decls, m_solved; - public: + public: bool operator()(const expr *e) const override; bool operator()(const term &t) const; @@ -68,7 +68,7 @@ class term_graph { class is_non_core : public i_expr_pred { std::function *m_non_core; - public: + public: is_non_core(std::function *nc) : m_non_core(nc) {} bool operator()(expr *n) override { if (m_non_core == nullptr) return false; @@ -82,16 +82,15 @@ class term_graph { struct term_eq { bool operator()(term const *a, term const *b) const; }; - ast_manager &m; - ptr_vector m_terms; - expr_ref_vector m_lits; // NSB: expr_ref_vector? - u_map m_app2term; - ast_ref_vector m_pinned; - projector *m_projector; - bool m_explicit_eq; - bool m_repick_repr; - u_map - m_term2app; // any representative change invalidates this cache + ast_manager & m; + ptr_vector m_terms; + expr_ref_vector m_lits; + u_map m_app2term; + ast_ref_vector m_pinned; + projector * m_projector = nullptr; + bool m_explicit_eq = false; + bool m_repick_repr = false; + u_map m_term2app; // any representative change invalidates this cache plugin_manager m_plugins; ptr_hashtable m_cg_table; vector> m_merge; @@ -138,7 +137,7 @@ class term_graph { void cground_percolate_up(term *t); void compute_cground(); - public: +public: term_graph(ast_manager &m); ~term_graph(); @@ -218,8 +217,9 @@ class term_graph { expr *rep_of(expr *e); using deqs = bit_vector; - struct add_deq_proc { - uint64_t m_deq_cnt = 0; + struct add_deq_proc { + unsigned m_deq_cnt = 0; + void inc_count(); void operator()(term *t1, term *t2); void operator()(ptr_vector &ts); }; @@ -239,7 +239,7 @@ class term_graph { app *get_const_in_class(expr *e); void set_explicit_eq() { m_explicit_eq = true; } - private: +private: add_deq_proc m_add_deq; void refine_repr_class(term *t); void refine_repr();