First attempt to encode NetKAT axioms directly in Z3.

* Datatypes for (simplified) packets, predicates, policies.

* A relation Eq for equivalence.

* The KA-* axioms but for Policies only (these will have to be
  replicated for Predicates, since I don't see how to do the slick
  overloading trick)

* Currently looping on the (commented-out) KA-LFP-* axioms... :-/