可能的Z3模式/触发器错误

Question

我尝试在以下smt2文件上运行Z3

(set-option :print-success false)
(set-info :smt-lib-version 2.6)
(set-option :smt.AUTO_CONFIG false)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR 1.5)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.CASE_SPLIT 3)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.BV.REFLECT true)
(set-option :smt.qi.max_multi_patterns 1000)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)
; done setting options
(declare-sort Ref 0)
(declare-sort Field 0)
(declare-sort Mask 0)
(declare-fun select_mask (Mask Ref Field) Real)
(declare-fun zero_mask () Mask)
(declare-sort Heap 0)
(declare-fun length (Heap Ref) Int)
(declare-fun length* (Heap Ref) Int)
(declare-fun select_heap (Heap Ref Field) Ref)
(declare-fun next () Field)
(declare-fun null () Ref)
(declare-fun this () Ref)
(declare-fun mask () Mask)
(declare-fun store_mask (Mask Ref Field Real) Mask)
(assert (forall ( ( ?x0 Mask) ( ?x1 Ref) ( ?x2 Field) ( ?x3 Real)) (! (= (select_mask (store_mask ?x0 ?x1 ?x2 ?x3) ?x1 ?x2)  ?x3) :weight 0)))
(assert (forall ( ( ?x0 Mask) ( ?x1 Ref) ( ?y1 Ref) ( ?x2 Field) ( ?y2 Field) ( ?x3 Real)) (! (=> (or  (not (= ?x1 ?y1)) (not (= ?x2 ?y2))) (= (select_mask (store_mask ?x0 ?x1 ?x2 ?x3) ?y1 ?y2) (select_mask ?x0 ?y1 ?y2))) :weight 0)))
(assert (forall ((o_2 Ref) (f_4 Field) ) (! (= (select_mask zero_mask o_2 f_4) 0.0)
:pattern ( (select_mask zero_mask o_2 f_4))
)))
(assert (forall ((heap Heap) (this Ref) ) (! (= (length heap this) (length* heap this))
:pattern ( (length heap this))
)))
(assert (forall ((heap Heap) (this Ref) ) (! (= (length heap this) (ite (= (select_heap heap this next) null) 1 (+ 1 (length* heap (select_heap heap this next)))))
:pattern ( (length heap this))
)))
(assert (not (= this null)))
(assert (= mask (store_mask zero_mask this next 1.0)))
(declare-fun heap () Heap)
(declare-fun valid-next () Field)
(push 1)
(set-info :boogie-vc-id test2)
(set-option :timeout 0)
(set-option :rlimit 0)
(assert
(or (<= (select_mask mask this next) 0.0)
(and (= (select_heap heap this next) this)
(or (> 1.0 (select_mask zero_mask null valid-next))
(and (<= 1.0 (select_mask zero_mask null valid-next))
(>= (length heap this) (length heap (select_heap heap this next))))))))
(check-sat)
(pop 1)

在我尝试的Z3版本中，4.8.6 - 4.8.9返回unknown，但4.8.10 - 4.9.1返回unsat。unsat结果似乎来自触发length公理，但似乎如果按顺序查看分离，Z3应该找到(= (select_heap heap this next) this)和(> 1.0 (select_mask zero_mask null valid-next))的部分模型，而不触发length公理并返回unknown。这是Z3中的一个bug吗?还是Z3没有提供关于查看断开的顺序的保证?

我还尝试删除push和pop行，这导致所有版本的Z3我试图返回unsat。

Answer 1

在修剪z3特定设置后，CVC4和CVC5也为此查询返回unsat。请注意，unknown与unsat并不不兼容:对于解算器现在返回unsat，它之前说的是unknown，这是完全可以的。(或者相反)。

如果CVC4/CVC4和z3都同意unsat，则调试方法为:

• 看看你是否能得到一个unsat核心，如果这是有意义的
• 根据您的期望断言将模型绑定到它应该是什么的额外条件。希望这样做能告诉你为什么它不令人满意。

如果您需要这个社区的更多帮助，您必须准确地指定您认为满足此公式的模型，并首先调试它以尽可能多地消除问题。祝你好运!