Z3 inefficient isTrue implementation

[ThomasHaas]

Z3's implementation of isTrue is

  protected boolean isTrue(Long pParam) {
    return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_TRUE);
  }

which in turn does at least 3 native calls.
Wouldn't it suffice to do the following?

  protected boolean isTrue(Long pParam) {
    return pParam.equals(z3True); // Z3 should only have a single instance of "true".
  }

Maybe there is a possibility to have multiple copies of the true value?

The reason that I'm asking is that the first implementation is considerably slower and it is very noticable when tracking the solver with the user propagators from #349. Indeed, on an Nqueens + propagator example, 1/3 (70 seconds!) of all time is spent just executing the isTrue function. The proposed solution is faster by at least two orders of magnitude.
I can fix this bottleneck directly in the user propagator (by just not using isTrue) but I would rather have a solution that benefits everyone (considering that isTrue/isFalse is called internally in many places).

[kfriedberger]

Thanks for your comment.
I reverted the changes from 819279b to avoid those JNI calls.
I have not measured any performance benefit, but it is possible if this method is called extensively.

[ThomasHaas]

Yeah, for the common use-case you won't notice much of a difference.
It only gets noticable when tracking the SMT solvers actions in the form of user propagators (though I decided to change the user propagator implementation to avoid isTrue).