diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index d3ce54984..8f3fcd5e7 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -41,6 +41,19 @@ NSB review: namespace seq { + void deps_to_lits(dep_tracker const& deps, + svector& eqs, + svector& lits) { + vector vs; + dep_manager::s_linearize(deps, vs); + for (dep_source const& d : vs) { + if (std::holds_alternative(d)) + eqs.push_back(std::get(d)); + else + lits.push_back(std::get(d)); + } + } + // Normalize an arithmetic expression using th_rewriter. // Simplifies e.g. (n - 1 + 1) to n, preventing unbounded growth // of power exponents during unwind/merge cycles. @@ -1461,6 +1474,7 @@ namespace seq { ++m_stats.m_num_solve_calls; m_sat_node = nullptr; m_sat_path.reset(); + m_conflict_sources.reset(); // Constraint.Shared: assert root-level length/Parikh constraints to the // solver at the base level, so they are visible during all feasibility checks. @@ -1504,6 +1518,9 @@ namespace seq { } if (r == search_result::unsat) { ++m_stats.m_num_unsat; + dep_tracker deps = m_dep_mgr.mk_empty(); + collect_conflict_deps(deps); + m_dep_mgr.linearize(deps, m_conflict_sources); return r; } // depth limit hit – double the bound and retry diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 1eb16c568..f99e478a6 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -329,6 +329,11 @@ namespace seq { // nullptr represents the empty dependency set. using dep_tracker = dep_manager::dependency*; + // partition dep_source leaves from deps into enode pairs and sat literals. + void deps_to_lits(dep_tracker const& deps, + svector& eqs, + svector& lits); + // ----------------------------------------------- // character-level substitution // mirrors ZIPT's CharSubst @@ -820,9 +825,6 @@ namespace seq { seq_util& seq() { return m_seq; } seq_util const& seq() const { return m_seq; } - dep_manager& dep_mgr() { return m_dep_mgr; } - dep_manager const& dep_mgr() const { return m_dep_mgr; } - // node management nielsen_node* mk_node(); nielsen_node* mk_child(nielsen_node* parent); @@ -907,8 +909,8 @@ namespace seq { // returns true if at least one child was generated bool generate_extensions(nielsen_node *node); - // collect dependency information from conflicting constraints - void collect_conflict_deps(dep_tracker& deps) const; + // conflict sources extracted after solve() returns unsat + vector const& conflict_sources() const { return m_conflict_sources; } // explain a conflict: partition the dep_source leaves into str_eq indices // (kind::eq) and str_mem indices (kind::mem). @@ -952,6 +954,14 @@ namespace seq { private: + vector m_conflict_sources; + + dep_manager& dep_mgr() { return m_dep_mgr; } + dep_manager const& dep_mgr() const { return m_dep_mgr; } + + // collect dependency information from conflicting constraints + void collect_conflict_deps(dep_tracker& deps) const; + search_result search_dfs(nielsen_node *node, ptr_vector& path); // Regex widening: overapproximate `str` by replacing variables with diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 2ccba32e3..3c320c2a3 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -579,29 +579,25 @@ namespace smt { // Conflict explanation // ----------------------------------------------------------------------- - void theory_nseq::deps_to_lits(seq::dep_tracker const& deps, enode_pair_vector& eqs, literal_vector& lits) { - vector vs; - m_nielsen.dep_mgr().linearize(deps, vs); - for (seq::dep_source const &d : vs) { - if (std::holds_alternative(d)) - eqs.push_back(std::get(d)); - else - lits.push_back(std::get(d)); - } - } - void theory_nseq::add_conflict_clause(seq::dep_tracker const& deps) { enode_pair_vector eqs; literal_vector lits; - deps_to_lits(deps, eqs, lits); + seq::deps_to_lits(deps, eqs, lits); ++m_num_conflicts; set_conflict(eqs, lits); } void theory_nseq::explain_nielsen_conflict() { - seq::dep_tracker deps = m_nielsen.dep_mgr().mk_empty(); - m_nielsen.collect_conflict_deps(deps); - add_conflict_clause(deps); + enode_pair_vector eqs; + literal_vector lits; + for (seq::dep_source const& d : m_nielsen.conflict_sources()) { + if (std::holds_alternative(d)) + eqs.push_back(std::get(d)); + else + lits.push_back(std::get(d)); + } + ++m_num_conflicts; + set_conflict(eqs, lits); } void theory_nseq::set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) { @@ -862,7 +858,7 @@ namespace smt { // conditional constraints: propagate with justification from dep_tracker enode_pair_vector eqs; literal_vector lits; - deps_to_lits(lc.m_dep, eqs, lits); + seq::deps_to_lits(lc.m_dep, eqs, lits); ctx.mark_as_relevant(lit); justification* js = ctx.mk_justification( diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 338c00eaf..1fdbbd895 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -113,7 +113,6 @@ namespace smt { // private helpers void populate_nielsen_graph(); void explain_nielsen_conflict(); - void deps_to_lits(seq::dep_tracker const& deps, enode_pair_vector& eqs, literal_vector& lits); void add_conflict_clause(seq::dep_tracker const& deps); void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits); euf::snode* get_snode(expr* e); diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index 71fcd327d..8e72742c3 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -1394,7 +1394,7 @@ static void test_solve_node_status_unsat() { SASSERT(root->is_currently_conflict()); } -// test that collect_conflict_deps returns deps after unsat +// test that conflict_sources is populated after unsat static void test_solve_conflict_deps() { std::cout << "test_solve_conflict_deps\n"; ast_manager m; @@ -1413,10 +1413,8 @@ static void test_solve_conflict_deps() { auto result = ng.solve(); SASSERT(result == seq::nielsen_graph::search_result::unsat); - seq::dep_tracker deps = ng.dep_mgr().mk_empty(); - ng.collect_conflict_deps(deps); - // deps should be non-empty since there's a conflict - SASSERT(deps != nullptr); + // conflict_sources should be non-empty since there's a conflict + SASSERT(!ng.conflict_sources().empty()); } // test dep_tracker (dependency_manager) linearize diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp index ec76a5238..56c0dc8d6 100644 --- a/src/test/seq_parikh.cpp +++ b/src/test/seq_parikh.cpp @@ -579,7 +579,7 @@ static void test_check_conflict_valid_k_exists() { ng.add_str_mem(x, regex); // lb=3, ub=5: length 4 is achievable (k=2) → no conflict - seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); + seq::dep_tracker dep = nullptr; ng.root()->set_lower_int_bound(x, 3, dep); ng.root()->set_upper_int_bound(x, 5, dep); @@ -607,7 +607,7 @@ static void test_check_conflict_no_valid_k() { ng.add_str_mem(x, regex); // lb=3, ub=3: only odd length 3 — never a multiple of 2 → conflict - seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); + seq::dep_tracker dep = nullptr; ng.root()->set_lower_int_bound(x, 3, dep); ng.root()->set_upper_int_bound(x, 3, dep); @@ -635,7 +635,7 @@ static void test_check_conflict_abc_star() { ng.add_str_mem(x, regex); // lb=5, ub=5 → no valid k (5 is not a multiple of 3) → conflict - seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); + seq::dep_tracker dep = nullptr; ng.root()->set_lower_int_bound(x, 5, dep); ng.root()->set_upper_int_bound(x, 5, dep); @@ -662,7 +662,7 @@ static void test_check_conflict_stride_one_never_conflicts() { euf::snode* regex = sg.mk(re); ng.add_str_mem(x, regex); - seq::dep_tracker dep = ng.dep_mgr().mk_leaf(sat::literal(0)); + seq::dep_tracker dep = nullptr; ng.root()->set_lower_int_bound(x, 7, dep); ng.root()->set_upper_int_bound(x, 7, dep);