Minizinc constraint against recursive function

Question

I want to use a function like this:

function int: nextr(var int: n)
if n <= 1
  2
elseif n <= 8
  n + 5
elseif n <= 68
  n + 13
elseif n <= 509
  n + 34
elseif n <= 3611
  n + 89
else n + 233

in a constraint that variable must satisfy any value in nextr(n), nextr(nextr(n)), nextr(next(nextr(n))), and so on.

Is there a way to specify such constraint in minizinc? If not possible generally, I'm OK with explicit recursion limit, but without tedious enumeration of all the steps?

Answer 1

Example:

The value of y is constrained to be equal

next(x) \/ next(next(x)) \/ ...

up to K levels of nesting.

function var int: nextr(var int: n) =
  if n <= 1 then
    2
  elseif n <= 8 then
    n + 5
  elseif n <= 68 then
    n + 13
  elseif n <= 509 then
    n + 34
  elseif n <= 3611 then
    n + 89
  else
    n + 233
  endif;

int: K = 10;

var int: x;
var int: y;
array[1..K] of var int: rec_up_to_k;

constraint forall (i in 1..K) (
  if i == 1 then
    rec_up_to_k[i] = nextr(x)
  else
    rec_up_to_k[i] = nextr(rec_up_to_k[i-1])
  endif
);

constraint exists (i in 1..K) (
  y = rec_up_to_k[i]
);

constraint x >= 0;

solve satisfy;

outputs:

x = 3612;
y = 3845;
rec_up_to_k = array1d(1..10, [3845, 4078, 4311, 4544, 4777, 5010, 5243, 5476, 5709, 5942]);
----------