Support of complex type constraints

[sergeypospelov]

The PR adds complex type constraints:

• UIsSubtypeExpr
• UIsSupertypeExpr

Details

UTypeSolver

Extracted verify function to a separated class UTypeSolver to simplify configuring.

Previously, the constraint (%1 == 42 || %2 <: A) caused RE, because USolverBase and UTypeSolver didn't support propositional variables for type constraints. The PR fixes it in the following way:

• While translating type constraints, keep their mkConsts declarations.
• When decoding a model, iterate over its declarations and get those one, which refer to type constraints. Include their interpretation.
• When performing a type constraints check, in UTypeSolver include the information about interpreted UIsSubtypeExpr and UIsSupertypeExpr.
• If the current region becomes empty, then add the conflict lemma with the reference disequalities and related propositional variables.

UIsSupertypeExpr

Add a special type constraint for expressing the type of the ref is supertype of the subtype.

class UIsSupertypeExpr<Type> internal constructor(
    ctx: UContext,
    val ref: UHeapRef,
    val subtype: Type,
) : USymbol<UBoolSort>(ctx) { ... }

Now it's unused, but it's necessary for type connections and virtual invokes, which will be added in the future.

Minor

• Changed type of refs in equality constraints from UHeapRef to USymbolicHeapRef
• Introduced UTransformer
• Added explicit error reasons in expressions and components
• Made some renames in UTypeSystem and related entities
• Added some simple optimizations in UTypeRegion

PR TODO:

• Tests
• Fix TODOs
• Comments
• Description

[sergeypospelov]

@Damtev, could you review again? Unresolve conversations if something is unclear.

[Damtev]

LGTM