CODEWITHSUNDEEP
recursionz3smtnon-deterministicz3-fixedpoint
Hinton
Hinton

Reputation: 2390

muZ3: Non-deterministic recursive call

Is there a way to perform a recursive call non-deterministically in a muZ3 relation specification? Specifically, I want to translate a function like the following:

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

to the muZ3 rule format.

Upvotes: 1

Views: 188

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can have a separate rule for the two cases:

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

Upvotes: 1

Related Questions