import type { TranslationContext } from "./translate.js";
import type { SemanticAssertion } from "../ast/nodes.js";
/**
 * Translate a SemanticAssertion into a Z3 boolean expression.
 *
 * Uses symbolic Z3 arrays (`ArraySort(IntSort, IntSort)`) and quantified
 * formulas. The `target` field names the array variable (e.g., `"result"`),
 * and `args` provides assertion-specific parameters.
 *
 * @returns Z3 boolean expression, or null if translation fails
 */
export declare function translateSemanticAssertion(tctx: TranslationContext, semantic: SemanticAssertion): any | null;
//# sourceMappingURL=translate-semantic.d.ts.map