Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    4128ce89
    Decouple ADT-dependencies from solvers · 4128ce89
    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
    4128ce89
    History
    Decouple ADT-dependencies from solvers
    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