объявление функции в z3

Можно ли в z3 объявить функцию, которая принимает в качестве аргумента другую функцию? Например, это

(declare-fun foo ( ((Int) Bool) ) Int)

не совсем работает. Спасибо.


z3
person JRR    schedule 12.05.2012    source источник

Ответы (2)


arrow_upward
8
arrow_downward

Как упоминал Леонардо, SMT-Lib не поддерживает функции более высокого порядка. Это не просто синтаксическое ограничение: рассуждение с функциями более высокого порядка (как правило) выходит за рамки того, с чем могут иметь дело решатели SMT. (Хотя в некоторых особых случаях можно использовать неинтерпретируемые функции.)

Если вам нужно рассуждать с помощью функций высшего порядка, то интерактивные средства доказательства теорем — это основное оружие выбора: Изабель, HOL, Coq является одним из примеров.

Однако иногда вы хотите, чтобы функции более высокого порядка не рассуждали о них, а просто упрощали задачи программирования. Язык ввода SMT-Lib не подходит для высокоуровневого программирования, которое обычно требуется конечным пользователям в практических ситуациях. Если это ваш вариант использования, то я бы рекомендовал не использовать SMT-Lib напрямую, а работать с языком программирования, который дает вам доступ к Z3 (или другим решателям SMT). Есть несколько вариантов, в зависимости от того, какой язык хоста наиболее подходит для вашего варианта использования:

  • Если вы являетесь пользователем Python, вам подойдет Z3Py, который только что появился в Z3 4.0,
  • Если вы являетесь пользователем Scala, загляните в Scala^Z3.
  • Если вы предпочитаете Haskell, взгляните на SBV.

Каждая привязка имеет свой собственный набор функций, Z3Py, вероятно, является наиболее универсальным, поскольку он напрямую поддерживается людьми Z3. (Он также обеспечивает доступ к внутренним компонентам Z3, которые остаются недоступными для других вариантов, по крайней мере, на данный момент.)

person alias    schedule 13.05.2012
comment
Теоретически также возможно преобразовать функции более высокого порядка в SMT-LIB, используя дефункционализацию. - person Anderson Green; 20.11.2019
comment
Конечно... Дефункционализация - отличная идея. Но это требует, чтобы вы заранее знали, какие именно функции можно использовать в позиции более высокого порядка; и гораздо более применим в компиляции и анализе всей программы. Если вы хотите рассуждать о функциях более высокого порядка (таких как map/filter и т. д.), это на самом деле не помогает. Попробуйте, например, доказать map f . map g = map (f . g), снабженное только определением map. - person alias; 20.11.2019

arrow_upward
6
arrow_downward

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

(объявить-fun foo ((Array Int Bool)) Int)

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

Вот пример: http://rise4fun.com/Z3/qsED

Руководство по Z3 содержит дополнительную информацию о Z3 и SMT.

person Leonardo de Moura    schedule 12.05.2012
comment
Ссылка на пример теперь не работает. - person Anderson Green; 19.03.2018