mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

#6423

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-26 12:06:02 -07:00
parent 1720addc4e
commit 2258b9b9b6
3 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/euf_internalize.cpp
View file

@ -224,6 +224,14 @@ namespace euf {
return; return;
} }
// check if it is trivial
expr_mark visited;
for (expr* arg : *e) {
if (visited.is_marked(arg))
return;
visited.mark(arg);
}
static const unsigned distinct_max_args = 32; static const unsigned distinct_max_args = 32;
if (sz <= distinct_max_args) { if (sz <= distinct_max_args) {
sat::literal_vector lits; sat::literal_vector lits;
@ -248,6 +256,7 @@ namespace euf {
func_decl_ref g(m.mk_fresh_func_decl("dist-g", "", 1, &u_ptr, srt), m); func_decl_ref g(m.mk_fresh_func_decl("dist-g", "", 1, &u_ptr, srt), m);
expr_ref a(m.mk_fresh_const("a", u), m); expr_ref a(m.mk_fresh_const("a", u), m);
expr_ref_vector eqs(m); expr_ref_vector eqs(m);
for (expr* arg : *e) { for (expr* arg : *e) {
expr_ref fapp(m.mk_app(f, arg), m); expr_ref fapp(m.mk_app(f, arg), m);
expr_ref gapp(m.mk_app(g, fapp.get()), m); expr_ref gapp(m.mk_app(g, fapp.get()), m);

5
src/sat/smt/pb_pb.cpp
View file

@ -39,6 +39,8 @@ namespace pb {
m_max_sum(0) { m_max_sum(0) {
for (unsigned i = 0; i < size(); ++i) { for (unsigned i = 0; i < size(); ++i) {
m_wlits[i] = wlits[i]; m_wlits[i] = wlits[i];
if (wlits[i].first > k)
m_wlits[i].first = k;
} }
update_max_sum(); update_max_sum();
} }
@ -47,9 +49,8 @@ namespace pb {
m_max_sum = 0; m_max_sum = 0;
for (unsigned i = 0; i < size(); ++i) { for (unsigned i = 0; i < size(); ++i) {
m_wlits[i].first = std::min(k(), m_wlits[i].first); m_wlits[i].first = std::min(k(), m_wlits[i].first);
if (m_max_sum + m_wlits[i].first < m_max_sum) { if (m_max_sum + m_wlits[i].first < m_max_sum)
throw default_exception("addition of pb coefficients overflows"); throw default_exception("addition of pb coefficients overflows");
}
m_max_sum += m_wlits[i].first; m_max_sum += m_wlits[i].first;
} }
} }

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

@ -1354,7 +1354,6 @@ namespace pb {
si(si), m_pb(m), si(si), m_pb(m),
m_lookahead(nullptr), m_lookahead(nullptr),
m_constraint_id(0), m_ba(*this), m_sort(m_ba) { m_constraint_id(0), m_ba(*this), m_sort(m_ba) {
TRACE("pb", tout << this << "\n";);
m_num_propagations_since_pop = 0; m_num_propagations_since_pop = 0;
} }
@ -1432,6 +1431,7 @@ namespace pb {
} }
if (!c->well_formed()) if (!c->well_formed())
IF_VERBOSE(0, verbose_stream() << *c << "\n"); IF_VERBOSE(0, verbose_stream() << *c << "\n");
SASSERT(c->well_formed());
VERIFY(c->well_formed()); VERIFY(c->well_formed());
if (m_solver && m_solver->get_config().m_drat) { if (m_solver && m_solver->get_config().m_drat) {
auto * out = s().get_drat().out(); auto * out = s().get_drat().out();