\myheading{Why variables are declared using \textit{declare-fun}?}

They mean this is nullary function, only returning a constant, nothing else.

SMT-LIB language has no idea about variables.

Can you get rid of variables?
For example, in C/C++ you can use this function for $\Pi$ constant instead of accessing a constant variable or using
preprocessor macro:

\begin{lstlisting}
double PI ()
{
        return 3.1415926;
};
\end{lstlisting}

In SMT-LIB world, you don't declare variables, you declare argumentless functions that value is either fixed:

\begin{lstlisting}
...
(declare-fun const1 () (_ BitVec 32))
(assert (= const1 (_ bv214013 32)))
...
\end{lstlisting}

... or it's \textit{connected} to another expression/function's value/etc.
This is why variables are declared using \TT{declare-fun} directive.
(However, Z3 support \TT{declare-const} directive, which is merely a syntactic sugar.)

One can go further: there are programming languages with no variables,
but they are not very practical for our mundane endeavours:
\url{https://en.wikipedia.org/wiki/Lambda_calculus}.

(And to extreme minimalism:
\url{https://en.wikipedia.org/wiki/Iota_and_Jot},
\url{https://en.wikipedia.org/wiki/Unlambda}.)

LISP has borrowed from some features of lambda calculus, while SMT-LIB language is a very simplified LISP.