在 Z3 中使用 Pure SMT-LIB2 检查规则的一致性

Question

如果有一套规则——

1 : 如果 x 则 a

2 : 如果 x 则 b

那么这些规则将是冲突的，因为我们不知道当 x 被触发时要执行的操作是什么。因此——

现在假设我要检查规则的一致性，例如 -

1: 如果 (100

2：如果 (110

显然规则 1 和 2 是冲突的，因为如果 m = 115 和 n = 205，那么输出可以是 200 或 220。

有没有办法使用 Z3 库检查上述规则的一致性？还是使用纯 SMT-lib2 ？请帮忙。如果您能给我一个可以在https://rise4fun.com/Z3/vd?frame=1&menu=0&course=1 上运行的实际代码示例，我将不胜感激。

谢谢

Answer 1

当然。

(declare-fun m () Int)
(declare-fun n () Int)

(define-fun rule1_applies () Bool (and (< 100 m) (< m 120) (< 200 n) (< n 220)))
(define-fun rule2_applies () Bool (and (< 110 m) (< m 120) (< 200 n) (< n 210)))

(declare-fun output0 () Int)

(define-fun output_rule1 () Int (ite rule1_applies 200 output0))
(define-fun output_rule2 () Int (ite rule2_applies 220 output0))

(assert (and rule1_applies rule2_applies (distinct output_rule1 output_rule2)))
(check-sat)
(get-value (m n))

有了这个，z3 产生：

sat
((m 111)
 (n 201))

我相信在这种情况下您正在寻找什么。

请注意，当您有超过 2 条规则时，您可能希望在建模时更加小心，以说明触发了某些规则子集，而不是像我上面所做的那样全部触发。如果您有 2 条规则，最终结果是一样的，但如果您有 3 条规则，您希望允许 {1, 2}、{1, 3}、{2, 3} 和 { 1、2、3}全部开火。后者可以通过计算谓词来建模，确保ruleN_applies 高的布尔值的数量至少为两个。如果您对此还有其他问题，请随时询问。