在Z3教程的第13.2.3节中,有一个很好的例子,说明如何减少在处理注入的公理化时必须实例化的模式数量.在该示例中,必须以单数形式表示的函数f将类型A的对象作为输入并返回类型B的对象.据我所知,排序A和B是分离的.
我有一个SMT问题(FOL + EUF)Z3似乎没有终止,我试图找出原因.我有一个函数f:A-> A我认为是单射的.问题可能是f的域和codomain重合吗？
提前感谢任何建议.
smt z3
smt ×1
z3 ×1