muZ3: недетерминированный рекурсивный вызов

Есть ли способ выполнить недетерминированный рекурсивный вызов в спецификации отношения muZ3? В частности, я хочу перевести функцию, подобную следующей:

int foo(int x) {
    ...
    if (*) y = foo(y);
    ...
}

в формат правила muZ3.


recursion z3 smt non-deterministic z3-fixedpoint
person Hinton    schedule 23.05.2014    source источник
comment
В процессе устранения неоднозначности тега [fixed-point] я изменил [fixed-point] на [z3-fixedpoint] в этом вопросе; однако я недостаточно знаком с Z3 или muZ3, чтобы быть полностью уверенным, что здесь это уместно. Не стесняйтесь, дайте мне знать и / или измените его на что-то другое, если я ошибаюсь.   -  person duplode    schedule 07.07.2019

Ответы (1)


arrow_upward
1
arrow_downward

У вас может быть отдельное правило для двух случаев:

  (declare-fun foo (Int Int) Bool)

   (assert (forall ((x Int) (y Int) (z Int))  (=> (and ... (foo x y) ...) (foo x z)))

   (assert (forall ((x Int) (y Int) (z Int))  (=> (and ... true ...) (foo x z)))
person Nikolaj Bjorner    schedule 10.06.2014