import { type Lattice, Top } from './lattice';
/**
 * The default limit of inferred constraints in {@link AbstractDomain|AbstractDomains}.
 */
export declare const DEFAULT_INFERENCE_LIMIT = 50;
/**
 * An abstract domain as complete lattice with a widening operator, narrowing operator, concretization function, and abstraction function.
 * All operations of value abstract domains should not modify the domain in-place but return new values using {@link create}.
 * @template Concrete - Type of an concrete element of the concrete domain for the abstract domain
 * @template Abstract - Type of an abstract element of the abstract domain representing possible elements (excludes `Top` and `Bot`)
 * @template Top      - Type of the Top element of the abstract domain representing all possible elements
 * @template Bot      - Type of the Bottom element of the abstract domain representing no possible elements
 * @template Value    - Type of the abstract elements of the abstract domain (defaults to `Abstract` or `Top` or `Bot`)
 */
export declare abstract class AbstractDomain<Concrete, Abstract, Top, Bot, Value extends Abstract | Top | Bot = Abstract | Top | Bot> implements Lattice<Abstract, Top, Bot, Value> {
    protected readonly _value: Value;
    constructor(value: Value);
    get value(): Value;
    abstract create(value: Abstract | Top | Bot): this;
    abstract top(): this & AbstractDomain<Concrete, Abstract, Top, Bot, Top>;
    abstract bottom(): this & AbstractDomain<Concrete, Abstract, Top, Bot, Bot>;
    abstract equals(other: this): boolean;
    abstract leq(other: this): boolean;
    abstract join(other: this): this;
    /**
     * Joins the current abstract value with multiple other abstract values.
     */
    joinAll(values: readonly this[]): this;
    abstract meet(other: this): this;
    /**
     * Meets the current abstract value with multiple other abstract values.
     */
    meetAll(values: readonly this[]): this;
    /**
     * Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
     */
    abstract widen(other: this): this;
    /**
     * Narrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
     */
    abstract narrow(other: this): this;
    /**
     * Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain.
     * The result should be `Top` if the number of concrete values would reach the `limit` or the resulting set would have infinite many elements.
     */
    abstract concretize(limit: number): ReadonlySet<Concrete> | typeof Top;
    /**
     * Maps a set of possible concrete values into an abstract value as abstraction function of the abstract domain (should additionally be provided as static function).
     */
    abstract abstract(concrete: ReadonlySet<Concrete> | typeof Top): this;
    abstract toJson(): unknown;
    abstract toString(): string;
    abstract isTop(): this is AbstractDomain<Concrete, Abstract, Top, Bot, Top>;
    abstract isBottom(): this is AbstractDomain<Concrete, Abstract, Top, Bot, Bot>;
    abstract isValue(): this is AbstractDomain<Concrete, Abstract, Top, Bot, Abstract>;
    /**
     * Joins an array of abstract values by joining the first abstract value with the other values in the array.
     * The provided array of abstract values must not be empty or a default value must be provided!
     */
    static joinAll<Domain extends AnyAbstractDomain>(values: Domain[], defaultValue?: Domain): Domain;
    /**
     * Meets an array of abstract values by meeting the first abstract value with the other values in the array.
     * The provided array of abstract values must not be empty or a default value must be provided!
     */
    static meetAll<Domain extends AnyAbstractDomain>(values: Domain[], defaultValue?: Domain): Domain;
    /**
     * Converts an element of an abstract domain into a string.
     */
    static toString(this: void, value: AnyAbstractDomain | unknown): string;
}
/**
 * A type representing any abstract domain without additional information.
 */
export type AnyAbstractDomain = AbstractDomain<unknown, unknown, unknown, unknown>;
/**
 * The type of the abstract values of an abstract domain (including the Top and Bottom element).
 * @template Domain - The abstract domain to get the abstract value type for
 */
export type AbstractValue<Domain extends AnyAbstractDomain> = Domain extends AbstractDomain<unknown, infer Value, infer Top, infer Bot> ? Value | Top | Bot : never;
/**
 * The type of the concrete domain of an abstract domain.
 * @template Domain - The abstract domain to get the concrete domain type for
 */
export type ConcreteDomain<Domain extends AnyAbstractDomain> = Domain extends AbstractDomain<infer Concrete, unknown, unknown, unknown> ? Concrete : never;
/**
 * The type of an abstract domain holding an abstract value of the domain.
 * @template Domain - The abstract domain abstract domain value type for
 */
export type AbstractDomainValue<Domain extends AnyAbstractDomain> = Domain extends AbstractDomain<infer Concrete, infer Value, infer Top, infer Bot> ? Domain & AbstractDomain<Concrete, Value, Top, Bot, Value> : never;
/**
 * The type an abstract domain holding the Top element (greatest element) of the domain.
 * @template Domain - The abstract domain to get the abstract domain top for
 */
export type AbstractDomainTop<Domain extends AnyAbstractDomain> = Domain extends AbstractDomain<infer Concrete, infer Value, infer Top, infer Bot> ? Domain & AbstractDomain<Concrete, Value, Top, Bot, Top> : never;
/**
 * The type an abstract domain holding the Bottom element (least element) of the domain.
 * @template Domain - The abstract domain to get the abstract domain bottom for
 */
export type AbstractDomainBottom<Domain extends AnyAbstractDomain> = Domain extends AbstractDomain<infer Concrete, infer Value, infer Top, infer Bot> ? Domain & AbstractDomain<Concrete, Value, Top, Bot, Bot> : never;