TODO

----------------------------------------------------------------------

support for debugging / understanding optimizations
- inference of undefs on the RHS (and LHS?) to help spot badly specified
  optimizations
- (optionally) print stuff like...
  - inferred types of operands, including range of bitwidths
  - inferred icmp conditions that work
  - which registers are ins and outs on the LHS and RHS
  - DAG view of the LHS and RHS, with arrows connecting registers that
    are the same across the two
- optionally print example operands for correct optimizations, not just
  incorrect ones

support sets of things as previously implemented by David

figure out ways to deal wtih solver timeout
- induction over bitwidth would be nice
- supporting multiple solvers would be nice

support definition of new symbols such as INT_MAX, John suggests macro semantics
- make these available by default via an implicit include file, perhaps

documentation

----------------------------------------------------------------------