recursion - muZ3: 非決定的な再帰呼び出し

Question

muZ3 リレーション仕様で非決定論的に再帰呼び出しを実行する方法はありますか? 具体的には、次のような関数を翻訳したいと思います。

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

muZ3 ルール形式に。

Answer 1

2 つのケースに対して個別のルールを設定できます。

  (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)))