Module Operator.ConcreteSource

Concrete interpreter using OCaml boolean and Z.t for values.

The interpreter values can be:

• {true, false, empty} for booleans;
• any Z.t or empty for integers;
• the set of bitvectors (represented by Z.t + empty). Empty is not an error, just a special value representing the absence of value.

But, considering that whenever an argument is empty, the result is empty, we can build an interpreter by focusing on the non-empty values, and just return an exception for the (infrequent) empty cases.