
I was wondering if there is any way to use the solve function for real vector variables .
For example when I have the code:
c1= np.random.random_integers(5,5,size=(1,N))
x = RealVector('x', N)
solve(c1*x>0)
I get the error: "z3types.Z3Exception: 'True, False pr Z3 Boolean expression expected'
Thanks,


Coordinator
Dec 6, 2012 at 12:36 AM

When you write "c1*x", do you mean the dot product of the vectors c1 and x?
If that is the case, we can define the dot product function and write the problem as:
from z3 import *
import random
def dot_product(V1, V2):
return Sum([x*y for x, y in zip(V1, V2)])
N = 4
c = [ random.randint(5, 5) for i in range(N) ]
x = RealVector('x', N)
print dot_product(c, x)
solve(dot_product(c, x) > 0)

