Encoding first order formula (or its tree) into binary string?
There is one encoding scheme which is particularly obvious. Under this encoding scheme, the encoding of the formula $a \Rightarrow (b \Rightarrow a)$ is
$$ a \Rightarrow (b \Rightarrow a). $$
A C program can parse this string into a tree if it needs to, but it's up to the program.

It is of course possible to think of many other encoding schemes, but unless you are interested in very weak complexity classes, the exact encoding scheme doesn't matter.

There is one fine point here: the alphabet is finite, but there could be formulas with arbitrarily many variables. There are many ways to solve this problem. For example, you can name variables in the form "$v$ + number", for example $v5$, $v107$, and so on. This uses only a finite alphabet (since we encode the number in decimal, using 10 symbols).