Z3 中的喇叭子句 [英] Horn clauses in Z3

问题描述

如果要分析的程序的语义是作为 Horn 子句给出的，Z3 现在支持求解归纳不变量(暗示所需的属性).

Z3 now supports solving for inductive invariants (implying a desired property) if the semantics of the program to analyze is given as Horn clauses.

z3.codeplex.com 上 Z3 源代码的 master 分支中的版本 但是不支持这个功能.由于 Z3 通过使用插值的 PDR 算法解决了这些 Horn 子句问题，因此我编译了 interp 分支(d8b31773b809)，它支持 (set-logic HORN).

The version in the master branch of the Z3 source code on z3.codeplex.com however does not support this feature. Since Z3 solves these Horn clauses problems by the PDR algorithm, which uses interpolation, I compiled instead the interp branch (d8b31773b809), which supports (set-logic HORN).

据我所知，Horn-clause 问题是用表示不变量的未知谓词来指定的，而 X×Y 上的谓词只是一个从 X×Y 到 Bool 的函数.到目前为止一切顺利.

As far as I understood, a Horn-clause problem is to be specified with unknown predicates representing invariants, and a predicate over X×Y is just a function from X×Y to Bool. So far so good.

我尝试的第一个示例只是为 for(int i=0; i<=10; i++) 循环推断归纳不变量的问题.

The first example I tried is just a problem of inferring an inductive invariant for a for(int i=0; i<=10; i++) loop.

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1)))))
(check-sat)

到目前为止一切顺利，获得了sat.现在刚刚添加了 (assert (not (inv 15)) 并且我得到了 unsat.然后我尝试了

So far so good, got sat. Now just added (assert (not (inv 15)) and I got unsat. I then tried

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (not (inv 15)))
(check-sat)

并得到unsat.

我做错了什么?

推荐答案

使用unstable"分支.interp"分支用于内部开发，该分支的状态可以波动.我得到了你的第二个问题的答案sat".

Use the "unstable" branch. The "interp" branch is for internal development and the state of this branch can fluctuate. I get the answer "sat" on your second problem.

第一个问题的一个稍微有趣的版本是:

A slightly more interesting version of the first problem is:

(set-logic HORN)
(declare-fun inv (Int) Bool)
(assert (inv 0))
(assert (forall ((I Int)) (or (> I 10) (not (inv I)) (inv (+ I 1))))) 
(assert (forall ((I Int)) (=> (inv I) (<= I 11))))
(check-sat)
(get-model)

它产生了明显的归纳不变量.如果将最后一个断言替换为

It produces the obvious inductive invariant. If you replace the last assertion by

(assert (forall ((I Int)) (=> (inv I) (<= I 10)))) 

相反，您会得到一个(难以阅读的)证明.

Instead you get a (hard to read) proof.

这篇关于Z3 中的喇叭子句的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！