Эквивалент define-fun в Z3 API - PullRequest
Новая
       5

Эквивалент define-fun в Z3 API

8 голосов
/ 12 октября 2011

Используя Z3 с текстовым форматом, я могу использовать define-fun, чтобы определить функции для повторного использования в дальнейшем.Например: 

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

Интересно, как создать define-fun с Z3 API (я использую F #) вместо повсеместного повторения тела функции.Я хочу использовать его, чтобы избежать дублирования и отладки формул.Я пробовал с Context.MkFuncDecl, но, похоже, он генерирует только неинтерпретированные функции.

1 Ответ

10 голосов
/ 12 октября 2011

Команда define-fun просто создает макрос. Обратите внимание, что стандарт SMT 2.0 не допускает рекурсивных определений. Z3 будет расширяться при каждом появлении my-div во время анализа. Команда define-fun может использоваться, чтобы сделать входной файл проще и легче для чтения, но внутренне это не очень помогает Z3.

В текущем API нет поддержки для создания макросов. Это не является реальным ограничением, поскольку мы можем определить функцию C или F #, которая создает экземпляры макроса. Однако кажется, что вы хотите отобразить (и вручную проверить) формулы, созданные с использованием API Z3. В этом случае макросы вам не помогут.

Одной из альтернатив является использование квантификаторов. Вы можете объявить неинтерпретированную функцию my-div и утверждать универсально выраженную формулу: 

(declare-fun mydiv (Real Real) Real)
(assert (forall ((x Real) (y Real))
                (= (mydiv x y)
                   (if (not (= y 0.0))
                       (/ x y)
                       0.0))))

Теперь вы можете создать формулу, используя неинтерпретированную функцию mydiv.

Этот вид количественной формулы может обрабатываться Z3. На самом деле, есть два варианта обработки этого вида квантификатора:

  1. Использовать поиск макросов: этот шаг предварительной обработки идентифицирует квантификаторы, которые по сути определяют макросы, и расширяет их. Однако расширение происходит только во время предварительной обработки, а не во время синтаксического анализа (т. Е. Время построения формулы). Чтобы включить поиск модели, вы должны использовать MACRO_FINDER=true
  2. Другой вариант - использовать MBQI (создание квантификатора на основе модели). Этот модуль также может обрабатывать этот вид квантификатора. Однако квантификаторы будут расширяться по требованию.

Конечно, время решения может сильно зависеть от того, какой подход вы используете. Например, если ваша формула является неудовлетворительной независимо от «значения» mydiv, то подход 2, вероятно, лучше.

...