我正在通过使用PDR引擎将语言编译为Z3的方式来验证用同步编程语言编写的方程式的属性。我使用一周前从Github的master分支编译的Z3 4.5.1。
为了您的好奇心,我使用了本文中提出的从同步语言Luster到Z3的翻译的派生词(但不必阅读它就可以理解我想要做什么)。
我的以下程序有问题,sat
虽然我认为应该返回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
-th值和n - 1
-th值之间的关系是正确的(这是规则2)。
该Main
关系指出,在某种程度上n > 0
,序列的值与给定的方程式是一致的(我不确定这是解释它的最佳方法,如果不清楚,请告诉我)。因此,规则3指出,如果at处的内存之间的关系以及at处n = 0
的内存与新值之间的关系n = 1
正确,那么我们将获得的一组连贯值n = 1
。规则4指出,如果我们在处有一个连贯的序列值集n
,并且它们与处的值之间的关系n + 1
是正确的,那么我们在会得到一个新的连贯的序列值集n + 1
。
最后一条规则是我们要检查的属性:给定一组连贯的值,我们不能将其设置ok
为false。
运行此命令时,我得到:
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))))
此行为是由于现已修复的错误所致。这里的讨论包含更正它的提交。
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句