mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +00:00
Code Activity

Bug fixes

Browse source
This commit is contained in:
CEisenhofer 2026-04-02 10:26:36 +02:00
parent 4c463ad813
commit 1e567a4a26
2 changed files with 24 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -250,9 +250,8 @@ namespace seq {
bool nielsen_node::add_constraint(constraint const &c) { bool nielsen_node::add_constraint(constraint const &c) {
if (graph().get_manager().is_and(c.fml)) { if (graph().get_manager().is_and(c.fml)) {
for (auto f : *to_app(c.fml)) { for (const auto f : *to_app(c.fml)) {
if (!add_constraint(constraint(f, c.dep, graph().get_manager()))) add_constraint(constraint(f, c.dep, graph().get_manager()));
return false;
} }
return true; return true;
} }
@ -1432,6 +1431,9 @@ namespace seq {
generate_node_length_constraints(node); generate_node_length_constraints(node);
assert_node_new_int_constraints(node); assert_node_new_int_constraints(node);
if (node->is_currently_conflict())
return search_result::unsat;
// integer feasibility check: the solver now holds all path constraints // integer feasibility check: the solver now holds all path constraints
// incrementally; just query the solver directly // incrementally; just query the solver directly
if (!cur_path.empty() && !check_int_feasibility()) { if (!cur_path.empty() && !check_int_feasibility()) {
@ -1443,6 +1445,7 @@ namespace seq {
} }
SASSERT(sr != simplify_result::satisfied || node->is_satisfied()); SASSERT(sr != simplify_result::satisfied || node->is_satisfied());
SASSERT(!node->is_currently_conflict());
if (node->is_satisfied()) { if (node->is_satisfied()) {
// Before declaring SAT, check leaf-node regex feasibility: // Before declaring SAT, check leaf-node regex feasibility:
@ -1464,6 +1467,8 @@ namespace seq {
if (depth >= m_depth_bound) if (depth >= m_depth_bound)
return search_result::unknown; return search_result::unknown;
SASSERT(!node->is_currently_conflict());
// generate extensions only once per node; children persist across runs // generate extensions only once per node; children persist across runs
if (!node->is_extended()) { if (!node->is_extended()) {
bool ext = generate_extensions(node); bool ext = generate_extensions(node);
@ -1474,6 +1479,8 @@ namespace seq {
++m_stats.m_num_extensions; ++m_stats.m_num_extensions;
} }
SASSERT(!node->is_currently_conflict());
// explore children // explore children
bool any_unknown = false; bool any_unknown = false;
for (nielsen_edge *e : node->outgoing()) { for (nielsen_edge *e : node->outgoing()) {
@ -1493,8 +1500,7 @@ namespace seq {
e->set_len_constraints_computed(true); e->set_len_constraints_computed(true);
for (const auto& sc : e->side_constraints()) { for (const auto& sc : e->side_constraints()) {
if (!e->tgt()->add_constraint(sc)) e->tgt()->add_constraint(sc);
return search_result::unsat;
} }
} }
@ -1556,12 +1562,10 @@ namespace seq {
while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) { while (prefix < lhs_toks.size() && prefix < rhs_toks.size()) {
euf::snode* lt = lhs_toks[prefix]; euf::snode* lt = lhs_toks[prefix];
euf::snode* rt = rhs_toks[prefix]; euf::snode* rt = rhs_toks[prefix];
if (m.are_equal(lt->get_expr(), rt->get_expr())) { if (m.are_equal(lt->get_expr(), rt->get_expr()))
++prefix; ++prefix;
} else if (m_sg.are_unit_distinct(lt, rt))
else if (m_sg.are_unit_distinct(lt, rt)) {
break; break;
}
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) { else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true); nielsen_edge* e = mk_edge(node, child, true);
@ -1579,6 +1583,8 @@ namespace seq {
eqs[eq_idx] = eqs.back(); eqs[eq_idx] = eqs.back();
eqs.pop_back(); eqs.pop_back();
if (lt->is_char())
std::swap(lt, rt);
nielsen_subst subst(lt, rt, eq.m_dep); nielsen_subst subst(lt, rt, eq.m_dep);
e->add_subst(subst); e->add_subst(subst);
child->apply_subst(m_sg, subst); child->apply_subst(m_sg, subst);
@ -1597,12 +1603,10 @@ namespace seq {
while (suffix < lsz - prefix && suffix < rsz - prefix) { while (suffix < lsz - prefix && suffix < rsz - prefix) {
euf::snode* lt = lhs_toks[lsz - 1 - suffix]; euf::snode* lt = lhs_toks[lsz - 1 - suffix];
euf::snode* rt = rhs_toks[rsz - 1 - suffix]; euf::snode* rt = rhs_toks[rsz - 1 - suffix];
if (m.are_equal(lt->get_expr(), rt->get_expr())) { if (m.are_equal(lt->get_expr(), rt->get_expr()))
++suffix; ++suffix;
} else if (m_sg.are_unit_distinct(lt, rt))
else if (m_sg.are_unit_distinct(lt, rt)) {
break; break;
}
else if (lt->is_char_or_unit() && rt->is_char_or_unit()) { else if (lt->is_char_or_unit() && rt->is_char_or_unit()) {
nielsen_node* child = mk_child(node); nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true); nielsen_edge* e = mk_edge(node, child, true);
@ -1614,6 +1618,8 @@ namespace seq {
eqs[eq_idx] = eqs.back(); eqs[eq_idx] = eqs.back();
eqs.pop_back(); eqs.pop_back();
if (lt->is_char())
std::swap(lt, rt);
nielsen_subst subst(lt, rt, eq.m_dep); nielsen_subst subst(lt, rt, eq.m_dep);
e->add_subst(subst); e->add_subst(subst);
child->apply_subst(m_sg, subst); child->apply_subst(m_sg, subst);

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

@ -646,17 +646,16 @@ namespace seq {
} }
void set_conflict(const backtrack_reason r, const dep_tracker confl) { void set_conflict(const backtrack_reason r, const dep_tracker confl) {
SASSERT(m_reason == backtrack_reason::unevaluated); if (m_conflict_internal != nullptr)
SASSERT(!m_conflict_internal); return;
SASSERT(m_conflict_external_literal == sat::null_literal); // We prefer internal conflicts (we need it as a justification for general conflicts)
m_reason = r; m_reason = r;
m_conflict_internal = confl; m_conflict_internal = confl;
} }
void set_external_conflict(sat::literal lit) { void set_external_conflict(sat::literal lit) {
SASSERT(m_reason == backtrack_reason::unevaluated); if (m_reason != backtrack_reason::unevaluated)
SASSERT(!m_conflict_internal); return;
SASSERT(m_conflict_external_literal == sat::null_literal);
m_reason = backtrack_reason::external; m_reason = backtrack_reason::external;
m_conflict_external_literal = ~lit; m_conflict_external_literal = ~lit;
} }