在解决以下 Horn 子句时如何解释 Z3 的行为？答案

【问题标题】：How to explain Z3's behavior when solving the following Horn clauses?在解决以下 Horn 子句时如何解释 Z3 的行为？
【发布时间】：2013-11-29 15:05:56
【问题描述】：

我正在使用来自不稳定分支的 Z3 来试验 Horn 子句（提交 61385c8489b7fda11b518a67fe308ea3cfe28c3d）。我可以让 Z3 推断出一些循环不变量，这很好。然而，通过以下简单的例子，我对 Z3 的行为感到困惑。我在这里错过了什么？

示例 1：

(set-logic HORN)
(declare-const C Int)
(assert (> C 2))
(check-sat)
(get-model)

我希望有一个模型，但收到“未知”。

示例 2：

(set-logic HORN)
(define-fun step ((I Int) (I1 Int)) Bool (= I1 (+ I 1)))
(define-fun post ((I1 Int)) Bool (= I1 10))
(declare-fun pre (Int) Bool)
(assert (forall ((I Int) (I1 Int)) (=> (and (pre I) (step I I1)) (post I1))))
(check-sat)
(get-model)

我希望一个模型告诉我一些关于 pre 的信息（例如，它是错误的或它适用于 9），但接收

sat
(model )

谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

我正在使用 Z3（在线和本地）执行您的示例 1，并且我正在获取

WARNING: unknown logic, ignoring set-logic command 
sat 
(model (define-fun C () Int 3) )

我正在使用 mathsat（本地）执行您的示例 2，并且正在获取

sat
( (C 3) )

【讨论】：

【解决方案2】：

我正在使用 Z3（在线和本地）执行您的示例 2，并且我正在获取

WARNING: unknown logic, ignoring set-logic command 
sat 
(model 
 (define-fun elem!0 () Int 0) 
 (define-fun elem!1 () Int 0) 
 (define-fun pre ((x!1 Int)) Bool false) 
 )

【讨论】：

感谢您的尝试，但请注意，我的问题涉及 Z3 的 PDR 引擎，用于解决喇叭子句。 (set-logic HORN) 部分很重要。这些示例可以很好地与其他引擎一起使用 - 这发生在您的案例中。