mirror of
https://github.com/Z3Prover/z3
synced 2026-03-11 15:50:29 +00:00
Replace dep_tracker class in seq_nielsen with uint_set
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
parent
f3018a563e
commit
5330bd20bc
4 changed files with 51 additions and 120 deletions
|
|
@ -23,7 +23,6 @@ Author:
|
|||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "math/lp/lar_solver.h"
|
||||
#include "util/bit_util.h"
|
||||
#include "util/hashtable.h"
|
||||
#include <algorithm>
|
||||
#include <cstdlib>
|
||||
|
|
@ -31,58 +30,6 @@ Author:
|
|||
|
||||
namespace seq {
|
||||
|
||||
// -----------------------------------------------
|
||||
// dep_tracker
|
||||
// -----------------------------------------------
|
||||
|
||||
dep_tracker::dep_tracker(unsigned num_bits) {
|
||||
unsigned words = (num_bits + 31) / 32;
|
||||
m_bits.resize(words, 0);
|
||||
}
|
||||
|
||||
dep_tracker::dep_tracker(unsigned num_bits, unsigned set_bit) : dep_tracker(num_bits) {
|
||||
if (set_bit < num_bits) {
|
||||
unsigned word_idx = set_bit / 32;
|
||||
unsigned bit_idx = set_bit % 32;
|
||||
m_bits[word_idx] = 1u << bit_idx;
|
||||
}
|
||||
}
|
||||
|
||||
void dep_tracker::merge(dep_tracker const& other) {
|
||||
if (other.m_bits.empty())
|
||||
return;
|
||||
if (m_bits.size() < other.m_bits.size())
|
||||
m_bits.resize(other.m_bits.size(), 0);
|
||||
for (unsigned i = 0; i < other.m_bits.size(); ++i)
|
||||
m_bits[i] |= other.m_bits[i];
|
||||
}
|
||||
|
||||
bool dep_tracker::is_superset(dep_tracker const& other) const {
|
||||
for (unsigned i = 0; i < other.m_bits.size(); ++i) {
|
||||
unsigned my_bits = (i < m_bits.size()) ? m_bits[i] : 0;
|
||||
if ((my_bits & other.m_bits[i]) != other.m_bits[i])
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool dep_tracker::empty() const {
|
||||
for (unsigned b : m_bits)
|
||||
if (b != 0) return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
void dep_tracker::get_set_bits(unsigned_vector& indices) const {
|
||||
for (unsigned i = 0; i < m_bits.size(); ++i) {
|
||||
unsigned word = m_bits[i];
|
||||
while (word != 0) {
|
||||
unsigned bit = i * 32 + ntz_core(word);
|
||||
indices.push_back(bit);
|
||||
word &= word - 1; // clear lowest set bit
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// -----------------------------------------------
|
||||
// str_eq
|
||||
// -----------------------------------------------
|
||||
|
|
@ -338,7 +285,7 @@ namespace seq {
|
|||
str_eq& eq = m_str_eq[i];
|
||||
eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement);
|
||||
eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement);
|
||||
eq.m_dep.merge(s.m_dep);
|
||||
eq.m_dep |= s.m_dep;
|
||||
eq.sort();
|
||||
}
|
||||
for (unsigned i = 0; i < m_str_mem.size(); ++i) {
|
||||
|
|
@ -346,7 +293,7 @@ namespace seq {
|
|||
mem.m_str = sg.subst(mem.m_str, s.m_var, s.m_replacement);
|
||||
// regex is typically ground, but apply subst for generality
|
||||
mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement);
|
||||
mem.m_dep.merge(s.m_dep);
|
||||
mem.m_dep |= s.m_dep;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -469,8 +416,8 @@ namespace seq {
|
|||
void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
|
||||
if (!m_root)
|
||||
m_root = mk_node();
|
||||
dep_tracker dep(m_root->str_eqs().size() + m_root->str_mems().size() + 1,
|
||||
m_root->str_eqs().size());
|
||||
dep_tracker dep;
|
||||
dep.insert(m_root->str_eqs().size());
|
||||
str_eq eq(lhs, rhs, dep);
|
||||
eq.sort();
|
||||
m_root->add_str_eq(eq);
|
||||
|
|
@ -480,8 +427,8 @@ namespace seq {
|
|||
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) {
|
||||
if (!m_root)
|
||||
m_root = mk_node();
|
||||
dep_tracker dep(m_root->str_eqs().size() + m_root->str_mems().size() + 1,
|
||||
m_root->str_eqs().size() + m_root->str_mems().size());
|
||||
dep_tracker dep;
|
||||
dep.insert(m_root->str_eqs().size() + m_root->str_mems().size());
|
||||
euf::snode* history = m_sg.mk_empty();
|
||||
unsigned id = next_mem_id();
|
||||
m_root->add_str_mem(str_mem(str, regex, history, id, dep));
|
||||
|
|
@ -2389,9 +2336,9 @@ namespace seq {
|
|||
if (!n->is_currently_conflict())
|
||||
continue;
|
||||
for (str_eq const& eq : n->str_eqs())
|
||||
deps.merge(eq.m_dep);
|
||||
deps |= eq.m_dep;
|
||||
for (str_mem const& mem : n->str_mems())
|
||||
deps.merge(mem.m_dep);
|
||||
deps |= mem.m_dep;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -2399,9 +2346,7 @@ namespace seq {
|
|||
SASSERT(m_root);
|
||||
dep_tracker deps;
|
||||
collect_conflict_deps(deps);
|
||||
unsigned_vector bits;
|
||||
deps.get_set_bits(bits);
|
||||
for (unsigned b : bits) {
|
||||
for (unsigned b : deps) {
|
||||
if (b < m_num_input_eqs)
|
||||
eq_indices.push_back(b);
|
||||
else
|
||||
|
|
|
|||
|
|
@ -98,10 +98,8 @@ Abstract:
|
|||
------------------------------------
|
||||
1. dep_tracker (DependencyTracker): ZIPT's DependencyTracker is a .NET
|
||||
class using a BitArray-like structure for tracking constraint origins.
|
||||
Z3's dep_tracker uses a dense bitvector stored as svector<unsigned>
|
||||
(32-bit words). The merge/is_superset/empty semantics are equivalent,
|
||||
but the representation is more cache-friendly and avoids managed-heap
|
||||
allocation.
|
||||
Z3 uses uint_set (a dense bitvector from util/uint_set.h) for the same
|
||||
purpose. The |=/subset_of/empty semantics are equivalent.
|
||||
|
||||
2. Substitution application (nielsen_node::apply_subst): ZIPT uses an
|
||||
immutable, functional style -- Apply() returns a new constraint if
|
||||
|
|
@ -276,23 +274,7 @@ namespace seq {
|
|||
// dependency tracker: bitvector tracking which input constraints
|
||||
// contributed to deriving a given constraint
|
||||
// mirrors ZIPT's DependencyTracker
|
||||
class dep_tracker {
|
||||
svector<unsigned> m_bits;
|
||||
public:
|
||||
dep_tracker() = default;
|
||||
explicit dep_tracker(unsigned num_bits);
|
||||
dep_tracker(unsigned num_bits, unsigned set_bit);
|
||||
|
||||
void merge(dep_tracker const& other);
|
||||
bool is_superset(dep_tracker const& other) const;
|
||||
bool empty() const;
|
||||
|
||||
// collect indices of all set bits into 'indices'
|
||||
void get_set_bits(unsigned_vector& indices) const;
|
||||
|
||||
bool operator==(dep_tracker const& other) const { return m_bits == other.m_bits; }
|
||||
bool operator!=(dep_tracker const& other) const { return !(*this == other); }
|
||||
};
|
||||
using dep_tracker = uint_set;
|
||||
|
||||
// -----------------------------------------------
|
||||
// character range and set types
|
||||
|
|
|
|||
|
|
@ -450,10 +450,8 @@ namespace smt {
|
|||
|
||||
void theory_nseq::deps_to_lits(seq::dep_tracker const& deps, enode_pair_vector& eqs, literal_vector& lits) {
|
||||
context& ctx = get_context();
|
||||
unsigned_vector bits;
|
||||
deps.get_set_bits(bits);
|
||||
unsigned num_input_eqs = m_nielsen.num_input_eqs();
|
||||
for (unsigned b : bits) {
|
||||
for (unsigned b : deps) {
|
||||
if (b < num_input_eqs) {
|
||||
eq_source const& src = m_state.get_eq_source(b);
|
||||
if (src.m_n1->get_root() == src.m_n2->get_root())
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ Abstract:
|
|||
#include "ast/ast_pp.h"
|
||||
#include <iostream>
|
||||
|
||||
// test dep_tracker basic operations
|
||||
// test dep_tracker (uint_set) basic operations
|
||||
static void test_dep_tracker() {
|
||||
std::cout << "test_dep_tracker\n";
|
||||
|
||||
|
|
@ -31,23 +31,26 @@ static void test_dep_tracker() {
|
|||
SASSERT(d0.empty());
|
||||
|
||||
// tracker with one bit set
|
||||
seq::dep_tracker d1(8, 3);
|
||||
seq::dep_tracker d1;
|
||||
d1.insert(3);
|
||||
SASSERT(!d1.empty());
|
||||
|
||||
// tracker with another bit
|
||||
seq::dep_tracker d2(8, 5);
|
||||
seq::dep_tracker d2;
|
||||
d2.insert(5);
|
||||
SASSERT(!d2.empty());
|
||||
|
||||
// merge
|
||||
seq::dep_tracker d3 = d1;
|
||||
d3.merge(d2);
|
||||
d3 |= d2;
|
||||
SASSERT(!d3.empty());
|
||||
SASSERT(d3.is_superset(d1));
|
||||
SASSERT(d3.is_superset(d2));
|
||||
SASSERT(!d1.is_superset(d2));
|
||||
SASSERT(d1.subset_of(d3));
|
||||
SASSERT(d2.subset_of(d3));
|
||||
SASSERT(!d2.subset_of(d1));
|
||||
|
||||
// equality
|
||||
seq::dep_tracker d4(8, 3);
|
||||
seq::dep_tracker d4;
|
||||
d4.insert(3);
|
||||
SASSERT(d1 == d4);
|
||||
SASSERT(d1 != d2);
|
||||
}
|
||||
|
|
@ -65,7 +68,7 @@ static void test_str_eq() {
|
|||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
|
||||
// basic equality
|
||||
seq::str_eq eq1(x, y, dep);
|
||||
|
|
@ -112,7 +115,7 @@ static void test_str_mem() {
|
|||
expr_ref star_fc(seq.re.mk_full_seq(str_sort), m);
|
||||
euf::snode* regex = sg.mk(star_fc);
|
||||
|
||||
seq::dep_tracker dep(4, 1);
|
||||
seq::dep_tracker dep; dep.insert(1);
|
||||
seq::str_mem mem(x, regex, e, 0, dep);
|
||||
|
||||
// x in regex is primitive (x is a single variable)
|
||||
|
|
@ -1322,37 +1325,40 @@ static void test_solve_conflict_deps() {
|
|||
SASSERT(!deps.empty());
|
||||
}
|
||||
|
||||
// test dep_tracker::get_set_bits
|
||||
// test dep_tracker (uint_set) iteration
|
||||
static void test_dep_tracker_get_set_bits() {
|
||||
std::cout << "test_dep_tracker_get_set_bits\n";
|
||||
|
||||
// empty tracker has no bits
|
||||
seq::dep_tracker d0;
|
||||
unsigned_vector bits0;
|
||||
d0.get_set_bits(bits0);
|
||||
for (unsigned b : d0) bits0.push_back(b);
|
||||
SASSERT(bits0.empty());
|
||||
|
||||
// single bit set at position 5
|
||||
seq::dep_tracker d1(16, 5);
|
||||
seq::dep_tracker d1;
|
||||
d1.insert(5);
|
||||
unsigned_vector bits1;
|
||||
d1.get_set_bits(bits1);
|
||||
for (unsigned b : d1) bits1.push_back(b);
|
||||
SASSERT(bits1.size() == 1);
|
||||
SASSERT(bits1[0] == 5);
|
||||
|
||||
// two bits merged
|
||||
seq::dep_tracker d2(16, 3);
|
||||
d2.merge(seq::dep_tracker(16, 11));
|
||||
seq::dep_tracker d2;
|
||||
d2.insert(3);
|
||||
d2.insert(11);
|
||||
unsigned_vector bits2;
|
||||
d2.get_set_bits(bits2);
|
||||
for (unsigned b : d2) bits2.push_back(b);
|
||||
SASSERT(bits2.size() == 2);
|
||||
SASSERT(bits2[0] == 3);
|
||||
SASSERT(bits2[1] == 11);
|
||||
|
||||
// test across word boundary (bit 31 and 32)
|
||||
seq::dep_tracker d3(64, 31);
|
||||
d3.merge(seq::dep_tracker(64, 32));
|
||||
seq::dep_tracker d3;
|
||||
d3.insert(31);
|
||||
d3.insert(32);
|
||||
unsigned_vector bits3;
|
||||
d3.get_set_bits(bits3);
|
||||
for (unsigned b : d3) bits3.push_back(b);
|
||||
SASSERT(bits3.size() == 2);
|
||||
SASSERT(bits3[0] == 31);
|
||||
SASSERT(bits3[1] == 32);
|
||||
|
|
@ -1543,7 +1549,7 @@ static void test_simplify_prefix_cancel() {
|
|||
euf::snode* aby = sg.mk_concat(a, sg.mk_concat(b, y));
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(abx, aby, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1573,7 +1579,7 @@ static void test_simplify_symbol_clash() {
|
|||
euf::snode* by = sg.mk_concat(b, y);
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(ax, by, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1598,7 +1604,7 @@ static void test_simplify_empty_propagation() {
|
|||
|
||||
// ε = x·y → forces x=ε, y=ε → all trivial → satisfied
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(e, xy, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1619,7 +1625,7 @@ static void test_simplify_empty_vs_char() {
|
|||
|
||||
// ε = A → rhs has non-variable token → conflict
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(e, a, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1645,7 +1651,7 @@ static void test_simplify_multi_pass_clash() {
|
|||
euf::snode* ac = sg.mk_concat(a, c);
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(ab, ac, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1667,7 +1673,7 @@ static void test_simplify_trivial_removal() {
|
|||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(e, e, dep)); // trivial
|
||||
node->add_str_eq(seq::str_eq(x, y, dep)); // non-trivial
|
||||
|
||||
|
|
@ -1689,7 +1695,7 @@ static void test_simplify_all_trivial_satisfied() {
|
|||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_eq(seq::str_eq(x, x, dep)); // trivial: same pointer
|
||||
node->add_str_eq(seq::str_eq(e, e, dep)); // trivial: both empty
|
||||
|
||||
|
|
@ -1716,7 +1722,7 @@ static void test_simplify_regex_infeasible() {
|
|||
|
||||
// ε ∈ to_re("A") → non-nullable → conflict
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1744,7 +1750,7 @@ static void test_simplify_nullable_removal() {
|
|||
|
||||
// ε ∈ star(to_re("A")) → nullable → satisfied, mem removed
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1772,7 +1778,7 @@ static void test_simplify_brzozowski_sat() {
|
|||
|
||||
// "A" ∈ to_re("A") → derivative consumes 'A' → ε ∈ ε-regex → satisfied
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(4, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
node->add_str_mem(seq::str_mem(a, regex, e, 0, dep));
|
||||
|
||||
auto sr = node->simplify_and_init(ng);
|
||||
|
|
@ -1795,7 +1801,7 @@ static void test_simplify_multiple_eqs() {
|
|||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
seq::nielsen_node* node = ng.mk_node();
|
||||
seq::dep_tracker dep(8, 0);
|
||||
seq::dep_tracker dep; dep.insert(0);
|
||||
|
||||
// eq1: ε = ε (trivial → removed)
|
||||
node->add_str_eq(seq::str_eq(e, e, dep));
|
||||
|
|
@ -2234,7 +2240,7 @@ static void test_length_constraints_deps() {
|
|||
for (auto const& c : constraints) {
|
||||
SASSERT(!c.m_dep.empty());
|
||||
unsigned_vector bits;
|
||||
c.m_dep.get_set_bits(bits);
|
||||
for (unsigned b : c.m_dep) bits.push_back(b);
|
||||
SASSERT(bits.size() == 1);
|
||||
SASSERT(bits[0] == 0);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue