Как я мог подтвердить аксиому в Z3Py? - PullRequest
Новая
       9

Как я мог подтвердить аксиому в Z3Py?

0 голосов
/ 03 февраля 2020

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

Я пытаюсь Чтобы определить аксиому, комбинирующую методы Length и Contains of Z3Py, пример моей идеи таков: 

lista = Const('lista', SeqSort(IntSort()))

a, b = Ints('a b')
solve(ForAll(lista, Length(lista)> 3))

Это фрагмент кода будет рассматриваться как аксиома? Это вернуло мне «нет решения», и я не понимаю, почему. Должен ли он поддержать список из двух элементов, правда?

1 Ответ

0 голосов
/ 03 февраля 2020

Этот вопрос очень запутанный, совсем не понятно, о чем вы спрашиваете. Аксиома обычно является выражением, выраженным количественно, то есть чем-то, что содержит Forall и / или Exists. Вот пример, скопированный из https://ericpony.github.io/z3py-tutorial/advanced-examples.htm: 

f = Function('f', IntSort(), IntSort(), IntSort())
x, y = Ints('x y')
print ForAll([x, y], f(x, y) == 0)
print Exists(x, f(x, x) >= 0)

a, b = Ints('a b')
solve(ForAll(x, f(x, x) == 0), f(a, b) == 1)

Как видите, аксиомы обычно используются для express свойств неинтерпретируемых функций: f в приведенном выше примере .

Ваше описание очень трудно расшифровать, но звучит так, как будто у вас может быть проблема XY: http://xyproblem.info/ Посмотрите, можете ли вы сформулировать вопрос с тем, чего именно вы пытаетесь достичь, вместо того, чтобы делать предположения! (Извините за каламбур!) Удачи!

Относительно вашей кодировки:

Давайте сосредоточимся на том, что вы написали: 

solve(ForAll(lista, Length(lista)> 3))

То, что вы здесь говорите, таково что для всех списков (которые вы назвали lista), их длина больше 3. В более математической записи вы указали: 

∀x. length (x) > 3

Это явно не так, поскольку Вы можете взять пустой список в качестве контрпримера.

В общем случае аксиомы создадут новую неинтерпретированную сортировку и / или неинтерпретированные функции и свойства их состояния. Вы указали, что вы новый пользователь, скорее всего, вам не понадобятся аксиомы для чего-либо практичного на этом уровне. Переполнение стека действительно работает лучше всего, когда вы задаете очень конкретные c вопросы по конкретным c темам, поэтому не стесняйтесь задавать другой вопрос.

...