extreme_values.h

Go to the documentation of this file.

 
#pragma once
 
#include "sdfg/options.h"
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/symbolic.h"
 
#include <memory>
#include <string>
#include <unordered_map>
 
namespace sdfg {
namespace symbolic {
 
struct DelinearizeResult;
 
// Default proof-search work budget (node visits per top-level query). Some
// queries over deeply-nested tile nests fan out into many fruitless sub-proofs;
// the cap bails them early with a conservative "unknown".
inline constexpr int64_t DEFAULT_BOUND_BUDGET = 50000;
 
// Budget for the bound queries of delinearization (`AssumptionsBounds`). A
// failed proof only keeps an access 1-D, and failing proofs exhaust the budget on every candidate split.
inline constexpr int64_t DELINEARIZATION_PROOF_BUDGET = 5000;
 
// Discoverable, threadable override for the budget above; shared by any analysis
// or pass that constructs a BoundAnalysis.
inline constexpr OptionKey<int64_t> BOUND_BUDGET{"symbolic.bound_budget"};

struct Interval {
    Expression lower;
    Expression upper;

    bool failed() const {
        return lower.is_null() && upper.is_null();
    }

    bool has_lower() const {
        return !lower.is_null();
    }

    bool has_upper() const {
        return !upper.is_null();
    }

    static Interval exact(const Expression& expr) {
        return {expr, expr};
    }

    static Interval failure() {
        return {SymEngine::null, SymEngine::null};
    }
};

class BoundAnalysis {
public:
    BoundAnalysis(
        const SymbolSet& parameters,
        const Assumptions& assumptions,
        bool use_tight_assumptions,
        int64_t budget = DEFAULT_BOUND_BUDGET,
        bool project_constraints = true
    );

    Interval bound(const Expression& expr);

    Expression lower_bound(const Expression& expr);

    Expression upper_bound(const Expression& expr);
 
private:
    static constexpr size_t MAX_DEPTH = 100;
    static constexpr size_t MAX_GENERATORS = 16;
 
    const SymbolSet& parameters_;
    const Assumptions& assumptions_;
    bool use_tight_;
    int64_t budget_;
    // When false, skip coupled-constraint projection: cheaper, sound, but looser bounds.
    bool project_constraints_;
 
    // Cycle detection: symbols currently being bounded
    SymbolSet visiting_;
 
    // Monotonic counter incremented every time the cycle guard in
    // `visit_symbol` fires (a symbol's resolution was abandoned because
    // we were already bounding it). Used by `visit()` to detect that a
    // subtree's result was influenced by the current `visiting_` state —
    // such context-tainted results must not be cached, because the same
    // expression evaluated outside the cycle could yield a tighter bound
    // (e.g. via coupled-constraint projection). Compared at entry vs.
    // exit of `visit_uncached`; if it grew, the result is tainted.
    size_t cycle_hits_ = 0;
 
    // Like `cycle_hits_`, for the `MAX_DEPTH` cutoff (results computed under it are depth-dependent).
    size_t limit_hits_ = 0;
 
    // Memoization cache for visit() results, keyed by canonical SymEngine
    // hash+eq on the input expression. Only results computed without hitting
    // the cycle guard, the depth limit, or the work budget are cached (including
    // failures and one-sided intervals): those depend solely on the expression
    // and this instance's fixed inputs. Tainted results are recomputed.
    struct BasicHash {
        size_t operator()(const Expression& e) const noexcept {
            return e->hash();
        }
    };
    struct BasicEq {
        bool operator()(const Expression& a, const Expression& b) const noexcept {
            return a.get() == b.get() || SymEngine::eq(*a, *b);
        }
    };
    std::unordered_map<Expression, Interval, BasicHash, BasicEq> cache_;
 
    Interval visit(const Expression& expr, size_t depth);
    Interval visit_uncached(const Expression& expr, size_t depth);
 
    Interval visit_symbol(const SymEngine::RCP<const SymEngine::Symbol>& sym, size_t depth);
    Interval visit_function(const SymEngine::RCP<const SymEngine::FunctionSymbol>& func, size_t depth);
    Interval visit_pow(const SymEngine::RCP<const SymEngine::Pow>& pow_expr, size_t depth);
    Interval visit_mul(const SymEngine::RCP<const SymEngine::Mul>& mul_expr, size_t depth);
    Interval visit_add(const SymEngine::RCP<const SymEngine::Add>& add_expr, size_t depth);
    Interval visit_max(const Expression& expr, size_t depth);
    Interval visit_min(const Expression& expr, size_t depth);
 
    // Add sub-strategies
    Interval visit_add_affine(const AffineCoeffs& coeffs, const SymbolVec& gens, size_t depth);
    Interval visit_add_polynomial(const Polynomial& poly, const SymbolVec& gens, size_t depth);
    Interval visit_add_argwise(const SymEngine::vec_basic& args, size_t depth);
 
    // Tightens an affine-sum interval by projecting coupled constraints onto
    // the SUM as a single linear functional. Per-symbol projection (already
    // done in `visit_symbol`) loses coupling: bounding `x + y` with the
    // constraint `x + y <= K` registered on both symbols would sum the
    // per-symbol upper bounds `x <= K - y` and `y <= K - x`, each resolved
    // independently down to `K`, yielding `2*K` instead of `K`.
    //
    // This helper looks for a non-negative integer linear combination of
    // registered constraints whose generator coefficients match those of the
    // input sum exactly. When such a combination exists, every term in the
    // sum cancels against the constraint combination, leaving a parameter-
    // only residue that is the tightening bound. Greedy per-generator search
    // is sufficient for the common patterns (single halo-guard constraint,
    // block-diagonal multi-axis stencil guards).
    //
    // Returns a (possibly partially-null) `Interval` to be intersected with
    // the result of the regular per-term bounding flow.
    Interval visit_add_coupled_constraints(const AffineCoeffs& coeffs, const SymbolVec& gens, size_t depth);
};
 
// ---- Backward-compatible free functions ----

Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight);

Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight);
 
// ---- Sound inequality proofs ----
//
// All `is_*` predicates return TRUE only when the inequality is provable from
// the supplied assumptions; FALSE means "unknown OR disproven" — callers must
// not interpret a false result as the negation of the predicate.
//
// Proof strategy (in order, all sound):
//   1. Direct: `symbolic::is_true(Op(a, b))` for trivially decidable cases.
//   2. Interval: compute `lower(a-b)` / `upper(a-b)` via `BoundAnalysis` and
//      compare against zero.
//   3. Min/Max descent: when the residue contains a `Min`/`Max` subexpression
//      in a monotone-nondecreasing position (e.g. additive top-level), recurse
//      on each replacement that yields a sound bound on the residue.
//
// Affine expressions over symbols with assumption-derived bounds are the
// expected input shape (subscript indices, stride differences). The descent
// is sound for these; for arbitrary expressions the interval step is the
// guaranteed-sound floor.

bool is_nonneg(const Expression& expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight = false);

bool is_positive(const Expression& expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight = false);

bool is_nonpos(const Expression& expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight = false);

bool is_negative(const Expression& expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight = false);

bool is_ge(
    const Expression& a,
    const Expression& b,
    const SymbolSet& parameters,
    const Assumptions& assumptions,
    bool tight = false
);

bool is_gt(
    const Expression& a,
    const Expression& b,
    const SymbolSet& parameters,
    const Assumptions& assumptions,
    bool tight = false
);

bool is_le(
    const Expression& a,
    const Expression& b,
    const SymbolSet& parameters,
    const Assumptions& assumptions,
    bool tight = false
);

bool is_lt(
    const Expression& a,
    const Expression& b,
    const SymbolSet& parameters,
    const Assumptions& assumptions,
    bool tight = false
);

bool is_eq(
    const Expression& a,
    const Expression& b,
    const SymbolSet& parameters,
    const Assumptions& assumptions,
    bool tight = false
);
 
// ---- BoundAnalysis-based overloads (cache-amortized) ----
//
// These overloads route all internal interval queries through the supplied
// `BoundAnalysis`, so the cache amortizes across many predicate calls under
// the same `(parameters, assumptions, tight)` triple. They omit the empty-
// parameter fallback that the legacy overloads perform when the caller's
// parameter set is non-empty; this fallback is a no-op for callers that
// already use empty parameters (e.g. `delinearize`) and matters only when
// proving inequalities about parameters themselves.

bool is_nonneg(const Expression& expr, BoundAnalysis& ba);

bool is_positive(const Expression& expr, BoundAnalysis& ba);

bool is_nonpos(const Expression& expr, BoundAnalysis& ba);

bool is_negative(const Expression& expr, BoundAnalysis& ba);

bool is_ge(const Expression& a, const Expression& b, BoundAnalysis& ba);

bool is_gt(const Expression& a, const Expression& b, BoundAnalysis& ba);

bool is_le(const Expression& a, const Expression& b, BoundAnalysis& ba);

bool is_lt(const Expression& a, const Expression& b, BoundAnalysis& ba);

bool is_eq(const Expression& a, const Expression& b, BoundAnalysis& ba);

class AssumptionsBounds {
public:
    explicit AssumptionsBounds(const Assumptions& assums)
        : assums_(assums), loose_(empty_params(), assums, /*tight=*/false, DELINEARIZATION_PROOF_BUDGET),
          tight_(empty_params(), assums, /*tight=*/true, DELINEARIZATION_PROOF_BUDGET) {
    }
 
    const Assumptions& assums() const {
        return assums_;
    }
    BoundAnalysis& loose() {
        return loose_;
    }
    BoundAnalysis& tight() {
        return tight_;
    }

    bool is_nonneg(const Expression& expr, const SymbolSet& parameters);
    bool is_positive(const Expression& expr, const SymbolSet& parameters);

    std::unordered_map<
        Expression,
        std::shared_ptr<const DelinearizeResult>,
        SymEngine::RCPBasicHash,
        SymEngine::RCPBasicKeyEq>&
    delinearize_memo() {
        return delinearize_memo_;
    }
 
private:
    static const SymbolSet& empty_params() {
        static const SymbolSet kEmpty;
        return kEmpty;
    }
 
    const Assumptions& assums_;
    BoundAnalysis loose_;
    BoundAnalysis tight_;
 
    // Keyed by (strict, parameter names), then expression.
    std::unordered_map<
        std::string,
        std::unordered_map<Expression, bool, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq>>
        proof_memo_;
 
    std::unordered_map<
        Expression,
        std::shared_ptr<const DelinearizeResult>,
        SymEngine::RCPBasicHash,
        SymEngine::RCPBasicKeyEq>
        delinearize_memo_;
};
 
} // namespace symbolic
} // namespace sdfg