CODEWITHSUNDEEP
numpyz3pymathematical-expressions
soolidsnake
soolidsnake

Reputation: 33

Mathematic equation

I have this equation : S = val.X^3 - val.X^2 + val.X -val

Knowing that all the the variables are int64, and S and val are known values,

what is the best way to solve it, I used numpy and Z3, but can't get the right answer, any lead would be helpful

Upvotes: -1

Views: 181

Answers (3)

ryu
ryu

Reputation: 1

s=val.x^3.x^2 + val.x - val

int64 and s.val are known values z3 are numphy unit.

s¹=val/3.to unit x divide xΔ2 initial by x-val-¹ proper add calculation to numpy unit

z3=val/int64 (z3 to unit val(x-val) divide unit as initial val3-²

Upvotes: -2

alias
alias

Reputation: 30460

Here's how you can code this using z3py, for the purposes of this example, I took S to be 40 and Val to be 2, but you can modify those values easily below in the corresponding lines for s.add:

from z3 import *

S   = BitVec ('S', 64)
X   = BitVec ('X', 64)
Val = BitVec ('Val', 64)

s = Solver()
s.add (S == 40)
s.add (Val == 2)
s.add (S == Val * X * X * X - Val * X * X + Val * X - Val)

res = s.check()

if res == sat:
   print s.model()
elif res == unsat:
   print "No solution"
else:
   print "Solver returned: " + res

When I run it, I get:

$ python b.py
[X = 4611686018427387907, Val = 2, S = 40]

This might look surprising, but remember that bit-vector arithmetic is modular; if you do the computation, you'll see that it indeed satisfies your equation.

Upvotes: 0

Victor Polo De Gyves Montero
Victor Polo De Gyves Montero

Reputation: 1097

This is adapted from https://docs.scipy.org/doc/numpy-1.13.0/reference/generated/numpy.roots.html

>>> import numpy as np
>>> valA=2.1
>>> valC=4.3
>>> valD=5.4
>>> valB=3.2
>>> coeff = [valA, valB, valC, valD]
>>> np.roots(coeff)
array([-1.38548682+0.j        , -0.06916135+1.36058497j,
   -0.06916135-1.36058497j])
>>>

Upvotes: 0

Related Questions