Z3 的模型似乎违反了约束

Question

在下面显示的 Z3 脚本中，我有三个关系 - 会话顺序 (so)、可见性 (vis) 和发生前 (hb)。其中一个约束有效地断言 hb = so ∪ vis，从那里它遵循 ∀a,b. so(a,b) ⇒ hb(a,b)。换句话说，对于两个常量 E1 和 E2，约束 (so E1 E2) 和 (not (hb E1 E2)) 不能同时满足。正如预期的那样，如果我同时声明两者，则 Z3 returns UNSAT。但是，如果我现在再次删除 (not (hb E1 E2)) 和 check-sat，则 Z3 returns 一个模型，其中 (so E1 E2) 的计算结果为真，但 (hb E1 E2) 的计算结果为假（参见 eval 语句在末尾）。这怎么可能？也非常感谢任何获得正确模型的解决方法！

我传给Z3的选项是smt.auto-config=false smt.mbqi=true smt.macro-finder=true，我用的Z3版本是4.8.0.

(declare-sort Eff) ; type of an effect
(declare-sort Ssn) ; type of a session
(declare-sort Oper) ; type of an operation
(declare-fun seqno (Eff) Int) ; each effect has a seqno
(declare-fun ssn (Eff) Ssn)
(declare-fun oper (Eff) Oper)
(declare-fun so (Eff Eff) Bool) ; session order
(declare-fun vis (Eff Eff) Bool) ; visibility
(declare-fun hb (Eff Eff) Bool) ; happens-before
(declare-fun NOP () Oper)
(declare-fun District_IncNextOID () Oper)
(declare-fun District_Add () Oper)
(declare-fun District_Get () Oper)
(declare-fun E2 () Eff)
(declare-fun E1 () Eff)
(declare-fun E0 () Eff)
;;
;; Cardinality constraints
;;
(assert (forall ((a0 Eff))
  (or (= a0 E0)
      (= a0 E1)
      (= a0 E2)
      )))
(assert (distinct E0 E1 E2 ))
(assert (forall ((a0 Oper))
  (or (= a0 District_Get)
      (= a0 District_Add)
      (= a0 District_IncNextOID)
      (= a0 NOP))))
(assert (distinct 
          District_Get
          District_Add
          District_IncNextOID
          NOP))
;;
;; Axioms
;;
;; session order relates sequential effects in 
;; the same session
(assert (forall ((a0 Eff) (a1 Eff))
  (let ((a!1 (and (not (= (oper a0) NOP))
                  (not (= (oper a1) NOP))
                  (= (ssn a0) (ssn a1))
                  (< (seqno a0) (seqno a1)))))
    (= (so a0 a1) a!1))))
;; session-order is transitive
(assert (forall ((a0 Eff) (a1 Eff) (a2 Eff))
  (=> (and (so a0 a1) (so a1 a2)) (so a0 a2))))
;; visibility is irreflexive
(assert (forall ((a0 Eff)) (not (vis a0 a0))))
;; visibility is anti-symmetric
(assert (forall ((a0 Eff) (a1 Eff)) 
  (=> (and (vis a0 a1) (vis a1 a0)) (= a0 a1))))
;; happens-before is (so ∪ vis)
(assert (forall ((a0 Eff) (a1 Eff)) 
  (=> (or (vis a0 a1) (so a0 a1)) (hb a0 a1))))
;; happens-before is transitive
(assert (forall ((a0 Eff) (a1 Eff) (a2 Eff))
  (=> (and (hb a0 a1) (hb a1 a2)) (hb a0 a2))))
;; happens-before is irreflexive
(assert (forall ((a0 Eff)) (not (hb a0 a0))))
;;
;; Check
;;
(assert (so E1 E2))
;(assert (not (hb E1 E2)))
(check-sat)
(get-model)
(eval (so E1 E2)) ; returns true
(eval (hb E1 E2)) ; returns false. Why?

Answer 1

我认为这是一个 z3 错误，我怀疑它与宏查找器选项有关。如果您删除 smt.macro-finder=true 参数（或不带任何参数调用），则不会出现此问题。

你绝对应该在他们的 github 跟踪器上报告。（我相信你已经做到了！）

关于建模：您是否尝试过 declare-datatypes 对 Eff 和 Oper 进行建模？您可以使它们成为简单的构造函数，从而摆脱它们的基数约束。（它们会被自动推断出来。）通过使用对此类数据类型建模的内部机制，而不是量化，您可能会获得更好的成绩。

Z3 的模型似乎违反了约束

Z3's model seems to violate the constraints

z3