CodePlexProject Hosting for Open Source Software
Documentation Stackoverflow
Example Grammar:
E ::= E + E | n
I need to prove that the grammar is ambiguous due to the following two paths:
E -> E + E -> E + E + E -> n + E + E E -> E + E -> n + E -> n + E + E
The idea is that one would compare the functions "sets" symbol1(symbol,index,time) (for a specific time t) and symbol2(symbol,index,time) - finding where they are equivalent - however having a different predecessor (i.e at time t-1)
The problem is I have no idea how to compare the two functions symbol1 and symbol2
I can post the code, if you're interested .... (its about a page and half worth, but that might be inappropriately long?).
The code is written in Z3Py.
I am using the following code:
eps = MkInfinitesimal() print(( (1 + eps)**2- 1**2)/eps < 2.00000000001) print(( (1 + eps)**2- 1**2)/eps > 2)
and the output is:
True True
Other example: Proving that diff(x^2, x) = 2*pi when x = pi and diff(x^2,x) = 2*e when x = e
Code:
eps1 = MkInfinitesimal() eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 pi = Pi() e = E() print(( (pi + eps2)**2- pi**2)/eps2 < 2*pi + eps1) print(( (pi + eps2)**2- pi**2)/eps2 > 2*pi) print(( (e + eps2)**2- e**2)/eps2 < 2*e + eps1) print(( (e + eps2)**2- e**2)/eps2 > 2*e)
Output:
True True True True
Other example: Proving that diff(x^3, x) = 3*x^2 when x = e or x = pi.
eps1 = MkInfinitesimal() eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 pi = Pi() e = E() print(( (pi + eps2)**3- pi**3)/eps2 < 3*pi**2 + eps1) print(( (pi + eps2)**3- pi**3)/eps2 > 3*pi**2) print(( (e + eps2)**3- e**3)/eps2 < 3*e**2 + eps1) print(( (e + eps2)**3- e**3)/eps2 > 3*e**2)
Other example:
[x] = MkRoots([-1, -1, 0, 0, 0, 1]) [y] = MkRoots([-197, 3131, -31*x**2, 0, 0, 0, 0, x]) [z] = MkRoots([-735*x*y, 7*y**2, -1231*x**3, 0, 0, y]) print(x.decimal(10)) print(y.decimal(10)) print(z.decimal(10)) eps1 = MkInfinitesimal() eps2 = MkInfinitesimal() # eps2 is infinitely smaller thant eps1 print(( (x + eps2)**2- x**2)/eps2 < 2*x + eps1) print(( (x + eps2)**2- x**2)/eps2 > 2*x) print(( (y + eps2)**2- y**2)/eps2 < 2*y + eps1) print(( (y + eps2)**2- y**2)/eps2 > 2*y) print(( (z + eps2)**2- z**2)/eps2 < 2*z + eps1) print(( (z + eps2)**2- z**2)/eps2 > 2*z)
1.1673039782? 0.0629726948? 31.4453571397? True True True True True True
This proof is correct? Please let me know if you know a better proof. Many thanks.
In Complex numbers in Z3 Leonardo de Moura was able to introduce and to compute with complex numbers in Z3.
Using the code proposed by Leonardo I am introducing and computing with quaternion numbers in Z3 according with the code presented here. Using this "quaternion " code I am solving the following problem:
x = Quaternion("x") s = Tactic('qfnra-nlsat').solver() s.add(x*x + 30 == 0, x.i3 > 0, x.i2 >0, x.i1 > 0) print(s.check()) m = s.model() print m
and the corresponding output is:
sat [x.r = 0, x.i1 = 1, x.i2 = 1, x.i3 = 5.2915026221?]
This result was verified using Maple.
x = Quaternion("x") y = Quaternion("y") z = Quaternion("z") s = Tactic('qfnra-nlsat').solver() s.add(x*y + 30 + x + y*z == 0, x - y + z == 10) print(s.check()) m = s.model() print m
sat [y.r = 1/8, z.r = 2601/64, y.i1 = 1/2, z.i1 = 45/8, y.i2 = -1/2, z.i2 = -45/8, y.i3 = -1/2, z.i3 = -45/8, x.i3 = 41/8, x.i2 = 41/8, x.i1 = -41/8, x.r = -1953/64]
Proving that
x * y != y * x
x = Quaternion("x") y = Quaternion("y") a1, b1, c1, d1 = Reals('a1 b1 c1 d1') a2, b2, c2, d2 = Reals('a2 b2 c2 d2') x.r = a1 x.i1 = b1 x.i2 = c1 x.i3 = d1 y.r = a2 y.i1 = b2 y.i2 = c2 y.i3 = d2 print simplify((x * y - y * x).r) print simplify((x * y - y * x).i1) print simplify((x * y - y * x).i2) print simplify((x * y - y * x).i3)
0 2·c2·d1 + -2·c1·d2 -2·b2·d1 + 2·b1·d2 2·b2·c1 + -2·b1·c2
Other example : Proving that the quaternions A = (1+ I)/sqrt(2), B =(1 + J)/sqrt(2) and C = (1 + K)/sqrt(2) generate a representation of the Braid Group, it is to say, we have that ABA = BAB , ACA = CAC and BCB = CBC.
A = Quaternion('A') B = Quaternion('B') C = Quaternion('C') A.r = 1/Sqrt(2) A.i1 = 1/Sqrt(2) A.i2 = 0 A.i3 = 0 B.r = 1/Sqrt(2) B.i1 = 0 B.i2 = 1/Sqrt(2) B.i3 = 0 C.r = 1/Sqrt(2) C.i1 = 0 C.i2 = 0 C.i3 = 1/Sqrt(2) print simplify((A*B*A-B*A*B).r) print simplify((A*B*A-B*A*B).i1) print simplify((A*B*A-B*A*B).i2) print simplify((A*B*A-B*A*B).i3) print "Proved : ABA = BAB:" print simplify((A*C*A-C*A*C).r) print simplify((A*C*A-C*A*C).i1) print simplify((A*C*A-C*A*C).i2) print simplify((A*C*A-C*A*C).i3) print "Proved : ACA = CAC:" print simplify((B*C*B-C*B*C).r) print simplify((B*C*B-C*B*C).i1) print simplify((B*C*B-C*B*C).i2) print simplify((B*C*B-C*B*C).i3) print "Proved : BCB = CBC:"
0 0 0 0 Proved : ABA = BAB. 0 0 0 0 Proved : ACA = CAC. 0 0 0 0 Proved : BCB = CBC.
Please let me know what do you think about the "quaternion" code and how the "quaternion" code can be improved. Many thanks.
The .net API has the following constructor for a Context:
Context (Dictionary< string, string > settings)
how to get a list of all the possible settings?
Specifically, I am interested in how to ask Z3 to produce an unsat core, ie the equivalent of the SMT lib produce-unsat-cores.
I'm actually using Z3py for scheduling solving problems and I'm trying to represent a 2 processors system where 4 process of different execution time must be done.
My actual data are :Process 1 : Arrival at 0 and execution time of 4Process 2 : Arrival at 1 and execution time of 3Process 3 : Arrival at 3 and execution time of 5Process 4 : Arrival at 1 and execution time of 2
I'm actually trying to represent each process while decomposing each in subprocess of equal time so my datatypes are like this :
Pn = Datatype('Pn') Pn.declare('1') Pn.declare('2') Pn.declare('3') Pn.declare('4') Pt = Datatype('Pt') Pt.declare('1') Pt.declare('2') Pt.declare('3') Pt.declare('4') Pt.declare('5') Process = Datatype('Process') Process.declare('cons' , ('name',Pn) , ('time', Pt)) Process.declare('idle')
where pn and pt are the process name and the part of the process (process 1 is in 4 parts, ...)
But now I don't know how I can represent my processors to add 3 rules I need : unicity (each sub process must be done 1 and only 1 time by only 1 processor) check arrival (the first part of a process can't be processed before it arrived) and order (each part of a process must be processed after the precedent)So I was thinking of using arrays to represent my 2 processors with this kind of declaration :
P = Array('P', IntSort() , Process)
But when I tried to execute it I got an error message saying :
Traceback (most recent call last): File "C:\Users\Alexis\Desktop\test.py", line 16, in <module> P = Array('P', IntSort() , Process) File "src/api/python\z3.py", line 3887, in Array File "src/api/python\z3.py", line 3873, in ArraySort File "src/api/python\z3.py", line 56, in _z3_assert Z3Exception: 'Z3 sort expected'
And know I don't know how handle it... must I create a new datatype and figure a way to add my rules ? or Is there a way to add datatypes to array which would let me create rules like this :
unicity = ForAll([x,y] , (Implies(x!=y,P[x]!=P[y])))
Thanks in advance
I'm aware that there is a simplex solver implemented in z3. Is it possible to use the solver for linear optimization? Where is the interface for the solver located in the z3 source code?
How can I simplify the Boolean expression obtained as a result of evaluating an uninterpreted function? For instance, in the example: http://rise4fun.com/Z3/G8sL,
(eval (f x y))
yields (not (and (not x) (not y)))
I want to instead get the expression (or x y).
(simplify (eval (f x y))
gives an error.
Find the value of R in the following circuit
This problem is solved using the following code:
R, V1, V2, Vo = Reals('R V1 V2 Vo') I1 = V1/(R -50) I2 = V2/(R + 10) g = - R*(I1 + I2) print g equations = [Vo == g] print equations problem = [Vo == -2 , V1 == 1, V2 == 0.5, R != -10, R != 50, R > 0] solve(equations + problem)
-R·(V1/(R - 50) + V2/(R + 10)) [Vo = -R·(V1/(R - 50) + V2/(R + 10))] [R = 143.8986691902?, V2 = 1/2, V1 = 1, Vo = -2]
Other example: Find the value of R in the following circuit
R, Vs, Ve, R1, R2 = Reals('R Vs Ve R1 R2') g1 = (Vs - Ve)/R1 print g1 g2 = Ve/R2 print g2 equations = [g1 == g2, R1 == 2*R - 100, R2 ==R] print equations problem = [Vs == 35 , Ve == 15, R > 0, R1 >0, R2 >0] solve(equations + problem)
(Vs - Ve)/R1 Ve/R2 [(Vs - Ve)/R1 = Ve/R2, R1 = 2·R - 100, R2 = R] [R = 150, Ve = 15, Vs = 35, R2 = 150, R1 = 200]
Rf, Rg, Vo, V1, V2, R1, R2, I1, I2, V = Reals('Rf Rg Vo V1 V2 R1 R2 I1 I2 V') equations = [V1 - V == R1*I1, V - Vo == Rf*I1, V2 - V == R2*I2, V == Rg*I2] print equations problem = [V1 == 10 , V2 == 15, R1 == 100, R2 == 200, Rf == 100, Rg ==500] solve(equations + problem)
and the corresponding output is
[V1 - V = R1·I1, V - Vo = Rf·I1, V2 - V = R2·I2, V = Rg·I2] [I1 = -1/140, Vo = 80/7, Rg = 500, Rf = 100, R2 = 200, R1 = 100, V2 = 15, V1 = 10, I2 = 3/140, V = 75/7]
Rf, Rg, Vo, V1, V2, R1, R2, I1, I2, V = Reals('Rf Rg Vo V1 V2 R1 R2 I1 I2 V') equations = [V1 - V == R1*I1, V - Vo == Rf*I1, V2 - V == R2*I2, V == Rg*I2, Rf == 200 + Rg] print equations problem = [V1 == 10 , V2 == 15, R1 == 100, R2 == 200, Vo == 20, Rg > 0, Rf >0 ] solve(equations + problem)
[V1 - V = R1·I1, V - Vo = Rf·I1, V2 - V = R2·I2, V = Rg·I2, Rf = 200 + Rg] [I1 = -0.0113999063?, Rg = 577.2001872658?, Vo = 20, R2 = 200, R1 = 100, V2 = 15, V1 = 10, I2 = 0.0193000468?, V = 11.1399906367?, Rf = 777.2001872658?]
Vi, R1, I1, Va, R2, I2, R4, R3, Vo= Reals('Vi R1 I1 Va R2 I2 R4 R3 Vo') equations = [Vi == R1*I1, -Va == R2*I1, Va == R4*I2, Va - Vo ==R3*(I1-I2)] print equations problem = [Vi == 1, R1 == 1000, R2 == 1000, R3 == 1000, R4 == 10] solve(equations + problem)
[Vi = R1·I1, -Va = R2·I1, Va = R4·I2, Va - Vo = R3·(I1 - I2)] [R4 = 10, R3 = 1000, R2 = 1000, R1 = 1000, Vi = 1, Vo = -102, I2 = -1/10, Va = -1, I1 = 1/1000]
Vi, R1, I1, Va, R2, I2, R4, R3, Vo= Reals('Vi R1 I1 Va R2 I2 R4 R3 Vo') equations = [Vi == R1*I1, -Va == R2*I1, Va == R4*I2, Va - Vo ==R3*(I1-I2), R2 == R1 - 100, R3 == R1 - 200] print equations problem = [Vi == 1, Vo == -10, R4 == 10, R1 >0, R2 > 0, R3 >0] solve(equations + problem)
[Vi = R1·I1, -Va = R2·I1, Va = R4·I2, Va - Vo = R3·(I1 - I2), R2 = R1 - 100, R3 = R1 - 200] [I1 = 0.0030468970?, R1 = 328.2027496108?, I2 = -0.0695310291?, R4 = 10, Vo = -10, Vi = 1, R3 = 128.2027496108?, R2 = 228.2027496108?, Va = -0.6953102918?]
Vi, V1, R, I1, V2, Ri, I2, R1, Vo, RF, A= Reals('Vi V1 R I1 V2 Ri I2 R1 Vo RF A') equations = [Vi-V1 == R*I1,V1 -V2 == Ri*I2, V2 == R1*I2, V1 - Vo ==RF*(I1-I2), Vo==A* (V2-V1)] print equations problem = [Vi == 1, R1 == 2000, Ri == 100, RF == 1000, R == 300, A == 100] set_option(rational_to_decimal=True) solve(equations + problem)
[Vi - V1 = R·I1, V1 - V2 = Ri·I2, V2 = R1·I2, V1 - Vo = RF·(I1 - I2), Vo = A·(V2 - V1)] [I2 = 0.0001658374?, A = 100, R = 300, RF = 1000, Ri = 100, R1 = 2000, Vi = 1, Vo = -1.6583747927?, I1 = 0.0021724709?, V1 = 0.3482587064?, V2 = 0.3316749585?]
Vi, V1, R, I1, V2, Ri, I2, R1, Vo, RF, A= Reals('Vi V1 R I1 V2 Ri I2 R1 Vo RF A') equations = [Vi-V1 == R*I1,V1 -V2 == Ri*I2, V2 == R1*I2, V1 - Vo ==RF*(I1-I2), Vo==A* (V2-V1), RF == R + 1000, Ri == R + 500, R1 == R + 1500] print equations problem = [Vi == 1, A == 100, Vo == -2, R >0, RF >0, R1 >0] set_option(rational_to_decimal=True) solve(equations + problem)
[Vi - V1 = R·I1, V1 - V2 = Ri·I2, V2 = R1·I2, V1 - Vo = RF·(I1 - I2), Vo = A·(V2 - V1), RF = R + 1000, Ri = R + 500, R1 = R + 1500] [I2 = 0.0000150298?, R = 830.6885937397?, I1 = 0.0011375745?, Vo = -2, A = 100, Vi = 1, RF = 1830.6885937397?, V1 = 0.0550298124?, V2 = 0.0350298124?, R1 = 2330.6885937397?, Ri = 1330.6885937397?]
What value of the resistance RB will provide balance of the bridge yielding Vo = 0
V, RC, RD, I1, VB, RA,RB, I2, VA, V2, R1, I3, R2, V1, R3, R4, I4, Vo = Reals('V RC RD I1 VB RA RB I2 VA V2 R1 I3 R2 V1 R3 R4 I4 Vo') equations = [V == (RC+RD)*I1, VB == RD*I1, V == (RA + RB)*I2, VA == RB*I2, VB-V2 == R1*I3, V2 == R2*I3, VA-V1 == R3*I4, V1 - Vo == R4*I4, V2 == V1, RD == RB + 10] print equations problem = [Vo == 0, V == 5, R1 == 10, R2 == 12, R3 == 10, R4 == 22, RA ==1, RC ==1, RB >0, RD >0] set_option(rational_to_decimal=True) solve(equations + problem)
[V = (RC + RD)·I1, VB = RD·I1, V = (RA + RB)·I2, VA = RB·I2, VB - V2 = R1·I3, V2 = R2·I3, VA - V1 = R3·I4, V1 - Vo = R4·I4, V2 = V1, RD = RB + 10] [I1 = 0.3626991607?, RB = 2.7855295545?, I2 = 1.3208191688?, I4 = 0.1149744009?, I3 = 0.2107864017?, RC = 1, RA = 1, R4 = 22, R3 = 10, R2 = 12, R1 = 10, V = 5, Vo = 0, V1 = 2.5294368214?, V2 = 2.5294368214?, VA = 3.6791808311?, VB = 4.6373008392?, RD = 12.7855295545?]
Please let me know what do you think and if you know a more efficient code for these kind of problems. Many thanks.
Please let me know what do you think and if you know a more efficient code for this problem. Many thanks.
Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13