mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-01 08:03:45 +00:00
Code Activity

We have to check for local conflicts before clearing the flag

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 11:42:30 +02:00
parent 598e4ede4e
commit 8eb0ac29d9
1 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1304,6 +1304,13 @@ namespace seq {
if (!m.inc()) if (!m.inc())
return search_result::unknown; return search_result::unknown;
#ifdef Z3DEBUG
if (m_stats.m_num_dfs_nodes % 1000 == 0) {
std::string dot = to_dot();
dot = dot;
}
#endif
// check DFS node budget (0 = unlimited) // check DFS node budget (0 = unlimited)
if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes) if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes)
return search_result::unknown; return search_result::unknown;
@ -1332,6 +1339,11 @@ namespace seq {
// that might have been added by an extension step // that might have been added by an extension step
assert_node_new_int_constraints(node); assert_node_new_int_constraints(node);
if (node->is_currently_conflict()) {
++m_stats.m_num_simplify_conflict;
return search_result::unsat;
}
// simplify constraints (idempotent after first call) // simplify constraints (idempotent after first call)
const simplify_result sr = node->simplify_and_init(cur_path); const simplify_result sr = node->simplify_and_init(cur_path);
@ -1363,7 +1375,7 @@ 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_general_conflict()) { if (node->is_currently_conflict()) {
++m_stats.m_num_simplify_conflict; ++m_stats.m_num_simplify_conflict;
return search_result::unsat; return search_result::unsat;
} }
@ -1379,7 +1391,7 @@ namespace seq {
} }
SASSERT(sr != simplify_result::satisfied || node->is_satisfied()); SASSERT(sr != simplify_result::satisfied || node->is_satisfied());
SASSERT(!node->is_general_conflict()); 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:
@ -1397,9 +1409,6 @@ namespace seq {
return search_result::sat; return search_result::sat;
} }
// This is the first time we accept local conflicts
// Before we only abort on global conflicts [we prefer those]
// Also we would leave the node in an "instable" state
if (node->is_currently_conflict()) if (node->is_currently_conflict())
return search_result::unsat; return search_result::unsat;