Распространение релевантности Z3 с помощью квантификаторов - PullRequest
Новая
       15

Распространение релевантности Z3 с помощью квантификаторов

0 голосов
/ 13 января 2020

Я видел примеры, в которых удается вернуть «все равно» в их решении. Я думаю, что это использует распространение релевантности Z3. (См. SO вопрос «Как заставить Z3 вернуть минимальную модель?» , SO вопрос «{ ссылка }» , в этой статье ).

Это позволяет: 

(set-option :smt.auto-config false)

(declare-const x Bool)
(declare-const y Bool)

(assert (or x y))
(assert x)

(check-sat)
(echo "Expect x is true")
(eval x) ; returns true
(echo "Expect y is don't care")
(eval y) ; returns y - i.e don'tcare

, что возвращает: 

sat
Expect x is true
true
Expect y is don't care
y

Как можно добиться чего-то подобного, когда задействованы квантификаторы? Например, в приведенном ниже примере не должно иметь значения, имеет ли зеленая машина сломанную трансмиссию. 

(set-option :smt.auto-config false)

(declare-sort Car)

(declare-fun working_engine (Car) Bool)
(declare-fun broken_transmission (Car) Bool)

(define-fun allCarsNeedFixing () Bool
  (forall ((c Car))
    (or
      (not (working_engine c))
      (broken_transmission c))))

(declare-const redCar Car)
(assert (working_engine redCar))

(declare-const greenCar Car)
(assert (not (working_engine greenCar)))

(assert allCarsNeedFixing)
(check-sat)

(echo "red car has working engine, expect true")
(eval (working_engine redCar)) ; returns true
(echo "red car has broken transmission, expect true")
(eval (broken_transmission redCar)) ; returns true

(echo "green car has working engine, expect false")
(eval (working_engine greenCar)) ; returns false
(echo "green car has broken transmission, expect don't care")
(eval (broken_transmission greenCar)) ; could return true or false

, которая возвращает: 

sat
red car has working engine, expect true
true
red car has broken transmission, expect true
true
green car has working engine, expect false
false
green car has broken transmission, expect don't care
true

Как получить окончательный результат для возврата "не волнует" в отличие от истины?

Эти примеры должны выполняться через Rise4Fun

...