Z3在(大概)可判定逻辑上超时

Question

我们正在试验一种用于功能程序验证的关系逻辑。我们的逻辑具有代数数据类型上的关系，以及关系上的等式和子集包含谓词。我们的验证程序执行归纳程序分析(结构归纳)，并生成足够强的归纳假设的验证条件(VC)。我们的核查程序产生的风险投资遵循以下格式：

bindings <var-type bindings> in <antecedent-predicate> => <consequent-predicate> end

下面是我们的过程生成的一个VC示例：http://pastebin.com/exncPHDA

我们使用以下规则对用SMT2语言生成的VC进行编码：

1. 每种具体类型(例如：“列表”)都会转换为未解释的排序。
2. 关系被编码为未解释的n进制函数，从未解释的排序到bool。
3. 关系断言(例如:r= R1 U R2，R= R1 X R2)被编码为对未解释的函数的prenex量化断言。

上述编码结果(想必)是有效命题(EPR)一阶逻辑中的一个公式.借助Z3，我们能够断言许多风险投资的有效性(不可满足的否定性)。然而，在某些情况下，当VC是无效的(否定为SAT)，Z3循环。上面给出的例子(http://pastebin.com/exncPHDA)就是这样一个VC，它的SMT2编码在这里给出了：http://pastebin.com/s8ezha7D。在断言此公式时，Z3似乎没有终止。

考虑到确定量化的布尔公式是很难的，决策过程的不终止也就不足为奇了。尽管如此，我们还是想知道在Z3中对公式进行编码时是否可以进行任何优化，以便使非终止的可能性最小-

1. 我们当前的编码创建了许多空集(即一个形式断言x:T，f (x )=false)和许多相同单例集的实例(即forall :t，(f(x) = true) <=> (x= v))。减少这种重复是否有帮助？
2. 由于程序的精化，我们目前有许多变量和传递等式。减少变量的数量有帮助吗？

另外，在确定不可满足的量化布尔公式时，Z3循环的可能性有多大？

Answer 1

在Z3中，我们说形式forall X, f(X) = T[X]的量词，其中X是变量的向量，f是未解释的函数，T是不包含f的术语/公式，是宏。Z3可以通过简单地替换所有出现的f来消除预处理步骤中的这些量词。选项:macro-finder打开此特性。

     (set-option :macro-finder true)

如果我们应用这一预处理步骤，则可以立即求解该示例。下面是与更新的脚本的链接：http://rise4fun.com/Z3/z2UJ

备注:在http://z3.codeplex.com的在制品(不稳定)分支中，此选项称为:smt.macro-finder.