mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

handle build warnings

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-06 15:13:31 +02:00
parent 7566f088f9
commit d33d6ebe83
8 changed files with 14 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/simplifiers/extract_eqs.cpp
View file

@ -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);

2
src/qe/mbp/mbp_arith.cpp
View file

@ -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<def> defs;
return m_imp->project(model, vars, lits, defs, false);
}

2
src/qe/mbp/mbp_arith.h
View file

@ -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<def>& defs) override;
void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }

2
src/qe/mbp/mbp_euf.cpp
View file

@ -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

2
src/qe/mbp/mbp_euf.h
View file

@ -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<def>& defs) override;
void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }

2
src/qe/mbp/mbp_plugin.h
View file

@ -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.

2
src/qe/qe_mbp.cpp
View file

@ -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()) {

2
src/sat/smt/q_mbi.cpp
View file

@ -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");
}
}