What does this code compute?

Here is a piece of code computing some function f from integers to integers. The challenge is to discover what does it compute.

0pt class Mystery { 
static int aux(int a, int b, int c){ 
        int d, e = a& b& c, f = 1; 
if (a != 0) { 
for (f = 0; (d = e&-e) != 0; e -= d) { 
                f += aux(a
-d, (b+d)*2, (c+d)/2); 
return f; 
static int f(int n) { 
return aux( ( 0<<n),0,0); 


A hint is: this program uses ints to represent sets of integers, more precisely subset of {0,…,31}.

  1. Introduce an axiomatic block which declares
  2. Interpret operation e&-e on isets, add a corresponding axiom
  3. Insert an assertion before the recursive call to aux in order to show termination of aux.
  4. (difficult) Can you figure out what does f compute?

This document was translated from LATEX by HEVEA.