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

Question

如果有一套规则 -

1 ：如果 x 则 a

2 ：如果 x 则 b

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

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

1：如果 (100 < m < 120) 且 (200 < n < 220) 则输出 = 200

2：如果 (110 < m < 120) 且 (200 < n <210) 则输出 =220

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

有没有一种方法可以使用 Z3 库检查上述规则的一致性？或者使用纯 SMT-lib2 ？请帮助。如果你能给我一个实际代码的例子，可以是运行 on 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 布尔值变高的数量至少为两个。如果您对此还有其他问题，请随时提出。

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

Using the Pure SMT-LIB2 in Z3 to check for consistency in rules

z3

smt

z3py

sat

choco