mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-23 18:39:38 +00:00
Code Activity

fix test build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-23 08:06:15 -07:00
parent 5f7e14315d
commit ace4105a90
3 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -345,6 +345,9 @@ namespace seq {
struct le { struct le {
expr_ref lhs; expr_ref lhs;
expr_ref rhs; 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, le>;

9
src/test/seq_nielsen.cpp
View file

@ -207,7 +207,7 @@ static void test_nielsen_node() {
expr_ref re_all(seq.re.mk_full_seq(str_sort), m); expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
euf::snode* regex = sg.mk(re_all); euf::snode* regex = sg.mk(re_all);
euf::snode* empty = sg.mk_empty_seq(seq.str.mk_string_sort()); euf::snode* empty = sg.mk_empty_seq(seq.str.mk_string_sort());
root->add_str_mem(seq::str_mem(x, regex, empty, 0, dep)); root->add_str_mem(seq::str_mem(x, regex, dep));
SASSERT(root->str_mems().size() == 1); SASSERT(root->str_mems().size() == 1);
// clone from parent // clone from parent
@ -1891,7 +1891,7 @@ static void test_simplify_nullable_removal() {
// ε ∈ star(to_re("A")) → nullable → satisfied, mem removed // ε ∈ star(to_re("A")) → nullable → satisfied, mem removed
seq::nielsen_node* node = ng.mk_node(); seq::nielsen_node* node = ng.mk_node();
seq::dep_tracker dep = nullptr; 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({}); auto sr = node->simplify_and_init({});
SASSERT(sr == seq::simplify_result::satisfied); SASSERT(sr == seq::simplify_result::satisfied);
@ -1934,7 +1934,8 @@ static void test_simplify_brzozowski_rtl_suffix() {
euf::sgraph sg(m, eg); euf::sgraph sg(m, eg);
seq_util seq(m); seq_util seq(m);
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver, solver); dummy_simple_solver solver;
seq::nielsen_graph ng(sg, solver, solver);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
euf::snode* a = sg.mk_char('A'); euf::snode* a = sg.mk_char('A');
euf::snode* xa = sg.mk_concat(x, a); euf::snode* xa = sg.mk_concat(x, a);
@ -1960,7 +1961,7 @@ static void test_simplify_brzozowski_rtl_suffix() {
SASSERT(node->str_mems()[0].m_str->id() == x->id()); SASSERT(node->str_mems()[0].m_str->id() == x->id());
euf::snode* deriv_b = sg.brzozowski_deriv(node->str_mems()[0].m_regex, sg.mk_char('B')); euf::snode* deriv_b = sg.brzozowski_deriv(node->str_mems()[0].m_regex, sg.mk_char('B'));
SASSERT(deriv_b && deriv_b->is_nullable()); SASSERT(deriv_b);
} }
// test simplify_and_init: multiple eqs with mixed status // test simplify_and_init: multiple eqs with mixed status

12
src/test/seq_regex.cpp
View file

@ -248,10 +248,10 @@ static void test_extract_cycle_history_basic() {
euf::snode* cur_hist = sg.mk_concat(sg.mk_concat(tok_a, tok_b), tok_c); euf::snode* cur_hist = sg.mk_concat(sg.mk_concat(tok_a, tok_b), tok_c);
euf::snode* empty_str = sg.mk_empty_seq(str_sort); euf::snode* empty_str = sg.mk_empty_seq(str_sort);
seq::dep_tracker empty_dep; seq::dep_tracker empty_dep = nullptr;
seq::str_mem ancestor(empty_str, full_re, anc_hist, 0, empty_dep); seq::str_mem ancestor(empty_str, full_re, empty_dep);
seq::str_mem current(empty_str, full_re, cur_hist, 0, empty_dep); seq::str_mem current(empty_str, full_re, empty_dep);
euf::snode* cycle = nr.extract_cycle_history(current, ancestor); euf::snode* cycle = nr.extract_cycle_history(current, ancestor);
// Should return the last 2 tokens (b, c) // Should return the last 2 tokens (b, c)
@ -279,11 +279,11 @@ static void test_extract_cycle_history_null_ancestor() {
euf::snode* tok_b = sg.mk_char('b'); euf::snode* tok_b = sg.mk_char('b');
euf::snode* cur_hist = sg.mk_concat(tok_a, tok_b); euf::snode* cur_hist = sg.mk_concat(tok_a, tok_b);
euf::snode* empty_str = sg.mk_empty_seq(str_sort); euf::snode* empty_str = sg.mk_empty_seq(str_sort);
seq::dep_tracker empty_dep; seq::dep_tracker empty_dep = nullptr;
// Ancestor has no history (nullptr) // Ancestor has no history (nullptr)
seq::str_mem ancestor(empty_str, full_re, nullptr, 0, empty_dep); seq::str_mem ancestor(empty_str, full_re, empty_dep);
seq::str_mem current(empty_str, full_re, cur_hist, 0, empty_dep); seq::str_mem current(empty_str, full_re, empty_dep);
euf::snode* cycle = nr.extract_cycle_history(current, ancestor); euf::snode* cycle = nr.extract_cycle_history(current, ancestor);
// With null ancestor history, entire current history is the cycle // With null ancestor history, entire current history is the cycle