Use subsolvers bounds rather than computing them inside nseq

src/smt/nseq_context_solver.h

@@ -20,6 +20,7 @@ Author:
 
 #include "smt/seq/seq_nielsen.h"
 #include "smt/smt_kernel.h"
+#include "smt/smt_arith_value.h"
 #include "params/smt_params.h"
 
 namespace smt {
@@ -32,6 +33,7 @@ namespace smt {
     class context_solver : public seq::simple_solver {
         smt_params  m_params;  // must be declared before m_kernel
         smt::kernel m_kernel;
+        arith_value m_arith_value;
 
         static smt_params make_seq_len_params() {
             smt_params p;
@@ -42,7 +44,10 @@ namespace smt {
     public:
         context_solver(ast_manager& m) :
             m_params(make_seq_len_params()),
-            m_kernel(m, m_params) {}
+            m_kernel(m, m_params),
+            m_arith_value(m) {
+            m_arith_value.init(&m_kernel.get_context());
+        }
 
         lbool check() override {
             // std::cout << "Checking:\n";
@@ -69,8 +74,19 @@ namespace smt {
             m_kernel.get_model(mdl);
         }
 
+        bool lower_bound(expr* e, rational& lo) const override {
+            bool is_strict = true;
+            return m_arith_value.get_lo(e, lo, is_strict) && !is_strict && lo.is_int();
+        }
+
+        bool upper_bound(expr* e, rational& hi) const override {
+            bool is_strict = true;
+            return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int();
+        }
+
         void reset() override {
             m_kernel.reset();
+            m_arith_value.init(&m_kernel.get_context());
         }
     };
 

src/smt/seq/seq_nielsen.h

@@ -163,10 +163,9 @@ Abstract:
     - IntEq / IntLe: integer equality and inequality constraints over Presburger
       arithmetic polynomials (PDD<BigInteger>) are entirely absent. The Z3 port
       has no ConstraintsIntEq or ConstraintsIntLe in nielsen_node.
-    - IntBounds / VarBoundWatcher: per-variable integer interval bounds and the
-      watcher mechanism that reruns bound propagation when a string variable is
-      substituted — PORTED as nielsen_node::{add_lower_int_bound,
-      add_upper_int_bound, watch_var_bounds, init_var_bounds_from_mems}.
+    - IntBounds / VarBoundWatcher: ZIPT-style cached interval maps and eager
+      watcher propagation are not stored in nielsen_node; bounds are queried
+      from the arithmetic subsolver on demand.
     - AddLowerIntBound() / AddHigherIntBound(): incremental interval tightening
       — PORTED as the above add_lower/upper_int_bound methods.
 
@@ -238,11 +237,10 @@ Author:
 #include "util/dependency.h"
 #include "util/map.h"
 #include "util/lbool.h"
+#include "util/rational.h"
 #include "ast/ast.h"
-#include "ast/arith_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/euf/euf_sgraph.h"
-#include <functional>
 #include <map>
 #include "model/model.h"
 
@@ -280,6 +278,10 @@ namespace seq {
         virtual void    push() = 0;
         virtual void    pop(unsigned num_scopes) = 0;
         virtual void    get_model(model_ref& mdl) { mdl = nullptr; }
+        // Optional bound queries on arithmetic expressions (non-strict integer bounds).
+        // Default implementation reports "unsupported".
+        virtual bool    lower_bound(expr* e, rational& lo) const { return false; }
+        virtual bool    upper_bound(expr* e, rational& hi) const { return false; }
         virtual void    reset() = 0;
     };
 
@@ -524,11 +526,6 @@ namespace seq {
         vector<str_mem>    m_str_mem;       // regex memberships
         vector<constraint> m_constraints;   // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe)
 
-        // per-variable integer bounds for len(var). Mirrors ZIPT's IntBounds.
-        // key: snode id of the string variable.
-        // default lb = 0 (unrestricted); default ub = UINT_MAX (unrestricted).
-        u_map<unsigned>                m_var_lb;   // lower bound: lb <= len(var)
-        u_map<unsigned>                m_var_ub;   // upper bound: len(var) <= ub
 
         // character constraints (mirrors ZIPT's DisEqualities and CharRanges)
         // key: snode id of the s_unit symbolic character
@@ -585,27 +582,11 @@ namespace seq {
         vector<constraint> const& constraints() const { return m_constraints; }
         vector<constraint>& constraints() { return m_constraints; }
 
-        // IntBounds: tighten the lower bound for len(var).
-        // Returns true if the bound was tightened (lb > current lower bound).
-        // When tightened without conflict, adds a constraint len(var) >= lb.
-        // When lb > current upper bound, sets arithmetic conflict (no constraint added)
-        // and still returns true (the bound value changed). Check is_general_conflict()
-        // separately to distinguish tightening-with-conflict from normal tightening.
-        // Mirrors ZIPT's AddLowerIntBound().
-        bool set_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep);
-
-        // IntBounds: tighten the upper bound for len(var).
-        // Returns true if the bound was tightened (ub < current upper bound).
-        // When tightened without conflict, adds a constraint len(var) <= ub.
-        // When current lower bound > ub, sets arithmetic conflict (no constraint added)
-        // and still returns true (the bound value changed). Check is_general_conflict()
-        // separately to distinguish tightening-with-conflict from normal tightening.
-        // Mirrors ZIPT's AddHigherIntBound().
-        bool set_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep);
-
-        // Query current bounds for a variable (default: 0 / UINT_MAX if not set).
-        unsigned var_lb(euf::snode* var) const;
-        unsigned var_ub(euf::snode* var) const;
+        // Query current bounds for a variable from the arithmetic subsolver.
+        // Falls der Subsolver keinen Bound liefert, werden konservative Defaults
+        // 0 / UINT_MAX verwendet.
+        bool lower_bound(expr* e, rational& lo) const;
+        bool upper_bound(expr* e, rational& up) const;
 
         // character constraint access (mirrors ZIPT's DisEqualities / CharRanges)
         u_map<ptr_vector<euf::snode>> const& char_diseqs() const { return m_char_diseqs; }
@@ -695,18 +676,7 @@ namespace seq {
         bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
                                dep_tracker const& dep, bool& changed);
 
-        // VarBoundWatcher: after applying substitution s, propagate the bounds
-        // of s.m_var to variables appearing in s.m_replacement.
-        // When var has bounds [lo, hi], derives bounds for variables in replacement
-        // using the known constant-length contribution of non-variable tokens.
-        // Mirrors ZIPT's VarBoundWatcher re-check mechanism.
-        void update_var_bounds(nielsen_subst const& s);
-
-        // Initialize per-variable Parikh bounds from this node's regex memberships.
-        // For each str_mem constraint (str ∈ regex) where regex has length bounds
-        // [min_len, max_len], adds lower/upper bound constraints for len(str).
-        // Called from simplify_and_init to populate IntBounds at node creation.
-        void init_var_bounds_from_mems();
+        // Length bounds are queried from the arithmetic subsolver when needed.
     };
 
     // search statistics collected during Nielsen graph solving
@@ -949,13 +919,13 @@ namespace seq {
         // accessor for the seq_regex module
         seq_regex* seq_regex_module() const { return m_seq_regex; }
 
+        dep_manager& dep_mgr() { return m_dep_mgr; }
+        dep_manager const& dep_mgr() const { return m_dep_mgr; }
+
     private:
 
         vector<dep_source, false> 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
         dep_tracker collect_conflict_deps() const;
 
@@ -1131,13 +1101,13 @@ namespace seq {
         // m_solver by search_dfs via push/pop, so a plain check() suffices.
         // l_undef (resource limit / timeout) is treated as feasible so that the
         // search continues rather than reporting a false unsatisfiability.
-        bool check_int_feasibility(nielsen_node* node);
+        bool check_int_feasibility();
 
         // check whether lhs <= rhs is implied by the path constraints.
         // mirrors ZIPT's NielsenNode.IsLe(): temporarily asserts NOT(lhs <= rhs)
         // and returns true iff the result is unsatisfiable (i.e., lhs <= rhs is
         // entailed).  Path constraints are already in the solver incrementally.
-        bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* node);
+        bool check_lp_le(expr* lhs, expr* rhs);
 
         // create an integer constraint: lhs <kind> rhs
         constraint mk_constraint(expr* fml, dep_tracker const& dep);

src/smt/seq/seq_parikh.cpp

@@ -267,8 +267,16 @@ namespace seq {
             // stride > 1 guaranteed from here onward.
             SASSERT(stride > 1);
 
-            unsigned lb = node.var_lb(mem.m_str);
-            unsigned ub = node.var_ub(mem.m_str);
+            rational lb_r, ub_r;
+            if (!node.lower_bound(mem.m_str->get_expr(), lb_r) || !node.upper_bound(mem.m_str->get_expr(), ub_r))
+                continue;
+
+            SASSERT(lb_r <= ub_r);
+            if (ub_r > INT_MAX)
+                continue;
+
+            const unsigned lb = (unsigned)lb_r.get_int32();
+            const unsigned ub = (unsigned)ub_r.get_int32();
 
             // Check: ∃k ≥ 0 such that lb ≤ min_len + stride * k ≤ ub ?
             //

src/smt/seq/seq_parikh.h

@@ -17,8 +17,8 @@ Abstract:
 
         len(str) = min_len + stride · k    (k ≥ 0, k fresh integer)
 
-    which tighten the arithmetic subproblem beyond the simple min/max
-    length bounds already produced by nielsen_node::init_var_bounds_from_mems().
+    which tighten the arithmetic subproblem beyond plain min/max bounds,
+    where concrete variable bounds are queried from the arithmetic subsolver.
 
     For example:
       • str ∈ (ab)*  → min_len = 0, stride = 2  → len(str) = 2·k
@@ -110,8 +110,8 @@ namespace seq {
         // Quick Parikh feasibility check (no solver call).
         //
         // For each single-variable membership str ∈ re, checks whether the
-        // modular constraint  len(str) = min_len + stride · k  (k ≥ 0)
-        // has any solution given the current per-variable bounds stored in
+        // modular constraint  len(str) = min_len + stride · k  (k >= 0)
+        // has any solution given the current per-variable bounds obtained via
         // node.var_lb(str) and node.var_ub(str).
         //
         // Returns true when a conflict is detected (no valid k exists for