mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

warnings

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 12:16:24 +01:00
parent f47fbdd714
commit 91a9feb5a8
4 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/fixed_bits.cpp
View file

@ -47,7 +47,7 @@ namespace polysat {
SASSERT(s.offset + s.length <= sz);
unsigned bw = s.length + s.offset;
unsigned K = sz - bw;
// unsigned K = sz - bw;
pdd lo = c.value(rational::power_of_two(sz - s.length) * (s.value + 1), sz);
pdd hi = c.value(rational::power_of_two(sz - s.length) * s.value, sz);
rational hi_val = rational::power_of_two(s.offset) * s.value;

2
src/sat/smt/polysat/monomials.cpp
View file

@ -142,7 +142,7 @@ namespace polysat {
bool monomials::mul(monomial const& mon, std::function<bool(rational const&)> const& p) {
unsigned free_index = UINT_MAX;
auto& m = mon.args[0].manager();
// auto& m = mon.args[0].manager();
for (unsigned j = mon.size(); j-- > 0; ) {
auto const& arg_val = mon.arg_vals[j];
if (p(arg_val))

5
src/sat/smt/polysat/saturation.cpp
View file

@ -38,13 +38,14 @@ namespace polysat {
if (l_false == operator()(idx))
return l_false;
}
// found conflict but no applicable saturation -> give up
if (has_conflict)
return l_undef;
return l_true;
}
lbool saturation::operator()(constraint_id idx) {
auto sc = c.get_constraint(idx);
// auto sc = c.get_constraint(idx);
auto vars = c.find_conflict_variables(idx);
for (auto v : vars)
if (resolve(v, idx))
@ -95,7 +96,7 @@ namespace polysat {
}
else
UNREACHABLE();
}
}
c.add_axiom(name, lemma.begin(), lemma.end(), is_redundant);
SASSERT(c.inconsistent());
}

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

@ -89,7 +89,7 @@ namespace polysat {
}
std::ostream& solver::display(std::ostream& out) const {
for (theory_var v = 0; v < get_num_vars(); ++v)
for (theory_var v = 0; v < (int)get_num_vars(); ++v)
if (m_var2pdd_valid.get(v, false))
out << "tv" << v << " is " << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
m_core.display(out);