\myheading{Art of problem solving}

\url{http://artofproblemsolving.com/wiki/index.php?title=2017_AMC_12A_Problems/Problem_2}:

\begin{lstlisting}
The sum of two nonzero real numbers is 4 times their product.
What is the sum of the reciprocals of the two numbers? 
\end{lstlisting}

We're going to solve this over real numbers:

\begin{lstlisting}[style=custompy]
from z3 import *

x, y = Reals('x y')

s=Solver()

s.add(x>0)
s.add(y>0)

s.add(x+y == 4*x*y)

print s.check()
m=s.model()
print "the model:"
print m
print "the answer:", m.evaluate (1/x + 1/y)
\end{lstlisting}

Instead of pulling values from the model and then compute the final result on Python's side, we can evaluate
an expression ($\frac{1}{x} + \frac{1}{y}$) \emph{inside} the model we've got:

\begin{lstlisting}
sat
the model:
[x = 1, y = 1/3]
the answer: 4
\end{lstlisting}