我是z3 SMT求解器的新手。我需要定义一个关系，而不是一个函数。我的意思是一个可以返回多个值的函数。我查了一下教程，却找不到任何东西。谢谢您能在这方面帮助我。
谢谢你
使用支持ArrayEx理论的逻辑之一，该逻辑提供Array排序和用于操纵数组的关联函数。然后，您可以让函数返回数组值，该数组值可以包含任意多个Ints或Bools或其他内容。
该SMT教程是一个很好的资源，它将许多SMT详细信息收集到一个地方。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句