log operator

[ott2]

To express graph connectivity of n-vertex graphs using adjacency matrices, we need to compute \log_2 n as one of the dimensions of an auxiliary matrix. Usually n is given as part of the instance, but we need something like

letting s be log2(n)
find A : matrix indexed by [0..s] of ...

or

letting s be such that (2**s <= n) /\ (2**(s+1) > n)
find A : matrix indexed by [0..s] of ...

to compute the size of the dimension at declaration time.

[ott2]

Workaround due to Pete Nightingale:

letting s be sum([1 | i : int(0..64), 2**i <= n])

[ozgurakgun]

Are you after log2 only? I assume this does not need to work on decision variables?

[ott2]

I was just wanting a built-in log2() operator for letting statements. If we add a log operator for decision variables, then Conjure would have to support things like

find x : int such that 2**x = 16
find y : int such that log2(y) = 4