0

If have a set of rules -

1 : If x then a

2 : If x then b

Then these rules shall be conflicting as we shall not know what is the action to be performed when x is triggered. Therefore -

Now suppose I want to check for consistency of rules such as -

1: If (100 < m < 120) and (200 < n < 220) then output = 200

2: If (110 < m < 120) and (200 < n <210) then output =220

Clearly rules 1 and 2 are conflicting because if m = 115 and n = 205, then output can be either 200 or 220.

Is there a way I can check for the consistency of the above rules using the Z3 library ? Or using the pure SMT-lib2 ? Pls help. If you can give me an example of the actual code which can be run on https://rise4fun.com/Z3/vd?frame=1&menu=0&course=1 I shall be really grateful.

Thank you

4

1 回答 1

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高的布尔值的数量至少为两个。如果您对此还有其他问题，请随时询问。

于 2018-06-12T20:12:06.880 回答