-
Etienne Kneuss authored
- ADTManager is responsible for computing dependencies between ADTs so that definitions can be grouped. - Simplify and generalize solver handling of RawArrays. - Remove dead-code in fair-z3 to parse non-ground models. - OptionManager was mostly useless, moved *Type to Library - MapGet can be implemented as (Some-value (Select m k)), as the solver will treat Some-value as uninterpreted if Select yields a None
Etienne Kneuss authored- ADTManager is responsible for computing dependencies between ADTs so that definitions can be grouped. - Simplify and generalize solver handling of RawArrays. - Remove dead-code in fair-z3 to parse non-ground models. - OptionManager was mostly useless, moved *Type to Library - MapGet can be implemented as (Some-value (Select m k)), as the solver will treat Some-value as uninterpreted if Select yields a None