mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

output

Browse source
This commit is contained in:
Jakob Rath 2023-01-09 17:19:58 +01:00
parent 181995a4fb
commit b6ea9e31e5
3 changed files with 15 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_pdd.cpp
View file

@ -1725,7 +1725,7 @@ namespace dd {
if (val.is_power_of_two(pow) && pow > 10)
return out << "2^" << pow;
for (int offset : {-2, -1, 1, 2})
if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10)
if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10 && pow < m.power_of_2())
return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen();
rational neg_val = mod(-val, m.two_to_N());
if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise

18
src/math/polysat/solver.cpp
View file

@ -977,18 +977,16 @@ namespace polysat {
lemmas.push_back(m_conflict.build_lemma());
appraise_lemma(lemmas.back());
}
SASSERT(best_score < lemma_score::max());
if (!best_lemma) {
verbose_stream() << "conflict: " << m_conflict << "\n";
verbose_stream() << "no lemma\n";
for (clause* cl: lemmas) {
for (sat::literal lit : *cl) {
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma
verbose_stream() << "is true " << lit << "\n";
if (!m_bvars.is_assigned(lit))
verbose_stream() << lit << " is not assigned \n";
}
verbose_stream() << *cl << "\n";
for (sat::literal lit : *cl)
verbose_stream() << " " << lit_pp(*this, lit) << "\n";
}
}
SASSERT(best_score < lemma_score::max());
VERIFY(best_lemma);
unsigned const jump_level = std::max(best_score.jump_level(), base_level());
@ -1334,9 +1332,9 @@ namespace polysat {
}
else {
sat::bool_var v = item.lit().var();
out << "\t" << item.lit() << " @" << m_bvars.level(v);
out << "\t" << lit_pp(*this, item.lit());
if (m_bvars.reason(v))
out << " " << *m_bvars.reason(v);
out << " reason " << *m_bvars.reason(v);
out << "\n";
}
}
@ -1365,7 +1363,7 @@ namespace polysat {
std::ostream& lit_pp::display(std::ostream& out) const {
auto c = s.lit2cnstr(lit);
out << lpad(4, lit) << ": " << rpad(30, c);
out << lpad(5, lit) << ": " << rpad(30, c);
if (!c)
return out;
out << " [ b:" << rpad(7, s.m_bvars.value(lit));

11
src/math/polysat/umul_ovfl_constraint.cpp
View file

@ -106,8 +106,9 @@ namespace polysat {
/**
* if p constant, q, propagate inequality
*/
bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive,
pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
bool umul_ovfl_constraint::narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
LOG("p: " << p0 << " := " << p);
LOG("q: " << q0 << " := " << q);
if (!p.is_val())
return false;
@ -142,9 +143,9 @@ namespace polysat {
return true;
}
bool umul_ovfl_constraint::try_viable(
solver& s, bool is_positive,
pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
bool umul_ovfl_constraint::try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q) {
LOG("p: " << p0 << " := " << p);
LOG("q: " << q0 << " := " << q);
signed_constraint sc(this, is_positive);
return s.m_viable.intersect(p0, q0, sc);
}