mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

more examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-09 08:02:12 -08:00
parent 7a31c6bc74
commit 7ffba3ebf4
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/api/python/z3num.py
View file

@ -58,6 +58,29 @@ class Numeral:
True
>>> Numeral(m[x])**2
2
We can also isolate the roots of polynomials.
>>> x0, x1, x2 = RealVarVector(3)
>>> r0 = isolate_roots(x0**5 - x0 - 1)
>>> r0
[1.1673039782?]
In the following example, we are isolating the roots
of a univariate polynomial (on x1) obtained after substituting
x0 -> r0[0]
>>> r1 = isolate_roots(x1**2 - x0 + 1, [ r0[0] ])
>>> r1
[-0.4090280898?, 0.4090280898?]
Similarly, in the next example we isolate the roots of
a univariate polynomial (on x2) obtained after substituting
x0 -> r0[0] and x1 -> r1[0]
>>> isolate_roots(x1*x2 + x0, [ r0[0], r1[0] ])
[2.8538479564?]
"""
def __init__(self, num, ctx=None):
if isinstance(num, Ast):