避免在 Z3 中截断大型模型

Question

对于大型模型，通过 Z3 Python API 使用的函数 model(( 会截断输出(在某些时候，模型会继续使用"..."(。

有没有办法避免这种情况？

Answer 1

如果我没记错的话，这是一个Python的"功能"。而不是str(...)尝试使用repr(...)，它应该产生一个可以被解释器读回(如果需要(的字符串。当然，您可以单独迭代模型元素，以使所有需要输出的字符串变小。例如，沿着以下行：

s = Solver()
# Add constraints...
print(s.check())
m = s.model()
for k in m:
print('%s=%s' % (k, m[k]))

Answer 2

我有一个下面的函数，它试图将str(self.solver.check(((给出的答案和str(self.solver.model(((给出的模型保存到文件名中

def createSMT2LIBFileSolution(self, fileName):
with open(fileName, 'w+') as foo:
foo.write(str(self.solver.check()))
foo.write(str(self.solver.model()))
foo.close()

问题的输出是：

sat[C5_VM1 = 0,
... //these "..." are added by me
VM6Type = 6,
ProcProv11 = 18,
VM2Type = 5,
...]

"...]"出现在所有被截断的文件的第 130 行。我不知道是Python还是Z3的东西。如果模型可以在少于 130 行上编写，一切都很好。