mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 13:56:08 +00:00
Code Activity

Detect that adding side constraint caused a conflict

Browse source
This commit is contained in:
CEisenhofer 2026-04-01 20:38:15 +02:00
parent 4524ebe614
commit 42f421ee09
2 changed files with 14 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -248,18 +248,23 @@ namespace seq {
return false; return false;
} }
void 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 (auto f : *to_app(c.fml)) {
add_constraint(constraint(f, c.dep, graph().get_manager())); if (!add_constraint(constraint(f, c.dep, graph().get_manager())))
return; return false;
}
return true;
} }
m_constraints.push_back(c); m_constraints.push_back(c);
if (m_graph.m_literal_if_false) { if (m_graph.m_literal_if_false) {
auto lit = m_graph.m_literal_if_false(c.fml); auto lit = m_graph.m_literal_if_false(c.fml);
if (lit != sat::null_literal) if (lit != sat::null_literal) {
set_external_conflict(lit); set_external_conflict(lit);
return false;
}
} }
return true;
} }
void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@ -1322,7 +1327,7 @@ namespace seq {
inc_run_idx(); inc_run_idx();
ptr_vector<nielsen_edge> cur_path; ptr_vector<nielsen_edge> cur_path;
// scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search
search_result r = search_dfs(m_root, cur_path); const search_result r = search_dfs(m_root, cur_path);
IF_VERBOSE(1, verbose_stream() IF_VERBOSE(1, verbose_stream()
<< " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes << " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes
<< " max_depth=" << m_stats.m_max_depth << " extensions=" << m_stats.m_num_extensions << " max_depth=" << m_stats.m_max_depth << " extensions=" << m_stats.m_num_extensions
@ -1488,7 +1493,8 @@ 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()) {
e->tgt()->add_constraint(sc); if (!e->tgt()->add_constraint(sc))
return search_result::unsat;
} }
} }

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

@ -585,7 +585,7 @@ namespace seq {
void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); } void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); }
void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); } void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); }
void add_constraint(constraint const &ic); bool add_constraint(constraint const &ic);
vector<constraint> const& constraints() const { return m_constraints; } vector<constraint> const& constraints() const { return m_constraints; }
vector<constraint>& constraints() { return m_constraints; } vector<constraint>& constraints() { return m_constraints; }