在 Z3 中定义带约束的代数数据类型 [英] Defining algebraic datatypes with constraints in Z3

问题描述

我看过一些在线资料，用于定义 Z3 中的 IntList 等代数数据类型.我想知道如何定义具有逻辑约束的代数数据类型.例如，如何定义代表正整数的 PosSort.

I've seen some online materials for defining algebraic datatypes like an IntList in Z3. I'm wondering how to define an algebraic datatype with logical constraints. For example, how to define a PosSort that stands for positive integers.

推荐答案

您正在寻找的是谓词-子类型化；据我所知，Yices 是唯一支持它的 SMT 求解器:http://yices.csl.sri.com/old/language.shtml

What you are looking for is called predicate-subtyping; and as far as I know Yices is the only SMT solver that supported it out of the box: http://yices.csl.sri.com/old/language.shtml

特别是，请参阅此处的示例:http://yices.csl.sri.com/old/language.shtml#language_dependent_types

In particular, see the examples here: http://yices.csl.sri.com/old/language.shtml#language_dependent_types

不幸的是，这是旧的" Yices，我认为不再支持这种特定的输入语言.正如 Malte 所提到的，SMTLib 也不支持谓词子类型化.

Unfortunately, this is "old" Yices, and I don't think this particular input-language is supported any longer. As Malte mentioned, SMTLib doesn't have support for predicate subtyping either.

假设您的输出 SMTLib 是生成的"，您可以插入检查"以确保所有元素都保留在域内.但这比较麻烦，不明确如何处理偏袒.规格不足是一个很好的技巧，但它会变得非常麻烦，并导致非常难以调试的规格.

Assuming your output SMTLib is "generated," you can insert "checks" to make sure all elements remain within the domain. But this is rather cumbersome and it is not clear how to deal with partiality. Underspecification is a nice trick, but it can get really hairy and lead to specifications that are very hard to debug.

如果您确实需要谓词子类型化，那么 SMT 求解器可能不是您的问题域的最佳选择.定理证明器、依赖类型语言等可能更合适.例如，一个实际的例子是用于 Haskell 程序的 LiquidHaskell 系统，它允许将谓词附加到类型以精确地执行您正在尝试的操作；并使用 SMT-solver 解除相关条件:https://ucsd-progsys.github.io/liquidhaskell-blog/

If you really need predicate subtyping, perhaps SMT solvers are not the best choice for your problem domain. Theorem provers, dependently typed languages, etc. might be more suitable. A practical example, for instance, is the LiquidHaskell system for Haskell programs, which allows predicates to be attached to types to do precisely what you are trying; and uses an SMT-solver to discharge the relevant conditions: https://ucsd-progsys.github.io/liquidhaskell-blog/

如果您想坚持使用 SMT 求解器并且不介意使用较旧的系统，我会推荐 Yices，它支持谓词子类型以对此类问题进行建模.在 SMT 解决方案的背景下，它曾经是(现在仍然是)这个想法的最佳实现之一.

If you want to stick to SMT-solvers and don't mind using an older system, I'd recommend Yices with its support for predicate subtyping for modeling such problems. It was (and still is) one of the finest implementations of this very idea in the context of SMT-solving.

这篇关于在 Z3 中定义带约束的代数数据类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！