mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 07:29:28 +00:00
Code Activity

deal with code smells/duplicate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-21 18:57:08 +02:00
parent 46364a1502
commit aed76af2b5
2 changed files with 36 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

94
src/smt/theory_nseq.cpp
View file

@ -974,9 +974,9 @@ namespace smt {
for (auto [a, b] : eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";
);
bool all_true =
all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; })
&& all_of(eqs, [&](auto eq) { return eq.first->get_root() == eq.second->get_root(); });
SASSERT(all_of(eqs, [&](auto eq) { return eq.first->get_root() == eq.second->get_root(); }));
bool all_true = all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; });
if (all_true) {
ctx.set_conflict(
@ -997,6 +997,36 @@ namespace smt {
}
}
void theory_nseq::set_propagate(enode_pair_vector const& eqs, literal_vector const& lits, literal p) {
SASSERT(all_of(eqs, [&](auto eq) { return eq.first->get_root() == eq.second->get_root(); }));
bool all_true = all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; });
TRACE(seq, tout << "nseq propagation: " << ctx.literal2expr(p) << " (" << eqs.size() << " eqs, "
<< lits.size() << " lits)\n";
for (auto lit : lits) tout << "<- " << ctx.literal2expr(lit) << "\n";
for (auto [a, b] : eqs) tout << "<- " << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";);
ctx.mark_as_relevant(p);
if (all_true) {
justification *js = ctx.mk_justification(ext_theory_propagation_justification(
get_id(), ctx, lits.size(), lits.data(), eqs.size(), eqs.data(), p));
ctx.assign(p, js);
}
else {
literal_vector clause;
for (literal lit : lits)
clause.push_back(~lit);
for (auto [a, b] : eqs)
clause.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
clause.push_back(p);
for (auto lit : clause)
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
}
}
// -----------------------------------------------------------------------
// Model generation
// -----------------------------------------------------------------------
@ -1267,43 +1297,8 @@ namespace smt {
for (auto const& d : les)
lits.push_back(mk_le_literal(d));
bool all_true = true;
literal_vector eq_lits;
for (auto [a, b] : eqs) {
literal lit_eq = mk_eq(a->get_expr(), b->get_expr(), false);
eq_lits.push_back(lit_eq);
ctx.mark_as_relevant(lit_eq);
all_true &= (ctx.get_assignment(lit_eq) == l_true);
}
for (literal dep_lit : lits) {
ctx.mark_as_relevant(dep_lit);
all_true &= (ctx.get_assignment(dep_lit) == l_true);
}
set_propagate(eqs, lits, lit);
ctx.mark_as_relevant(lit);
if (all_true) {
justification* js = ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), ctx,
lits.size(), lits.data(),
eqs.size(), eqs.data(),
lit));
ctx.assign(lit, js);
}
else {
literal_vector clause;
for (literal dep_lit : lits)
clause.push_back(~dep_lit);
for (literal lit_eq : eq_lits)
clause.push_back(~lit_eq);
clause.push_back(lit);
ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
}
TRACE(seq, tout << "nseq length propagation: " << mk_pp(lc.m_expr, m) << " (" << eqs.size() << " eqs, "
<< lits.size() << " lits)\n";
for (auto lit : lits) tout << "<- " << ctx.literal2expr(lit) << "\n";
for (auto [a, b] : eqs) tout << "<- " << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";);
++m_num_length_axioms;
return true;
}
@ -1560,26 +1555,7 @@ namespace smt {
for (auto const &d : dep_les)
dep_lits.push_back(mk_le_literal(d));
bool all_true = all_of(dep_lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; }) &&
all_of(eqs, [&](auto e) { return e.first->get_root() == e.second->get_root(); });
ctx.mark_as_relevant(lit_prop);
if (all_true) {
justification *js = ctx.mk_justification(ext_theory_propagation_justification(
get_id(), ctx, dep_lits.size(), dep_lits.data(), eqs.size(), eqs.data(), lit_prop));
ctx.assign(lit_prop, js);
}
else {
literal_vector clause;
for (literal dep_lit : dep_lits)
clause.push_back(~dep_lit);
for (auto [a, b] : eqs)
clause.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
clause.push_back(lit_prop);
for (auto lit : clause)
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), clause.size(), clause.data());
}
set_propagate(eqs, dep_lits, lit_prop);
TRACE(seq, tout << "nseq length coherence check: length " << l << " with gradient " << g
<< " is incompatible for " << mk_pp(s, m) << ", propagated " << mk_pp(prop_expr, m)

1
src/smt/theory_nseq.h
View file

@ -117,6 +117,7 @@ namespace smt {
void populate_nielsen_graph();
void explain_nielsen_conflict();
void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
void set_propagate(enode_pair_vector const &eqs, literal_vector const &lits, literal p);
void add_nielsen_assumptions();
euf::snode* get_snode(expr* e);