检查 Z3PY 中数组（as-array）的所有解决方案

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 行时它会返回未知

还有其他方法吗？

------- 编辑 -------

我找到了一种方法来获取 as-array 形式的数组的所有可能模型，这是上一个问题，我所做的方法是创建一个表示数组大小的变量，并从 i = 0 到 i = n（其中 n 是大小），将 a[i]!= x 设为“a”数组，将“x”设为“a[i]”的值。

我现在的问题是我有一个“mk-pair”形式的数据类型，它的第一个参数是一个as-array 形式的数组和一个指示数组大小的整数。

当我得到一个模型时，我的格式是 mk-pair(as-array, 30)（例如），是数组大小的 30。

问题是我找不到获取所有可能模型的方法，因为如果我否认数据类型（a != x，假设“a”是数据类型，“x”是它的值） ，它返回我未知，如果我做第一个（as-array [0]！= x），我真正否认的是as-array，而不是变量“a”（形式为mk-pair（as -array, Int) ) 并且当我多次询问模型时，我得到了重复的结果。

有什么办法吗？

Answer 1

这是一个频繁的请求。您的阻塞子句必须修改以考虑数组的可能性。它还应该注意数据类型、函数、浮点数......绝对可行，这个答案的代码会让你开始：(Z3Py) checking all solutions for equation

请注意，您通常不能“阻止”函数。数组也可能有问题，因为如果它们具有无限支持，您将无法将它们“重铸”为阻止程序。 （也就是说，考虑一个将 i'th 元素映射到值 i 的数组。没有限定的表示形式，您可以在没有量词的情况下轻松地在 SMTLib 中编写。）除了这些考虑之外，我相信上面的答案可以让你走得更远，处理大多数情况。