抽象 Z3/SMT-LIB 中的断言组

Question

Z3 中是否有很好的机制来抽象断言？我想创建一个“函数”，它接收参数并对这些参数进行断言，其中可能包含“局部变量”定义。

假设我有一个String，我想断言它代表一个介于 13 和 24 之间的十进制数。我可以编写一个关于字符串的正则表达式断言的组合，并将它与 str.to.int 范围断言结合起来。我可以直接做到这一点，但如果我有几十个这样的变量我想做出断言，它就会重复。我可以使用外部语言 API，或者在 Z3 中定义一个返回布尔值的宏/函数并断言它是真的，但这感觉有点间接。这里有什么惯用语？我希望 Z3 能够像手动编写断言一样容易解决

Answer 1

你可以使用define-fun来定义一个布尔函数f，这样你就可以(assert (f x y z ...))，其中f当然可以是多个条件的结合。 define-fun 将被 Z3 的 SMT2 前端内联，也就是说，它不应该有任何运行时成本。

（Z3 也支持通过(forall ((x ...)) (= (f x ...) ...)) 定义的宏，但您需要显式应用模型查找器策略来内联它们。）