Как выполнить исключение квантификатора с помощью Python API Z3

Как я могу выполнить исключение квантификатора с помощью Python API Z3? Хотя я проверил руководство и API, не смог этого сделать.

У меня есть формула с квантификатором существования, и я хочу, чтобы Z3 выдал мне новую формулу, чтобы этот квантор был удален. По сути, я хочу сделать то же самое:

Как скрыть переменную с помощью Z3

но с интерфейсом Python. Также моя формула находится в линейной арифметике.

Спасибо!

Дополнение: после исключения квантора я «добавлю» бескванторную формулу к другой. Итак, если я использую тактику, есть ли способ преобразовать подцель (которая является результатом тактики) в выражение в линейной арифметике?


z3 smt z3py
person blurium    schedule 28.07.2013    source источник

Ответы (3)


arrow_upward
5
arrow_downward

Для этого вы можете использовать тактику исключения квантификатора (см. Строку документации Tactic.apply):

from z3 import Ints, Tactic, Exists, And
x, t1, t2 = Ints('x t1 t2')
t = Tactic('qe')
print t(Exists(x, And(t1 < x, x < t2)))
person tbormer    schedule 29.07.2013
comment
Думаю, нам не нужно туда подавать заявку. См. Ниже: rise4fun.com/Z3Py/sQs0 Проблема, с которой я столкнулся, заключается в том, что я не могу использовать вывод тактики, которая является подцелью, и с другим выражением. См. Ниже: rise4fun.com/Z3Py/m7wq Каким-то образом мне нужно преобразовать подцель в логическое выражение . Есть ли способ сделать это? - person blurium; 29.07.2013
comment
Результатом является объект ApplyResult, с которым вы можете использовать as_expr(). См. Документацию по API: research.microsoft .com / en-us / um / redmond / projects / z3 / и вот ваш пример: rise4fun. ru / Z3Py / BNDc - person Taylor T. Johnson; 30.07.2013
comment
@blurium Вы правы насчет заявки, спасибо, что напомнили мне об этом. - person tbormer; 30.07.2013

arrow_upward
0
arrow_downward

Возможное решение с использованием Z3Py онлайн:

x, t1, t2 = Reals('x t1 t2')
g = Goal()
g.add(Exists(x, And(t1 < x, x < t2)))
t = Tactic('qe')
print t(g)

Вывод:

[[¬(0 ≤ t1 + -1·t2)]]

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

person Juan Ospina    schedule 29.07.2013
comment
Проблема, с которой я сталкиваюсь с Tactic, заключается в том, что его результат является подцелью и принадлежит классу ApplyResult, и я хочу продолжить, а результирующее выражение без квантификатора с другим, а затем я получаю сообщение об ошибке: «Ожидается логическое выражение True, False или Z3. 'как здесь: rise4fun.com/Z3Py/Kll9 Есть ли способ преобразовать подцель в выражение Я могу дальше манипулировать? - person blurium; 29.07.2013

arrow_upward
0
arrow_downward

Возможное решение с использованием Redlog of reduce:

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

person Juan Ospina    schedule 29.07.2013
comment
Есть ли у вас какие-либо идеи, что более эффективно при устранении квантификатора - Reduce Redlog или Z3? Другими словами, какой из них лучше масштабируется с точки зрения количества переменных и количества терминов в выражении, для которого мы выполняем исключение квантора? - person blurium; 31.07.2013
comment
Я думаю, что Redlog более мощный и эффективный, чем Z3, выполняющий исключение квантификатора. - person Juan Ospina; 31.07.2013