Look-up table generator
root
Requires SWI-Prolog + Z3.
Usage:
$ swipl -s luts.pl
?- solve(Bits, Table, MaxSize, Expr).
where:
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.
Example:
?- 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