diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 73ba8889a..d63597120 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -219,17 +219,11 @@ namespace seq { m_str_eq.reset(); m_str_mem.reset(); m_constraints.reset(); - m_char_diseqs.reset(); m_char_ranges.reset(); m_str_eq.append(parent.m_str_eq); m_str_mem.append(parent.m_str_mem); m_constraints.append(parent.m_constraints); - // clone character disequalities - - for (auto const &[k,v] : parent.m_char_diseqs) - m_char_diseqs.insert(k, v); - // clone character ranges for (auto const &[k, v] : parent.m_char_ranges) m_char_ranges.insert(k, std::make_pair(v.first.clone(), v.second)); @@ -295,12 +289,20 @@ namespace seq { mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep); } } - if (s.is_char_subst()) { - expr* v = s.m_var->get_expr(); - expr* repl = s.m_replacement->get_expr(); - expr* eq = sg.get_manager().mk_eq(v, repl); - add_constraint(constraint(eq, s.m_dep, sg.get_manager())); + const unsigned var_id = s.m_var->id(); + + if (s.is_char_subst()) { + ast_manager& m = graph().get_manager(); + add_constraint( + constraint( + m.mk_eq(s.m_var->get_expr(), s.m_replacement->get_expr()), s.m_dep, m)); + + if (m_char_ranges.contains(var_id)) { + auto range = m_char_ranges.find(var_id); // copy exactly + m_char_ranges.remove(var_id); + add_char_range(s.m_replacement, range.first, range.second); + } } } @@ -320,21 +322,6 @@ namespace seq { m_char_ranges.insert(id, std::make_pair(range.clone(), dep)); } - void nielsen_node::add_char_diseq(euf::snode* sym_char, euf::snode* other, dep_tracker dep) { - SASSERT(sym_char && sym_char->is_unit()); - SASSERT(other && other->is_unit()); - unsigned id = sym_char->id(); - if (!m_char_diseqs.contains(id)) - m_char_diseqs.insert(id, vector>()); - vector>& existing = m_char_diseqs.find(id); - // check for duplicates - for (auto& s : existing) { - if (s.first == other) - return; - } - existing.push_back(std::make_pair(other, dep)); - } - bool nielsen_node::lower_bound(expr* e, rational& lo) const { SASSERT(e); return m_graph.m_solver.lower_bound(e, lo); @@ -351,58 +338,6 @@ namespace seq { return m_graph.m_solver.upper_bound(e, up); } - void nielsen_node::apply_char_subst(euf::sgraph& sg, char_subst const& s, dep_tracker dep) { - if (!s.m_var) return; - - // replace occurrences of s.m_var with s.m_val in all string constraints - for (auto &eq : m_str_eq) { - eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_val); - eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_val); - eq.sort(); - } - for (auto &mem : m_str_mem) { - mem.m_str = sg.subst(mem.m_str, s.m_var, s.m_val); - mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_val); - } - - const unsigned var_id = s.m_var->id(); - - if (s.m_val->is_unit()) { - // symbolic char → symbolic char: check disequalities - if (m_char_diseqs.contains(var_id)) { - const auto& diseqs = m_char_diseqs.find(var_id); - for (const auto& d : diseqs) { - if (d.first == s.m_val) { - m_is_general_conflict = true; - set_conflict(backtrack_reason::character_range, d.second); - return; - } - } - m_char_diseqs.remove(var_id); - m_char_ranges.remove(var_id); - } - } - else { - SASSERT(s.m_val->is_char()); - // symbolic char → concrete char: check range constraints - if (m_char_ranges.contains(var_id)) { - auto& range = m_char_ranges.find(var_id); - unsigned ch_val = 0; - seq_util& seq = sg.get_seq_util(); - expr* unit_expr = s.m_val->get_expr(); - expr* ch_expr = nullptr; - bool have_char = unit_expr && seq.str.is_unit(unit_expr, ch_expr) && seq.is_const_char(ch_expr, ch_val); - if (have_char && !range.first.contains(ch_val)) { - m_is_general_conflict = true; - set_conflict(backtrack_reason::character_range, graph().dep_mgr().mk_join(dep, range.second)); - return; - } - m_char_diseqs.remove(var_id); - m_char_ranges.remove(var_id); - } - } - } - // ----------------------------------------------- // nielsen_graph // ----------------------------------------------- @@ -4100,7 +4035,7 @@ nielsen_graph::generate_length_constraints(vector& constraint bool nielsen_graph::solve_sat_path_raw(model_ref& mdl) { mdl = nullptr; if (m_sat_path.empty() && (!m_sat_node || - (m_sat_node->constraints().empty() && m_sat_node->char_diseqs().empty() && m_sat_node->char_ranges().empty()))) + (m_sat_node->constraints().empty() && m_sat_node->char_ranges().empty()))) return false; // Re-assert the sat-path constraints into m_solver (which holds only root-level @@ -4118,28 +4053,16 @@ nielsen_graph::generate_length_constraints(vector& constraint if (m_sat_node) { for (auto const& ic : m_sat_node->constraints()) m_solver.assert_expr(ic.fml); - for (auto const& dis : m_sat_node->char_diseqs()) { - ptr_vector dist; - dist.reserve((unsigned)dis.m_value.size()); - for (unsigned i = 0; i < dis.m_value.size(); ++i) { - dist.push_back(dis.m_value[i].first->get_expr()); - } - m_solver.assert_expr(m.mk_distinct(dist.size(), dist.data())); - } - // NSB code review: there is a seprate sort for characters - bv_util arith(m); for (auto const& kvp : m_sat_node->char_ranges()) { expr_ref_vector cases(m); const auto& var = m_sg.nodes()[kvp.m_key]->get_expr(); const auto& ranges = kvp.m_value.first.ranges(); cases.reserve(ranges.size()); - SASSERT(var->get_sort()->get_family_id() == arith.get_family_id()); - unsigned bitCnt = arith.get_bv_size(var); for (unsigned i = 0; i < ranges.size(); ++i) { cases.push_back(m.mk_and( - arith.mk_ule(arith.mk_numeral(ranges[i].m_lo, bitCnt), var), - arith.mk_ule(var, arith.mk_numeral(ranges[i].m_hi - 1, bitCnt)) + seq().mk_le(seq().mk_char(ranges[i].m_lo), var), + seq().mk_le(var, seq().mk_char(ranges[i].m_hi - 1)) )); } m_solver.assert_expr(m.mk_or(cases)); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 4e761a6c2..3c0a496e6 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -338,31 +338,6 @@ namespace seq { svector& eqs, svector& lits); - // ----------------------------------------------- - // character-level substitution - // mirrors ZIPT's CharSubst - // ----------------------------------------------- - - // maps a symbolic char (s_unit snode) to a concrete or symbolic char - struct char_subst { - euf::snode* m_var; // the symbolic char being substituted (s_unit) - euf::snode* m_val; // replacement: s_char (concrete) or s_unit (symbolic) - - char_subst(): m_var(nullptr), m_val(nullptr) {} - char_subst(euf::snode* var, euf::snode* val): - m_var(var), m_val(val) { - SASSERT(var && var->is_unit()); - SASSERT(val && (val->is_char() || val->is_unit())); - } - - // true when the replacement is a concrete character - bool is_eliminating() const { return m_val && m_val->is_char(); } - - bool operator==(char_subst const& o) const { - return m_var == o.m_var && m_val == o.m_val; - } - }; - // string equality constraint: lhs = rhs // mirrors ZIPT's StrEq (both sides are regex-free snode trees) struct str_eq { @@ -540,7 +515,6 @@ namespace seq { // character constraints (mirrors ZIPT's DisEqualities and CharRanges) // key: snode id of the s_unit symbolic character - u_map>> m_char_diseqs; // ?c != {?d, ?e, ...} u_map> m_char_ranges; // ?c in [lo, hi) // edges @@ -607,21 +581,13 @@ namespace seq { bool lower_bound(expr* e, rational& lo) const; bool upper_bound(expr* e, rational& up) const; - // character constraint access (mirrors ZIPT's DisEqualities / CharRanges) - u_map>> char_diseqs() const { return m_char_diseqs; } + // character constraint access (mirrors ZIPT's CharRanges) u_map> char_ranges() const { return m_char_ranges; } // add a character range constraint for a symbolic char. // intersects with existing range; sets conflict if result is empty. void add_char_range(euf::snode* sym_char, char_set const& range, dep_tracker dep); - // add a character disequality: sym_char != other - void add_char_diseq(euf::snode* sym_char, euf::snode* other, dep_tracker dep); - - // apply a character-level substitution to all constraints. - // checks disequalities and ranges; sets conflict on violation. - void apply_char_subst(euf::sgraph& sg, char_subst const& s, dep_tracker dep); - // edge access ptr_vector const& outgoing() const { return m_outgoing; } void add_outgoing(nielsen_edge* e) { m_outgoing.push_back(e); } diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 53c290f60..f03b206cc 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -508,14 +508,6 @@ namespace seq { kv.m_value.first.display(out); out << "
"; } - // character disequalities - for (auto const& kv : m_char_diseqs) { - if (!any) { out << "Cnstr:
"; any = true; } - if (!hasDiseq) { out << "Diseq:
"; hasDiseq = true; } - for (auto& d : kv.m_value) { - out << "?" << kv.m_key << " ≠ ?" << d.first->id() << "
"; - } - } // integer constraints for (auto const& ic : m_constraints) { if (!any) { out << "Cnstr:
"; any = true; }