mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

Deleted leftover code from subsumption

Browse source
This commit is contained in:
CEisenhofer 2026-03-04 17:42:14 +01:00
parent e4787e57f6
commit 4e7d83f996
2 changed files with 0 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -505,26 +505,6 @@ namespace seq {
return m_str_mem.empty();
}
bool nielsen_node::is_subsumed_by(nielsen_node const& other) const {
// check if every non-trivial constraint in 'other' also appears in 'this'.
// trivial str_eqs (both sides empty/equal) are always satisfied and
// do not affect subsumption.
for (str_eq const& oeq : other.m_str_eq) {
if (oeq.is_trivial()) continue;
bool found = false;
for (str_eq const& teq : m_str_eq)
if (teq == oeq) { found = true; break; }
if (!found) return false;
}
for (str_mem const& omem : other.m_str_mem) {
bool found = false;
for (str_mem const& tmem : m_str_mem)
if (tmem == omem) { found = true; break; }
if (!found) return false;
}
return true;
}
bool nielsen_node::has_opaque_terms() const {
auto is_opaque = [](euf::snode* n) { return n && n->kind() == euf::snode_kind::s_other; };
for (str_eq const& eq : m_str_eq) {
@ -606,21 +586,6 @@ namespace seq {
if (sr == simplify_result::satisfied || node->is_satisfied())
return search_result::sat;
// subsumption pruning: if any previously explored node has a subset
// of our constraints and was found to be a conflict, this node must
// also be a conflict. Mirrors ZIPT's FindExisting() lookup.
for (nielsen_node* other : m_nodes) {
if (other == node) continue;
if (other->eval_idx() != m_run_idx) continue;
if (!other->is_general_conflict()) continue;
if (node->is_subsumed_by(*other)) {
++m_stats.m_num_subsumptions;
node->set_general_conflict(true);
node->set_reason(backtrack_reason::subsumption);
return search_result::unsat;
}
}
// depth bound check
if (depth >= m_depth_bound)
return search_result::unknown;

1
src/smt/theory_nseq.cpp
View file

@ -530,7 +530,6 @@ namespace smt {
st.update("nseq unsat", ns.m_num_unsat);
st.update("nseq unknown", ns.m_num_unknown);
st.update("nseq simplify clash", ns.m_num_simplify_conflict);
st.update("nseq subsumptions", ns.m_num_subsumptions);
st.update("nseq extensions", ns.m_num_extensions);
st.update("nseq fresh vars", ns.m_num_fresh_vars);
st.update("nseq max depth", ns.m_max_depth);