Z3 使用 PDR 引擎给出意想不到的结果

Question

我正在验证以同步编程语言编写的方程式的属性，方法是使用 PDR 引擎将所述语言编译为 Z3。我使用 Z3 4.5.1 从 Github 的大师 b运行ch 一周前编译。

为了您的好奇心，我使用了 this paper 中提出的同步语言 Lustre 到 Z3 的 t运行slation 的派生词（但没有必要阅读它来理解我想要的内容做）。

我对以下程序有问题，returns sat 虽然我认为它应该 return unsat:

(declare-var out Int)
(declare-var next_out Int)
(declare-var mem Int)
(declare-var next_mem Int)
(declare-var ok Bool)
(declare-var next_ok Bool)
(declare-rel Init (Int Int Bool))
(declare-rel Trans (Int Int Bool Int Int Bool))
(declare-rel Main (Int Int Bool))
(declare-rel Error ())

(rule (=> (= mem 0) (Init out mem ok)))
(rule (=> (and (= next_ok (>= next_out 0))
               (= next_mem (+ mem 1))
               (= next_out mem))
          (Trans out mem ok next_out next_mem next_ok)))
(rule (=> (and (Init out mem ok)
               (Trans out mem ok next_out next_mem next_ok))
          (Main next_out next_mem next_ok)))
(rule (=> (and (Trans out mem ok next_out next_mem next_ok)
               (Main out mem ok))
          (Main next_out next_mem next_ok)))
(rule (=> (and (Main out mem ok)
               (not ok))
          Error))

(query Error :print-certificate true)

我会尽量简化我的意图，这样您就不必阅读论文了。我们定义三个序列 mem、out 和 ok 以便：

forall n > 0. mem(n) = mem(n - 1) + 1 with mem(0) = 0
and           out(n) = mem(n - 1)
and           ok(n) = out(n) >= 0

我们要证明 forall n > 0. ok(n) = true.

在Z3程序中，可以把mem、out和ok看成是n - 1处序列的值（或包含前一个的记忆）序列的值）和 next_* 作为 n 处的值。

Init 关系表明初始方程是正确的（即 n = 0 的方程），在我们的例子中我们只有 mem = 0 而 out 和ok 是免费的（这是规则 1）。 Trans 关系确定第 n 个值和第 n - 1 个值之间的关系是正确的（即规则 2）。

Main 关系指出，对于某个 n > 0，序列的值与给定的方程一致（我不确定这是解释它的最佳方式，如果不清楚请告诉我）。因此，规则 3 指出，如果 n = 0 处的记忆之间的关系以及这些记忆与 n = 1 处的新值之间的关系是正确的，那么我们会得到一组连贯的 n = 1 值.规则 4 指出，如果我们在 n 处有一组连贯的序列值，并且它们与 n + 1 处的值之间的关系是正确的，那么我们将在 [= 处得到一组新的连贯序列值=42=].

最后一条规则是我们要检查的属性：给定一组连贯的值，我们不能让 ok 为假。

当我运行这个时，我得到：

sat
(and (Main!slice!1 false) (not (>= (:var 5) 0)) (Main!slice!1 true))

我不明白为什么。我错过了什么吗？

编辑

我继续研究这个问题，试图理解 Z3 用我给他的东西做了什么。

我运行它带有选项 fixedpoint.xform.inline_eager=false ，（我想）这使得它内联更少。当运行冗长级别 1 时，我看到在第一次应用 N7datalog15mk_rule_inlinerE 之后我有 5 条规则而不是 3 条（完整输出见下文）。我也有以下结果：

unsat
(define-fun I ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (>= x!1 0))
(define-fun T ((x!0 Int) (x!1 Int) (x!2 Bool) (x!3 Int) (x!4 Int) (x!5 Bool)) Bool
  (and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))
(define-fun M ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (and x!2 (>= x!1 1)))

这与原来的完全不同......所以除非我对上面的选项的作用有误，否则我想这是一个错误所以我会打开一个问题。

满输出

运行 z3 <file> -smt2 -v:1:

(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...6 rules 0s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...3 rules 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...3 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...3 rules 0s)
Entering level 1
Entering level 2

2 query!0 closed
  true 1
 1 Main!slice!1 closed
   (not Main!slice!1_0_n) 182
  0 Main!slice!1 closed
    true 1
goals 0
sat
(and (Main!slice!1 false) (not (>= (:var 5) 0)) (Main!slice!1 true))

运行 z3 <file> -smt2 -v:1 fixedpoint.xform.inline_eager=false:

(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...6 rules 0s)
(transform N7datalog27mk_quantifier_instantiationE...no-op 0s)
(transform N7datalog8mk_scaleE...no-op 0s)
(transform N7datalog18mk_karr_invariantsE...no-op 0s)
(transform N7datalog14mk_array_blastE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog12mk_bit_blastE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...5 rules 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...5 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog13mk_coi_filterE...no-op 0s)
(transform N7datalog25mk_interp_tail_simplifierE...5 rules 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog15mk_rule_inlinerE...no-op 0s)
(transform N7datalog22mk_subsumption_checkerE...no-op 0s)
(transform N7datalog8mk_sliceE...no-op 0s)
Entering level 1
Entering level 2
Entering level 3
(define-fun Init ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (>= x!1 0))
(define-fun Main ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (and (>= x!1 1) x!2))
(define-fun Trans ((x!0 Int)
 (x!1 Int)
 (x!2 Bool)
 (x!3 Int)
 (x!4 Int)
 (x!5 Bool)) Bool
  (and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))
unsat
(define-fun Init ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (>= x!1 0))
(define-fun Main ((x!0 Int) (x!1 Int) (x!2 Bool)) Bool
  (and x!2 (>= x!1 1)))
(define-fun Trans ((x!0 Int)
 (x!1 Int)
 (x!2 Bool)
 (x!3 Int)
 (x!4 Int)
 (x!5 Bool)) Bool
  (and (<= (+ x!1 (* (- 1) x!4)) (- 1)) (= x!5 (>= x!1 0))))

Answer 1

此行为是由于一个错误引起的，该错误现已修复。讨论 here 包含更正它的提交。

Z3 使用 PDR 引擎给出意想不到的结果

Z3 giving unexpected result with the PDR engine

z3