z3: do the orders of constraints being asserted affect the orders they are evaluated?

Question

My z3py code is doing inference and experiencing some performance (latency) issues. Currently I am trying to come up with some heuristics to prune the search space to hopefully boost the speed of inference.

My question is: do the orders of constraints being asserted affect the orders they are evaluated? In other words, if a constraint can significantly reduce the search space, should I assert it first so that, after being evaluated, many impossible solutions will be rule out at an early stage?

Answer 1

The ordering of assertions can make a difference for the heuristics later, but there is no pre-defined order that would perform the "best". Asserting particular constraints earlier does, in general, not mean that they will be solved first.