到目前为止，parallel_enable参数仍然导致此函数在单线程模式下工作并阻塞主线程

我认为您对此误解。 z3在并行模式下运行意味着您可以从单个Python线程调用它，然后它为自己生成多个OS级线程，从而完成工作，清理线程并为您返回结果。它不能奇迹般地使没有GIL的Python运行。
从Python的角度来看，它一次仍然执行一件事，而另一件事是调用z3。它一直保持着GIL。因此，如果在运行计算时看到一个以上的CPU内核/线程被使用，那是z3并行模式的影响，内部分支到多个线程。

还有另一件事，就是释放GIL，就像阻止I / O操作一样。魔术不会发生这种情况，为此有一个呼叫对：

  

PyThreadState * PyEval_SaveThread（）
  释放全局解释器锁（如果已创建），并将线程状态重置为NULL，返回先前的线程状态（非NULL）。如果已创建锁，则当前线程必须已获取它。

     

无效 PyEval_RestoreThread（PyThreadState * tstate）
  获取全局解释器锁（如果已创建），并将线程状态设置为 tstate ，该状态不能为NULL。如果已创建锁，则当前线程一定不能获取它，否则会发生死锁。

这些是C调用，因此扩展开发人员可以访问它们。当开发人员知道代码可以运行很长时间而无需访问Python内部时，可以使用PyEval_SaveThread()，然后Python可以继续使用其他Python线程。而且，无论什么时候做完，线程都可以重新引入自身，并使用PyEval_RestoreThread()申请GIL。
但是，只有当开发人员使它们发生时，这些事情才会发生。使用z3可能并非如此。

要直接回答您的问题：不，Python代码不能释放GIL并保持其释放状态，因为GIL是Python线程在处理过程中必须持有的锁。因此，每当返回Python“指令”时，GIL就会再次保留。

显然，我设法以某种方式不包含我想要的链接，所以它们位于页面https://docs.python.org/3/c-api/init.html#thread-state-and-the-global-interpreter-lock上（链接的段落讨论了我不久总结的内容）。

Z3是开放源代码（https://github.com/Z3Prover/z3），并且源代码既不包含PyEval_SaveThread，也不包含包装快捷键Py_BEGIN_ALLOW_THREADS的字符序列。

但是，它有一个并行的Python示例btw。 https://github.com/Z3Prover/z3/blob/master/examples/python/parallel.py，并

from multiprocessing.pool import ThreadPool

所以我认为它可能已经过测试并且可以与multiprocessing一起使用。