Модель Z3, кажется, нарушает ограничения - PullRequest
Новая
       5

Модель Z3, кажется, нарушает ограничения

0 голосов
/ 25 октября 2018

В скрипте 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, а в версии 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?

1 Ответ

0 голосов
/ 25 октября 2018

Я думаю, что это ошибка z3, и я подозреваю, что это с опцией поиска макросов.Если вы удалите аргумент smt.macro-finder=true (или вызовете без каких-либо аргументов), у вас не возникнет этой проблемы.

Вы обязательно должны сообщить об этом на их трекер github.(Что, я думаю, вы уже сделали!)

По поводу моделирования: Вы пробовали declare-datatypes для моделирования Eff и Oper?Вы можете сделать их простыми конструкторами и таким образом избавить их от ограничений на количество элементов.(Они будут автоматически выведены.) Вы можете получить больший пробег, используя внутренние механизмы моделирования таких типов данных вместо количественного определения.

...