Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment