z3 - Procedural Attachment in Z3

Question

I am using z3py I have a predicate over two integers that needs to be evaluated using a custom algorithm. I have been trying to get it implemented, without much success. Apparently, what I need is a procedural attachment, which is now deprecated. Could anybody tell me how I might impelement this in z3py? I understand that it involves use of Tactics, but I am afraid I haven't managed to figure out how to use them. I wouldn't mind using the deprecated way either, as long as it works.

Answer 1

没有程序性依附策略。所有战术都在Z3内部实现；你可以从外面制定战术。以前版本的 Z3 公开了一种注册“用户理论”的方法。这已被弃用，因为 (1) Z3 的源代码现在可用，因此用户可以直接使用他们的自定义理论进行编译，(2) 用户理论抽象缺乏对模型生成的适当支持。您当然可以尝试具有用户理论扩展的以前版本的 Z3，但不支持。