import type { FeasibilityIR } from './ir.js';
/** IR format version. Bump on any breaking change to the IR structure. */
export declare const FEASIBILITY_IR_VERSION = "1.0.0";
/** Target logic string carried on the IR and emitted into SMT-LIB.
 *  QF_SLIA = quantifier-free strings + linear integer arithmetic. */
export declare const FEASIBILITY_LOGIC = "QF_SLIA";
/** The requested action, distilled to the fields the obligation needs. Modeled
 *  on ActionIntent.action (src/types/policy.ts) but kept minimal and decoupled
 *  so the compiler is a pure function of plain data. */
export interface FeasibilityPolicyInput {
    /** The scope the action requires, e.g. 'data:read'. */
    scopeRequired: string;
    /** Spend the action would consume, if any. */
    spend?: number;
    /** ISO 8601 timestamp the action is evaluated at. Used only to encode the
     *  temporal-window obligation as a constraint; it is NOT read from a clock. */
    evaluatedAt?: string;
}
/** The granted delegation envelope, distilled to the fields the obligation
 *  needs. Modeled on Delegation (src/types/passport.ts). */
export interface FeasibilityDelegationInput {
    /** Scopes granted by the delegation. */
    scope: string[];
    /** Spend ceiling, if the delegation carries one. */
    spendLimit?: number;
    /** Spend already consumed under this delegation. */
    spentAmount?: number;
    /** Max delegation depth permitted. */
    maxDepth: number;
    /** Current depth of this delegation in its chain. */
    currentDepth: number;
    /** Delegation expiry, ISO 8601. */
    expiresAt: string;
    /** Delegation not-valid-before, ISO 8601, if set. */
    notBefore?: string;
    /** Whether the delegation has been revoked. */
    revoked?: boolean;
}
/** Inputs to {@link compileFeasibility}. */
export interface CompileFeasibilityInput {
    policy: FeasibilityPolicyInput;
    delegation: FeasibilityDelegationInput;
}
/** Compile a policy + delegation envelope into the feasibility IR.
 *  Pure and deterministic: no clock, no randomness, sorted output. */
export declare function compileFeasibility(input: CompileFeasibilityInput): FeasibilityIR;
/** Emit a deterministic SMT-LIB 2 string for a feasibility IR.
 *  Pure function of the IR; same IR always yields the same string. The emitted
 *  script declares the variables, asserts each constraint, and ends with
 *  (check-sat). It introduces no solver dependency: it is text the caller may
 *  hand to any SMT solver out of band. This module does not run a solver. */
export declare function emitSmtLib(ir: FeasibilityIR): string;
/** Convenience: compile then emit SMT-LIB in one call. Deterministic. */
export declare function compileToSmtLib(input: CompileFeasibilityInput): string;
//# sourceMappingURL=compiler.d.ts.map