We present Affinitree, a compositional framework for analyzing Deep Neural Networks (DNNs) based on three elementary principles: (1) symbolic execution, (2) infeasible path elimination, and (3) abstraction. The combination of these principles allows one to elegantly solve a number of interesting analysis and verification tasks, like traditional verification problems with pre- and post-conditions, model explanations in terms of semantically equivalent decision trees, concolic execution for slice-oriented testing, and visual verification of two-dimensional slices. The paper illustrates the flexibility of Affinitree over three different use cases covering fairness evaluation, adversarial examples, and counterfactuals. Affinitree is available as a modular open source library for replication, experimentation, and extension.