z3/src/smt/theory_nseq.h

/*++
Copyright (c) 2026 Microsoft Corporation

Module Name:

    theory_nseq.h

Abstract:

    ZIPT string solver theory for Z3.
    Implements theory_nseq, a theory plugin for string/sequence constraints
    using the Nielsen transformation graph (Nielsen graph).

Author:

    Clemens Eisenhofer 2026-03-01
    Nikolaj Bjorner (nbjorner) 2026-03-01

--*/
#pragma once

#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_axioms.h"
#include "ast/euf/euf_egraph.h"
#include "ast/euf/euf_sgraph.h"
#include "smt/smt_theory.h"
#include "smt/smt_arith_value.h"
#include "smt/seq/seq_nielsen.h"
#include "smt/seq/seq_state.h"   // tracked_str_eq, tracked_str_mem
#include "smt/seq/seq_regex.h"
#include "smt/seq_model.h"
#include "smt/nseq_context_solver.h"

namespace smt {

    class theory_nseq : public theory {
        seq_util       m_seq;
        arith_util     m_autil;
        th_rewriter    m_th_rewriter;
        seq_rewriter   m_rewriter;
        arith_value    m_arith_value;
        euf::egraph    m_egraph;  // private egraph (not shared with smt context)
        euf::sgraph    m_sgraph;  // private sgraph
        // m_context_solver must be declared before m_nielsen: its address is passed
        // to the m_nielsen constructor and must remain stable for the object's lifetime.
        sub_solver m_length_solver;
        context_solver m_context_solver;
        seq::nielsen_graph m_nielsen;
        seq::axioms m_axioms;
        seq::seq_regex     m_regex;   // regex membership pre-processing
        seq_model     m_model;   // model construction helper

        // propagation queue items (variant over the distinct propagation cases)
        using eq_item   = tracked_str_eq;    // string equality
        using deq_item   = tracked_str_deq;    // string disequality
        using mem_item  = tracked_str_mem;   // regex membership
        struct axiom_item { expr* e; };      // structural axiom for term e

        using prop_item = std::variant<eq_item, deq_item, mem_item, axiom_item>;

        vector<prop_item>       m_prop_queue;
        unsigned                m_prop_qhead = 0;
        obj_hashtable<expr>     m_axiom_set;   // dedup guard for axiom_item enqueues
        obj_hashtable<expr>     m_no_diseq_set;     // track expressions that should not trigger new disequality axioms
        hashtable<literal, obj_hash<literal>, default_eq<literal>>    m_ignored_mem;     // track membership constraints that should not be passed to Nielsen
        expr_ref_vector         m_relevant_lengths;     // track variables whose lengths are relevant
        obj_map<expr, unsigned> m_gradient_cache;
        sat::literal_vector     m_nielsen_literals;   // literals created by a Nilsen check
        sat::literal            m_assumption_lit;     // literal used as assumption to bound search to selected literal assignments
        unsigned                m_max_unfolding_depth = 0;

        // SAT-path revalidation: m_constraint_gen changes only when the
        // 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_last_constraint_added = 0;
        bool                    m_can_hot_restart = false;

        // statistics
        unsigned m_num_conflicts        = 0;
        unsigned m_num_final_checks     = 0;
        unsigned m_num_sat_revalidations = 0;   // times the cached SAT path was reused instead of rebuilding
        unsigned m_num_length_axioms    = 0;
        bool     m_digits_initialized   = false;

        // map from context enode to private sgraph snode
        obj_map<expr, euf::snode*> m_expr2snode;


        // higher-order terms (seq.map, seq.mapi, seq.foldl, seq.foldli)
        ptr_vector<app>  m_ho_terms;
        unsigned         m_num_ho_unfolds = 0;

        // stoi (str.to_int) coherence tracking
        ptr_vector<expr>        m_stoi_terms;   // stoi terms that need coherence checking
        obj_hashtable<expr>     m_stoi_set;     // dedup guard for m_stoi_terms
        obj_map<expr, unsigned> m_stoi_depth;   // max k for which stoi_axiom(e, k) was called

        // unhandled boolean string predicates (prefixof, suffixof, contains, etc.)
        unsigned         m_num_unhandled_bool = 0;

        bool has_unhandled_preds() const { return m_num_unhandled_bool > 0; }
        void push_unhandled_pred();

        // required virtual methods
        bool internalize_atom(app* a, bool gate_ctx) override;
        bool internalize_term(app* term) override;
        void apply_sort_cnstr(enode *n, sort *s) override;
        theory_var mk_var(enode* n) override;
        void new_eq_eh(theory_var v1, theory_var v2) override;
        void new_diseq_eh(theory_var v1, theory_var v2) override;
        theory* mk_fresh(context* ctx) override;
        void display(std::ostream& out) const override;


        // optional overrides
        bool can_propagate() override;
        void propagate() override;
        void init() override;
        void assign_eh(bool_var v, bool is_true) override;
        void relevant_eh(app* n) override;
        final_check_status final_check_eh(unsigned) override;
        void push_scope_eh() override;
        void pop_scope_eh(unsigned num_scopes) override;
        void init_model(model_generator& mg) override;
        model_value_proc* mk_value(enode* n, model_generator& mg) override;
        void finalize_model(model_generator& mg) override;
        void validate_model(proto_model& mdl) override;
        void collect_statistics(::statistics& st) const override;
        bool should_research(expr_ref_vector &) override;
        void add_theory_assumptions(expr_ref_vector &assumptions) override;

        char const* get_name() const override { return "nseq"; }

        // private helpers
        void populate_nielsen_graph();
        void explain_nielsen_conflict();
        void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
        void set_propagate(enode_pair_vector const &eqs, literal_vector const &lits, literal p);
        bool add_nielsen_assumptions();
        euf::snode* get_snode(expr* e);

        // propagation dispatch helpers
        void propagate_eq(tracked_str_eq const& eq);
        void propagate_deq(tracked_str_deq const& deq);
        void propagate_pos_mem(tracked_str_mem const& mem);
        void enqueue_axiom(expr* e);
        void dequeue_axiom(expr* e);
        void ensure_length_var(expr* e);

        // higher-order term unfolding
        bool unfold_ho_terms();

        // arithmetic value queries for length reasoning
        bool get_num_value(expr* e, rational& val) const;
        bool lower_bound(expr* e, rational& lo) const;
        bool upper_bound(expr* e, rational& hi) const;
        bool get_length(expr* e, rational& val);
        void add_length_axiom(literal lit);
        bool propagate_length_lemma(literal lit, seq::length_constraint const& lc);
        bool assert_nonneg_for_all_vars();
        bool assert_length_constraints();

        // Regex membership pre-check: for each variable with regex constraints,
        // check intersection emptiness before running DFS.
        //   l_true  → found empty intersection, conflict asserted, return FC_CONTINUE
        //   l_false → all variables' regex constraints satisfiable and no word
        //             equations / disequalities, return FC_DONE (SAT)
        //   l_undef → inconclusive, proceed to DFS
        lbool check_regex_memberships_precheck();

        bool check_length_coherence();

        // stoi axiom helpers
        void add_stoi_nseq_axioms(expr* stoi_e);
        bool check_stoi_coherence();

    public:
        theory_nseq(context& ctx);
    };

}