import type { UnsafeZ3Api, EmscriptenModule, Z3_context, Z3_ast, Z3_rcf_num, RcfInterval } from './types.js';
/**
 * Exact string extraction with explicit length.
 *
 * Z3_get_lstring returns a C string pointer and writes the length to
 * an out-param. This avoids lossy UTF8ToString conversions for strings
 * that contain null bytes or where exact length matters.
 *
 * C signature:
 *   Z3_char_ptr Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length)
 */
export declare function getExactString(mod: EmscriptenModule, raw: UnsafeZ3Api, ctx: Z3_context, ast: Z3_ast): {
    str: string;
    length: number;
};
/**
 * Exact floating-point sign extraction.
 *
 * Returns the sign bit of an FP numeral. False = positive, true = negative.
 * Throws if the AST is NaN (invalid argument per Z3 docs).
 *
 * C signature:
 *   bool Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, bool* sgn)
 */
export declare function getFpaSign(mod: EmscriptenModule, raw: UnsafeZ3Api, ctx: Z3_context, ast: Z3_ast): {
    success: boolean;
    isNegative: boolean;
};
/**
 * Extract interval information for an algebraic real value.
 *
 * Returns the lower and upper bounds of the isolating interval,
 * along with whether each bound is infinite or open.
 *
 * C signature:
 *   int Z3_rcf_interval(Z3_context c, Z3_rcf_num a,
 *     bool* lower_is_inf, bool* lower_is_open, Z3_rcf_num* lower,
 *     bool* upper_is_inf, bool* upper_is_open, Z3_rcf_num* upper)
 */
export declare function getRcfInterval(mod: EmscriptenModule, raw: UnsafeZ3Api, ctx: Z3_context, a: Z3_rcf_num): {
    result: number;
    interval: RcfInterval;
};
//# sourceMappingURL=model-inspection.d.ts.map