Z3 中的程序附件 [英] Procedural Attachment in Z3

问题描述

我正在使用 z3py 我有一个关于需要使用自定义算法评估的两个整数的谓词.我一直在努力实现它，但没有取得多大成功.显然，我需要的是一个程序附件，现在已弃用.有人能告诉我如何在 z3py 中实现这个吗?我知道它涉及使用 Tactics，但恐怕我还没有弄清楚如何使用它们.我也不介意使用已弃用的方式，只要它有效.

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.

推荐答案

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

There is no procedural attachment tactic. All tactics are implemented inside of Z3; you can compose tactics from outside. Previous versions of Z3 exposed a way to register a "user theory". This was deprecated since (1) the source of Z3 is now available so users can compile with their custom theories directly, (2) the user-theory abstraction lacked proper support for model generation. You can of course try previous versions of Z3 that have the user theory extension, but it is not supported.

这篇关于Z3 中的程序附件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！