Look-up table generator


Requires SWI-Prolog + Z3.

 $ swipl -s luts.pl
 ?- solve(Bits, Table, MaxSize, Expr).
 Bits is the bitwidth of all operations;
 Table is a list of input-output pairs;
 MaxSize is the maximum expression size to search (size = # of operations)
  (MaxSize > 3 can be very slow!);
 Expr is the output expression.

 ?- solve(8, [1-2,3-4,5-5,8-10], 3, Expr).
 Expr = binop(and, constant(15), binop(sub, constant(10), binop(lshr, constant(176), input(0)))).

Remember when implementing in C (or whatever), all operations are modulo 2^Bits.
Use type casts liberally!

Future work:
 * more operations (e.g. popcount &c.)
 * per-operation bit width limits
 * branches (ite)
 * processor-specific operation specification
 * C formatted output