I’m trying to write a solver using Z3’s .NET library for the Towers puzzle format. Adding the constraints for “every row and column has a distinct permutation of 1-5” is simple enough, especially cribbing from the Sudoku solver provided as an example for Z3. However, I am stuck on the “Exactly X towers are visible from the left/right/top/bottom of each row/column” constraint, and specifically checking how many towers are visible from each point. It should be as simple as
int tallestSoFar = 0;
int towersSoFar = 0;
int[] section = X[i];
for (int ii = 0; ii < section.Length; ii++)
{
if (section[ii] > tallestSoFar)
{
tallestSoFar = section[ii];
towersSoFar++;
}
}
However, this does not work when X
and section
are made of IntExpr’s rather than actual ints. How would I express this in the syntax Z3 would recognize?