liblisa::encoding

Function merge_encodings_semantically

pub fn merge_encodings_semantically<A: Arch>(
    overlapping_groups: Vec<Vec<EncodingWithFilters<A, SynthesizedComputation>>>,
    solver: &impl SolverProvider,
) -> Vec<EncodingWithFilters<A, SynthesizedComputation>>
Expand description

Performs an eager merging of a collection of crate::encoding::Encodings.

Encodings are merged if they overlap and their semantics are equivalent. An SMT solver is used to determine if the semantics are equivalent.