Как я могу использовать пустой метод в списке в Z3Py? - PullRequest
Новая
       11

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

0 голосов
/ 30 января 2020

В z3py я хотел бы использовать функцию Empty в Z3py (https://z3prover.github.io/api/html/z3py_8py_source.html#l09944)

Я пытался сделать это так: 

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))
solve(Empty(iseq)!= True)


# get a model and print it:
if s.check() == sat:
    print (s.model())

но я возвращаю "Z3Exception: непоследовательность, сортировка нерегулярных выражений передана пустым"

Я также пытался очистить (iseq) только обратно мне пустую последовательность чего-либо, но у меня это не сработало

1 Ответ

1 голос
/ 30 января 2020

Здесь происходит несколько вещей:

  • Вы объявляете решающий объект s = Solver (), но затем вы вызываете функцию solve. solve создает свой собственный решатель. Вместо этого просто используйте s.add.

  • Empty создает последовательность с учетом сортировки. Вы не можете позвонить на iseq. Это сообщение об ошибке, которое вы получаете.

Я предполагаю, что все, что вы пытаетесь сказать: объявите iseq, убедитесь, что оно не пустое. Вы должны закодировать это следующим образом: 

from z3 import *

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))

# assert it's not empty
s.add (Length(iseq) != 0)

# get a model and print it:
if s.check() == sat:
    print (s.model())

z3 говорит: 

$ python a.py
[iseq = Unit(2)]

Итак, он дал вам модель, где iseq - это одиночная последовательность, содержащая число 2 ; не пусто, что удовлетворяет установленному нами ограничению.

Вот пример, который использует Empty для создания пустой последовательности: 

from z3 import *

s = Solver()

# Give a name to integer sequences
ISeq = SeqSort(IntSort())

# declare a sequence of integers
iseq = Const('iseq', ISeq)

# make sure it's empty!
s.add (iseq == Empty(ISeq))

# get a model and print it:
if s.check() == sat:
    print (s.model())

z3 говорит: 

[iseq = Empty(Seq(Int))]

Обратите внимание, что z3py по сути является функциональным языком; как только вы утверждаете, что что-то равно чему-то другому, вы можете , а не изменить это значение, как вы могли бы на императивном языке, например, скажем, Python. Надеюсь, это поможет!

...