z3 - Z3 中的乐趣返回多个元素

Question

据我所知，我可以声明一个返回多个元素的函数。假设我有一个函数 x，它接收一个排序 T 并返回一个排序 U 和一个排序 R

(declare-sort T) (declare-sort R) (declare-sort U)

（声明乐趣 x (T) (UR)）

那么，当调用函数 x 返回元素时，我该如何访问......可以说我需要断言将 U 传递给一个函数，将 R 传递给另一个函数.. 可以这样做吗？

Answer 1

您的示例不是格式良好的 SMT-LIB2。它不解析。（错误“第 3 行第 23 列：排序构造函数的参数数量无效”） http://www.smtlib.org深入描述了 SMT-LIB2 语法和语义。