## TP5 - Reduced products

The goal of this session is to implement in our analyzer the reduced products between two simple non-relational domains: the interval domain and the parity domain.

#### Parity domain

A first (straightforward) step is to implement a parity domain, able to discover whether each
variable is even or odd. We suggest implementing a domain able to abstract a set of integers into a
parity information (`VALUE_DOMAIN`

signature), and apply it to the
generic `NonRelational`

functor we developed in the previous
sessions, able to lift a `VALUE_DOMAIN`

into an
`ENVIRONMENT_DOMAIN`

by assigning an abstract property
independently to each variable.

#### Reduction

We wish to implement the reduced product in a generic way, with as few dependencies as possible on the domains we wish to combine.

Note that there are two choices: we can either develop a reduction at the
`ENVIRONMENT_DOMAIN`

level, or at the
`VALUE_DOMAIN`

level (as seen in the course). The later is simpler
but is limited to non-relational domains. Nevertheless, we suggest working at the
`VALUE_DOMAIN`

level for simplicity, as this is all what is needed
to combine intervals and parities.

Ideally, the reduced product is then a generic functor
`ReducedProduct`

taking **three** arguments:

- a first abstract domain module
`A:VALUE_DOMAIN`

; - a second abstract domain module
`B:VALUE_DOMAIN`

; - a module containing only the reduction function between the two domains:
`val reduce: A.t -> B.t -> A.t * B.t`

and the functor outputs a module of signature `VALUE_DOMAIN`

.

(equivalently, the functor can take a single module argument that packs the two abstract domains and a reduction function)

That way, given two existing domain implementations, building their reduced product boils down to implementing only one new module, with a single function.