检查Z3PY中数组（按数组）的所有解决方案

Question

我的问题是，我必须为as-array形式的数组获取所有可能的模型。我为此编写的代码如下：

s = Solver()
check = s.check()
while (str(check) == "sat"):
      mod = s.model()
      block = []
      for var in mod.decls():
         block.append(var() != mod[var])
      s.add(Or(block))
      check = s.check()

[var可以采用其他类型的值as-array，当我运行s.add(Or(block))行时，下次我运行check = s.check行时，它将返回未知值

还有其他方法吗？

Answer 1

这是经常提出的要求。您的阻塞子句将必须修改以考虑数组的可能性。它还应该注意数据类型，函数，浮点数……绝对可行，并且此答案的代码将带您入门：(Z3Py) checking all solutions for equation

请注意，您一般不能使用“阻止”功能。阵列也可能会出现问题，因为如果阵列有无限的支持，您将无法将其“重铸”为阻塞物。 （也就是说，考虑将第i个元素映射到值i的数组。对此没有有限的表示，您可以轻松地在SMTLib中编写而无需使用量词。）除了这些考虑之外，我相信上面的答案可以使您走得足够远，可以处理大多数情况。