using 'solve' for real vector variables

Dec 5, 2012 at 11:21 PM

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 5, 2012 at 11:36 PM

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)