CODEWITHSUNDEEP
z3
Gowtham Kaki
Gowtham Kaki

Reputation: 377

Z3's model seems to violate the constraints

In the Z3 script shown below, I have three relations - session-order (so), visibility (vis), and happens-before (hb). One of the constraints effectively asserts hb = so ∪ vis, from where it follows that ∀a,b. so(a,b) ⇒ hb(a,b). In other words, for two constants E1 and E2, the constraints(so E1 E2) and (not (hb E1 E2)) are not simultaneously satisfiable. As expected, Z3 returns UNSAT if I assert both. However, if I now remove (not (hb E1 E2)) and check-sat again, then Z3 returns a model where (so E1 E2) evaluates to true, but (hb E1 E2) evaluates to false (see eval statements at the end). How is this possible? Any workarounds to get correct model are also very much appreciated!

The options I pass to Z3 are smt.auto-config=false smt.mbqi=true smt.macro-finder=true, and the Z3 version I use 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?

Upvotes: 0

Views: 87

Answers (1)

alias
alias

Reputation: 30418

I think this is a z3 bug, and I suspect it is with the macro-finder option. If you remove the smt.macro-finder=true argument (or call without any arguments), you don't have this problem.

You should definitely report at their github tracker. (Which I believe you already did!)

Regarding modeling: Did you try declare-datatypes for modeling Eff and Oper? You can make them simple constructors and thus would get rid of the cardinality constraints for them. (They would be automatically inferred.) You might get better mileage by using the internal mechanisms of modeling such datatypes, instead of quantification.

Upvotes: 2

Related Questions