From 71d7d70080744333f7745fdd64475053806f68e8 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Tue, 12 May 2026 14:00:50 +0200 Subject: [PATCH] Missing dependency bug. Still not fixed, but better now --- src/ast/euf/euf_sgraph.cpp | 24 ++++++++++++++++++ src/ast/euf/euf_snode.h | 4 +++ src/smt/nseq_context_solver.h | 47 +++++++++++++++++++++-------------- src/smt/seq/seq_nielsen.cpp | 39 +++++++++++++++++++++-------- src/smt/seq/seq_nielsen.h | 4 +++ 5 files changed, 89 insertions(+), 29 deletions(-) diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index fc9dfbf66..a8774de8e 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -97,6 +97,9 @@ namespace euf { if (m_seq.re.is_range(e)) return snode_kind::s_range; + if (m.is_ite(e)) + return snode_kind::s_ite; + if (m_seq.re.is_to_re(e)) return snode_kind::s_to_re; @@ -251,6 +254,15 @@ namespace euf { n->m_length = 1; break; + case snode_kind::s_ite: + SASSERT(n->num_args() == 3); + n->m_ground = n->arg(0)->is_ground() && n->arg(1)->is_ground() && n->arg(2)->is_ground(); + n->m_regex_free = n->arg(1)->is_regex_free() && n->arg(2)->is_regex_free(); + n->m_is_classical = false; + n->m_level = 1; + n->m_length = 1; + break; + case snode_kind::s_to_re: SASSERT(n->num_args() == 1); n->m_ground = n->arg(0)->is_ground(); @@ -508,7 +520,18 @@ namespace euf { return mk_concat(s1, s2); return n; } + if (n->is_ite() && var->is_unit()) { + // We only need to replace in case we are replacing units; + // we would not generate any proper string replacements that propagates into the ite + auto s1 = subst(n->arg(0), var, replacement); + auto s2 = subst(n->arg(1), var, replacement); + auto s3 = subst(n->arg(2), var, replacement); + if (s1 != n->arg(0) || s2 != n->arg(1) || s3 != n->arg(2)) + return mk(expr_ref(m.mk_ite(s1->get_expr(), s2->get_expr(), s3->get_expr()), m)); + return n; + } // for non-concat compound nodes (power, star, etc.), no substitution into children + // TODO: This might change in the future foe e.g., powers return n; } @@ -744,6 +767,7 @@ namespace euf { case snode_kind::s_full_char: return "full_char"; case snode_kind::s_full_seq: return "full_seq"; case snode_kind::s_range: return "range"; + case snode_kind::s_ite: return "ite"; case snode_kind::s_to_re: return "to_re"; case snode_kind::s_in_re: return "in_re"; } diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index 1f2559f60..1bd50b160 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -53,6 +53,7 @@ namespace euf { s_full_char, // full character set (OP_RE_FULL_CHAR_SET) s_full_seq, // full sequence set r=.* (OP_RE_FULL_SEQ_SET) s_range, // character range [lo,hi] (OP_RE_RANGE) + s_ite, // ite (OP_ITE) s_to_re, // string to regex (OP_SEQ_TO_RE) s_in_re // regex membership (OP_SEQ_IN_RE) }; @@ -188,6 +189,9 @@ namespace euf { bool is_range() const { return m_kind == snode_kind::s_range; } + bool is_ite() const { + return m_kind == snode_kind::s_ite; + } bool is_to_re() const { return m_kind == snode_kind::s_to_re; } diff --git a/src/smt/nseq_context_solver.h b/src/smt/nseq_context_solver.h index ed31478ec..3324c8ab9 100644 --- a/src/smt/nseq_context_solver.h +++ b/src/smt/nseq_context_solver.h @@ -53,9 +53,10 @@ namespace smt { // Tracked assumption literals. // m_assump_lits[i] and m_frame_bounds together encode a stack of // frames, one frame per push(). pop(n) removes the top n frames. - expr_ref_vector m_assump_lits; // live assumption exprs - svector m_frame_bounds; // m_assump_lits.size() at each push() - u_map m_lid_to_dep; // literal expr-id -> dep + expr_ref_vector m_assump_lits; // assumption exprs; they will be reused, so it only grows + obj_map m_assump_lit2id; // the index represented by the assumption expression + svector m_frame_bounds; // m_deps.size() at each push() + svector m_deps; // id -> dep // Scratch dep_manager for joining core deps; reset before each check(). seq::dep_manager m_core_dep_mgr; @@ -78,19 +79,19 @@ namespace smt { lbool check() override { m_core_dep_mgr.reset(); - m_last_core = nullptr; + m_last_core = m_core_dep_mgr.mk_empty(); lbool r; if (m_assump_lits.empty()) { r = m_kernel.check(); } else { r = m_kernel.check(m_assump_lits.size(), m_assump_lits.data()); if (r == l_false) { - unsigned cnt = m_kernel.get_unsat_core_size(); + const unsigned cnt = m_kernel.get_unsat_core_size(); for (unsigned i = 0; i < cnt; ++i) { - expr* ce = m_kernel.get_unsat_core_expr(i); - seq::dep_tracker d = nullptr; - if (m_lid_to_dep.find(ce->get_id(), d)) - m_last_core = m_core_dep_mgr.mk_join(m_last_core, d); + expr_ref ce(m_kernel.get_unsat_core_expr(i), m_kernel.m()); + SASSERT(m_assump_lit2id.contains(ce)); + const unsigned id = m_assump_lit2id[ce]; + m_last_core = m_core_dep_mgr.mk_join(m_last_core, m_deps[id]); } } } @@ -103,26 +104,33 @@ namespace smt { return; } ast_manager& m = m_kernel.m(); - expr_ref lit(m.mk_fresh_const("_a", m.mk_bool_sort()), m); - m_kernel.assert_expr(m.mk_or(m.mk_not(lit), e)); - m_lid_to_dep.insert_if_not_there(lit->get_id(), dep); - m_assump_lits.push_back(lit); + expr* l; + if (m_assump_lits.size() <= m_deps.size()) { + SASSERT(m_assump_lits.size() == m_deps.size()); + l = m.mk_fresh_const("_a", m.mk_bool_sort()); + m_assump_lit2id.insert(l, m_assump_lits.size()); + m_assump_lits.push_back(l); + } + else + l = m_assump_lits.get(m_deps.size()); + m_kernel.assert_expr(m.mk_or(m.mk_not(l), e)); + m_deps.push_back(dep); } void push() override { m_kernel.push(); - m_frame_bounds.push_back((unsigned)m_assump_lits.size()); + m_frame_bounds.push_back(m_deps.size()); } void pop(unsigned n) override { SASSERT(n <= m_frame_bounds.size()); unsigned target = m_frame_bounds[m_frame_bounds.size() - n]; - while ((unsigned)m_assump_lits.size() > target) { - m_lid_to_dep.erase(m_assump_lits.back()->get_id()); - m_assump_lits.pop_back(); + while (m_deps.size() > target) { + m_deps.pop_back(); } - for (unsigned i = 0; i < n; ++i) + for (unsigned i = 0; i < n; i++) { m_frame_bounds.pop_back(); + } m_kernel.pop(n); } @@ -150,8 +158,9 @@ namespace smt { m_kernel.reset(); m_arith_value.init(&m_kernel.get_context()); m_assump_lits.reset(); + m_assump_lit2id.reset(); m_frame_bounds.reset(); - m_lid_to_dep.reset(); + m_deps.reset(); m_core_dep_mgr.reset(); m_last_core = nullptr; } diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 4013f46b9..41ce1c104 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -35,6 +35,7 @@ NSB review: #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/seq_skolem.h" #include "ast/rewriter/var_subst.h" +#include "smt/smt_enode.h" #include "util/statistics.h" #include #include @@ -313,10 +314,20 @@ namespace seq { for (auto &mem : m_str_mem) { auto new_str = sg.subst(mem.m_str, s.m_var, s.m_replacement); auto new_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); + std::cout << "Applying substitution " + << mk_pp(s.m_var->get_expr(), graph().m) << " / " + << mk_pp(s.m_replacement->get_expr(), graph().m) << " to " << + mk_pp(new_regex->get_expr(), graph().m) << std::endl; if (new_str != mem.m_str || new_regex != mem.m_regex) { - mem.m_str = new_str; - mem.m_regex = new_regex; - mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep); + mem.m_str = new_str; + mem.m_regex = new_regex; + mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep); + } + if (new_regex != mem.m_regex) { + std::cout << "Got: " << mk_pp(new_regex->get_expr(), graph().get_manager()) << std::endl; + } + else { + std::cout << "No change!" << std::endl; } } @@ -1806,9 +1817,10 @@ namespace seq { // integer feasibility check: the solver now holds all path constraints // incrementally; just query the solver directly if (!cur_path.empty() && !check_int_feasibility()) { - dep_tracker dep = get_subsolver_dependency(node); - node->set_conflict(backtrack_reason::arithmetic, dep); + dep_tracker deps = get_subsolver_dependency(node); + node->set_conflict(backtrack_reason::arithmetic, deps); node->set_general_conflict(); + ++m_stats.m_num_arith_infeasible; return search_result::unsat; } @@ -1885,8 +1897,9 @@ namespace seq { add_subst_length_constraints(e); 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); + } } @@ -3916,7 +3929,6 @@ namespace seq { nielsen_node *child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); for (auto f : cs) { - std::cout << "sc: " << mk_pp(f, m) << std::endl; e->add_side_constraint(constraint(f, mem.m_dep, m)); } for (str_mem &cm : child->str_mems()) { @@ -4485,6 +4497,14 @@ namespace seq { } } + void nielsen_graph::assert_to_subsolver(const constraint& c) { + m_solver.assert_expr(c.fml, c.dep); + } + + void nielsen_graph::assert_to_subsolver(expr* e) { + m_solver.assert_expr(e); + } + void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) { // Assert only the constraints that are new to this node (beyond those // inherited from its parent via clone_from). The parent's constraints are @@ -4501,8 +4521,7 @@ namespace seq { node->set_external_conflict(lit, c.dep); return; } - m_solver.assert_expr(c.fml); - + assert_to_subsolver(c); } } @@ -4612,7 +4631,7 @@ namespace seq { expr_ref rhs_plus_one(a.mk_add(rhs, one), m); m_solver.push(); - m_solver.assert_expr(a.mk_ge(lhs, rhs_plus_one)); + assert_to_subsolver(a.mk_ge(lhs, rhs_plus_one)); lbool result = m_solver.check(); m_solver.pop(1); if (result == l_false) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index fdd63b009..14c91cac1 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -1038,6 +1038,10 @@ namespace seq { // Add a dependency leaf for lhs <= rhs and join it to dep. void add_le_dependency(dep_tracker& dep, nielsen_node* n, expr* lhs, expr* rhs); + void assert_to_subsolver(const constraint& c); + + void assert_to_subsolver(expr* e); + // Assert the constraints of `node` that are new relative to its // parent (indices [m_parent_ic_count..end)) into the current solver scope. // Called by search_dfs after simplify_and_init so that the newly derived