Rename Z3 class to Z3C0, create abstract Z3 base class

The Z3 helper class is specific to a partial order encoding.
All FN macros rely on these specifics.

Create abstract base class that has only the bare essentials.
Add clock SMT sort function for easier experiments
Add happens_before() function

If we change the SMT sort of clocks, their ordering might require
a different Z3 C++ operator, e.g. ult() for unsigned bit vectors.