当 Z3 返回一个具有未解释排序的模型时，例如Q，它使用形式为 的常量Q!val!0。
但是，如果我从头开始创建查询并将这个符号称为 的居民Q，那么 Z3 理所当然地抱怨这Q!val!0是一个未知常数。
本质上，我试图让 Z3 枚举 的所有居民Q，方法是要求它给我一个与之前返回的模型不同的模型。因此，在随后对 Z3 的调用中，我需要引用这些常量。
有没有办法使用 SMT-Lib2 接口来做到这一点？
问问题
282 次
当 Z3 返回一个具有未解释排序的模型时，例如Q，它使用形式为 的常量Q!val!0。
但是，如果我从头开始创建查询并将这个符号称为 的居民Q，那么 Z3 理所当然地抱怨这Q!val!0是一个未知常数。
本质上，我试图让 Z3 枚举 的所有居民Q，方法是要求它给我一个与之前返回的模型不同的模型。因此，在随后对 Z3 的调用中，我需要引用这些常量。
有没有办法使用 SMT-Lib2 接口来做到这一点？