diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index cc9854687..ffc8c7cb7 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -76,7 +76,7 @@ namespace euf { void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { auto [f, p, d] = e(); - expr* x, * y; + expr* x = nullptr, * y = nullptr; if (m.is_eq(f, x, y)) { if (x == y) return; @@ -87,7 +87,7 @@ namespace euf { if (is_uninterp_const(y)) eqs.push_back(dependent_eq(e.fml(), to_app(y), expr_ref(x, m), d)); } - expr* c, * th, * el, * x1, * y1, * x2, * y2; + expr* c = nullptr, * th = nullptr, * el = nullptr, * x1, * y1 = nullptr, * x2 = nullptr, * y2 = nullptr; if (m_ite_solver && m.is_ite(f, c, th, el)) { if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) { if (!m_allow_bool && m.is_bool(x1)) @@ -203,7 +203,7 @@ namespace euf { if (!m_enabled) return; auto [f, p, d] = e(); - expr* x, * y; + expr* x = nullptr, * y = nullptr; if (m.is_eq(f, x, y) && bv.is_bv(x)) { solve_eq(f, x, y, d, eqs); solve_eq(f, y, x, d, eqs); @@ -233,7 +233,7 @@ namespace euf { void solve_mod(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { if (!m_eliminate_mod) return; - expr* u, * z; + expr* u = nullptr, * z = nullptr; rational r1, r2; if (!a.is_mod(x, u, z)) return; @@ -251,7 +251,7 @@ namespace euf { } void solve_to_real(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { - expr* z, *u; + expr* z = nullptr, *u = nullptr; rational r; if (!a.is_to_real(x, z) || !is_uninterp_const(z)) return; @@ -270,7 +270,7 @@ namespace euf { void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { if (!a.is_add(x)) return; - expr* u, * z; + expr* u = nullptr, * z = nullptr; rational r; expr_ref term(m); unsigned i = 0; @@ -407,7 +407,7 @@ break; if (!m_enabled) return; auto [f, p, d] = e(); - expr* x, * y; + expr* x = nullptr, * y = nullptr; if (m.is_eq(f, x, y) && a.is_int_real(x)) { solve_eq(f, x, y, d, eqs); solve_eq(f, y, x, d, eqs); diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 05347b61f..b7b896640 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -725,7 +725,7 @@ namespace mbp { return m_imp->project1(model, var, vars, lits); } - bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + bool arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { vector defs; return m_imp->project(model, vars, lits, defs, false); } diff --git a/src/qe/mbp/mbp_arith.h b/src/qe/mbp/mbp_arith.h index 666ffffc4..1323032eb 100644 --- a/src/qe/mbp/mbp_arith.h +++ b/src/qe/mbp/mbp_arith.h @@ -29,7 +29,7 @@ namespace mbp { bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; } family_id get_family_id() override; - bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); } diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp index 1e4f63250..bd92be83a 100644 --- a/src/qe/mbp/mbp_euf.cpp +++ b/src/qe/mbp/mbp_euf.cpp @@ -58,7 +58,7 @@ namespace mbp { } - bool euf_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + bool euf_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { if (vars.empty()) return false; // check if there is a variable of uninterp sort diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h index abb7524c0..f706b0664 100644 --- a/src/qe/mbp/mbp_euf.h +++ b/src/qe/mbp/mbp_euf.h @@ -26,7 +26,7 @@ namespace mbp { bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; } family_id get_family_id() override; - bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); } diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index fb9be76dc..5e7dae8c7 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -69,7 +69,7 @@ namespace mbp { virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; } virtual family_id get_family_id() { return null_family_id; } - virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; + virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; /** \brief project vars modulo model, return set of definitions for eliminated variables. diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index c18144efc..57a7fee56 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -466,7 +466,7 @@ public: TRACE(qe, tout << "after project " << m.get_family_name(p->get_family_id()) << ": " << vars << "\n"); } else if (p) - (*p)(model, vars, fmls); + p->project(model, vars, fmls); } TRACE(qe, tout << "projecting " << vars << "\n"); while (!vars.empty() && !fmls.empty() && !defs && m.limit().inc()) { diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index ec9b1a0a6..a6eb4910d 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -356,7 +356,7 @@ namespace q { if (!p->project(*m_model, vars, fmls, m_defs)) return expr_ref(m); } - else if (!(*p)(*m_model, vars, fmls)) { + else if (!p->project(*m_model, vars, fmls)) { TRACE(q, tout << "theory projection failed - use value\n"); } }