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 ...) ...))定义的宏，但是您需要显式地应用模型查找器策略来内联它们。)