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
Sure.
(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))
With this, z3 produces:
sat
((m 111)
(n 201))
Which is what you're looking for in this instance, I believe.
Note that when you have more than 2 rules, you probably want to be more careful in your modeling to say that some subset of rules fired instead of all of them like I did above. In case you have 2 rules, that ends up being the same thing, but if you have 3 rules, you want to allow for the possibilities of {1, 2}, {1, 3}, {2, 3}, and {1, 2, 3} all firing. This latter can be modeled by counting predicates, by making sure the number of ruleN_applies booleans that go high is at least two. Feel free to ask if you've further questions regarding that.