Как получить «более сильные» упрощения союзов в Z3? - PullRequest
Новая
       5

Как получить «более сильные» упрощения союзов в Z3?

2 голосов
/ 26 сентября 2011

Используя Z3 версии 2.18, я пытаюсь упростить формулы, такие как:

  • (и (> (- (- x 1) 1) 0) (> x 0))
  • (или (> (- (- x 1) 1) 0) (> x 0))

в надежде получить что-то вроде: (> x 2) и (> x 0).

Я запускаю Z3 со следующим входным файлом, где F - одна из приведенных выше формул: 

(set-option set-param "STRONG_CONTEXT_SIMPLIFIER" "true")
(declare-const x Int)
(simplify F)

Хорошо работает с дизъюнкцией, где я получаю следующий вывод: 

(let (($x35 (<= x 0)))
(not $x35))

Однако с соединением я получаю: 

(not (or (<= x 0) (<= x 2)))

Есть ли способ заставить Z3 еще больше упростить приведенную выше формулу? Я надеюсь, что смогу получить (not (<= x 2)).

PS: есть ли способ заставить Z3 встроить свой вывод (т.е. иметь (not (<= x 0)) вместо (let (($x35 (<= x 0))) (not $x35)))

Спасибо, Гас

1 Ответ

1 голос
/ 26 сентября 2011

Нет, вы не можете сделать это на Z3 2.x.

Z3 3.x имеет новый (полностью совместимый) интерфейс SMT 2.0.Z3 3.x имеет несколько новых функций, таких как «язык спецификации стратегии», основанный на тактике и тактике.Я пока что не "рекламирую", потому что он работает.Основная идея описана в этой слайд-колоде .Этот язык может использоваться, чтобы делать то, что вы хотите.Вам просто нужно написать: 

(declare-const x Int)
(assert (not (or (<= x 0) (<= x 2))))
(apply (and-then simplify propagate-bounds))

Вы можете найти все доступные тактики с помощью команд: 

(help-strategy)
(help apply)
(help check-sat-using)
...