Finite function analysis and manipulation

I have searched for quite a while on algorithms/data structures or even
ready-made libraries for the following purpose:

I want to work with finite functions (ff) in the following way:

(I will be a bit sloppy about the exact definition of image and
preimage domains,
those can be easily checked, we may assume for the following,
that the functions always operate on a set of natural numbers 1 ... n;
by choosing a sufficiently large n we have only one domain in which we
have to work).

construction:
A) construct small finite functions, for instance by providing a table,
or an expression,
boolean equation, Binary-Decision-Diagram, etc.
B) Given two contructed ffs A and B form a new one by
B1) concatenation B \circ A
B2) Pairing: (A,B) (there are actually two ways of pairing,
either we mean x \mapsto (A(x),B(x)) or (x,y) \mapsto
(A(x),B(y)),
but this is essentially the same, as we can view the second
as concatenations
of projections and A resp. B)

Having constructed more complex functions this way, I want to analyse
the functions,
for instance:

(most of the following questions can equally formulated in terms of the
partition
the function creates on the pre-image set by the equivalence relation
x \equ y <==> F(x) = F(y))

1) Is the resulting function constant,
2) or more generally, how many images does it have, which are these
3) given a value, give one or all preimages for that value (in case it
exitsts)
4) give the size of the largest pre-image set resulting in the same
image
5) given two functions A and B (with same image and pre-image sets)
is one a refinement of the other, more precisely, does A(x) = A(y)
imply
B(x) = B(y)?

Not necessary, but desirable:
complexity of the function for implementation as a circuit,
including appropriate encodings for the inputs and outputs.

Of course all these are decidable, we could enumerate the
input space.
I also would not be surprised if an invidual problem of the above is
so hard, that it cannot be done essentially faster than input
enumeration.
BUT, if I do repeated operations, say, do an analysis of A and B, and
then
add a small function C and want to analyse (A \circ C, B);
aren't there chances that this can be much faster than repeated
enumeration?

Thank you very much,

Andreas

.