2
В z3 можно ли объявить функцию, которая принимает другую функцию в качестве аргумента? Например, этоОбъявление функции в z3
(declare-fun foo (((Int) Bool)) Int)
не работает. Благодарю.
A
ответ
4
Как упоминал Леонардо, SMT-Lib делает не позволяет выполнять функции более высокого порядка. Это не просто синтаксическое ограничение. Рассуждение с функциями более высокого порядка (вообще) за пределами того, с чем могут справиться решатели SMT. (. Хотя интерпретируемые функции могут использоваться в некоторых особых случаях)
Если вам нужно причине с функциями высшего порядка, то интерактивные доказательства теорем являются основным оружием выбора: Isabelle, HOL, Coq являются одними из примеры.
Однако иногда вам нужны функции более высокого порядка , а не, чтобы рассуждать о них, а просто упрощать задачи программирования. Язык ввода SMT-Lib не подходит для высокоуровневого программирования, которое конечным пользователям обычно требуется в практических ситуациях. Если это ваш прецедент, я бы рекомендовал не использовать SMT-Lib напрямую, а скорее работать с языком программирования, который дает вам доступ к Z3 (или другим решателям SMT). Есть несколько вариантов, в зависимости от того, что хост язык является наиболее подходящим для вашего случая использования:
- Если вы являетесь пользователем Python, Z3Py что только поставляется с Z3 4.0 является путь,
- Если вы пользователь Scala, затем просмотрите Scala^Z3.
- Если Haskell - ваш предпочтительный язык, ознакомьтесь с SBV.
У каждой привязки есть свой собственный набор функций, Z3Py, вероятно, самый универсальный, поскольку он напрямую поддерживается людьми Z3. (Он также обеспечивает доступ к внутренним компонентам Z3, которые по-прежнему недоступны для других вариантов, по крайней мере, на данный момент.)
5
Нет, это невозможно. Однако вы можете определить функцию, которая принимает массив в качестве аргумента.
(объявлять-весело Foo ((Array Int Bool)) Int)
Вы можете использовать этот трюк, чтобы имитировать функции высокого порядка, как в вашем вопросе.
Вот пример: http://rise4fun.com/Z3/qsED
Z3 guide содержит больше информации о Z3 и SMT.