\myheading{SMT-solver as a calculator}

It's important to know that SMT-solver, like almost any \ac{PL}, can be used as a generic calculator.

\lstinputlisting[caption=Using Z3Py API,style=custompy]{equations/calc/1.py}

\lstinputlisting[caption=The result]{equations/calc/1.txt}

Or in SMT-LIB 2.0 form:

\lstinputlisting[style=customsmt]{equations/calc/2.smt}

\lstinputlisting[caption=The result]{equations/calc/2.txt}

Think about it as about electronic circuit -- you can build an adder out from full-adders and logic gates.
(We will do this soon: \ref{simple_adder}.)
Then you turn on your circuit and get the result at the adder's output.

Now the \textit{inverse calculator}.
Can we solve the equation like $x+3=17$?

\lstinputlisting[style=customsmt]{equations/calc/3.smt}

\lstinputlisting[caption=The result]{equations/calc/3.txt}

(0xe is 14.)