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

fix tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-22 10:54:00 -07:00
parent 3873f387be
commit 5f7e14315d
5 changed files with 26 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/smt/theory_nseq.cpp
View file

@ -443,8 +443,7 @@ namespace smt {
void theory_nseq::propagate_pos_mem(tracked_str_mem const& mem) {
if (!mem.m_str || !mem.m_regex)
return;
SASSERT(mem.well_formed());
// regex is ∅ → conflict
if (m_regex.is_empty_regex(mem.m_regex)) {
@ -1380,7 +1379,7 @@ namespace smt {
for (unsigned i = 0; i < mems.size(); ++i) {
auto const& mem = *mems[i];
SASSERT(mem.m_str && mem.m_regex);
SASSERT(mem.well_formed());
if (mem.is_primitive()) {
auto& vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector());
vec.push_back(i);
@ -1393,21 +1392,18 @@ namespace smt {
return l_undef;
// Check if there are any eq items in the queue (needed for SAT condition below).
bool has_eqs = false;
for (auto const& item : m_prop_queue)
if (std::holds_alternative<eq_item>(item)) { has_eqs = true; break; }
bool has_eqs = any_of(m_prop_queue, [](auto p) { return std::holds_alternative<eq_item>(p); });
bool any_undef = false;
// Check intersection emptiness for each variable.
for (auto& kv : var_to_mems) {
unsigned var_id = kv.m_key;
unsigned_vector const& mem_indices = kv.m_value;
for (auto &[var_id, mem_indices] : var_to_mems) {
ptr_vector<euf::snode> regexes;
for (unsigned i : mem_indices) {
euf::snode* re = mems[i]->m_regex;
if (re)
regexes.push_back(re);
SASSERT(re);
regexes.push_back(re);
}
if (regexes.empty())
continue;
@ -1463,7 +1459,8 @@ namespace smt {
u_map<unsigned_vector> var_to_mems;
for (unsigned i = 0; i < mems.size(); ++i) {
auto const &mem = mems[i];
if (mem.is_primitive() && mem.m_str) {
SASSERT(mem.well_formed());
if (mem.is_primitive()) {
auto &vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector());
vec.push_back(i);
}
@ -1494,10 +1491,9 @@ namespace smt {
unsigned_vector const &mem_indices = var_to_mems[var_id];
ptr_vector<euf::snode> regexes;
for (const unsigned i : mem_indices) {
euf::snode *re = mems[i].m_regex;
if (re)
regexes.push_back(re);
for (auto i : mem_indices) {
SASSERT(mems[i].well_formed());
regexes.push_back(mems[i].m_regex);
}
SASSERT(!regexes.empty());

3
src/test/euf_seq_plugin.cpp
View file

@ -46,14 +46,12 @@ static void test_sgraph_basic() {
SASSERT(sx->is_var());
SASSERT(!sx->is_ground());
SASSERT(sx->is_regex_free());
SASSERT(!sx->is_nullable());
SASSERT(sx->length() == 1);
euf::snode* se = sg.mk(empty);
SASSERT(se);
SASSERT(se->is_empty());
SASSERT(se->is_ground());
SASSERT(se->is_nullable());
SASSERT(se->length() == 0);
euf::snode* sxy = sg.mk(xy);
@ -172,7 +170,6 @@ static void test_seq_plugin_star_merge() {
sg.mk(star_star);
euf::snode* s = sg.find(star_x);
SASSERT(s && s->is_star());
SASSERT(s->is_nullable());
std::cout << g << "\n";
}

16
src/test/euf_sgraph.cpp
View file

@ -38,7 +38,6 @@ static void test_sgraph_classify() {
SASSERT(sx && sx->is_var());
SASSERT(!sx->is_ground());
SASSERT(sx->is_regex_free());
SASSERT(!sx->is_nullable());
SASSERT(sx->level() == 1);
SASSERT(sx->length() == 1);
SASSERT(sx->is_token());
@ -48,7 +47,6 @@ static void test_sgraph_classify() {
euf::snode* se = sg.mk(empty);
SASSERT(se && se->is_empty());
SASSERT(se->is_ground());
SASSERT(se->is_nullable());
SASSERT(se->level() == 0);
SASSERT(se->length() == 0);
SASSERT(!se->is_token());
@ -59,7 +57,6 @@ static void test_sgraph_classify() {
euf::snode* sca = sg.mk(unit_a);
SASSERT(sca && sca->is_char());
SASSERT(sca->is_ground());
SASSERT(!sca->is_nullable());
SASSERT(sca->level() == 1);
SASSERT(sca->length() == 1);
SASSERT(sca->is_token());
@ -71,7 +68,6 @@ static void test_sgraph_classify() {
SASSERT(sxy && sxy->is_concat());
SASSERT(!sxy->is_ground());
SASSERT(sxy->is_regex_free());
SASSERT(!sxy->is_nullable());
SASSERT(sxy->level() == 2);
SASSERT(sxy->length() == 2);
SASSERT(sxy->num_args() == 2);
@ -98,7 +94,6 @@ static void test_sgraph_regex() {
euf::snode* str = sg.mk(to_re_x);
SASSERT(str && str->is_to_re());
SASSERT(!str->is_regex_free());
SASSERT(!str->is_nullable()); // to_re(x) nullable iff x nullable, x is var so not nullable
SASSERT(str->num_args() == 1);
// star
@ -106,7 +101,6 @@ static void test_sgraph_regex() {
euf::snode* ss = sg.mk(star_x);
SASSERT(ss && ss->is_star());
SASSERT(!ss->is_regex_free());
SASSERT(ss->is_nullable()); // star is always nullable
SASSERT(ss->num_args() == 1);
// full_seq (.*)
@ -114,39 +108,33 @@ static void test_sgraph_regex() {
euf::snode* sfs = sg.mk(full_seq);
SASSERT(sfs && sfs->is_full_seq());
SASSERT(sfs->is_ground());
SASSERT(sfs->is_nullable());
// full_char (.)
expr_ref full_char(seq.re.mk_full_char(str_sort), m);
euf::snode* sfc = sg.mk(full_char);
SASSERT(sfc && sfc->is_full_char());
SASSERT(sfc->is_ground());
SASSERT(!sfc->is_nullable());
// empty set, fail
sort_ref re_sort(seq.re.mk_re(str_sort), m);
expr_ref empty_set(seq.re.mk_empty(re_sort), m);
euf::snode* sfail = sg.mk(empty_set);
SASSERT(sfail && sfail->is_fail());
SASSERT(!sfail->is_nullable());
// union: to_re(x) | star(to_re(x)), nullable because star is
expr_ref re_union(seq.re.mk_union(to_re_x, star_x), m);
euf::snode* su = sg.mk(re_union);
SASSERT(su && su->is_union());
SASSERT(su->is_nullable()); // star_x is nullable
// intersection: to_re(x) & star(to_re(x)), nullable only if both are
expr_ref re_inter(seq.re.mk_inter(to_re_x, star_x), m);
euf::snode* si = sg.mk(re_inter);
SASSERT(si && si->is_intersect());
SASSERT(!si->is_nullable()); // to_re(x) is not nullable
// complement of to_re(x): nullable because to_re(x) is not nullable
expr_ref re_comp(seq.re.mk_complement(to_re_x), m);
euf::snode* sc = sg.mk(re_comp);
SASSERT(sc && sc->is_complement());
SASSERT(sc->is_nullable()); // complement of non-nullable is nullable
// in_re
expr_ref in_re(seq.re.mk_in_re(x, star_x), m);
@ -176,7 +164,6 @@ static void test_sgraph_power() {
SASSERT(sp && sp->is_power());
SASSERT(!sp->is_ground()); // base x is not ground
SASSERT(sp->is_regex_free());
SASSERT(!sp->is_nullable()); // base x is not nullable
SASSERT(sp->num_args() >= 1);
sg.display(std::cout);
@ -400,14 +387,12 @@ static void test_sgraph_concat_metadata() {
euf::snode* sxz = sg.mk(xz);
SASSERT(!sxz->is_ground());
SASSERT(sxz->is_regex_free());
SASSERT(!sxz->is_nullable());
SASSERT(sxz->length() == 2);
SASSERT(sxz->level() == 2);
// concat(empty, empty): nullable (both empty)
expr_ref empty2(seq.str.mk_concat(empty, empty), m);
euf::snode* see = sg.mk(empty2);
SASSERT(see->is_nullable());
SASSERT(see->is_ground());
SASSERT(see->length() == 0);
@ -466,7 +451,6 @@ static void test_sgraph_factory() {
// mk_empty
euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
SASSERT(e && e->is_empty());
SASSERT(e->is_nullable());
SASSERT(e->length() == 0);
// mk_concat with empty absorption

19
src/test/seq_nielsen.cpp
View file

@ -127,7 +127,7 @@ static void test_str_mem() {
euf::snode* regex = sg.mk(star_fc);
seq::dep_tracker dep = nullptr;
seq::str_mem mem(x, regex, e, 0, dep);
seq::str_mem mem(x, regex, dep);
// x in regex is primitive (x is a single variable)
SASSERT(mem.is_primitive());
@ -136,7 +136,7 @@ static void test_str_mem() {
// concatenation is not primitive
euf::snode* a = sg.mk_char('A');
euf::snode* xa = sg.mk_concat(x, a);
seq::str_mem mem2(xa, regex, e, 1, dep);
seq::str_mem mem2(xa, regex, dep);
SASSERT(!mem2.is_primitive());
SASSERT(mem2.contains_var(x));
}
@ -280,7 +280,6 @@ static void test_nielsen_graph_populate() {
euf::snode* regex = sg.mk(re_all);
ng.add_str_mem(x, regex);
SASSERT(ng.root()->str_mems().size() == 1);
SASSERT(ng.root()->str_mems()[0].m_id == 0);
// add another equality: concat(x, A) = concat(A, y)
euf::snode* xa = sg.mk_concat(x, a);
@ -456,8 +455,6 @@ static void test_multiple_memberships() {
SASSERT(ng.root() != nullptr);
SASSERT(ng.root()->str_mems().size() == 2);
SASSERT(ng.root()->str_mems()[0].m_id == 0);
SASSERT(ng.root()->str_mems()[1].m_id == 1);
ng.display(std::cout);
}
@ -1866,7 +1863,7 @@ static void test_simplify_regex_infeasible() {
// ε ∈ to_re("A") → non-nullable → conflict
seq::nielsen_node* node = ng.mk_node();
seq::dep_tracker dep = nullptr;
node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
node->add_str_mem(seq::str_mem(e, regex, dep));
auto sr = node->simplify_and_init({});
SASSERT(sr == seq::simplify_result::conflict);
@ -1922,7 +1919,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 = nullptr;
node->add_str_mem(seq::str_mem(a, regex, e, 0, dep));
node->add_str_mem(seq::str_mem(a, regex, dep));
auto sr = node->simplify_and_init({});
SASSERT(sr == seq::simplify_result::satisfied);
@ -1954,7 +1951,7 @@ static void test_simplify_brzozowski_rtl_suffix() {
// x·"A" ∈ to_re("BA") → RTL consume trailing 'A' → x ∈ to_re("B")
seq::nielsen_node* node = ng.mk_node();
seq::dep_tracker dep = nullptr;
node->add_str_mem(seq::str_mem(xa, regex, e, 0, dep));
node->add_str_mem(seq::str_mem(xa, regex, dep));
auto sr = node->simplify_and_init({});
SASSERT(sr == seq::simplify_result::proceed);
@ -3294,7 +3291,8 @@ static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::sno
static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {
rational lb;
if (!node->lower_bound(var->get_expr(), lb))
seq::dep_tracker d = nullptr;
if (!node->lower_bound(var->get_expr(), lb, d))
return 0;
SASSERT(lb.is_unsigned());
return lb.is_unsigned() ? lb.get_unsigned() : 0;
@ -3302,7 +3300,8 @@ static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {
static unsigned queried_ub(seq::nielsen_node* node, euf::snode* var) {
rational ub;
if (!node->upper_bound(var->get_expr(), ub))
seq::dep_tracker d = nullptr;
if (!node->upper_bound(var->get_expr(), ub, d))
return UINT_MAX;
SASSERT(ub.is_unsigned());
return ub.is_unsigned() ? ub.get_unsigned() : UINT_MAX;

10
src/test/seq_parikh.cpp
View file

@ -324,7 +324,7 @@ static void test_generate_constraints_ab_star() {
seq::dep_manager dm;
sat::literal lit = sat::null_literal; // dummy literal for dependency tracking
seq::dep_tracker dep = dm.mk_leaf(lit);
seq::str_mem mem(x, regex, nullptr, 0, dep);
seq::str_mem mem(x, regex, dep);
vector<seq::constraint> out;
parikh.generate_parikh_constraints(mem, out);
@ -371,7 +371,7 @@ static void test_generate_constraints_bounded_loop() {
euf::snode* regex = sg.mk(re);
seq::dep_manager dm;
seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
seq::str_mem mem(x, regex, nullptr, 0, dep);
seq::str_mem mem(x, regex, dep);
vector<seq::constraint> out;
parikh.generate_parikh_constraints(mem, out);
@ -408,7 +408,7 @@ static void test_generate_constraints_stride_one() {
euf::snode* regex = sg.mk(re);
seq::dep_manager dm;
seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
seq::str_mem mem(x, regex, nullptr, 0, dep);
seq::str_mem mem(x, regex, dep);
vector<seq::constraint> out;
parikh.generate_parikh_constraints(mem, out);
@ -431,7 +431,7 @@ static void test_generate_constraints_fixed_length() {
euf::snode* regex = sg.mk(re);
seq::dep_manager dm;
seq::dep_tracker dep = dm.mk_leaf(sat::null_literal);
seq::str_mem mem(x, regex, nullptr, 0, dep);
seq::str_mem mem(x, regex, dep);
vector<seq::constraint> out;
parikh.generate_parikh_constraints(mem, out);
@ -455,7 +455,7 @@ static void test_generate_constraints_dep_propagated() {
seq::dep_manager dm;
sat::literal lit(7);
seq::dep_tracker dep = dm.mk_leaf(lit);
seq::str_mem mem(x, regex, nullptr, 0, dep);
seq::str_mem mem(x, regex, dep);
vector<seq::constraint> out;
parikh.generate_parikh_constraints(mem, out);