gistfile1.txt

stephentu@fender ~$ ipython
Python 2.7.9 |Continuum Analytics, Inc.| (default, Mar  9 2015, 16:20:48) 
Type "copyright", "credits" or "license" for more information.

IPython 3.1.0 -- An enhanced Interactive Python.
Anaconda is brought to you by Continuum Analytics.
Please check out: http://continuum.io/thanks and https://binstar.org
?         -> Introduction and overview of IPython's features.
%quickref -> Quick reference.
help      -> Python's own help system.
object?   -> Details about 'object', use 'object??' for extra details.

In [1]: from z3 import *

In [2]: s = Solver()

In [3]: a, b, ep = Real('a'), Real('b'), Real('ep')

In [5]: s.add (ep > 0)

In [6]: s.add(a > 0)

In [8]: s.add( ((1+a)**4-1)/4 + ((1+a)**2)*(b*b) + (b**4) - ep*( (a**4) + a*a*b*b + (b**4) + a*a + b*b ) <= ((1+a)**2-1)/2 + b*b )

In [9]: s
Out[9]: 
[ep > 0,
 a > 0,
 ((1 + a)**4 - 1)/4 + (1 + a)**2*b*b + b**4 -
 ep*(a**4 + a*a*b*b + b**4 + a*a + b*b) <=
 ((1 + a)**2 - 1)/2 + b*b]

In [10]: s.add( a*a/2 + b*b >= 10000 * ep )

In [14]: s.add(ep <= 0.1)

In [15]: s.check()
Out[15]: unsat