NuZ：看到已经放弃的规则了吗？

Question

是否可以检查 NuZ 放弃了问题的哪些软断言？

让我们看这个例子：

(declare-fun x () Int)
(declare-fun y () Int)

(assert-soft (=> (= x 2) (= y 1)) :weight 1)
(assert-soft (=> (= x 3) (= y 2)) :weight 1)
(assert-soft (=> (= x 4) (= y 2)) :weight 1)
(assert-soft (=> (= x 4) (= y 3)) :weight 1)

;(assert (= x 1))
;(assert (= x 2))
;(assert (= x 3))
(assert (= x 4))

;(assert (not (= y 3)))

(check-sat)
(get-model)

结果显示为：

 |-> 1
sat
(model
  (define-fun y () Int
    3)
  (define-fun x () Int
    4)
)

成本是1，但是放弃了哪些规则？

当然，在这个简单的例子中很容易推导出来。在更复杂的场景下，可能会有些困难甚至不可能。

Answer 1

一层间接就可以了：

(declare-fun A1 () Bool)
(declare-fun A2 () Bool)
(declare-fun B1 () Bool)

(declare-fun x () Int)
(declare-fun y () Int)

(assert-soft (= A1 true) :weight 1)
(assert-soft (= A2 true) :weight 2)
(assert-soft (= B1 true) :weight 2)

(assert (=> A1 (=> (and (<= 2 x) (<= x 7)) (= y 1))))
(assert (=> A2 (=> (and (<= 3 x) (<= x 6)) (= y 2))))
(assert (=> B1 (=> (and (<= 4 x) (<= x 9)) (= y 3))))

(assert (= x 4))

(check-sat)
(get-model)

此代码产生：

 |-> 3
sat
(model
  (define-fun A1 () Bool false)
  (define-fun y () Int 2)
  (define-fun A2 () Bool true)
  (define-fun B1 () Bool false)
  (define-fun x () Int 4)
)

对于 A1、A2 和 B1，您可以确切地知道使用了哪些规则，放弃了哪些规则。

NuZ：看到已经放弃的规则了吗？

NuZ: See the rules that have been given up?

optimization

z3