From e1cf20f9bd99f6914ca6c83fe4215b51e4dd6c49 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 9 Mar 2026 14:21:06 +0100 Subject: [PATCH] Added timeout Some bugfixes --- src/smt/seq/seq_nielsen.cpp | 70 ++++++++++++++++++++----------------- src/smt/seq/seq_nielsen.h | 10 +++++- src/smt/theory_nseq.cpp | 1 + src/test/nseq_zipt.cpp | 19 +++++++++- 4 files changed, 65 insertions(+), 35 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 8da4396a6..5125b4284 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -967,7 +967,6 @@ namespace seq { mem.m_str = sg.drop_first(mem.m_str); mem.m_regex = deriv; mem.m_history = sg.mk_concat(mem.m_history, first); - changed = true; } } @@ -990,10 +989,8 @@ namespace seq { continue; // satisfied, drop m_str_mem[wi++] = mem; } - if (wi < m_str_mem.size()) { + if (wi < m_str_mem.size()) m_str_mem.shrink(wi); - changed = true; - } if (is_satisfied()) return simplify_result::satisfied; @@ -1044,6 +1041,8 @@ namespace seq { // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it. m_depth_bound = 3; while (true) { + if (m_cancel_fn && m_cancel_fn()) + break; if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth) break; inc_run_idx(); @@ -1070,6 +1069,10 @@ namespace seq { ++m_stats.m_num_dfs_nodes; m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth); + // check for external cancellation (timeout, user interrupt) + if (m_cancel_fn && m_cancel_fn()) + return search_result::unknown; + // revisit detection: if already visited this run, return cached status. // mirrors ZIPT's NielsenNode.GraphExpansion() evalIdx check. if (node->eval_idx() == m_run_idx) { @@ -1486,7 +1489,7 @@ namespace seq { // into two shorter equations with optional padding variable: // // eq1: LHS[0..lhsIdx] · [pad if padding<0] = [pad if padding>0] · RHS[0..rhsIdx] - // eq2: [pad if padding>0] · LHS[lhsIdx..] = RHS[rhsIdx..] · [pad if padding<0] + // eq2: LHS[lhsIdx..] · [pad if padding>0] = [pad if padding<0] · RHS[rhsIdx..] // // Creates a single progress child. // ----------------------------------------------------------------------- @@ -1564,17 +1567,14 @@ namespace seq { e->add_side_int(mk_int_constraint(len_pad, abs_pad, int_constraint_kind::eq, eq.m_dep)); } // 2) len(eq1_lhs) = len(eq1_rhs) - { - expr_ref l1 = compute_length_expr(eq1_lhs); - expr_ref r1 = compute_length_expr(eq1_rhs); - e->add_side_int(mk_int_constraint(l1, r1, int_constraint_kind::eq, eq.m_dep)); - } + expr_ref l1 = compute_length_expr(eq1_lhs); + expr_ref r1 = compute_length_expr(eq1_rhs); + e->add_side_int(mk_int_constraint(l1, r1, int_constraint_kind::eq, eq.m_dep)); + // 3) len(eq2_lhs) = len(eq2_rhs) - { - expr_ref l2 = compute_length_expr(eq2_lhs); - expr_ref r2 = compute_length_expr(eq2_rhs); - e->add_side_int(mk_int_constraint(l2, r2, int_constraint_kind::eq, eq.m_dep)); - } + expr_ref l2 = compute_length_expr(eq2_lhs); + expr_ref r2 = compute_length_expr(eq2_rhs); + e->add_side_int(mk_int_constraint(l2, r2, int_constraint_kind::eq, eq.m_dep)); return true; } @@ -1732,7 +1732,6 @@ namespace seq { } bool nielsen_graph::generate_extensions(nielsen_node *node) { - // Modifier priority chain mirrors ZIPT's ModifierBase.TypeOrder. // The first modifier that produces edges is used and returned immediately. // Priority 1: deterministic modifiers (single child, always progress) @@ -1751,7 +1750,7 @@ namespace seq { if (apply_const_num_unwinding(node)) return ++m_stats.m_mod_const_num_unwinding, true; - // Priority 5: EqSplit - split regex-free equation into two (single progress child) + // Priority 5: EqSplit - split equations into two (single progress child) if (apply_eq_split(node)) return ++m_stats.m_mod_eq_split, true; @@ -1866,34 +1865,39 @@ namespace seq { // ----------------------------------------------------------------------- bool nielsen_graph::apply_power_epsilon(nielsen_node* node) { - euf::snode* power = find_power_token(node); + euf::snode *power = find_power_token(node); if (!power) return false; SASSERT(power->is_power() && power->num_args() >= 1); - euf::snode* base = power->arg(0); + euf::snode *base = power->arg(0); dep_tracker dep; - for (str_eq const& eq : node->str_eqs()) - if (!eq.is_trivial()) { dep = eq.m_dep; break; } + for (str_eq const &eq : node->str_eqs()) { + if (!eq.is_trivial()) { + dep = eq.m_dep; + break; + } + } + + nielsen_node* child; + nielsen_edge* e; // Branch 1: base → ε (if base is a variable, substitute it to empty) // This makes u^n = ε^n = ε for any n. if (base->is_var()) { - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(base, m_sg.mk_empty(), dep); - e->add_subst(s); - child->apply_subst(m_sg, s); + child = mk_child(node); + e = mk_edge(node, child, true); + nielsen_subst s1(base, m_sg.mk_empty(), dep); + e->add_subst(s1); + child->apply_subst(m_sg, s1); } // Branch 2: replace the power token itself with ε (n = 0 semantics) - { - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(power, m_sg.mk_empty(), dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } + child = mk_child(node); + e = mk_edge(node, child, true); + nielsen_subst s2(power, m_sg.mk_empty(), dep); + e->add_subst(s2); + child->apply_subst(m_sg, s2); return true; } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index ef55be8c1..a812f90d6 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -238,6 +238,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/euf/euf_sgraph.h" #include "math/lp/lar_solver.h" +#include namespace seq { @@ -452,7 +453,8 @@ namespace seq { m_var(var), m_replacement(repl), m_dep(dep) { SASSERT(var != nullptr); SASSERT(repl != nullptr); - SASSERT(var->is_var()); + // var may be s_var or s_power; sgraph::subst uses pointer identity matching + SASSERT(var->is_var() || var->is_power()); } // an eliminating substitution does not contain the variable in the replacement @@ -724,6 +726,9 @@ namespace seq { unsigned m_num_input_mems = 0; nielsen_stats m_stats; + // external cancellation callback: returns true if solving should abort + std::function m_cancel_fn; + // ----------------------------------------------- // Integer subsolver using lp::lar_solver // Replaces ZIPT's SubSolver (auxiliary Z3 instance) @@ -770,6 +775,9 @@ namespace seq { // maximum overall search depth (0 = unlimited) void set_max_search_depth(unsigned d) { m_max_search_depth = d; } + // set a cancellation callback; solve() checks this periodically + void set_cancel_fn(std::function fn) { m_cancel_fn = std::move(fn); } + // generate next unique regex membership id unsigned next_mem_id() { return m_next_mem_id++; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index cebce6da9..e231ea82a 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -45,6 +45,7 @@ namespace smt { void theory_nseq::init() { m_arith_value.init(&get_context()); + m_nielsen.set_cancel_fn([this]() { return get_context().get_cancel_flag(); }); } // ----------------------------------------------------------------------- diff --git a/src/test/nseq_zipt.cpp b/src/test/nseq_zipt.cpp index fac62fa28..50ad6d9de 100644 --- a/src/test/nseq_zipt.cpp +++ b/src/test/nseq_zipt.cpp @@ -27,6 +27,7 @@ Abstract: #include #include #include +#include // ----------------------------------------------------------------------- // Helper: build a string snode from a notation string. @@ -174,24 +175,40 @@ struct nseq_fixture { euf::snode* R(const char* s) { return rb.parse(s); } }; +static constexpr int TEST_TIMEOUT_SEC = 10; + +static void set_timeout(nseq_fixture& f) { + auto start = std::chrono::steady_clock::now(); + f.ng.set_cancel_fn([start]() { + auto elapsed = std::chrono::steady_clock::now() - start; + return std::chrono::duration_cast(elapsed).count() >= TEST_TIMEOUT_SEC; + }); +} + static bool eq_sat(const char* lhs, const char* rhs) { + std::cout << "Checking equation: " << lhs << " = " << rhs << std::endl; nseq_fixture f; + set_timeout(f); f.ng.add_str_eq(f.S(lhs), f.S(rhs)); return f.ng.solve() == seq::nielsen_graph::search_result::sat; } static bool eq_unsat(const char* lhs, const char* rhs) { + std::cout << "Checking equation: " << lhs << " = " << rhs << std::endl; nseq_fixture f; + set_timeout(f); f.ng.add_str_eq(f.S(lhs), f.S(rhs)); return f.ng.solve() == seq::nielsen_graph::search_result::unsat; } static bool mem_sat(std::initializer_list> mems) { nseq_fixture f; + set_timeout(f); for (auto& [str, re] : mems) f.ng.add_str_mem(f.S(str), f.R(re)); return f.ng.solve() == seq::nielsen_graph::search_result::sat; } static bool mem_unsat(std::initializer_list> mems) { nseq_fixture f; + set_timeout(f); for (auto& [str, re] : mems) f.ng.add_str_mem(f.S(str), f.R(re)); return f.ng.solve() == seq::nielsen_graph::search_result::unsat; @@ -201,7 +218,7 @@ static bool mem_unsat(std::initializer_list> // String equation tests (ZIPT: CheckStrEquations) // ----------------------------------------------------------------------- static void test_zipt_str_equations() { - std::cout << "test_zipt_str_equations\n"; + std::cout << "test_zipt_str_equations:" << std::endl; VERIFY(eq_sat ("abab", "XX")); // abab = XX (X="ab") VERIFY(eq_sat ("aX", "YX")); // aX = YX (Y="a")