В ответ на вопрос this question Лео предложил использовать кванторы для определения функций. Предположим, мне нужно всего лишь применить функцию только 1 раз, а использование квантификатора влияет на производительность Z3?Использует ли квантификатор влияние производительности Z3?
Как это сравнить с случаем, когда я объявляю функцию без параметров и без кванторов (поскольку я использую только функцию только 1 раз)?
Вы можете использовать опцию smt.macro_finder = true для преобразования квантифицированных равенств в макросы. По умолчанию это отключено, поэтому лучше определить макросы для функций, которые вы применяете только один раз. Это также означает, что Z3 заканчивается использованием общего решателя на основе квантификатора. В некоторых случаях функции, определенные макросами, используя команды «define-fun», удобны для формул, которые являются чисто битовыми или чисто линейными арифметическими. В этих случаях Z3 использует более эффективные настройки. Например, Z3 использует распространение «релевантности», чтобы избежать создания избыточного квантификатора. распространение релевантности приходит со своими собственными накладными расходами, что допустимо с квантованными формулами, но не является хорошей идеей для бескванторных формул.