import type { Expression, Param, EdictModule } from "../ast/nodes.js";
import type { SolverContext } from "./solver-context.js";
export interface TranslationContext {
    /** Solver context with high-level API (Int, Bool, Real, Solver, Not, And, Or, ...) */
    ctx: SolverContext;
    /** name → Z3 variable */
    variables: Map<string, any>;
    errors: TranslationError[];
    /** Module for function lookup during call inlining (optional) */
    module?: EdictModule;
    /** Current call inlining depth for recursion guard (default 0) */
    callDepth?: number;
    /** Functions currently being inlined to prevent recursion */
    visitedFunctions?: Set<string>;
}
export interface TranslationError {
    contractId: string;
    functionName: string;
    unsupportedNodeKind: string;
}
/**
 * Create Z3 variables for each function parameter based on Param.type.
 * Returns false if any param has an unsupported type (no Z3 variable created for it).
 */
export declare function createParamVariables(tctx: TranslationContext, params: Param[]): boolean;
/**
 * Translate an Edict Expression to a Z3 expression.
 * Returns null for unsupported expression kinds (pushes TranslationError).
 */
export declare function translateExpr(tctx: TranslationContext, expr: Expression, contractId: string, functionName: string): any | null;
/**
 * Walk an Expression[] accumulating `let` bindings, returning the last
 * expression's Z3 translation. Used by: if branches, match arms, block
 * bodies, and function body walking in verify.ts.
 */
export declare function translateExprList(tctx: TranslationContext, exprs: Expression[], contractId: string, functionName: string): any | null;
//# sourceMappingURL=translate.d.ts.map