mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Fixed propagation rule

Browse source
This commit is contained in:
CEisenhofer 2026-06-10 17:55:14 +02:00
parent aec52551c3
commit f9f16550e0
3 changed files with 28 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_split.cpp
View file

@ -86,7 +86,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
seq_util::rex& rex = re();
ast_manager& mm = m();
// std::cout << "compute " << mk_pp(r, m()) << std::endl;
// std::cout << "compute sigma of " << mk_pp(r, m()) << std::endl;
sort* seq_sort = nullptr;
if (!sq.is_re(r, seq_sort))
@ -169,18 +169,21 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
expr_ref left(mm), right(mm);
if (i == 0)
left = rex.mk_epsilon(seq_sort);
else
else {
for (unsigned j = 0; j < i; ++j) {
expr* arg = ap->get_arg(j);
left = left ? expr_ref(rex.mk_concat(left, arg), mm) : expr_ref(arg, mm);
}
}
if (i == n - 1)
right = rex.mk_epsilon(seq_sort);
else
for (unsigned j = i + 1; j < n; ++j) {
else {
right = ap->get_arg(i + 1);
for (unsigned j = i + 2; j < n; ++j) {
expr* arg = ap->get_arg(j);
right = right ? expr_ref(rex.mk_concat(right, arg), mm) : expr_ref(arg, mm);
right = rex.mk_concat(right, arg);
}
}
for (auto const& [d, nn] : sigma_arg) {
const expr_ref p = m_rw.mk_re_append(left, d);
@ -282,8 +285,7 @@ bool seq_split::compute(expr* r, split_set& result, unsigned threshold, split_mo
// { <D,N>, <D',N> } -> <D | D', N> (by_left = false, group by N)
// Only fires on syntactically-identical (perfectly-shared) key components, so
// it is a conservative instance of the rule.
void seq_split::merge_by(split_set& pairs, bool by_left) const {
seq_util::rex& r = re();
void seq_split::merge_by(split_set& pairs, const bool by_left) const {
ast_manager& mm = m();
obj_map<expr, unsigned> idx; // key component -> position in `out`
split_set out;

30
src/smt/theory_nseq.cpp
View file

@ -198,6 +198,7 @@ namespace smt {
auto e1 = n1->get_expr();
auto e2 = n2->get_expr();
TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n");
//std::cout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << std::endl;
if (m_seq.is_re(e1)) {
expr_ref s(m);
auto r = m_rewriter.mk_symmetric_diff(e1, e2);
@ -286,14 +287,14 @@ namespace smt {
void theory_nseq::assign_eh(bool_var v, bool is_true) {
try {
expr* e = ctx.bool_var2expr(v);
// std::cout << "assigned [" << sat::literal(v, is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
//std::cout << "assigned [" << sat::literal(v, !is_true) << "] " << mk_pp(e, m) << " = " << is_true << std::endl;
expr *s = nullptr, *re = nullptr, *a = nullptr, *b = nullptr;
TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
if (m_seq.str.is_in_re(e, s, re)) {
euf::snode* sn_str = get_snode(s);
euf::snode* sn_re = get_snode(re);
literal lit(v, !is_true);
seq::dep_tracker dep = nullptr;
const literal lit(v, !is_true);
const seq::dep_tracker dep = nullptr;
if (is_true) {
ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep));
@ -304,7 +305,7 @@ namespace smt {
// ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership
// so the Nielsen graph sees it uniformly; the original negative literal
// is kept in mem_source for conflict reporting.
expr_ref re_compl(m_seq.re.mk_complement(re), m);
const expr_ref re_compl(m_seq.re.mk_complement(re), m);
euf::snode* sn_re_compl = get_snode(re_compl.get());
ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep));
@ -337,9 +338,9 @@ namespace smt {
enode* n1 = ensure_enode(a);
enode* n2 = ensure_enode(b);
if (n1->get_root() != n2->get_root()) {
auto v1 = mk_var(n1);
auto v2 = mk_var(n2);
literal lit(v, false);
const auto v1 = mk_var(n1);
const auto v2 = mk_var(n2);
const literal lit(v, false);
ctx.mark_as_relevant(n1);
ctx.mark_as_relevant(n2);
TRACE(seq, tout << "is-eq " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n");
@ -536,12 +537,11 @@ namespace smt {
zstring str;
const expr_ref arg(to_app(re)->get_arg(0), m);
if (m_seq.str.is_string(arg, str)) {
literal_vector lits;
lits.push_back(~mem.lit);
lits.push_back(mk_literal(m.mk_eq(m_seq.str.mk_string(str), arg)));
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
const expr_ref eq(m.mk_eq(s, arg), m);
ctx.mk_th_axiom(get_id(), ~mem.lit, mk_literal(eq));
m_ignored_mem.insert(mem.lit);
ctx.push_trail(insert_map(m_ignored_mem, mem.lit));
return;
}
}
@ -575,6 +575,11 @@ namespace smt {
// we give up
return;
//std::cout << "Pairs:\n";
//for (auto& pair: pairs) {
// std::cout << mk_pp(pair.m_d, m) << " ; " << mk_pp(pair.m_n, m) << std::endl;
//}
m_rewriter.simplify_split(pairs);
if (pairs.empty()) {
@ -716,6 +721,7 @@ namespace smt {
}
else if (std::holds_alternative<mem_item>(item)) {
auto const& mem = std::get<mem_item>(item);
std::cout << "Adding " << seq::mem_pp(mem, m) << std::endl;
int triv = m_regex.check_trivial(mem);
if (triv > 0) {
++num_mems;
@ -1424,7 +1430,7 @@ namespace smt {
return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int();
}
bool theory_nseq::get_length(expr* e, rational& val) {
bool theory_nseq::get_length(expr* e, rational& val) const {
rational val1;
expr* e1 = nullptr;
expr* e2 = nullptr;

2
src/smt/theory_nseq.h
View file

@ -164,7 +164,7 @@ namespace smt {
bool get_num_value(expr* e, rational& val) const;
bool lower_bound(expr* e, rational& lo) const;
bool upper_bound(expr* e, rational& hi) const;
bool get_length(expr* e, rational& val);
bool get_length(expr* e, rational& val) const;
void add_length_axiom(literal lit);
bool propagate_length_lemma(literal lit, seq::length_constraint const& lc);
bool assert_nonneg_for_all_vars();