Использование Pure SMT-LIB2 в Z3 для проверки согласованности в правилах - PullRequest
Новая
       104

Использование Pure SMT-LIB2 в Z3 для проверки согласованности в правилах

0 голосов
/ 12 июня 2018

Если есть набор правил -

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, я буду очень признателен.

Спасибо

1 Ответ

0 голосов
/ 12 июня 2018

Конечно. 

(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 правила, это в конечном итоге одно и то же, но если у вас есть 3 правила, вы хотите учесть возможности {1, 2}, {1, 3}, {2, 3} и {1, 2, 3} все стрельба.Это последнее можно смоделировать, посчитав предикаты, убедившись, что число ruleN_applies булевых значений, имеющих высокое значение, равно как минимум двум.Не стесняйтесь спрашивать, если у вас есть дополнительные вопросы по этому поводу.

...