From 315a09aea8a6239be4d630058e126e270cd12a90 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 20 May 2026 17:24:57 +0200 Subject: [PATCH] [WIP] Try to replace "recursive reusage" of variables by seq.slice --- src/smt/seq/seq_nielsen.cpp | 103 +++++++++++++++------------------ src/smt/seq/seq_nielsen.h | 33 ++++------- src/smt/seq/seq_nielsen_pp.cpp | 9 +-- src/smt/seq/seq_parikh.cpp | 6 +- src/smt/theory_nseq.cpp | 33 ++++++----- src/smt/theory_nseq.h | 4 +- src/test/seq_nielsen.cpp | 56 +----------------- 7 files changed, 88 insertions(+), 156 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 92e18b3a5..716cf9826 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -321,7 +321,7 @@ namespace seq { // We have to add all - even if some of it conflict // [otw. we would leave the node partially initialized] for (const auto f : *to_app(c.fml)) { - add_constraint(constraint(f, c.dep, m)); + add_constraint(constraint(f, c.dep, c.internal, m)); } return; } @@ -371,8 +371,7 @@ namespace seq { expr* var_c_expr = s.m_var->arg(0)->get_expr(); expr* repl_c_expr = s.m_replacement->arg(0)->get_expr(); add_constraint( - constraint( - m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, m)); + constraint(m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, false, m)); if (m_char_ranges.contains(var_id)) { const auto range = m_char_ranges.find(var_id); // copy exactly @@ -426,7 +425,7 @@ namespace seq { seq.mk_le(seq.mk_char(ranges[i].m_lo), var), seq.mk_le(var, seq.mk_char(ranges[i].m_hi - 1))); } - add_constraint(constraint(m.mk_or(cases), dep, m)); + add_constraint(constraint(m.mk_or(cases), dep, false, m)); } // ----------------------------------------------- // nielsen_graph @@ -519,16 +518,6 @@ namespace seq { m_root->add_str_mem(str_mem(str, regex, dep)); } - void nielsen_graph::inc_run_idx() { - if (m_run_idx == UINT_MAX) { - for (nielsen_node* n : m_nodes) - n->reset_counter(); - m_run_idx = 1; - } - else - ++m_run_idx; - } - void nielsen_graph::reset() { for (nielsen_node* n : m_nodes) dealloc(n); @@ -539,7 +528,6 @@ namespace seq { m_root = nullptr; m_sat_node = nullptr; m_sat_path.reset(); - m_run_idx = 0; m_depth_bound = 0; m_fresh_cnt = 0; m_root_constraints_asserted = false; @@ -567,7 +555,7 @@ namespace seq { // just assume it to be correct // Just add the constraint - we do not have to recompute it // [also it is on the set of side-conditions if we assert a satisfied node] - n->add_constraint(constraint(le, dep, m)); + n->add_constraint(constraint(le, dep, false, m)); } // ----------------------------------------------------------------------- @@ -1708,7 +1696,6 @@ namespace seq { } if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth) break; - inc_run_idx(); ptr_vector cur_path; // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search const search_result r = search_dfs(m_root, cur_path); // the main search loop @@ -1783,29 +1770,17 @@ namespace seq { if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes) return search_result::unknown; - // revisit detection: if already visited this run (e.g., iterative deepening), return cached status. - // mirrors ZIPT's NielsenNode.GraphExpansion() evalIdx check. - const unsigned eval_idx = node->eval_idx(); - if (eval_idx == m_run_idx) { - if (node->is_satisfied()) { - m_sat_node = node; - m_sat_path = cur_path; - return search_result::sat; - } - if (node->is_currently_conflict()) - return search_result::unsat; - return search_result::unknown; + if (node->is_satisfied()) { + m_sat_node = node; + m_sat_path = cur_path; + return search_result::sat; } - node->set_eval_idx(m_run_idx); - SASSERT(!node->is_general_conflict()); - if (eval_idx > 0) - // adding the side-conditions from the edge - // when generating this node might trigger a local conflict - node->clear_local_conflict(); // clear local conflicts from previous runs + if (node->is_currently_conflict()) + return search_result::unsat; // we might need to tell the SAT solver about the new integer inequalities // that might have been added by an extension step - assert_node_new_int_constraints(node); + assert_node_side_constraints(node); if (node->is_currently_conflict()) { ++m_stats.m_num_simplify_conflict; @@ -1841,7 +1816,7 @@ namespace seq { // Also generate per-node |LHS| = |RHS| length constraints for descendant // equations (root constraints are already at the base level). generate_node_length_constraints(node); - assert_node_new_int_constraints(node); + assert_node_side_constraints(node); if (node->is_currently_conflict()) { ++m_stats.m_num_simplify_conflict; @@ -1873,7 +1848,7 @@ namespace seq { node->set_conflict(backtrack_reason::regex, dep); return search_result::unsat; } - assert_node_new_int_constraints(node); + assert_node_side_constraints(node); // We need to have everything asserted before reporting SAT // (otw. the outer solver might assume false-assigned literals to be true) if (node->is_currently_conflict()) { @@ -3971,7 +3946,7 @@ namespace seq { nielsen_node *child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); for (const auto f : cs) { - e->add_side_constraint(constraint(f, mem.m_dep, m)); + e->add_side_constraint(constraint(f, mem.m_dep, false, m)); } for (str_mem &cm : child->str_mems()) { if (cm == mem) { @@ -4281,11 +4256,21 @@ namespace seq { dep_tracker nielsen_graph::collect_conflict_deps() const { dep_tracker deps = nullptr; - // We enumerate all nodes rather than having a "todo"-list, as - // hypothetically the graph could contain cycles in the future - for (nielsen_node const* n : m_nodes) { + // todo: Add visit set if the graph could contain cycles in the future + // enumerating all nodes would not work due to hot-restarts having created + // children that are currently not relevant + vector to_visit; + to_visit.push_back(m_root); + while (!to_visit.empty()) { + nielsen_node const* n = to_visit.back(); + to_visit.pop_back(); if (n->reason() == backtrack_reason::children_failed) { SASSERT(n->m_conflict_external_literal == sat::null_literal); + SASSERT(!n->m_conflict_internal); + for (unsigned i = n->outgoing().size(); i > 0; i--) { + nielsen_edge const* e = n->outgoing()[i - 1]; + to_visit.push_back(e->tgt()); + } continue; } // not true anymore since we might have done a hot-restart where we previously created the child: @@ -4362,7 +4347,7 @@ namespace seq { tout << "Length constraint from LHS " << snode_label_html(eq.m_lhs, m) << " to " << len_lhs << ":\n"; tout << "Length constraint from RHS " << snode_label_html(eq.m_rhs, m) << " to " << len_rhs << "\n"); expr_ref len_eq(m.mk_eq(len_lhs, len_rhs), m); - constraints.push_back(length_constraint(len_eq, eq.m_dep, length_kind::eq, m)); + constraints.push_back(length_constraint(len_eq, eq.m_dep, length_kind::eq, true, m)); // collect variables for non-negativity constraints euf::snode_vector tokens; @@ -4374,7 +4359,7 @@ namespace seq { expr_ref len_var(seq.str.mk_length(tok->get_expr()), m); expr_ref ge_zero(a.mk_ge(len_var, a.mk_int(0)), m); TRACE(seq, tout << "non-negative length " << ge_zero << "\n"); - constraints.push_back(length_constraint(ge_zero, eq.m_dep, length_kind::nonneg, m)); + constraints.push_back(length_constraint(ge_zero, eq.m_dep, length_kind::nonneg, true, m)); } } } @@ -4393,14 +4378,14 @@ namespace seq { if (min_len > 0) { expr_ref bound(a.mk_ge(len_str, a.mk_int(min_len)), m); TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n"); - constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); + constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, false, m)); } // generate len(str) <= max_len when bounded if (max_len < UINT_MAX) { expr_ref bound(a.mk_le(len_str, a.mk_int(max_len)), m); TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n"); - constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); + constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, false, m)); } } } @@ -4482,7 +4467,7 @@ namespace seq { continue; has_non_elim = true; // Assert LHS >= 0 - e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep)); + e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep, true)); } // Step 2: Bump mod counts for all non-eliminating variables at once. @@ -4494,7 +4479,13 @@ namespace seq { for (auto const &[idx, lhs] : lhs_exprs) { auto const& s = substs[idx]; expr_ref rhs = compute_length_expr(s.m_replacement); - e->add_side_constraint(mk_constraint(m.mk_eq(lhs, rhs), s.m_dep)); + e->add_side_constraint(mk_constraint(m.mk_eq(lhs, rhs), s.m_dep, true)); + // otw. we have equality as a side-constraint in the Nielsen node + // and adding the Nielsen assumption will force the phase of the equality to true + // however the arith.-solver will axiomatize it as <= && >= which do not have a phase + // hence it might get assigned false by decision which is a performance problem + // e->add_side_constraint(mk_constraint(a.mk_le(lhs, rhs), s.m_dep)); + // e->add_side_constraint(mk_constraint(a.mk_ge(lhs, rhs), s.m_dep)); } // Step 4: Restore mod counts (temporary bump for computing RHS only). @@ -4547,7 +4538,7 @@ namespace seq { m_length_solver.assert_expr(e); } - void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) const { + void nielsen_graph::assert_node_side_constraints(nielsen_node* node) const { // Assert only the constraints that are new to this node (beyond those // inherited from its parent via clone_from). The parent's constraints are // already present in the enclosing solver scope; asserting them again would @@ -4585,7 +4576,7 @@ namespace seq { expr_ref len_lhs = compute_length_expr(eq.m_lhs); expr_ref len_rhs = compute_length_expr(eq.m_rhs); - node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep)); + node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep, true)); // non-negativity for each variable (mod-count-aware) euf::snode_vector tokens; @@ -4595,7 +4586,7 @@ namespace seq { if (tok->is_var() && !seen_vars.contains(tok->id())) { seen_vars.insert(tok->id()); expr_ref len_var = compute_length_expr(tok); - node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep)); + node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep, true)); } } } @@ -4611,9 +4602,9 @@ namespace seq { expr_ref len_str = compute_length_expr(mem.m_str); if (min_len > 0) - node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep)); + node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep, true)); if (max_len < UINT_MAX) - node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep)); + node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep, true)); } } @@ -4674,14 +4665,14 @@ namespace seq { dep = m_length_solver.core(); m_length_solver.pop(1); if (result == l_false) { - n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, m)); + n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, false, m)); return true; } return false; } - constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep) const { - return constraint(fml, dep, m); + constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep, bool internal) const { + return constraint(fml, dep, internal, m); } expr* nielsen_graph::get_power_exponent(euf::snode* power) { diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index b03a89f42..9323428be 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -499,6 +499,7 @@ namespace seq { struct constraint { expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression) dep_tracker dep; // tracks which input constraints contributed + bool internal; // don't push back to the outer solver (helpful if not necessary and it would reveal internal variables) static expr_ref simplify(expr* f, ast_manager& m) { //th_rewriter th(m); @@ -508,9 +509,10 @@ namespace seq { } constraint(ast_manager& m): - fml(m), dep(nullptr) {} - constraint(expr* f, dep_tracker const& d, ast_manager& m): - fml(simplify(f, m)), dep(d) {} + fml(m), dep(nullptr), internal(true) {} + + constraint(expr* f, dep_tracker const& d, const bool internal, ast_manager& m): + fml(simplify(f, m)), dep(d), internal(internal) {} std::ostream& display(std::ostream& out) const; }; @@ -527,13 +529,14 @@ namespace seq { expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1) dep_tracker m_dep; // tracks which input constraints contributed length_kind m_kind; // determines propagation strategy + bool m_internal; - length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {} - length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m): - m_expr(e, m), m_dep(dep), m_kind(kind) {} + length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg), m_internal(true) {} + length_constraint(expr* e, dep_tracker const& dep, length_kind kind, const bool internal, ast_manager& m): + m_expr(e, m), m_dep(dep), m_kind(kind), m_internal(internal) {} constraint to_constraint() const { - return constraint(m_expr, m_dep, m_expr.get_manager()); + return constraint(m_expr, m_dep, m_internal, m_expr.get_manager()); } }; @@ -603,9 +606,6 @@ namespace seq { bool m_is_progress = false; bool m_node_len_constraints_generated = false; // true after generate_node_length_constraints runs - // evaluation index for run tracking - unsigned m_eval_idx = 0; - // Parikh filter: set to true once apply_parikh_to_node has been applied // to this node. Prevents duplicate constraint generation across DFS runs. bool m_parikh_applied = false; @@ -724,10 +724,6 @@ namespace seq { bool is_progress() const { return m_is_progress; } - unsigned eval_idx() const { return m_eval_idx; } - void set_eval_idx(unsigned idx) { m_eval_idx = idx; } - void reset_counter() { m_eval_idx = 0; } - // clone constraints from a parent node void clone_from(nielsen_node const& parent); @@ -849,7 +845,6 @@ namespace seq { nielsen_node* m_root = nullptr; nielsen_node* m_sat_node = nullptr; ptr_vector m_sat_path; - unsigned m_run_idx = 0; unsigned m_depth_bound = 0; unsigned m_max_search_depth = 0; unsigned m_max_nodes = 0; // 0 = unlimited @@ -969,10 +964,6 @@ namespace seq { void add_str_eq(euf::snode* lhs, euf::snode* rhs); void add_str_mem(euf::snode* str, euf::snode* regex); - // run management - unsigned run_idx() const { return m_run_idx; } - void inc_run_idx(); - // access all nodes ptr_vector const& nodes() const { return m_nodes; } unsigned num_nodes() const { return m_nodes.size(); } @@ -1065,7 +1056,7 @@ namespace seq { // 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 // bounds become visible to subsequent check() and check_lp_le() calls. - void assert_node_new_int_constraints(nielsen_node* node) const; + void assert_node_side_constraints(nielsen_node* node) const; private: @@ -1316,7 +1307,7 @@ namespace seq { bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep); // create an integer constraint: lhs rhs - constraint mk_constraint(expr* fml, dep_tracker const& dep) const; + constraint mk_constraint(expr* fml, dep_tracker const& dep, bool internal = false) const; // get the exponent expression from a power snode (arg(1)) static expr * get_power_exponent(euf::snode* power); diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index ac7c2938d..944870023 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -537,9 +537,10 @@ namespace seq { out << "
"; } // integer constraints - std::vector int_constraints(m_constraints.size()); + std::vector int_constraints; for (auto const& ic : m_constraints) { - int_constraints.push_back(constraint_html(ic, names, next_id, m)); + int_constraints.push_back( + (ic.internal ? "[I] " : "") + constraint_html(ic, names, next_id, m)); } if (!int_constraints.empty()) { // eliminate duplicates @@ -635,8 +636,6 @@ namespace seq { out << ", color=darkred"; else if (n->is_currently_conflict()) out << ", color=red"; - else if (n->eval_idx() != m_run_idx) // inactive, not visited this run - out << ", color=blue"; out << "];\n"; } @@ -669,8 +668,6 @@ namespace seq { nielsen_edge* ep = const_cast(e); if (sat_edges.contains(ep)) out << ", color=green"; - else if (e->tgt()->eval_idx() != m_run_idx) - out << ", color=blue"; else if (e->tgt()->is_currently_conflict()) out << ", color=red"; diff --git a/src/smt/seq/seq_parikh.cpp b/src/smt/seq/seq_parikh.cpp index 383d82180..57184426c 100644 --- a/src/smt/seq/seq_parikh.cpp +++ b/src/smt/seq/seq_parikh.cpp @@ -210,11 +210,11 @@ namespace seq { expr_ref stride_expr(a.mk_int(stride), m); expr_ref stride_k(a.mk_mul(stride_expr, k_var), m); expr_ref rhs(a.mk_add(min_expr, stride_k), m); - out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, m)); + out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, false, m)); // Constraint 2: k ≥ 0 expr_ref zero(a.mk_int(0), m); - out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, m)); + out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, false, m)); // Constraint 3 (optional): k ≤ max_k when max_len is bounded. // max_k = floor((max_len - min_len) / stride) @@ -226,7 +226,7 @@ namespace seq { unsigned range = max_len - min_len; unsigned max_k = range / stride; expr_ref max_k_expr(a.mk_int(max_k), m); - out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, m)); + out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, false, m)); } } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index e479f8b3d..d1d8342b4 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -225,7 +225,8 @@ namespace smt { seq::dep_tracker dep = nullptr; ctx.push_trail(restore_vector(m_prop_queue)); m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); - ++m_constraint_gen; + m_last_constraint_added = ctx.get_scope_level(); + m_can_hot_restart = false; } catch(const std::exception&) { #ifdef Z3DEBUG @@ -285,7 +286,8 @@ namespace smt { if (is_true) { ctx.push_trail(restore_vector(m_prop_queue)); m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep)); - ++m_constraint_gen; + m_last_constraint_added = ctx.get_scope_level(); + m_can_hot_restart = false; } else { // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership @@ -295,7 +297,8 @@ namespace smt { euf::snode* sn_re_compl = get_snode(re_compl.get()); ctx.push_trail(restore_vector(m_prop_queue)); m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep)); - ++m_constraint_gen; + m_last_constraint_added = ctx.get_scope_level(); + m_can_hot_restart = false; } } else if (m_seq.str.is_prefix(e)) { @@ -371,7 +374,9 @@ namespace smt { m_sgraph.pop(num_scopes); // A pop may remove constraints and/or unassign forced Nielsen // literals; conservatively invalidate the cached SAT path. - ++m_constraint_gen; + if (m_can_hot_restart && ctx.get_scope_level() - num_scopes < m_last_constraint_added) + // we popped one of the constraints used to build the Nielsen graph + m_can_hot_restart = false; } catch(const std::exception&) { #ifdef Z3DEBUG @@ -584,6 +589,7 @@ namespace smt { void theory_nseq::populate_nielsen_graph() { m_nielsen.reset(); + m_can_hot_restart = true; unsigned num_eqs = 0, num_mems = 0; @@ -686,7 +692,7 @@ namespace smt { // Fast path: if no new string eq/mem arrived and no scope was popped // since the last successful solve, the Nielsen graph can be (at least) // partially be reused - if (m_solved_gen == m_constraint_gen) { + if (m_can_hot_restart) { // SAT leaf are identical to what we would rebuild. All of the leaf's // arithmetic side-constraints are already assigned true by the outer // solver, so the model is valid — skip the rebuild and re-solve. @@ -703,8 +709,6 @@ namespace smt { // fall through - no reason to rebuild the Nielsen graph // everything that is not a general conflict needs to be recomputed // but we can keep the general conflicts (which can be a lot!) - 1 == 1; - 0 == 0; std::stack to_visit; to_visit.push(m_nielsen.root()); while (!to_visit.empty()) { @@ -726,6 +730,7 @@ namespace smt { } } m_nielsen.clear_sat_node(); + m_length_solver.reset(); } else { // let's rebuild the whole Nielsen graph @@ -739,7 +744,7 @@ namespace smt { SASSERT(m_nielsen.root()); - m_nielsen.assert_node_new_int_constraints(m_nielsen.root()); + m_nielsen.assert_node_side_constraints(m_nielsen.root()); ++m_num_final_checks; @@ -789,10 +794,6 @@ namespace smt { // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl; #endif - // Snapshot generation so the fast path can skip a full rebuild - // on the next call if no new constraints arrive in the meantime. - m_solved_gen = m_constraint_gen; - if (result == seq::nielsen_graph::search_result::unsat) { IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";); TRACE(seq, tout << "nseq final_check: solve UNSAT\n"); @@ -850,7 +851,11 @@ namespace smt { bool all_sat = true; ctx.push_trail(reset_vector(m_nielsen_literals)); for (auto const& c : m_nielsen.sat_node()->constraints()) { - // std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; + if (c.internal) { + std::cout << "Skipping internall assumption: "<< mk_pp(c.fml, m) << std::endl; + continue; + } + std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; auto lit = mk_literal(c.fml); m_nielsen_literals.push_back(lit); // Ensure Nielsen assumptions participate in SAT search instead of @@ -904,7 +909,7 @@ namespace smt { set_conflict(eqs, lits); #ifdef Z3DEBUG -#if 1 +#if 0 // Pass constraints to a subsolver to check correctness modulo legacy solver { smt_params p; diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 6d4cd407c..785d92d21 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -73,8 +73,8 @@ namespace smt { // Nielsen-relevant constraint set changes (new str eq/mem, or a pop). // m_solved_gen is the generation at the last successful SAT solve; // when it still equals m_constraint_gen the cached sat path is reusable. - unsigned m_constraint_gen = 0; - unsigned m_solved_gen = UINT_MAX; + unsigned m_last_constraint_added = 0; + bool m_can_hot_restart = false; // statistics unsigned m_num_conflicts = 0; diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp index b8a489673..c4547ceb0 100644 --- a/src/test/seq_nielsen.cpp +++ b/src/test/seq_nielsen.cpp @@ -409,26 +409,6 @@ static void test_nielsen_expansion() { ng.display(std::cout); } -// test run index management -static void test_run_idx() { - std::cout << "test_run_idx\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - - dummy_simple_solver solver; - seq::context_solver_i context_solver; - seq::nielsen_graph ng(sg, solver, context_solver); - SASSERT(ng.run_idx() == 0); - - ng.inc_run_idx(); - SASSERT(ng.run_idx() == 1); - - ng.inc_run_idx(); - SASSERT(ng.run_idx() == 2); -} - // test multiple regex memberships static void test_multiple_memberships() { std::cout << "test_multiple_memberships\n"; @@ -1661,36 +1641,6 @@ static void test_solve_children_failed_reason() { SASSERT(result == seq::nielsen_graph::search_result::unsat); } -// test that eval_idx is set during solve -static void test_solve_eval_idx_tracking() { - std::cout << "test_solve_eval_idx_tracking\n"; - ast_manager m; - reg_decl_plugins(m); - euf::egraph eg(m); - euf::sgraph sg(m, eg); - - dummy_simple_solver solver; - seq::context_solver_i context_solver; - seq::nielsen_graph ng(sg, solver, context_solver); - euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort()); - euf::snode* a = sg.mk_char('A'); - // x = A·x would be infinite without depth bound, but - // x = A is simple and satisfiable - ng.add_str_eq(x, a); - - unsigned run_before = ng.run_idx(); - auto result = ng.solve(); - SASSERT(result == seq::nielsen_graph::search_result::sat); - - // run_idx should have been incremented - SASSERT(ng.run_idx() > run_before); - - // root's eval_idx should match current run_idx - seq::nielsen_node* root = ng.root(); - SASSERT(root->eval_idx() == ng.run_idx()); -} - - // ----------------------------------------------------------------------- // Direct simplify_and_init tests // ----------------------------------------------------------------------- @@ -3438,14 +3388,14 @@ static void add_len_ge(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::sno ast_manager& m = ng.get_manager(); arith_util arith(m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); - node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, m)); + node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, false, m)); } static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::snode* var, unsigned ub, seq::dep_tracker dep) { ast_manager& m = ng.get_manager(); arith_util arith(m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); - node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, m)); + node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, false, m)); } static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) { @@ -3959,7 +3909,6 @@ void tst_seq_nielsen() { test_nielsen_subst_apply(); test_nielsen_graph_reset(); test_nielsen_expansion(); - test_run_idx(); test_multiple_memberships(); test_backedge(); test_eq_split_basic(); @@ -4004,7 +3953,6 @@ void tst_seq_nielsen() { test_solve_node_extended_flag(); test_solve_mixed_eq_mem_sat(); test_solve_children_failed_reason(); - test_solve_eval_idx_tracking(); test_simplify_prefix_cancel(); test_simplify_suffix_cancel_rtl(); test_simplify_symbol_clash();