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.)