Add theory_seq_len: partial axiom instantiation for sequence length constraints

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/smt/theory_seq_len.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    theory_seq_len.h
+
+Abstract:
+
+    Theory solver for sequence length constraints.
+
+    Handles the theory of sequences (seq_decl_plugin) using partial axiom
+    instantiation:
+    - Axiomatizes (seq.len S) >= 0 for all sequence variables S.
+    - Derives stronger lower/upper bounds on seq.len based on the structure of S.
+    - Axiomatizes S in RegEx by extracting semi-linear length constraints from
+      the regex. For example, if RegEx is (aa)*, it asserts (seq.len S) = 2*X_s
+      where X_s >= 0 is a fresh integer variable.
+    - Returns FC_DONE in final_check (incomplete but sound partial solver).
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-03-10
+
+--*/
+#pragma once
+
+#include "ast/seq_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "model/seq_factory.h"
+#include "smt/smt_theory.h"
+#include "smt/smt_model_generator.h"
+
+namespace smt {
+
+    class theory_seq_len : public theory {
+        seq_util        m_util;
+        arith_util      m_autil;
+
+        // -----------------------------------------------------------------------
+        // Virtual overrides required by theory base class
+        // -----------------------------------------------------------------------
+        bool internalize_atom(app* atom, bool gate_ctx) override;
+        bool internalize_term(app* term) override;
+        void new_eq_eh(theory_var, theory_var) override {}
+        void new_diseq_eh(theory_var, theory_var) override {}
+        theory* mk_fresh(context* new_ctx) override;
+        char const* get_name() const override { return "seq-len"; }
+        void display(std::ostream& out) const override;
+
+        // -----------------------------------------------------------------------
+        // Optional overrides
+        // -----------------------------------------------------------------------
+        void assign_eh(bool_var v, bool is_true) override;
+        final_check_status final_check_eh(unsigned) override { return FC_DONE; }
+        void push_scope_eh() override { theory::push_scope_eh(); }
+        void pop_scope_eh(unsigned num_scopes) override { theory::pop_scope_eh(num_scopes); }
+        void init_model(model_generator& mg) override;
+
+        // -----------------------------------------------------------------------
+        // Axiom generation helpers
+        // -----------------------------------------------------------------------
+
+        // Assert (seq.len e) >= 0.
+        void add_length_non_neg(expr* e);
+
+        // Assert length axioms implied by S in R (when the membership is true).
+        // lit is the literal for (S in R).
+        void add_regex_length_axioms(expr* s, expr* r, literal lit);
+
+        // Returns true if the regex r has a fixed length (min==max).
+        bool has_fixed_length(expr* r, unsigned& len) const;
+
+        // Extract semi-linear length constraint for a regex.
+        // Returns true if a useful constraint can be extracted.
+        // If so, sets:
+        //   period > 0: lengths are of the form (base + period*k), k >= 0
+        //   period == 0: length is exactly base
+        bool get_length_constraint(expr* r, unsigned& base, unsigned& period) const;
+
+        // Helper: internalize and get literal for an expr.
+        literal mk_literal(expr* e);
+
+        // Helper: assert a clause (disjunction of literals).
+        void assert_axiom(literal_vector& lits);
+
+    public:
+        theory_seq_len(context& ctx);
+    };
+
+}