带有量词的公式包含trans函数声明。Z3 成功找到模型并打印出来。但它也打印模型中未在模型中任何地方使用的函数trans!1!4464，如 ..。trans!7!4463它是什么？如何禁用此输出？
这是查询：http ://dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2 ，这是 Z3 的输出 - http://dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt
问问题
147 次
1 回答
1
回想一下，Z3 返回的模型可以看作是简单的函数式程序。您的公式在 UFBV 片段中。Z3 使用几个模块来决定这个片段。每个模块将公式F转换为“更简单”的公式F'，并生成将模型转换为模型F'的过程F。我们称这些程序为：“模型转换器”。例如，模型转换器将消除对在FtoF'转换中引入的辅助函数和常量的解释。一些辅助定义无法删除，似乎它们用于解释其他定义。我们应该将它们视为“辅助功能”。他们还为已消除的符号创建了解释。
在您的示例中，发生以下情况：最后一个模块生成一个包含trans!...andk!...符号的模型。此模型适用于甚至不包含trans. 该功能trans已被淘汰。当我们应用模型转换器时， 的解释trans是基于 all 的解释构建的trans!...。在这一点上，trans!...符号k!...仍然被使用，因为对trans所有trans!...符号的解释和函数的解释trans!...都对函数符号的引用k!...。在这一步，模型中没有不必要的符号。然而，在后面的步骤中，通过展开和trans的定义来简化对 的解释trans!...k!.... 所以，经过这个简化步骤，本质trans!...上k!...都是“死代码”。
话虽如此，Z3返回的模型是正确的，即它是您公式的模型。我承认这些额外的符号令人讨厌且不必要。为了消除它们，我们应用了相当于“死代码”消除步骤。我们真的很接近下一个版本。因此，此功能在下一个版本中将不可用，但我将在下一个版本中添加它。
于 2012-03-12T06:02:45.513 回答