Hello,
The Function shortcut creates an uninterpreted function application (i.e. you are asking the solver to find an interpretation for the function that satisfies the formula).
For example:
ftype1 = FunctionType(REAL, [REAL]) # Create the function type real -> real
ftype2 = FunctionType(REAL, [REAL, INT]) # Create the function type real -> int -> real
f = Symbol("f", ftype1) # Create a function f that maps reals to reals
g = Symbol("g", ftype2) # Create a function g that maps pairs of reals * int to reals
check = Equals(Function(f, [Real(1)]), Function(g, (Real(2), Int(4))) # f(1) = g(2.0, 4)
check_sat(check) # returns true, because it is possible to construct a function f and a function g respecting the constraints
check2 = And(check, Equals(Function(f, [Real(1)]), Real(2)), Equals(Function(g, (Real(2), Int(4)), Real(3)) # f(1.0) = g(2.0, 4) & f(1.0) = 2.0 & g(2.0, 4) = 3.0
check_sat(check2) # returns false, because it is not possible to construct a function f and a function g respecting the constraints
Hope this helps,
Andrea