z3 - Z3 使用量词的相关性传播

Question

我已经看到在他们的解决方案中设法返回“不关心”的示例。我认为这利用了 Z3 的相关性传播。（参见SO 问题“我如何让 Z3 返回最小模型？”，SO 问题“https://stackoverflow.com/questions/28289410/z3-eliminate-dont-care-variables/28302963”，本文）。

这允许：

(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

如何获得最终结果以返回“不关心”而不是 true？

这些示例应通过Rise4Fun执行

标签： z3smt