overhaul the formula hierarchy

The current mix of subclass with operator types is a mess.

Consider an implentation of all operators as the following struct:

struct node {
   enum operator op;
   int serial;    // also serves as a hash 
   int ref_count;
   int deg;       // number of children
   node[1] children;
};

At construction, the struct would be allocated with enough size for "deg" children, regardless of the node[1] type (which is there just because 0-sized arrays are unspecified in C++11). There is no hierarchy. Visitors are not needed anymore, and should be replaced with plain switch.

This struct can probably be packed (we do not need 32 bits for each of the first 4 fields.)

A formula class can be used to encapsulate a node* and perform automatic reference counting.

(This design is inspired by the code of CVC4.)