I am trying to run the code below with Z3py and the main problem is that I want to find the arguments for my function using a solver. And I want to use the arguments as integer and real inside my function.
<code>
x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
</code>
<code>
x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
</code>
x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
However, this code results in a TypeError:’ArithRef’ object cannot be interpreted as an integer. I know I cannot use k as it is but I couldn’t find a way to make it work.
Is this possible? Thank you in advance!
I tried to write this as well:
<code>x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
</code>
<code>x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
</code>
x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable
s = Solver() #initialize the solver
#this is the function that takes x and k and does some calculations with them
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
x0 = 10
s.add(Exists((x,k), And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative
s.check()
This results in a ArgumentError: argument 2: <class ‘TypeError’>: wrong type
While z3py allows mixing/matching Python and z3 constructs, it does not allow for arbitrary python expressions to be used symbolically. (This would be an extremely hard thing to do.)
In particular, the call to range is not supported with a symbolic-variable.
Note that your loop over k creates a non-linear problem (multiplying variables together), which is already difficult for SMT solvers.
Your best bet would be to do an incremental search over k. Something like:
<code>from z3 import *
x = Real('x')
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
for k in range(10):
print(f"Trying k: {k}")
s = Solver()
s.add(x > 0)
s.add(And(f(x, k) < 0))
r = s.check()
if(r == sat):
print(s.model())
break
else:
print(f"Solver said: {r}")
</code>
<code>from z3 import *
x = Real('x')
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
for k in range(10):
print(f"Trying k: {k}")
s = Solver()
s.add(x > 0)
s.add(And(f(x, k) < 0))
r = s.check()
if(r == sat):
print(s.model())
break
else:
print(f"Solver said: {r}")
</code>
from z3 import *
x = Real('x')
def f(x, k):
for i in range(k):
x = x*1.099-1
return x
for k in range(10):
print(f"Trying k: {k}")
s = Solver()
s.add(x > 0)
s.add(And(f(x, k) < 0))
r = s.check()
if(r == sat):
print(s.model())
break
else:
print(f"Solver said: {r}")
This prints:
<code>Trying k: 0
Solver said: unsat
Trying k: 1
[x = 500/1099]
</code>
<code>Trying k: 0
Solver said: unsat
Trying k: 1
[x = 500/1099]
</code>
Trying k: 0
Solver said: unsat
Trying k: 1
[x = 500/1099]
You probably wanted to assert some other constraints to make this more interesting. (For instance, you have an Exists(x), which goes unused; but you also have x0 = 10. Not quite clear what you’re trying to express.)