fused many-multiply-add and better SAT encoding for binary

make a function [a] -> [a] -> a for scalar product (with default impl)

and make an encoding that directly builds the wallace tree or similar