how to use Numba to run z3py solver on GPU

Question

I want to run z3 solver methods such as 'solver.check()' on GPU using Numba to speed up solving. Is it possible? How can I do it?

I tested '@jit' but I can't get result.

Edit:

This is my code:

@jit
def solve(self, goal):
    solver = z3.Solver()
    solver.reset()
    solver.add(goal.as_expr())
    satisfiability = solver.check()  # Check satisfiability

goal parameter is z3 Goal object

Answer 1

No, this is not possible. Numba does not support all Python features nor all Python libraries. Please read the documentation for more information about this. Besides this, this is also not possible to run a CPU code on the GPUs because they are completely different hardware architectures (and even if this would be possible, the resulting code would be certainly much slower on GPUs). For more information please read: this and this.