## Wednesday, December 9, 2015

### Fun and Games with CRV: Einstein's Puzzle (Revisited)

Two weeks ago, Aurelian from AMIQ published a post on how to solve the so-called Einstein's puzzle using e. At the end, he challenged us readers to try and improve on his solution. Not being one to shy away, I rolled up my sleeves and got to work.

He started out by defining a struct to hold the information about a resident:

```<'
struct resident {
nationality : nationality_t;
house_color : house_color_t;
cigarette : cigarette_t;
pet : pet_t;
drink : drink_t;
};
'>
```

He gave up on this idea after he tried to constrain the residents to have unique nationalities, house colors, etc. Here's what he tried:

```<'
struct neighborhood {
keep residents.nationality.is_a_permutation(all_values(nationality_t));
// ...
};
'>
```

This looks reasonable, right? Why didn't it work then? That's because even though residents.nationality returns a list of all residents' nationalities, it isn't generative. I didn't find anything normative in the Language Reference or the Generation User Guide that explicitly states this, but this seems to be the case. The proper way of ensuring all nationalities are unique is to use the all_different(...) pseudo-method:

```<'
struct neighborhood {
keep residents.all_different(it.nationality);
// ...
};
'>
```

Now that we've got our infrastructure set up, it's time to start converting the 15 facts into code. There are three types of facts given to us. The first type only involves individual residents. For example, we know that the one living in the red house is English. This can be represented as a constraint inside the resident class itself:

```<'
extend resident {
keep nationality == ENGLISH => house_color == RED; // #1
};
'>
```

There are seven more such constraints, but I won't show them here, since they are very similar to this one. You can find the complete code on SourceForge.

The second type of fact we know about our residents describes a characteristic of the resident living in a particular house. For example, we know that the resident in the first house is Norwegian. This kind of constraint needs to be added to the neighborhood:

```<'
extend neighborhood {
keep residents[0].nationality == NORWEGIAN; // #9
};
'>
```

The third type of fact gives hints about residents in relation to their neighbors. For example, we know that the green house is located to the left of the white house. Here we need to loop over all elements of the list. Per definition, the green house can't be the last one in the list, because then it wouldn't be located to the left of anything:

```<'
extend neighborhood {
// #4
keep for each (resident) in residents {
resident.house_color == GREEN =>
index < 4 and residents[index+1].house_color == WHITE;
};
};
'>
```

The fact that the Blend smoker lives next to the cat owner is a bit more involved, but it follows the same principle. This means that the Blend smoker is either located to the left (which is the same situation as before) or is located to the right, in which case the respective house can't be the first one:

```<'
extend neighborhood {
// #10
keep for each (resident) in residents {
resident.cigarette == BLEND =>
index < 4 and residents[index+1].pet == CAT or
index > 0 and residents[index-1].pet == CAT;
};
};
'>
```

Since we have three more such constraints to write, we could save ourselves some typing by defining a macro:

```<'
define <neighbors'statement> "<first'exp> neighbors <second'exp>" as {
extend neighborhood {
keep for each (resident) in residents {
resident.<first'exp> =>
index < 4 and residents[index+1].<second'exp> or
index > 0 and residents[index-1].<second'exp>;
};
};
};
'>
```

The macro "call" would look like this:

```<'
cigarette == BLEND neighbors pet == CAT; // #10
'>
```

With these three types of constraints we can model all fifteen facts and solve the puzzle. I was pretty surprised that it worked the first time and gave the right solution - the German keeps the fish. When I solved the zebra puzzle in SystemVerilog (which is essentially the same puzzle as this one, just with slightly different facts about the residents) I ran into problems because I used the implication operator. Basically, saying that the English resident lives in the red house doesn't just mean that nationality == ENGLISH => house_color == RED, but that at the same time house_color == RED => nationality == ENGLISH. There isn't any equivalence operator (also called double implication) in e, but this can be expressed using the equality operator, "==":

```<'
extend resident {
keep (nationality == ENGLISH) == (house_color == RED); // #1
};
'>
```

I've shown you my solution. Now it's time to pass the baton to you and challenge you to improve it even more.