mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

replace seq::le by generic expr_ref

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-16 23:10:44 -07:00
parent e72c082818
commit b75acc5c14
8 changed files with 184 additions and 201 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/seq/seq_nielsen.cpp
View file

@ -45,7 +45,7 @@ NSB review:
namespace seq {
void deps_to_lits(dep_tracker deps, svector<enode_pair> &eqs, svector<sat::literal> &lits, vector<le>& les) {
void deps_to_lits(dep_tracker deps, svector<enode_pair> &eqs, svector<sat::literal> &lits, vector<expr_ref>& es) {
vector<dep_source> vs;
dep_manager::s_linearize(deps, vs);
for (dep_source const &d : vs) {
@ -54,7 +54,7 @@ namespace seq {
else if (std::holds_alternative<sat::literal>(d))
lits.push_back(std::get<sat::literal>(d));
else
les.push_back(std::get<le>(d));
es.push_back(std::get<expr_ref>(d));
}
}
@ -552,13 +552,12 @@ namespace seq {
void nielsen_graph::add_le_dependency(dep_tracker& dep, nielsen_node* n, expr* lhs, expr* rhs) {
SASSERT(lhs);
SASSERT(rhs);
expr_ref lhs_ref(lhs, m);
expr_ref rhs_ref(rhs, m);
expr_ref le(a.mk_le(lhs, rhs), m);
// just assume it to be correct
dep_tracker d = m_dep_mgr.mk_leaf(le{ lhs_ref, rhs_ref });
dep_tracker d = m_dep_mgr.mk_leaf(le);
// Just add the constraint - we do not have to recompute it
// [also it is on the set of side-conditions if we assert a satisfied node]
n->add_constraint(constraint(a.mk_le(lhs_ref, rhs_ref), d, m));
n->add_constraint(constraint(le, d, m));
dep = m_dep_mgr.mk_join(dep, d);
}
@ -4261,7 +4260,7 @@ namespace seq {
// NSB review: this is one of several methods exposed for testing
void nielsen_graph::test_aux_explain_conflict(svector<enode_pair>& eqs,
svector<sat::literal>& mem_literals,
vector<le>& les) const {
vector<expr_ref>& es) const {
SASSERT(m_root);
auto deps = collect_conflict_deps();
vector<dep_source> vs;
@ -4271,8 +4270,8 @@ namespace seq {
eqs.push_back(std::get<enode_pair>(d));
else if (std::holds_alternative<sat::literal>(d))
mem_literals.push_back(std::get<sat::literal>(d));
else if (std::holds_alternative<le>(d))
les.push_back(std::get<le>(d));
else if (std::holds_alternative<expr_ref>(d))
es.push_back(std::get<expr_ref>(d));
}
}

14
src/smt/seq/seq_nielsen.h
View file

@ -315,16 +315,8 @@ namespace seq {
using enode_pair = std::pair<smt::enode *, smt::enode *>;
// arithmetic implication dependency: lhs <= rhs
struct le {
expr_ref lhs;
expr_ref rhs;
bool operator==(le const &other) const {
return lhs == other.lhs && rhs == other.rhs;
}
};
using dep_source = std::variant<sat::literal, enode_pair, le>;
using dep_source = std::variant<sat::literal, enode_pair, expr_ref>;
// Arena-based dependency manager: builds an immutable tree of dep_source
@ -366,7 +358,7 @@ namespace seq {
void deps_to_lits(dep_tracker deps,
svector<enode_pair>& eqs,
svector<sat::literal>& lits,
vector<le>& les);
vector<expr_ref>& es);
// string equality constraint: lhs = rhs
// mirrors ZIPT's StrEq (both sides are regex-free snode trees)
@ -1003,7 +995,7 @@ namespace seq {
// Must be called after solve() returns unsat.
void test_aux_explain_conflict(svector<enode_pair> &eqs,
svector<sat::literal> &mem_literals,
vector<le>& les) const;
vector<expr_ref>& es) const;
// accumulated search statistics

31
src/smt/theory_nseq.cpp
View file

@ -595,15 +595,6 @@ namespace smt {
enqueue_axiom(n);
}
literal theory_nseq::mk_le_literal(seq::le const &d) {
expr_ref le_expr(m_autil.mk_le(d.lhs, d.rhs), m);
if (!ctx.b_internalized(le_expr))
ctx.internalize(le_expr, true);
literal lit = ctx.get_literal(le_expr);
ctx.mark_as_relevant(lit);
return lit;
}
// -----------------------------------------------------------------------
// Final check: build Nielsen graph and search
// -----------------------------------------------------------------------
@ -884,7 +875,7 @@ namespace smt {
else if (std::holds_alternative<sat::literal>(d))
lits.push_back(std::get<sat::literal>(d));
else
lits.push_back(mk_le_literal(std::get<seq::le>(d)));
lits.push_back(mk_literal(std::get<expr_ref>(d)));
}
++m_num_conflicts;
set_conflict(eqs, lits);
@ -938,8 +929,8 @@ namespace smt {
else if (std::holds_alternative<sat::literal>(d))
kernel.assert_expr(ctx.literal2expr(std::get<sat::literal>(d)));
else {
auto const& p = std::get<seq::le>(d);
kernel.assert_expr(m_autil.mk_le(p.lhs, p.rhs));
auto const& e = std::get<expr_ref>(d);
kernel.assert_expr(e);
}
}
auto res = kernel.check();
@ -1357,10 +1348,10 @@ namespace smt {
// conditional constraints: propagate with justification from dep_tracker
enode_pair_vector eqs;
literal_vector lits;
vector<seq::le> les;
seq::deps_to_lits(lc.m_dep, eqs, lits, les);
for (auto const& d : les)
lits.push_back(mk_le_literal(d));
vector<expr_ref> es;
seq::deps_to_lits(lc.m_dep, eqs, lits, es);
for (auto const& e : es)
lits.push_back(mk_literal(e));
set_propagate(eqs, lits, lit);
@ -1752,12 +1743,12 @@ namespace smt {
enode_pair_vector eqs;
literal_vector dep_lits;
vector<seq::le> dep_les;
vector<expr_ref> dep_exprs;
for (unsigned idx : mem_indices)
seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_les);
seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_exprs);
for (auto const &d : dep_les)
dep_lits.push_back(mk_le_literal(d));
for (auto const &e : dep_exprs)
dep_lits.push_back(mk_literal(e));
set_propagate(eqs, dep_lits, lit_prop);

1
src/smt/theory_nseq.h
View file

@ -151,7 +151,6 @@ namespace smt {
bool propagate_length_lemma(literal lit, seq::length_constraint const& lc);
bool assert_nonneg_for_all_vars();
bool assert_length_constraints();
literal mk_le_literal(seq::le const &le);
// Regex membership pre-check: for each variable with regex constraints,
// check intersection emptiness before running DFS.