首页 文章

Z3超时（推测）可判定逻辑

提问于
浏览 次
0

我们正在尝试用于功能程序验证的关系逻辑 . 我们的逻辑配备了代数数据类型的关系以及关系中的相等和子集包含谓词 . 我们的验证程序执行归纳程序分析（结构归纳）并生成具有足够强的归纳假设的验证条件（VC） . 我们的验证程序生成的VC遵循以下格式：

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

以下是我们的程序生成的示例VC：http://pastebin.com/exncPHDA

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

  • 每种具体类型（例如：'列表）都转换为未解释的排序 .

  • 关系被编码为未解释的n-ary函数，从未解释的排序到bool .

  • 关系断言（例如：R = R1 U R2，R = R1 X R2）被编码为未解释函数的预定量断言 .

上述编码的结果（推测）是有效命题（EPR）一阶逻辑中的公式 . 在Z3的帮助下，我们能够证明许多VC的有效性（否定的不可靠性） . 但是，在某些情况下，当VC无效（否定是SAT）时，Z3会循环 . 上面给出的例子（http://pastebin.com/exncPHDA）是一个这样的VC，其SMT2编码在这里给出：http://pastebin.com/s8ezha7D . 断言这个公式时，Z3似乎没有终止 .

鉴于决定量化的布尔公式是NEXPTIME的难度，决策程序的不终止并不是很令人惊讶 . 尽管如此，我们想知道在Z3中对公式进行编码时是否可以进行任何优化，以便最不可能实现非终止 -

  • 我们当前的编码创建了许多空集（即形式forall x：T，f（x）= false的一个断言）和相同单例集的许多实例（即forall x：T，（f（x）= true） <=>（x = v）） . 减少这种重复有助于吗？

  • 由于计划的详细阐述，我们目前有许多变量和传递等式 . 变量数量的减少有帮助吗？

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

z3

1 回答

  • 1

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

    (set-option :macro-finder true)

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

    备注：在http://z3.codeplex.com的正在进行中（不稳定）分支中，此选项称为 :smt.macro-finder .

    回复于

相关问题