据我所知，我可以声明一个返回多个元素的函数。假设我有一个函数 x，它接收排序 T 并返回排序 U 和排序 R
(声明排序 T) (声明排序 R) (声明排序 U)
(声明-fun x (T) (U R))
当调用函数 x 时，我如何访问返回元素......假设我需要断言将 U 传递给一个函数并将 R 传递给另一个函数......这可以做到吗？
最佳答案
您的示例的 SMT-LIB2 格式不正确。它不解析。 (错误“第 3 行第 23 列:排序构造函数的参数数量无效”) http://www.smtlib.org深入描述了SMT-LIB2语法和语义。
关于z3 - Z3 返回多个元素的乐趣，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/24139335/