z3py упрощение выражения

Я пытаюсь упростить выражение с помощью z3py, но не могу найти никакой документации о том, что делают разные тактики. Лучший ресурс, который я нашел, - это вопрос о переполнении стека, который перечисляет все тактики по названию.

Может ли кто-нибудь связать меня с подробной документацией по доступной тактике? Онлайн-руководств по питону недостаточно.

Или кто-то может порекомендовать лучший способ добиться этого.

Примером проблемы является такое выражение, как:

x < 5, x < 4, x < 3, x = 1 Я хотел бы упростить это до x = 1.

В этом примере работает тактика unit-subsume-simplify.

Но когда я пробую более сложный пример, такой как x > 1, x < 5, x != 3, x != 4, в результате получаю x > 1, x < 5, x ≠ 3, x ≠ 4. Когда я захочу x = 2.

Как лучше всего добиться такого упрощения с помощью z3py?

Мое текущее решение.

Спасибо Мэтт


z3 z3py
person bettsmatt    schedule 18.07.2013    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Возможное решение:

x = Int('x')
s = Solver()
s.add(x < 5, x < 4, x < 3, x == 1)
print s.check()
m = s.model()
print m
s1 = Solver()
s1.add(x > 1, x < 5, x != 3, x != 4)
print s1.check()
m1 = s1.model()
print m1

Выход:

sat
[x = 1]
sat
[x = 2]

Запустите это решение в Интернете, здесь

person Juan Ospina    schedule 18.07.2013
comment
Спасибо, но я не ищу решения для решателей. Я хочу убрать более слабые термины и упростить выражение. Для ввода: x < 5, x < 4, x < 3 Хочу результат: x < 3 - person bettsmatt; 19.07.2013
comment
Я не эксперт, но думаю, что для вашей проблемы лучше использовать пакет Redlog от Reduce. - person Juan Ospina; 19.07.2013

arrow_upward
0
arrow_downward

Пример с Redlog of Reduce. Пожалуйста, дайте мне знать, что вы думаете.

введите описание изображения здесь

person Juan Ospina    schedule 18.07.2013