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

Don't use enodes for justifying disequality conflicts

Browse source
This commit is contained in:
CEisenhofer 2026-06-09 15:40:28 +02:00
parent 3c39fc4238
commit 069068ce5e
5 changed files with 65 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,6 +35,7 @@ NSB review:
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/seq_skolem.h"
#include "ast/rewriter/var_subst.h"
#include "smt/smt_enode.h"
#include "util/statistics.h"
#include <algorithm>
#include <complex>
@ -442,18 +443,10 @@ namespace seq {
// nielsen_graph
// -----------------------------------------------
nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i& ctx_solver):
m(sg.get_manager()),
a(sg.get_manager()),
m_seq(sg.get_seq_util()),
m_sg(sg),
m_rw(m),
m_sk(m, m_rw),
m_length_solver(solver),
m_context_solver(ctx_solver),
m_partial_dfa_pin(sg.get_manager()),
m_parikh(alloc(seq_parikh, sg)),
m_seq_regex(alloc(seq::seq_regex, sg)) {
nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver)
: m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_sk(m, m_rw),
m_length_solver(solver), m_context_solver(ctx_solver), m_partial_dfa_pin(sg.get_manager()),
m_parikh(alloc(seq_parikh, sg)), m_seq_regex(alloc(seq::seq_regex, sg)) {
// Answer projection-state membership queries during projection-aware
// derivatives (the sgraph cannot reach the partial DFA otherwise).
m_sg.set_projection_oracle(this);
@ -466,14 +459,14 @@ namespace seq {
reset();
}
bool nielsen_graph::projection_state_in_Q(expr* state, unsigned nu) {
bool nielsen_graph::projection_state_in_Q(expr *state, unsigned nu) {
if (!state || nu == 0)
return false;
const unsigned sid = state->get_id();
// r ∈ Q_nu iff r is incident to a partial-DFA edge whose extraction
// index lies in [1, nu] (the "edges marked ≤ ν" subautomaton of the
// implementation-aspects section of the paper).
auto incident = [&](std::unordered_map<unsigned, unsigned_vector> const& adj) {
auto incident = [&](std::unordered_map<unsigned, unsigned_vector> const &adj) {
auto it = adj.find(sid);
if (it == adj.end())
return false;
@ -489,68 +482,58 @@ namespace seq {
return incident(m_partial_dfa_out) || incident(m_partial_dfa_in);
}
euf::snode* nielsen_graph::mk_projection_term(euf::snode* root_re, unsigned nu) {
SASSERT(root_re && root_re->get_expr());
// π_{Q_nu, {root}}(root): current state == accepting state == root.
expr_ref proj = m_sg.mk_re_proj(root_re->get_expr(), root_re->get_expr(), nu);
return m_sg.mk(proj);
}
nielsen_node* nielsen_graph::mk_node() {
nielsen_node *nielsen_graph::mk_node() {
const unsigned id = m_nodes.size();
nielsen_node* n = alloc(nielsen_node, *this, id);
nielsen_node *n = alloc(nielsen_node, *this, id);
m_nodes.push_back(n);
SASSERT(n->id() == m_nodes.size() - 1);
return n;
}
nielsen_node* nielsen_graph::mk_child(nielsen_node* parent) {
nielsen_node* child = mk_node();
nielsen_node *nielsen_graph::mk_child(nielsen_node *parent) {
nielsen_node *child = mk_node();
child->clone_from(*parent);
child->m_parent_ic_count = parent->constraints().size();
return child;
}
nielsen_edge* nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule,
nielsen_edge *nielsen_graph::mk_edge(nielsen_node *src, nielsen_node *tgt, const char *rule,
const bool is_progress) {
SASSERT(src != nullptr);
SASSERT(tgt != nullptr);
nielsen_edge* e = alloc(nielsen_edge, src, tgt, rule, is_progress);
nielsen_edge *e = alloc(nielsen_edge, src, tgt, rule, is_progress);
m_edges.push_back(e);
src->add_outgoing(e);
return e;
}
void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) {
void nielsen_graph::add_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r) const {
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
str_eq eq(lhs, rhs, dep);
eq.sort();
// check if root node contains this equation already
if (std::ranges::any_of(m_root->str_eqs(), [&](const str_eq& e) {
return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs;
}))
if (std::ranges::any_of(m_root->str_eqs(),
[&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; }))
// already present, no need to add again
return;
m_root->add_str_eq(eq);
}
void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) {
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
void nielsen_graph::add_str_deq(euf::snode *lhs, euf::snode *rhs, sat::literal l) const {
const dep_tracker dep = m_dep_mgr.mk_leaf(l);
str_deq deq(lhs, rhs, dep);
// check if root node contains this equation already
if (std::ranges::any_of(m_root->str_deqs(), [&](const str_deq& e) {
return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs;
}))
if (std::ranges::any_of(m_root->str_deqs(),
[&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; }))
// already present, no need to add again
return;
m_root->add_str_deq(deq);
}
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) {
void nielsen_graph::add_str_mem(euf::snode *str, euf::snode *regex, sat::literal l) const {
// check if root node contains this membership constraint already
if (std::ranges::any_of(m_root->str_mems(), [&](const str_mem& e) {
return e.m_regex == regex && e.m_str == str;
}))
if (std::ranges::any_of(m_root->str_mems(),
[&](const str_mem &e) { return e.m_regex == regex && e.m_str == str; }))
// already present, no need to add again
return;
const dep_tracker dep = m_dep_mgr.mk_leaf(l);
@ -558,29 +541,29 @@ namespace seq {
}
// test-friendly overloads (no external dependency tracking)
void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
void nielsen_graph::add_str_eq(euf::snode *lhs, euf::snode *rhs) {
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
str_eq eq(lhs, rhs, dep);
eq.sort();
m_root->add_str_eq(eq);
}
void nielsen_graph::add_str_deq(euf::snode* lhs, euf::snode* rhs) {
void nielsen_graph::add_str_deq(euf::snode *lhs, euf::snode *rhs) {
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
str_deq deq(lhs, rhs, dep);
m_root->add_str_deq(deq);
}
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) {
void nielsen_graph::add_str_mem(euf::snode *str, euf::snode *regex) {
const dep_tracker dep = nullptr;
m_root->add_str_mem(str_mem(str, regex, dep));
}
void nielsen_graph::reset() {
for (nielsen_node* n : m_nodes) {
for (nielsen_node *n : m_nodes) {
dealloc(n);
}
for (nielsen_edge* e : m_edges) {
for (nielsen_edge *e : m_edges) {
dealloc(e);
}
m_nodes.reset();
@ -591,15 +574,15 @@ namespace seq {
m_depth_bound = 0;
m_fresh_cnt = 0;
m_root_constraints_asserted = false;
//m_mod_cnt.reset();
// m_mod_cnt.reset();
m_partial_dfa_edges.reset();
m_partial_dfa_out.clear();
m_partial_dfa_in.clear();
m_partial_dfa_edge_index.clear();
m_partial_dfa_pin.reset();
m_projection_extract_idx = 0;
//m_length_trail.reset();
//m_length_info.reset();
// m_length_trail.reset();
// m_length_info.reset();
m_dep_mgr.reset();
m_length_solver.reset();
SASSERT(m_nodes.empty());
@ -608,7 +591,7 @@ namespace seq {
SASSERT(m_sat_node == nullptr);
}
void nielsen_graph::add_le_dependency(const dep_tracker dep, nielsen_node* n, expr* lhs, expr* rhs) const {
void nielsen_graph::add_le_dependency(const dep_tracker dep, nielsen_node *n, expr *lhs, expr *rhs) const {
SASSERT(lhs);
SASSERT(rhs);
const expr_ref le(a.mk_le(lhs, rhs), m);
@ -618,6 +601,13 @@ namespace seq {
n->add_constraint(constraint(le, dep, m));
}
euf::snode *nielsen_graph::mk_projection_term(euf::snode *root_re, unsigned nu) {
SASSERT(root_re && root_re->get_expr());
// π_{Q_nu, {root}}(root): current state == accepting state == root.
expr_ref proj = m_sg.mk_re_proj(root_re->get_expr(), root_re->get_expr(), nu);
return m_sg.mk(proj);
}
// -----------------------------------------------------------------------
// nielsen_node: simplify_and_init
// -----------------------------------------------------------------------

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

@ -1060,9 +1060,9 @@ namespace seq {
ptr_vector<nielsen_edge> const& sat_path() const { return m_sat_path; }
// add constraints to the root node from external solver
void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r);
void add_str_deq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r);
void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l);
void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) const;
void add_str_deq(euf::snode* lhs, euf::snode* rhs, sat::literal l) const;
void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) const;
// test-friendly overloads (no external dependency tracking)
void add_str_eq(euf::snode* lhs, euf::snode* rhs);

10
src/smt/seq/seq_state.h
View file

@ -29,19 +29,19 @@ namespace smt {
struct tracked_str_eq : seq::str_eq {
enode *m_l, *m_r;
tracked_str_eq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep)
tracked_str_eq(euf::snode *lhs, euf::snode *rhs, enode *l, enode *r, seq::dep_tracker const &dep)
: str_eq(lhs, rhs, dep), m_l(l), m_r(r) {}
};
struct tracked_str_deq : seq::str_deq {
enode *m_l, *m_r;
tracked_str_deq(euf::snode *lhs, euf::snode *rhs, smt::enode *l, smt::enode *r, seq::dep_tracker const &dep)
: str_deq(lhs, rhs, dep), m_l(l), m_r(r) {}
sat::literal lit;
tracked_str_deq(euf::snode *lhs, euf::snode *rhs, const sat::literal lit, seq::dep_tracker const &dep)
: str_deq(lhs, rhs, dep), lit(lit) {}
};
struct tracked_str_mem : seq::str_mem {
sat::literal lit;
tracked_str_mem(euf::snode *str, euf::snode *regex, sat::literal lit, seq::dep_tracker const &dep)
tracked_str_mem(euf::snode *str, euf::snode *regex, const sat::literal lit, seq::dep_tracker const &dep)
: str_mem(str, regex, dep), lit(lit) {}
};

28
src/smt/theory_nseq.cpp
View file

@ -267,9 +267,10 @@ namespace smt {
else {
euf::snode *s1 = get_snode(e1);
euf::snode *s2 = get_snode(e2);
seq::dep_tracker dep = nullptr;
const seq::dep_tracker dep = nullptr;
ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(deq_item(s1, s2, get_enode(v1), get_enode(v2), dep));
expr_ref eq_expr(m.mk_not(m.mk_eq(e1, e2)), m);
m_prop_queue.push_back(deq_item(s1, s2, ctx.get_literal(eq_expr), dep));
m_last_constraint_added = ctx.get_scope_level();
m_can_hot_restart = false;
}
@ -437,16 +438,16 @@ namespace smt {
}
}
void theory_nseq::propagate_eq(tracked_str_eq const& eq) {
void theory_nseq::propagate_eq(tracked_str_eq const &eq) const {
// When s1 = s2 is learned, ensure len(s1) and len(s2) are
// internalized so congruence closure propagates len(s1) = len(s2).
ensure_length_var(eq.m_l->get_expr());
ensure_length_var(eq.m_r->get_expr());
}
void theory_nseq::propagate_deq(tracked_str_deq const& eq) {
ensure_length_var(eq.m_l->get_expr());
ensure_length_var(eq.m_r->get_expr());
void theory_nseq::propagate_deq(tracked_str_deq const& eq) const {
ensure_length_var(eq.m_lhs->get_expr());
ensure_length_var(eq.m_rhs->get_expr());
}
void theory_nseq::propagate_pos_mem(tracked_str_mem const& mem) {
@ -706,8 +707,8 @@ namespace smt {
}
if (std::holds_alternative<deq_item>(item)) {
SASSERT(!get_fparams().m_nseq_axiomatize_diseq);
auto const& eq = std::get<deq_item>(item);
m_nielsen.add_str_deq(eq.m_lhs, eq.m_rhs, eq.m_l, eq.m_r);
auto const& deq = std::get<deq_item>(item);
m_nielsen.add_str_deq(deq.m_lhs, deq.m_rhs, deq.lit);
++num_deqs;
}
else if (std::holds_alternative<mem_item>(item)) {
@ -917,9 +918,6 @@ namespace smt {
<< (m_nielsen.sat_node() ? "set" : "null") << "\n");
// Nielsen found a consistent assignment for positive constraints.
SASSERT(has_eq_or_diseq_or_mem); // we should have axiomatized them
bool all_sat = add_nielsen_assumptions();
if (!check_length_coherence())
return FC_CONTINUE;
@ -927,6 +925,9 @@ namespace smt {
return FC_CONTINUE;
CTRACE(seq, !has_unhandled_preds(), display(tout << "done\n"));
bool all_sat = add_nielsen_assumptions();
if (!all_sat)
return FC_CONTINUE;
@ -1149,7 +1150,10 @@ namespace smt {
for (auto [a, b] : eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";
);
SASSERT(all_of(eqs, [&](auto eq) { return eq.first->get_root() == eq.second->get_root(); }));
for (auto& eq : eqs) {
std::cout << mk_pp(eq.first->get_expr(), m) << " == " << mk_pp(eq.second->get_expr(), m) << std::endl;
SASSERT(eq.first->get_root() == eq.second->get_root());
};
bool all_true = all_of(lits, [&](auto lit) { return ctx.get_assignment(lit) == l_true; });

4
src/smt/theory_nseq.h
View file

@ -150,8 +150,8 @@ namespace smt {
euf::snode* get_snode(expr* e);
// propagation dispatch helpers
void propagate_eq(tracked_str_eq const& eq);
void propagate_deq(tracked_str_deq const& deq);
void propagate_eq(tracked_str_eq const& eq) const;
void propagate_deq(tracked_str_deq const& deq) const;
void propagate_pos_mem(tracked_str_mem const& mem);
void enqueue_axiom(expr* e);
void dequeue_axiom(expr* e);