как определить-fun с помощью C # API

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

 （define-fun test((a Int) (b Int)) Int
      （ite  (and (> a 2) (<= b 3))
             1
             (ite （and (<= a 2)(> b 10))
                  2
                  a
             )
       )
  ）

поэтому мне интересно, как определить fun с помощью C # API, поскольку Context.MkFuncDecl используется только для создания неинтерпретируемых функций.


api c# z3
person Community    schedule 28.06.2012    source источник
comment
Я задавал точно такой же вопрос раньше: "> stackoverflow.com/questions/7740556/   -  person pad    schedule 28.06.2012
comment
кажется, что есть новый API С#, мне интересно, есть ли какой-либо прямой метод для определения удовольствия не с помощью квантификаторов?   -  person    schedule 28.06.2012

Ответы (1)


arrow_upward
2
arrow_downward

define-fun — это всего лишь механизм определения макросов в SMT 2.0. Это не добавляет мощности решателям SMT. Мы поддерживаем его в API, так как пользователь может создать функцию, реализующую макрос на его любимом языке. То есть мы можем создать функцию C# с именем test, которая с учетом a и b возвращает выражение ite в вашем вопросе. Вот пример того, как это сделать в Python:

http://rise4fun.com/Z3Py/to1

Вот еще один пример, определяющий функцию min, которая получает произвольное количество аргументов:

http://rise4fun.com/Z3Py/Vvp

person Leonardo de Moura    schedule 28.06.2012
comment
Спасибо, я решил проблему. Однако есть еще одна проблема, вы можете узнать о квантификаторе и фиксированной точке, z3-in-c-sharp" title="при запуске квантификатора существования и фиксированной точки z3 в c Sharp появляется ошибка"> stackoverflow.com/questions/11264914/ не могли бы вы мне помочь? - person ; 29.06.2012