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将返回UNSAT。但是，如果我现在再次删除(not (hb E1 E2))和check-sat，那么Z3将返回一个模型，其中(so E1 E2)值为true，而(hb E1 E2)值为false (请参见最后的eval语句)。这怎麽可能？任何的解决办法，以获得正确的模型，也非常感谢！

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

(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吗？您可以使它们成为简单的构造函数，从而消除它们的基数约束。(它们将自动推断。)通过使用这些数据类型建模的内部机制，而不是量化，您可以获得更好的里程。