Есть ли в Z3 способ сгенерировать неопределенное количество предположений для проверки?

Моя программа Python использует Z3 Python API. Он генерирует ряд предположений, которые Z3 проверяет с помощью команды:

check(P1, P2,....Pn)

Затем я получаю unsat ядро ​​с помощью команды:

unsat_core()

Есть ли способ использовать в моей программе на Python команду check(P1, P2,....Pn), не зная заранее количество утверждений? Количество допущений определяется во время выполнения кода и меняется при каждом запуске.

Заранее спасибо!


python z3 z3py
person Heldib    schedule 24.09.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Конечно. Вы можете поместить свои предположения в кортеж и просто использовать распаковку кортежа< /а>.

eg.

my_assumptions = (P1, P2, ...Pn)
check(*my_assumptions)

В зависимости от того, как структурирована ваша программа, вам может потребоваться сначала создать/добавить предположения в список, а затем преобразовать список в кортеж.

person Gerrat    schedule 24.09.2014