/*++
  Copyright (c) 2025 Microsoft Corporation

  --*/
#pragma once

#include "math/lp/nla_coi.h"

namespace nla {

    class core;
    class lar_solver;    
    class mul_saturate : common {

        struct var_sign {
            lpvar v = lp::null_lpvar;
            bool is_neg = false;
            u_dependency* dep = nullptr;
        };
        coi m_coi;
        // source of multiplication constraint
        u_map<lp::constraint_index> m_new_mul_constraints;
        svector<var_sign> m_var_signs;
        tracked_uint_set m_seen_vars;
        indexed_uint_set m_to_refine;
        scoped_ptr<lp::lar_solver> local_solver;
        ptr_vector<u_dependency> m_ci2dep;
        vector<rational> m_values;
        struct eq {
            bool operator()(unsigned_vector const& a, unsigned_vector const& b) const {
                return a == b;
            }
        };
        map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
        u_map<unsigned_vector> m_mon2vars;

        // initialization
        void init_solver();
        void init_vars();
        void init_monomial(unsigned mon_var);

        bool constraint_is_true(lp::constraint_index ci);
        void insert_monomials_from_constraint(lp::constraint_index ci);

        // additional variables and monomials and constraints
        lpvar add_monomial(svector<lp::lpvar> const& vars);
        bool is_int(svector<lp::lpvar> const& vars) const;
        lpvar add_var(bool is_int);
        void add_multiply_constraints();
        void add_multiply_constraint(lp::constraint_index con_id, lp::lpvar mi, lpvar x);

        // solving
        lbool solve(lp::explanation& ex);

        // lemmas
        void add_lemma(lp::explanation const& ex);

        std::ostream& display(std::ostream& out) const;
        std::ostream& display_product(std::ostream& out, svector<lpvar> const& vars) const;
        std::ostream& display_constraint(std::ostream& out, lp::constraint_index ci) const;
        std::ostream& display_constraint(std::ostream& out, vector<std::pair<rational, lpvar>> const& lhs,
                                         lp::lconstraint_kind k, rational const& rhs) const;

    public:
        mul_saturate(core* core);
        lbool saturate();
    };

}