From d620f20c63059e4c96ecfe1b58b3648f9f2f3afc Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 13 Apr 2026 14:06:06 +0200 Subject: [PATCH] Simplify code --- src/smt/seq/seq_nielsen.cpp | 69 +++++-------------------------------- src/smt/seq/seq_nielsen.h | 7 ---- src/smt/seq_model.cpp | 18 ---------- src/smt/theory_nseq.cpp | 30 +++++++++++----- 4 files changed, 29 insertions(+), 95 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 7df78cf0c..33e06e293 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1056,11 +1056,9 @@ namespace seq { } else { // we only know for sure that one is smaller than the other - expr_ref d(m_graph.mk_fresh_int_var()); - expr_ref zero_e(m_graph.a.mk_int(0), m); - expr_ref d_plus_smaller(m_graph.a.mk_add(d, smaller_exp), m); - add_constraint(m_graph.mk_constraint(m_graph.a.mk_ge(d, zero_e), eq.m_dep)); - add_constraint(m_graph.mk_constraint(m.mk_eq(d_plus_smaller, larger_exp), eq.m_dep)); + expr_ref d(m_graph.a.mk_sub(larger_exp, smaller_exp), m); + expr_ref zero(m_graph.a.mk_int(0), m); + add_constraint(m_graph.mk_constraint(m_graph.a.mk_ge(d, zero), eq.m_dep)); expr_ref pw(seq.str.mk_power(lb, d), m); euf::snode*& larger_side = lp_le_rp ? eq.m_rhs : eq.m_lhs; larger_side = dir_concat(sg, sg.mk(pw), larger_side, fwd); @@ -1082,7 +1080,7 @@ namespace seq { bool fwd = od == 0; while (!mem.m_str->is_empty()) { euf::snode* tok = dir_token(mem.m_str, fwd); - if (!tok || !tok->is_char()) + if (!tok || !tok->is_char_or_unit()) break; euf::snode* deriv = fwd ? sg.brzozowski_deriv(mem.m_regex, tok) @@ -3003,8 +3001,6 @@ namespace seq { if (mem.is_primitive() || !mem.m_regex->is_classical()) continue; - std::cout << "Factoring " << mk_pp(mem.m_str->get_expr(), m) << " ∈ " << mk_pp(mem.m_regex->get_expr(), m) << std::endl; - euf::snode* first = mem.m_str->first(); SASSERT(first); euf::snode* tail = m_sg.drop_first(mem.m_str); @@ -3013,9 +3009,6 @@ namespace seq { tau_pairs pairs; compute_tau(m, m_seq, m_sg, mem.m_regex->get_expr(), pairs); - bool any_child = false; - dep_tracker conflict_dep = mem.m_dep; - for (auto const& pair : pairs) { euf::snode* sn_p = m_sg.mk(pair.m_p); euf::snode* sn_q = m_sg.mk(pair.m_q); @@ -3030,19 +3023,13 @@ namespace seq { // Also check intersection with other primitive constraints on `first` ptr_vector regexes_p; regexes_p.push_back(sn_p); - dep_tracker local_dep = nullptr; for (auto const& prev_mem : node->str_mems()) { - if (prev_mem.m_str == first) { + if (prev_mem.m_str == first) regexes_p.push_back(prev_mem.m_regex); - local_dep = m_dep_mgr.mk_join(local_dep, prev_mem.m_dep); - } } - if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) { - conflict_dep = m_dep_mgr.mk_join(conflict_dep, local_dep); + if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) continue; - } - any_child = true; nielsen_node* child = mk_child(node); mk_edge(node, child, true); @@ -3060,11 +3047,6 @@ namespace seq { child->add_str_mem(str_mem(tail, sn_q, mem.m_history, next_mem_id(), mem.m_dep)); } - if (!any_child) { - node->set_conflict(backtrack_reason::regex, conflict_dep); - node->set_general_conflict(); - } - return true; } return false; @@ -4107,8 +4089,8 @@ namespace seq { return false; // definitely infeasible } rational rhs_lo, lhs_up; - if (m_solver.lower_bound(lhs, lhs_lo) && - m_solver.upper_bound(rhs, rhs_up)) { + if (m_solver.upper_bound(lhs, lhs_up) && + m_solver.lower_bound(rhs, rhs_lo)) { if (lhs_up <= rhs_lo) return true; // definitely feasible @@ -4148,41 +4130,6 @@ namespace seq { return expr_ref(m.mk_fresh_const(name.c_str(), a.mk_int()), m); } - 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_ranges().empty()))) - return false; - - // Re-assert the sat-path constraints into m_solver (which holds only root-level - // constraints at this point) and extract a model via the injected simple_solver. - // The sat path was found by DFS which verified feasibility at every step via - // check_int_feasibility, so all constraints along this path are jointly satisfiable - // and do not require incremental skipping. - IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";); - m_solver.push(); - if (m_sat_node) { - for (auto const& ic : m_sat_node->constraints()) { - m_solver.assert_expr(ic.fml); - } - } - lbool result = m_solver.check(); - IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints result: " << result << "\n";); - if (result == l_true) { - m_solver.get_model(mdl); - IF_VERBOSE(1, if (mdl) { - verbose_stream() << " raw_model:\n"; - for (unsigned i = 0; i < mdl->get_num_constants(); ++i) { - func_decl* fd = mdl->get_constant(i); - expr* val = mdl->get_const_interp(fd); - if (val) verbose_stream() << " " << fd->get_name() << " = " << mk_bounded_pp(val, m, 3) << "\n"; - } - }); - } - m_solver.pop(1); - return mdl.get() != nullptr; - } - // ----------------------------------------------------------------------- // Regex widening: overapproximate string and check intersection emptiness // Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 85cda96b2..fe387e1b2 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -933,13 +933,6 @@ namespace seq { // max_len == UINT_MAX means unbounded. void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len); - // solve all integer constraints along the sat_path and return - // a model mapping integer variables to concrete values. - // Must be called after solve() returns sat. - // Returns true if a satisfying model was found. - // Caller takes ownership of the returned model pointer. - bool solve_sat_path_raw(model_ref& mdl); - // accessor for the seq_regex module seq_regex* seq_regex_module() const { return m_seq_regex; } diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 65257a538..2bd176a30 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -147,7 +147,6 @@ namespace smt { m_var_values.reset(); m_var_regex.reset(); m_trail.reset(); - m_int_model = nullptr; m_mg = &mg; m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model()); @@ -220,7 +219,6 @@ namespace smt { m_var_values.reset(); m_var_regex.reset(); m_trail.reset(); - m_int_model = nullptr; m_mg = nullptr; m_factory = nullptr; } @@ -374,22 +372,6 @@ namespace smt { else exp_val = rational(0); } - else if (exp_expr && m_int_model.get()) { - expr_ref result(m); - if (m_int_model->eval_expr(exp_expr, result, true) && arith.is_numeral(result, exp_val)) { - // evaluated from int model - } - else if (m_mg) { - proto_model& pm = m_mg->get_model(); - if (pm.eval(exp_expr, result, true) && arith.is_numeral(result, exp_val)) { - // evaluated from proto_model - } - else - exp_val = rational(0); - } - else - exp_val = rational(0); - } else if (exp_expr && m_mg) { expr_ref result(m); proto_model& pm = m_mg->get_model(); diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index e58e56153..fc874fe86 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -613,7 +613,9 @@ namespace smt { if (!m_nielsen_literals.empty() && m_nielsen.sat_node() != nullptr && all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) { IF_VERBOSE(1, verbose_stream() << "nseq final_check: satifiable state revisited\n"); - return FC_DONE; + // Re-run solving/model extraction instead of early exiting on a + // cached SAT node. This avoids stale sat paths after additional + // SAT assignments were introduced in prior FC_CONTINUE rounds. } // unfold higher-order terms when sequence structure is known @@ -693,8 +695,13 @@ namespace smt { // Nielsen found a consistent assignment for positive constraints. SASSERT(has_eq_or_mem); // we should have axiomatized them - if (!add_nielsen_assumptions()) - return FC_CONTINUE; + if (!add_nielsen_assumptions()) { + // If assumptions remain undefined, returning SAT can yield + // unsound/invalid models because the chosen Nielsen branch + // is not yet committed in the outer SAT core. + IF_VERBOSE(1, verbose_stream() << "nseq final_check: unresolved assumptions, FC_GIVEUP\n";); + return FC_GIVEUP; + } if (!check_length_coherence()) return FC_CONTINUE; @@ -730,17 +737,22 @@ namespace smt { //std::cout << "Nielsen assumptions:\n"; ctx.push_trail(reset_vector(m_nielsen_literals)); for (auto const& c : m_nielsen.sat_node()->constraints()) { - bool was_internalized = ctx.e_internalized(c.fml); auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); - std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; + // Ensure Nielsen assumptions participate in SAT search instead of + // remaining permanently undefined under pure phase hints. + ctx.mark_as_relevant(lit); + // std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; switch (ctx.get_assignment(lit)) { case l_true: break; case l_undef: - //std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << "\n"; + std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << std::endl; has_undef = true; - ctx.force_phase(lit); + // Commit the chosen Nielsen assumption to the SAT core so it + // cannot remain permanently undefined in a partial model. + ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.force_phase(lit); IF_VERBOSE(2, verbose_stream() << "nseq final_check: adding nielsen assumption " << c.fml << "\n";); TRACE(seq, tout << "assign: " << c.fml << "\n"); @@ -749,10 +761,10 @@ namespace smt { // this should not happen because nielsen checks for this before returning a satisfying path. IF_VERBOSE(1, verbose_stream() << "nseq final_check: nielsen assumption " << c.fml << " is false\n";); - ctx.force_phase(lit); has_undef = true; + ctx.mk_th_axiom(get_id(), 1, &lit); ctx.force_phase(lit); - //std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl; + std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl; break; } }